From 1dcc2138112a11a7dde44994676d56b784c75f81 Mon Sep 17 00:00:00 2001 From: Sarah Grebing Date: Thu, 31 Aug 2017 07:22:09 +0200 Subject: [PATCH] new implementation of cases handling --- .../formal/psdbg/interpreter/Interpreter.java | 167 ++++++++++++++---- 1 file changed, 133 insertions(+), 34 deletions(-) diff --git a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java index 524bc234..d302e391 100644 --- a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java +++ b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java @@ -1,6 +1,7 @@ package edu.kit.iti.formal.psdbg.interpreter; +import com.google.common.collect.Sets; import edu.kit.iti.formal.psdbg.interpreter.assignhook.VariableAssignmentHook; import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode; import edu.kit.iti.formal.psdbg.interpreter.data.State; @@ -12,8 +13,10 @@ import edu.kit.iti.formal.psdbg.parser.Visitor; 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.Type; +import javafx.util.Pair; import lombok.Getter; import lombok.Setter; +import sun.reflect.generics.reflectiveObjects.NotImplementedException; import java.util.*; import java.util.logging.Logger; @@ -186,68 +189,61 @@ public class Interpreter extends DefaultASTVisitor } else { return false; } - } - /** - * @param casesStatement - * @return - */ - @Override - public Object visit(CasesStatement casesStatement) { + public Object visitOld(CasesStatement casesStatement) { enterScope(casesStatement); State beforeCases = peekState(); List> allGoalsBeforeCases = beforeCases.getGoals(); + //copy the list of goal nodes for keeping track of goals + Set> toMatch = new HashSet<>(allGoalsBeforeCases); //global List after all Case Statements - List> goalsAfterCases = new ArrayList<>(); - //copy the list of goal nodes for keeping track of goals - Set> remainingGoalsSet = new HashSet<>(allGoalsBeforeCases); + List> resultingGoals = new ArrayList<>(); + //handle cases List cases = casesStatement.getCases(); - for (GoalNode goalBeforeCase : allGoalsBeforeCases) { - State createdState = newState(goalBeforeCase);//to allow the case to retrieve goal + Map> goalToCaseMapping = matchGoalsToCases(allGoalsBeforeCases, casesStatement); + + for (GoalNode goal : allGoalsBeforeCases) { + newState(goal); //to allow the visit method for the case stmt to retrieve goal + boolean result = false; for (CaseStatement aCase : cases) { result = (boolean) aCase.accept(this); if (result) { //remove goal from set for default - remainingGoalsSet.remove(goalBeforeCase); + toMatch.remove(goal); //case statement matched and was executed break; } } - //remove state from stack - State stateAfterCase = popState(); - // System.out.println("State after Case " + stateAfterCase.getSelectedGoalNode().toCellTextForKeYData()); - if (result && stateAfterCase.getGoals() != null) { - goalsAfterCases.addAll(stateAfterCase.getGoals()); - } + State stateAfterCase = popState(); //remove state from stack + if (result && stateAfterCase.getGoals() != null) { + resultingGoals.addAll(stateAfterCase.getGoals()); + } } //for all remaining goals execute default - if (!remainingGoalsSet.isEmpty()) { + if (!toMatch.isEmpty()) { VariableAssignment va = new VariableAssignment(); Statements defaultCase = casesStatement.getDefaultCase(); - for (GoalNode goal : remainingGoalsSet) { - - goalsAfterCases.addAll(executeBody(defaultCase, goal, va).getGoals()); + for (GoalNode goal : toMatch) { + resultingGoals.addAll(executeBody(defaultCase, goal, va).getGoals()); } - - } //exit scope and create a new state using the union of all newly created goals State newStateAfterCases; - if (!goalsAfterCases.isEmpty()) { + if (!resultingGoals.isEmpty()) { //goalsAfterCases.forEach(node -> node.exitScope()); - Stream> goalNodeStream = goalsAfterCases.stream().filter(tGoalNode -> !(tGoalNode.isClosed())); + Stream> goalNodeStream = resultingGoals.stream().filter(tGoalNode -> !(tGoalNode.isClosed())); List> openGoalListAfterCases = goalNodeStream.collect(Collectors.toList()); if (openGoalListAfterCases.size() == 1) { @@ -263,6 +259,51 @@ public class Interpreter extends DefaultASTVisitor return null; } + private Map> matchGoalsToCases(List> allGoalsBeforeCases, CasesStatement cases) { + //list of cases + List caseStmts = cases.getCases(); + //remaining goals + Set> setOfRemainingGoals = Sets.newHashSet(allGoalsBeforeCases); + + //returnMap + Map> returnMap = new HashMap<>(); + + for (CaseStatement caseStmt : caseStmts) { + Map, VariableAssignment> goalNodeVariableAssignmentMap = matchGoal(setOfRemainingGoals, caseStmt); + //put all matched goals to returnMap for case + goalNodeVariableAssignmentMap.keySet().forEach(tGoalNode -> + { + returnMap.put(tGoalNode, new Pair(goalNodeVariableAssignmentMap.get(tGoalNode), caseStmt.getBody())); + }); + setOfRemainingGoals.removeAll(goalNodeVariableAssignmentMap.keySet()); + } + + if (!setOfRemainingGoals.isEmpty()) { + VariableAssignment va = new VariableAssignment(); + Statements defaultCase = cases.getDefaultCase(); + for (GoalNode goal : setOfRemainingGoals) { + returnMap.put(goal, new Pair(va, defaultCase)); + // resultingGoals.addAll(executeBody(defaultCase, goal, va).getGoals()); + } + } + return returnMap; + + //matchGoal(allGoalsBeforeCases, acase) + + /* + * //for all remaining goals execute default + if (!toMatch.isEmpty()) { + VariableAssignment va = new VariableAssignment(); + Statements defaultCase = casesStatement.getDefaultCase(); + for (GoalNode goal : toMatch) { + resultingGoals.addAll(executeBody(defaultCase, goal, va).getGoals()); + } + } + + * + * */ + } + /** * Match a set of goal nodes against a matchpattern of a case and return the matched goals together with instantiated variables * @@ -270,17 +311,75 @@ public class Interpreter extends DefaultASTVisitor * @param aCase * @return */ - private Map, VariableAssignment> matchGoal(Set> allGoalsBeforeCases, SimpleCaseStatement aCase) { + private Map, VariableAssignment> matchGoal(Set> allGoalsBeforeCases, CaseStatement aCase) { HashMap, VariableAssignment> matchedGoals = new HashMap<>(); - Expression matchExpression = aCase.getGuard(); - for (GoalNode goal : allGoalsBeforeCases) { - VariableAssignment va = evaluateMatchInGoal(matchExpression, goal); - if (va != null) { - matchedGoals.put(goal, va); + if (aCase.isClosedStmt == false) { + SimpleCaseStatement caseStmt = (SimpleCaseStatement) aCase; + Expression matchExpression = caseStmt.getGuard(); + for (GoalNode goal : allGoalsBeforeCases) { + VariableAssignment va = evaluateMatchInGoal(matchExpression, goal); + if (va != null) { + matchedGoals.put(goal, va); + } } + return matchedGoals; + } else { + throw new NotImplementedException(); } - return matchedGoals; + } + + /** + * @param casesStatement + * @return + */ + @Override + public Object visit(CasesStatement casesStatement) { + enterScope(casesStatement); + State beforeCases = peekState(); + + List> allGoalsBeforeCases = beforeCases.getGoals(); + //copy the list of goal nodes for keeping track of goals + Set> toMatch = new HashSet<>(allGoalsBeforeCases); + + //global List after all Case Statements + List> resultingGoals = new ArrayList<>(); + + //handle cases + List cases = casesStatement.getCases(); + + Map> goalToCaseMapping = matchGoalsToCases(allGoalsBeforeCases, casesStatement); + + goalToCaseMapping.forEach((goalNode, variableAssignmentStatementsPair) -> { + State createdState = newState(goalNode); + executeBody(variableAssignmentStatementsPair.getValue(), goalNode, variableAssignmentStatementsPair.getKey()); + //stmts.accept(this); + + State stateAfterCase = popState(); //remove state from stack + if (stateAfterCase.getGoals() != null) { + resultingGoals.addAll(stateAfterCase.getGoals()); + } + }); + + //exit scope and create a new state using the union of all newly created goals + + State newStateAfterCases; + if (!resultingGoals.isEmpty()) { + //goalsAfterCases.forEach(node -> node.exitScope()); + Stream> goalNodeStream = resultingGoals.stream().filter(tGoalNode -> !(tGoalNode.isClosed())); + List> openGoalListAfterCases = goalNodeStream.collect(Collectors.toList()); + + if (openGoalListAfterCases.size() == 1) { + newStateAfterCases = new State(openGoalListAfterCases, 0); + } else { + newStateAfterCases = new State(openGoalListAfterCases, null); + } + stateStack.push(newStateAfterCases); + } + + //stateStack.peek().getGoals().removeAll(beforeCases.getGoals()); + exitScope(casesStatement); + return null; } /** -- 2.26.2