Commit 19df8932 authored by Lulu Luong's avatar Lulu Luong

merge with master

parent 42f19000
Pipeline #33463 passed with stages
in 2 minutes and 7 seconds
...@@ -211,7 +211,7 @@ public interface ASTTraversal<T> extends Visitor<T> { ...@@ -211,7 +211,7 @@ public interface ASTTraversal<T> extends Visitor<T> {
} }
@Override @Override
default T visit(DerivableCase derivableCase){ default T visit(DerivableCase derivableCase) {
derivableCase.getExpression().accept(this); derivableCase.getExpression().accept(this);
derivableCase.getBody().accept(this); derivableCase.getBody().accept(this);
return null; return null;
......
...@@ -414,8 +414,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> { ...@@ -414,8 +414,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
Expression pattern = (Expression) ctx.derivableExpression.accept(this); Expression pattern = (Expression) ctx.derivableExpression.accept(this);
((DerivableCase) cs).setExpression(pattern); ((DerivableCase) cs).setExpression(pattern);
pattern.setParent(cs); pattern.setParent(cs);
} else } else {
{
cs = new GuardedCaseStatement(); cs = new GuardedCaseStatement();
Expression<ParserRuleContext> guard = (Expression<ParserRuleContext>) ctx.expression().accept(this); Expression<ParserRuleContext> guard = (Expression<ParserRuleContext>) ctx.expression().accept(this);
((GuardedCaseStatement) cs).setGuard(guard); ((GuardedCaseStatement) cs).setGuard(guard);
......
...@@ -7,13 +7,13 @@ import lombok.NoArgsConstructor; ...@@ -7,13 +7,13 @@ import lombok.NoArgsConstructor;
@Data @Data
@NoArgsConstructor @NoArgsConstructor
public class DerivableCase extends CaseStatement{ public class DerivableCase extends CaseStatement {
private Expression expression; private Expression expression;
public DerivableCase(Statements copy, Expression copy1) { public DerivableCase(Statements copy, Expression copy1) {
super(copy); super(copy);
this.expression=copy1; this.expression = copy1;
} }
@Override @Override
......
...@@ -43,7 +43,9 @@ import lombok.Setter; ...@@ -43,7 +43,9 @@ import lombok.Setter;
public class MatchExpression extends Expression<ScriptLanguageParser.MatchPatternContext> { public class MatchExpression extends Expression<ScriptLanguageParser.MatchPatternContext> {
//private Signature signature = new Signature(); //private Signature signature = new Signature();
private Expression pattern; private Expression pattern;
@Deprecated @Getter @Setter @Deprecated
@Getter
@Setter
private boolean isDerivable = false; private boolean isDerivable = false;
@Deprecated @Deprecated
private Expression derivableTerm; private Expression derivableTerm;
......
...@@ -148,8 +148,6 @@ public class KeyInterpreter extends Interpreter<KeyData> { ...@@ -148,8 +148,6 @@ public class KeyInterpreter extends Interpreter<KeyData> {
} }
@Override @Override
public Object visit(LetStatement let) { public Object visit(LetStatement let) {
enterScope(let); enterScope(let);
......
...@@ -67,7 +67,7 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> { ...@@ -67,7 +67,7 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
State<KeyData> state = interpreter.getCurrentState(); State<KeyData> state = interpreter.getCurrentState();
//multiple goals exist //multiple goals exist
if(state.getGoals().size() > 1) { if (state.getGoals().size() > 1) {
throw new IllegalStateException("Multiple open goals: Please use a selector."); throw new IllegalStateException("Multiple open goals: Please use a selector.");
/* /*
//TODO: Utils showWarning //TODO: Utils showWarning
......
...@@ -62,7 +62,7 @@ public class KeYMatcher implements MatcherApi<KeyData> { ...@@ -62,7 +62,7 @@ public class KeYMatcher implements MatcherApi<KeyData> {
Proof proof = kd.getData().getProof(); Proof proof = kd.getData().getProof();
TermValue tv = (TermValue) pattern.getData(); TermValue tv = (TermValue) pattern.getData();
Term term = tv.getTerm(); Term term = tv.getTerm();
if(term == null) { if (term == null) {
Services services = kd.getData().getProof().getServices(); Services services = kd.getData().getProof().getServices();
try { try {
term = new TermBuilder(services.getTermFactory(), services).parseTerm(tv.getTermRepr()); term = new TermBuilder(services.getTermFactory(), services).parseTerm(tv.getTermRepr());
...@@ -96,10 +96,10 @@ public class KeYMatcher implements MatcherApi<KeyData> { ...@@ -96,10 +96,10 @@ public class KeYMatcher implements MatcherApi<KeyData> {
if (isDerivable) { if (isDerivable) {
//find the open goal node //find the open goal node
Goal toSet= null; Goal toSet = null;
if(goalList.head().node().isClosed()){ if (goalList.head().node().isClosed()) {
toSet = goalList.tail().head(); toSet = goalList.tail().head();
} else{ } else {
toSet = goalList.head(); toSet = goalList.head();
} }
KeyData kdataNew = new KeyData(kd.getData(), toSet); KeyData kdataNew = new KeyData(kd.getData(), toSet);
......
...@@ -34,7 +34,7 @@ public class KeyMatcherDerivableTest { ...@@ -34,7 +34,7 @@ public class KeyMatcherDerivableTest {
System.out.println(proof); System.out.println(proof);
// Assert.assertNotNull(a); // Assert.assertNotNull(a);
Assert.assertEquals(1, proof.getSubtreeGoals(proof.root()).size()); Assert.assertEquals(1, proof.getSubtreeGoals(proof.root()).size());
} }
......
...@@ -220,8 +220,8 @@ public class Interpreter<T> extends DefaultASTVisitor<Object> ...@@ -220,8 +220,8 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
GoalNode<T> selectedGoal = currentStateToMatch.getSelectedGoalNode(); GoalNode<T> selectedGoal = currentStateToMatch.getSelectedGoalNode();
assert currentStateToMatch.getGoals().contains(selectedGoal); assert currentStateToMatch.getGoals().contains(selectedGoal);
Value v = evaluate(pattern); Value v = evaluate(pattern);
if(v.getType() == TypeFacade.ANY_TERM){ if (v.getType() == TypeFacade.ANY_TERM) {
GoalNode<T> newGoalNode= matcherApi.isDerivable(selectedGoal, v); GoalNode<T> newGoalNode = matcherApi.isDerivable(selectedGoal, v);
try { try {
enterScope(derivableCase); enterScope(derivableCase);
...@@ -238,7 +238,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object> ...@@ -238,7 +238,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
exitScope(derivableCase); exitScope(derivableCase);
} }
} else { } else {
throw new RuntimeException("A derivable expression must contain a term. Received a"+v.getType()); throw new RuntimeException("A derivable expression must contain a term. Received a" + v.getType());
} }
} }
......
...@@ -191,9 +191,9 @@ public class MatchEvaluator extends DefaultASTVisitor<List<VariableAssignment>> ...@@ -191,9 +191,9 @@ public class MatchEvaluator extends DefaultASTVisitor<List<VariableAssignment>>
Operator op = e.getOperator(); Operator op = e.getOperator();
Expression expr = e.getExpression(); Expression expr = e.getExpression();
List<VariableAssignment> exValue = (List<VariableAssignment>) expr.accept(this); List<VariableAssignment> exValue = (List<VariableAssignment>) expr.accept(this);
if(exValue.isEmpty()){ if (exValue.isEmpty()) {
return transformTruthValue(Value.TRUE); return transformTruthValue(Value.TRUE);
}else{ } else {
return transformTruthValue(Value.FALSE); return transformTruthValue(Value.FALSE);
} }
......
...@@ -129,7 +129,7 @@ public class InteractiveModeController { ...@@ -129,7 +129,7 @@ public class InteractiveModeController {
.filter(keyDataGoalNode -> goalsbeforePrune.contains(keyDataGoalNode.getData().getGoal())) .filter(keyDataGoalNode -> goalsbeforePrune.contains(keyDataGoalNode.getData().getGoal()))
.collect(Collectors.toList()); .collect(Collectors.toList());
if(prunedChildren.size() == 0) { if (prunedChildren.size() == 0) {
//TODO: add Utils.showInfoD //TODO: add Utils.showInfoD
return; return;
} }
...@@ -162,10 +162,10 @@ public class InteractiveModeController { ...@@ -162,10 +162,10 @@ public class InteractiveModeController {
//TODO: buggy cuz allstatements of same node removed //TODO: buggy cuz allstatements of same node removed
//remove statement from cases / script //remove statement from cases / script
Statements statements = (cases.get(pruneNode.parent()) == null)? cases.get(pruneNode) : cases.get(pruneNode.parent()); Statements statements = (cases.get(pruneNode.parent()) == null) ? cases.get(pruneNode) : cases.get(pruneNode.parent());
int i = statements.size()-1; int i = statements.size() - 1;
while(statements.get(i) != pruneStatement && i >= 0) { while (statements.get(i) != pruneStatement && i >= 0) {
statements.remove(i); statements.remove(i);
i--; i--;
} }
......
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