Commit 2e63600e authored by Sarah Grebing's avatar Sarah Grebing
Browse files

bug fix: now possible to evalute "case true:"

parent 1dcc2138
...@@ -191,6 +191,13 @@ public class Interpreter<T> extends DefaultASTVisitor<Object> ...@@ -191,6 +191,13 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
} }
} }
/**
* Old visit method, for deocumentation purposes
*
* @param casesStatement
* @return
*/
@Deprecated
public Object visitOld(CasesStatement casesStatement) { public Object visitOld(CasesStatement casesStatement) {
enterScope(casesStatement); enterScope(casesStatement);
State<T> beforeCases = peekState(); State<T> beforeCases = peekState();
...@@ -259,6 +266,12 @@ public class Interpreter<T> extends DefaultASTVisitor<Object> ...@@ -259,6 +266,12 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
return null; return null;
} }
/**
* Computes which goals are handled by the different cases in the order the cases appear in the script
* @param allGoalsBeforeCases
* @param cases all cases as ordered list
* @return a mapping of each goal to the matched case body together with variableassignments from the matching process
*/
private Map<GoalNode, Pair<VariableAssignment, Statements>> matchGoalsToCases(List<GoalNode<T>> allGoalsBeforeCases, CasesStatement cases) { private Map<GoalNode, Pair<VariableAssignment, Statements>> matchGoalsToCases(List<GoalNode<T>> allGoalsBeforeCases, CasesStatement cases) {
//list of cases //list of cases
List<CaseStatement> caseStmts = cases.getCases(); List<CaseStatement> caseStmts = cases.getCases();
...@@ -288,20 +301,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object> ...@@ -288,20 +301,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
} }
return returnMap; return returnMap;
//matchGoal(allGoalsBeforeCases, acase)
/*
* //for all remaining goals execute default
if (!toMatch.isEmpty()) {
VariableAssignment va = new VariableAssignment();
Statements defaultCase = casesStatement.getDefaultCase();
for (GoalNode<T> goal : toMatch) {
resultingGoals.addAll(executeBody(defaultCase, goal, va).getGoals());
}
}
*
* */
} }
/** /**
...@@ -325,6 +325,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object> ...@@ -325,6 +325,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
} }
return matchedGoals; return matchedGoals;
} else { } else {
//handle try and closes
throw new NotImplementedException(); throw new NotImplementedException();
} }
} }
...@@ -391,7 +392,6 @@ public class Interpreter<T> extends DefaultASTVisitor<Object> ...@@ -391,7 +392,6 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
*/ */
private VariableAssignment evaluateMatchInGoal(Expression matchExpression, GoalNode<T> goal) { private VariableAssignment evaluateMatchInGoal(Expression matchExpression, GoalNode<T> goal) {
enterScope(matchExpression); enterScope(matchExpression);
// System.out.println("Goal to match " + goal.toCellTextForKeYData());
MatchEvaluator mEval = new MatchEvaluator(goal.getAssignments(), goal, matcherApi); MatchEvaluator mEval = new MatchEvaluator(goal.getAssignments(), goal, matcherApi);
mEval.getEntryListeners().addAll(entryListeners); mEval.getEntryListeners().addAll(entryListeners);
mEval.getExitListeners().addAll(exitListeners); mEval.getExitListeners().addAll(exitListeners);
......
package edu.kit.iti.formal.psdbg.interpreter; package edu.kit.iti.formal.psdbg.interpreter;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode; import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.parser.data.Value;
import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment; import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor; import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
import edu.kit.iti.formal.psdbg.parser.Visitor; import edu.kit.iti.formal.psdbg.parser.Visitor;
import edu.kit.iti.formal.psdbg.parser.ast.*; import edu.kit.iti.formal.psdbg.parser.ast.*;
import edu.kit.iti.formal.psdbg.parser.data.Value;
import edu.kit.iti.formal.psdbg.parser.types.SimpleType; import edu.kit.iti.formal.psdbg.parser.types.SimpleType;
import edu.kit.iti.formal.psdbg.parser.types.TypeFacade; import edu.kit.iti.formal.psdbg.parser.types.TypeFacade;
import lombok.Getter; import lombok.Getter;
...@@ -57,6 +57,11 @@ public class MatchEvaluator extends DefaultASTVisitor<List<VariableAssignment>> ...@@ -57,6 +57,11 @@ public class MatchEvaluator extends DefaultASTVisitor<List<VariableAssignment>>
return evaluateExpression(op, left, right); return evaluateExpression(op, left, right);
} }
@Override
public List<VariableAssignment> visit(BooleanLiteral booleanLiteral) {
return transformTruthValue(Value.from(booleanLiteral));
}
/** /**
* Decide whether to evaluate using the MatchEvaluator or the standard evaluator depending on the content of the expression * Decide whether to evaluate using the MatchEvaluator or the standard evaluator depending on the content of the expression
* *
...@@ -207,7 +212,7 @@ public class MatchEvaluator extends DefaultASTVisitor<List<VariableAssignment>> ...@@ -207,7 +212,7 @@ public class MatchEvaluator extends DefaultASTVisitor<List<VariableAssignment>>
if (v.getType().equals(SimpleType.BOOL)) { if (v.getType().equals(SimpleType.BOOL)) {
List<VariableAssignment> transformedValue = new ArrayList<>(); List<VariableAssignment> transformedValue = new ArrayList<>();
if (v.getData().equals(Value.TRUE)) { if (((Boolean) v.getData()).booleanValue() == ((Boolean) Value.TRUE.getData()).booleanValue() || v.getData().equals(Value.TRUE)) {
transformedValue.add(new VariableAssignment(null)); transformedValue.add(new VariableAssignment(null));
} }
return transformedValue; return transformedValue;
......
...@@ -8,7 +8,7 @@ import org.dockfx.DockNode; ...@@ -8,7 +8,7 @@ import org.dockfx.DockNode;
/** /**
* This controller manages a list of {@link InspectionView} and the associated {@link DockNode}s. * This controller manages a list of {@link InspectionView} and the associated {@link DockNode}s.
* *
* Espeically, this class holds the active tab, which is connected with the {@link edu.kit.iti.formal.psdbg.interpreter.graphs.ProofTreeController}, * Especially, this class holds the active tab, which is connected with the {@link edu.kit.iti.formal.psdbg.interpreter.graphs.ProofTreeController},
* and shows the current interpreter state. * and shows the current interpreter state.
* *
* @author weigl * @author weigl
......
...@@ -21,6 +21,9 @@ import javafx.util.StringConverter; ...@@ -21,6 +21,9 @@ import javafx.util.StringConverter;
import java.util.stream.Collectors; import java.util.stream.Collectors;
/**
* KeY Proof Tree
*/
public class ProofTree extends BorderPane { public class ProofTree extends BorderPane {
private ObjectProperty<Proof> proof = new SimpleObjectProperty<>(); private ObjectProperty<Proof> proof = new SimpleObjectProperty<>();
private ObjectProperty<Node> root = new SimpleObjectProperty<>(); private ObjectProperty<Node> root = new SimpleObjectProperty<>();
......
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