Commit a7bc41b8 authored by Alexander Weigl's avatar Alexander Weigl

Diffing and UI improvements

parent 90894510
Pipeline #15062 failed with stage
in 1 minute and 49 seconds
package edu.kit.iti.formal.psdbg.parser;
import edu.kit.iti.formal.psdbg.parser.ast.*;
public class ASTDiff implements Visitor<ASTNode> {
private ASTNode other;
private ProofScript newScript;
@Override
public ProofScript visit(ProofScript proofScript) {
newScript = new ProofScript();
newScript.setName(proofScript.getName());
newScript.setSignature(proofScript.getSignature());
other = ((ProofScript) other).getBody();
newScript.setBody(visit(newScript.getBody()));
return newScript;
}
@Override
public ASTNode visit(AssignmentStatement assign) {
return null;
}
@Override
public ASTNode visit(BinaryExpression e) {
return null;
}
@Override
public ASTNode visit(MatchExpression match) {
return null;
}
@Override
public ASTNode visit(TermLiteral term) {
return null;
}
@Override
public ASTNode visit(StringLiteral string) {
return null;
}
@Override
public ASTNode visit(Variable variable) {
return null;
}
@Override
public ASTNode visit(BooleanLiteral bool) {
return null;
}
@Override
public Statements visit(Statements statements) {
Statements s = new Statements();
Statements other = (Statements) this.other;
assert statements.size() <= other.size();
int i = 0;
for (; i < statements.size(); i++) {
if (statements.get(i).eq(other.get(i))) {
break;
}
}
for (int j = i; j < other.size(); j++) {
s.add(other.get(i));
}
return s;
}
@Override
public ASTNode visit(IntegerLiteral integer) {
return null;
}
@Override
public ASTNode visit(CasesStatement cases) {
return null;
}
@Override
public ASTNode visit(DefaultCaseStatement defCase) {
return null;
}
@Override
public ASTNode visit(CallStatement call) {
return null;
}
@Override
public ASTNode visit(TheOnlyStatement theOnly) {
return null;
}
@Override
public ASTNode visit(ForeachStatement foreach) {
return null;
}
@Override
public ASTNode visit(RepeatStatement repeat) {
return null;
}
@Override
public ASTNode visit(Signature signature) {
return null;
}
@Override
public ASTNode visit(Parameters parameters) {
return null;
}
@Override
public ASTNode visit(UnaryExpression e) {
return null;
}
@Override
public ASTNode visit(TryCase TryCase) {
return null;
}
@Override
public ASTNode visit(GuardedCaseStatement guardedCaseStatement) {
return null;
}
@Override
public ASTNode visit(CaseStatement caseStatement) {
return null;
}
@Override
public ASTNode visit(SubstituteExpression subst) {
return null;
}
@Override
public ASTNode visit(ClosesCase closesCase) {
return null;
}
public ProofScript diff(ProofScript old, ProofScript rev) {
other = rev;
return (ProofScript) visit(old);
}
}
......@@ -125,4 +125,8 @@ public abstract class ASTNode<T extends ParserRuleContext>
} while (n != null);
return true;
}
public boolean eq(ASTNode other) {
return equals(other);
}
}
......@@ -74,4 +74,17 @@ public class AssignmentStatement
return type != null;
}
@Override
public boolean eq(ASTNode o) {
if (this == o) return true;
if (o == null || getClass() != o.getClass()) return false;
if (!super.equals(o)) return false;
AssignmentStatement that = (AssignmentStatement) o;
if (!getLhs().eq(that.getLhs())) return false;
if (!getRhs().eq(that.getRhs())) return false;
return getType() != null ? getType().equals(that.getType()) : that.getType() == null;
}
}
......@@ -64,9 +64,20 @@ public class CallStatement extends Statement<ScriptLanguageParser.ScriptCommandC
*/
@Override
public CallStatement copy() {
CallStatement s = new CallStatement(command, parameters.copy());
s.setRuleContext(this.getRuleContext());
return s;
}
@Override
public boolean eq(ASTNode o) {
if (this == o) return true;
if (o == null || getClass() != o.getClass()) return false;
if (!super.equals(o)) return false;
CallStatement that = (CallStatement) o;
if (!getCommand().equals(that.getCommand())) return false;
return getParameters().equals(that.getParameters());
}
}
......@@ -53,4 +53,15 @@ public abstract class CaseStatement extends Statement<ScriptLanguageParser.Cases
*/
@Override public abstract CaseStatement copy();
@Override
public boolean equals(Object o) {
if (this == o) return true;
if (o == null || getClass() != o.getClass()) return false;
if (!super.equals(o)) return false;
CaseStatement that = (CaseStatement) o;
return getBody().eq(that.getBody());
}
}
......@@ -66,4 +66,21 @@ public class CasesStatement extends Statement<ScriptLanguageParser.CasesStmtCont
c.setRuleContext(this.ruleContext);
return c;
}
@Override
public boolean equals(Object o) {
if (this == o) return true;
if (o == null || getClass() != o.getClass()) return false;
if (!super.equals(o)) return false;
CasesStatement that = (CasesStatement) o;
for (int i = 0; i < cases.size(); i++) {
if(!cases.get(i).eq(that.cases.get(i)))
return false;
}
return getDefCaseStmt() != null ? getDefCaseStmt().eq(that.getDefCaseStmt()) : that.getDefCaseStmt() == null;
}
}
......@@ -44,4 +44,15 @@ public class ClosesCase extends CaseStatement {
return cs;
}
@Override
public boolean eq(ASTNode o) {
if (this == o) return true;
if (!(o instanceof ClosesCase)) return false;
if (!super.equals(o)) return false;
ClosesCase that = (ClosesCase) o;
return getClosesGuard() != null ? getClosesGuard().eq(that.getClosesGuard()) : that.getClosesGuard() == null;
}
}
......@@ -37,6 +37,24 @@ public class DefaultCaseStatement extends Statement<ScriptLanguageParser.StmtLis
dcs.setRuleContext(this.ruleContext);
return dcs;
}
@Override
public boolean equals(Object o) {
if (this == o) return true;
if (o == null || getClass() != o.getClass()) return false;
if (!super.equals(o)) return false;
DefaultCaseStatement that = (DefaultCaseStatement) o;
return getBody().eq(that.getBody());
}
@Override
public int hashCode() {
int result = super.hashCode();
result = 31 * result + getBody().hashCode();
return result;
}
}
......
......@@ -40,4 +40,16 @@ public abstract class GoalSelector<T extends ParserRuleContext>
@Getter
@Setter
@NonNull private Statements body = new Statements();
@Override
public boolean eq(ASTNode o) {
if (this == o) return true;
if (o == null || getClass() != o.getClass()) return false;
if (!super.equals(o)) return false;
GoalSelector<?> that = (GoalSelector<?>) o;
return getBody() != null ? getBody().eq(that.getBody()) : that.getBody() == null;
}
}
......@@ -37,5 +37,15 @@ public class GuardedCaseStatement extends CaseStatement {
return scs;
}
@Override
public boolean eq(ASTNode o) {
if (this == o) return true;
if (o == null || getClass() != o.getClass()) return false;
if (!super.equals(o)) return false;
GuardedCaseStatement that = (GuardedCaseStatement) o;
return getGuard().eq(that.getGuard());
}
}
......@@ -23,7 +23,6 @@ package edu.kit.iti.formal.psdbg.parser.ast;
*/
import edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser;
import edu.kit.iti.formal.psdbg.parser.Visitor;
import lombok.EqualsAndHashCode;
......@@ -46,11 +45,13 @@ import java.util.function.Function;
public class Parameters extends ASTNode<ScriptLanguageParser.ParametersContext> {
private final Map<Variable, Expression> parameters = new LinkedHashMap<>();
@Override public <T> T accept(Visitor<T> visitor) {
@Override
public <T> T accept(Visitor<T> visitor) {
return visitor.visit(this);
}
@Override public Parameters copy() {
@Override
public Parameters copy() {
Parameters p = new Parameters();
forEach((k, v) -> p.put(k.copy(), v.copy()));
p.setRuleContext(this.getRuleContext());
......@@ -138,18 +139,38 @@ public class Parameters extends ASTNode<ScriptLanguageParser.ParametersContext>
}
public Expression computeIfPresent(Variable key,
BiFunction<? super Variable, ? super Expression, ? extends Expression> remappingFunction) {
BiFunction<? super Variable, ? super Expression, ? extends Expression> remappingFunction) {
return parameters.computeIfPresent(key, remappingFunction);
}
public Expression compute(Variable key,
BiFunction<? super Variable, ? super Expression, ? extends Expression> remappingFunction) {
BiFunction<? super Variable, ? super Expression, ? extends Expression> remappingFunction) {
return parameters.compute(key, remappingFunction);
}
public Expression merge(Variable key, Expression value,
BiFunction<? super Expression, ? super Expression, ? extends Expression> remappingFunction) {
BiFunction<? super Expression, ? super Expression, ? extends Expression> remappingFunction) {
return parameters.merge(key, value, remappingFunction);
}
@Override
public boolean eq(ASTNode o) {
if (this == o) return true;
if (o == null || getClass() != o.getClass()) return false;
if (!super.equals(o)) return false;
Parameters that = (Parameters) o;
for (Map.Entry<Variable, Expression> e : that.parameters.entrySet()) {
if (!e.getValue().eq(get(e.getKey())))
return false;
}
for (Map.Entry<Variable, Expression> e : parameters.entrySet()) {
if (!e.getValue().eq(that.get(e.getKey())))
return false;
}
return true;
}
}
......@@ -59,4 +59,18 @@ public class ProofScript extends ASTNode<ScriptLanguageParser.ScriptContext> {
}
@Override
public boolean eq(ASTNode o) {
if (this == o) return true;
if (!(o instanceof ProofScript)) return false;
if (!super.equals(o)) return false;
ProofScript that = (ProofScript) o;
if (getName() != null ? !getName().equals(that.getName()) : that.getName() != null) return false;
if (getSignature() != null ? !getSignature().eq(that.getSignature()) : that.getSignature() != null)
return false;
return getBody() != null ? getBody().eq(that.getBody()) : that.getBody() == null;
}
}
......@@ -59,4 +59,6 @@ public class RepeatStatement extends GoalSelector<ScriptLanguageParser.RepeatStm
rs.setRuleContext(this.ruleContext);
return rs;
}
}
......@@ -23,7 +23,6 @@ package edu.kit.iti.formal.psdbg.parser.ast;
*/
import edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser;
import edu.kit.iti.formal.psdbg.parser.Visitor;
import edu.kit.iti.formal.psdbg.parser.types.Type;
......@@ -42,16 +41,18 @@ import java.util.function.Function;
* @author Alexander Weigl
* @version 1 (29.04.17)
*/
@EqualsAndHashCode(callSuper = false, of="sig")
@EqualsAndHashCode(callSuper = false, of = "sig")
@ToString
public class Signature extends ASTNode<ScriptLanguageParser.ArgListContext> implements Map<Variable, Type> {
private final Map<Variable, Type> sig = new LinkedHashMap<>();
@Override public <T> T accept(Visitor<T> visitor) {
@Override
public <T> T accept(Visitor<T> visitor) {
return visitor.visit(this);
}
@Override public Signature copy() {
@Override
public Signature copy() {
Signature signature = new Signature();
forEach((k, v) -> signature.put(k.copy(), v));
signature.setRuleContext(this.ruleContext);
......@@ -144,17 +145,17 @@ public class Signature extends ASTNode<ScriptLanguageParser.ArgListContext> impl
}
public Type computeIfPresent(Variable key,
BiFunction<? super Variable, ? super Type, ? extends Type> remappingFunction) {
BiFunction<? super Variable, ? super Type, ? extends Type> remappingFunction) {
return sig.computeIfPresent(key, remappingFunction);
}
public Type compute(Variable key,
BiFunction<? super Variable, ? super Type, ? extends Type> remappingFunction) {
BiFunction<? super Variable, ? super Type, ? extends Type> remappingFunction) {
return sig.compute(key, remappingFunction);
}
public Type merge(Variable key, Type value,
BiFunction<? super Type, ? super Type, ? extends Type> remappingFunction) {
BiFunction<? super Type, ? super Type, ? extends Type> remappingFunction) {
return sig.merge(key, value, remappingFunction);
}
}
......@@ -161,15 +161,18 @@ public class Statements extends ASTNode<ScriptLanguageParser.StmtListContext>
statements.forEach(action);
}
@Override public String toString() {
@Override
public String toString() {
return "Statements{" + "statements=" + statements + '}';
}
@Override public <T> T accept(Visitor<T> visitor) {
@Override
public <T> T accept(Visitor<T> visitor) {
return visitor.visit(this);
}
@Override public Statements copy() {
@Override
public Statements copy() {
Statements s = new Statements();
forEach(e -> {
Statement ecopy = e.copy();
......@@ -180,4 +183,17 @@ public class Statements extends ASTNode<ScriptLanguageParser.StmtListContext>
return s;
}
@Override
public boolean eq(ASTNode o) {
if (this == o) return true;
if (!(o instanceof Statements)) return false;
if (!super.equals(o)) return false;
Statements that = (Statements) o;
for (int i = 0; i < statements.size(); i++) {
if (!statements.get(i).eq(that.statements.get(i))) {
return false;
}
}
return true;
}
}
......@@ -31,4 +31,6 @@ public class TryCase extends CaseStatement {
tc.setRuleContext(this.getRuleContext());
return tc;
}
}
package edu.kit.iti.formal.psdbg.parser;
import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
import org.junit.Test;
import java.io.File;
import java.io.IOException;
import java.util.List;
import static org.junit.Assert.assertEquals;
public class ASTDiffTest {
private static final String PREFIX = "src/test/resources/edu/kit/iti/formal/psdbg/parser";
@Test
public void testDiff1() throws IOException {
List<ProofScript> o = Facade.getAST(new File(PREFIX, "test_diff_1.kps"));
ASTDiff astDiff = new ASTDiff();
ProofScript res = astDiff.diff(o.get(0), o.get(1));
assertEquals(
o.get(2).accept(new PrettyPrinter()),
res.accept(new PrettyPrinter())
);
}
}
\ No newline at end of file
script A() {
A;
B;
C;
D;
}
script A() {
A;
B;
C;
D;
E;F;
}
script A() {
E;F;
}
script A() {
A;
B;
C;
cases {
case x=2:
a;
}
}
script A() {
A;
B;
C;
F;
}
script A() {
E;F;
}
......@@ -71,12 +71,12 @@ public class KeYProofFacade {
/**
* reload the current proof. synchronously because only the first load is slow.
*/
public void reload() throws ProofInputException, ProblemLoaderException {
public void reload(File problemFile) throws ProofInputException, ProblemLoaderException {
if (contract.get() != null) {// reinstante the contract
setProof(getEnvironment().createProof(
contract.get().getProofObl(getEnvironment().getServices())));
} else {
setProof(KeYApi.loadFromKeyFile(proof.get().getProofFile()).getLoadedProof().getProof());
setProof(KeYApi.loadFromKeyFile(problemFile).getLoadedProof().getProof());
}
}
......
......@@ -16,6 +16,8 @@ import edu.kit.iti.formal.psdbg.interpreter.exceptions.ScriptCommandNotApplicabl
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import org.key_project.util.collection.ImmutableList;
import java.util.HashMap;
......@@ -27,6 +29,8 @@ import java.util.Map;
*/
@RequiredArgsConstructor
public class RuleCommandHandler implements CommandHandler<KeyData> {
private static final Logger LOGGER = LogManager.getLogger(RuleCommandHandler.class);
@Getter
private final Map<String, Rule> rules;
......@@ -53,7 +57,7 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
KeyData kd = expandedNode.getData();
Map<String, String> map = new HashMap<>();
params.asMap().forEach((k, v) -> map.put(k.getIdentifier(), v.getData().toString()));
System.out.println(map);
LOGGER.info("Execute {} with {}", call, map);
try {
map.put("#2", call.getCommand());
EngineState estate = new EngineState(kd.getProof());
......
......@@ -19,10 +19,12 @@ import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.dbg.*;
import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
import javafx.application.Platform;
import javafx.beans.binding.BooleanBinding;
import javafx.collections.FXCollections;
import javafx.concurrent.Service;
import javafx.concurrent.Task;
import javafx.event.ActionEvent;
import javafx.event.EventHandler;
import javafx.fxml.FXML;
import javafx.fxml.Initializable;
import javafx.scene.control.*;
......@@ -76,6 +78,36 @@ public class DebuggerMain implements Initializable {
@FXML
private DockPane dockStation;
@FXML
private ToggleButton togBtnCommandHelp;
@FXML
private ToggleButton togBtnProofTree;
@FXML
private ToggleButton togBtnActiveInspector;
@FXML
private ToggleButton togBtnWelcome;
@FXML
private ToggleButton togBtnCodeDock;
@FXML
private CheckMenuItem miCommandHelp;
@FXML
private CheckMenuItem miCodeDock;
@FXML
private CheckMenuItem miWelcomeDock;
@FXML
private CheckMenuItem miActiveInspector;
@FXML
private CheckMenuItem miProofTree;
private JavaArea javaArea = new JavaArea();
private DockNode javaAreaDock = new DockNode(javaArea, "Java Source",
......@@ -135,6 +167,33 @@ public class DebuggerMain implements Initializable {
Utils.addDebugListener(model.executeNotPossibleProperty(), "executeNotPossible");