Commit a280e9f6 authored by Sarah Grebing's avatar Sarah Grebing

bugfix newline after logicprinter

parent 9f657295
......@@ -98,13 +98,9 @@ public class MatcherFacadeTest {
shouldMatch("1*j", "1 + ?Y", "[]");
shouldMatch("1*j", "1 * ?Y", "[{?Y=j}]");
//does not match
shouldMatch("1*j", "?Y * 1", "[{?Y=j}]");
//shouldMatch("f(a) ==> f(a), f(b)" , "==> f(?X)", [{?X=a}]);
//shouldMatch("f(a) ==> f(a), f(b)" , "f(a) ==> f(?X)", [{?X=a}]);
//shouldNotMatch("f(a) ==> f(a), f(b)" , "f(?X) ==> f(?X), f(a)");
}
@Test
......
package edu.kit.iti.formal.psdbg.interpreter;
import de.uka.ilkd.key.api.ProofApi;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.Name;
import de.uka.ilkd.key.logic.Term;
......@@ -163,10 +162,11 @@ public class KeYMatcher implements MatcherApi<KeyData> {
private Value<String> toValueTerm(KeyData currentState, Term matched) {
String reprTerm = LogicPrinter.quickPrintTerm(matched, currentState.getEnv().getServices());
//Hack: to avoid newlines
String reprTermReformatted = reprTerm.trim();
return new Value<>(
new TermType(new SortType(matched.sort())),
reprTerm
reprTermReformatted
);
}
......
......@@ -4,7 +4,6 @@ import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
import de.uka.ilkd.key.macros.scripts.EngineState;
import de.uka.ilkd.key.macros.scripts.ProofScriptCommand;
import de.uka.ilkd.key.macros.scripts.meta.ProofScriptArgument;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Node;
import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
......@@ -15,10 +14,14 @@ import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
import org.apache.commons.io.IOUtils;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import org.key_project.util.collection.ImmutableList;
import java.io.IOException;
import java.net.URISyntaxException;
import java.net.URL;
import java.util.Collection;
import java.util.HashMap;
import java.util.Iterator;
......@@ -61,7 +64,11 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
GoalNode<KeyData> expandedNode = state.getSelectedGoalNode();
KeyData kd = expandedNode.getData();
Map<String, String> map = new HashMap<>();
params.asMap().forEach((k, v) -> map.put(k.getIdentifier(), v.getData().toString()));
params.asMap().forEach((k, v) -> {
System.out.println("v.getData().toString() = " + v.getData().toString());
map.put(k.getIdentifier(), v.getData().toString());
}
);
try {
EngineState estate = new EngineState(kd.getProof());
estate.setGoal(kd.getNode());
......@@ -100,6 +107,17 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
@Override
public String getHelp(CallStatement call) {
ProofScriptCommand c = commands.get(call.getCommand());
URL res = getClass().getResource("/commands/" + call.getCommand() + ".html");
try {
return IOUtils.toString(res.toURI(), "utf-8");
} catch (NullPointerException | IOException | URISyntaxException e) {
return "No Help found for " + call.getCommand();
}
/*
StringBuilder html = new StringBuilder();
......@@ -150,5 +168,6 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
html.append("</body></html>");
return html.toString();
*/
}
}
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<title>Title</title>
</head>
<body>
</body>
</html>
\ No newline at end of file
......@@ -27,7 +27,7 @@ var1 : type := value;
var2 := value;
```
Both statements declare a variable, in the later we directly assign a value, in
Both statements declare a variable, in the latter case (`var1` and `var2`) we directly assign a value, in
the first form `var0` receives a default value.
### Types and Literals
......@@ -42,7 +42,7 @@ We have following types: `INT`, `TERM<Sort>`, `String`.
* `TERM<S>` represents a term of sort `S` in KeY.
`S` can be any sort of KeY. If the sort is ommitied, then `S=Any`.
`S` can be any sort given by KeY. If the sort is ommitied, then `S=Any`.
```
`f(x)`
......@@ -59,9 +59,9 @@ We have following types: `INT`, `TERM<Sort>`, `String`.
### Special Variables
Not all variables are equal
To expose settings of the underlying prover to the user we include special variables:
* `MAX_STEPS` : amount
* `MAX_STEPS` : amount denotes the maximum number of proof steps the underlying prover is allowed to perform
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment