From fbb4f8e4ce84795f86c987c25da64c20f62d9bd1 Mon Sep 17 00:00:00 2001 From: Sarah Grebing Date: Wed, 17 May 2017 10:52:04 +0200 Subject: [PATCH] minor improevment in interpreter and fixed bug in grammar --- .../proofscriptparser/ScriptLanguage.g4 | 2 +- .../kit/formal/interpreter/AbstractState.java | 5 +- .../kit/formal/interpreter/ErrorState.java | 5 + .../edu/kit/formal/interpreter/Evaluator.java | 1 + .../edu/kit/formal/interpreter/GoalNode.java | 5 + .../kit/formal/interpreter/Interpreter.java | 109 +++++++++++++++--- .../edu/kit/formal/interpreter/State.java | 15 +++ .../edu/kit/formal/interpreter/Value.java | 1 + 8 files changed, 123 insertions(+), 20 deletions(-) diff --git a/src/main/antlr4/edu/kit/formal/proofscriptparser/ScriptLanguage.g4 b/src/main/antlr4/edu/kit/formal/proofscriptparser/ScriptLanguage.g4 index baa2aacc..fbfedf9c 100644 --- a/src/main/antlr4/edu/kit/formal/proofscriptparser/ScriptLanguage.g4 +++ b/src/main/antlr4/edu/kit/formal/proofscriptparser/ScriptLanguage.g4 @@ -75,7 +75,7 @@ literals : */ matchPattern - : MATCH pattern=expression + : MATCH matchPattern=expression (USING LBRACKET argList RBRACKET)? ; diff --git a/src/main/java/edu/kit/formal/interpreter/AbstractState.java b/src/main/java/edu/kit/formal/interpreter/AbstractState.java index 7461071f..b4971dd5 100644 --- a/src/main/java/edu/kit/formal/interpreter/AbstractState.java +++ b/src/main/java/edu/kit/formal/interpreter/AbstractState.java @@ -29,8 +29,5 @@ public abstract class AbstractState { public abstract GoalNode getSelectedGoalNode(); - public State copy() { - // return new State(); - return null; - } + public abstract State copy(); } diff --git a/src/main/java/edu/kit/formal/interpreter/ErrorState.java b/src/main/java/edu/kit/formal/interpreter/ErrorState.java index 45add434..a47434ac 100644 --- a/src/main/java/edu/kit/formal/interpreter/ErrorState.java +++ b/src/main/java/edu/kit/formal/interpreter/ErrorState.java @@ -22,4 +22,9 @@ public class ErrorState extends AbstractState { public GoalNode getSelectedGoalNode() { return null; } + + @Override + public State copy() { + return null; + } } diff --git a/src/main/java/edu/kit/formal/interpreter/Evaluator.java b/src/main/java/edu/kit/formal/interpreter/Evaluator.java index c7c8c099..356cadcc 100644 --- a/src/main/java/edu/kit/formal/interpreter/Evaluator.java +++ b/src/main/java/edu/kit/formal/interpreter/Evaluator.java @@ -12,6 +12,7 @@ import java.util.List; * Class handling evaluation of expressions (visitor for expressions) * * @author S.Grebing + * @author A. Weigl */ public class Evaluator extends DefaultASTVisitor { private GoalNode currentState; diff --git a/src/main/java/edu/kit/formal/interpreter/GoalNode.java b/src/main/java/edu/kit/formal/interpreter/GoalNode.java index 764d7d94..adc81092 100644 --- a/src/main/java/edu/kit/formal/interpreter/GoalNode.java +++ b/src/main/java/edu/kit/formal/interpreter/GoalNode.java @@ -108,4 +108,9 @@ public class GoalNode { this.assignments = this.assignments.pop(); return assignments; } + + public GoalNode deepCopy() { + //TODO method does nothing helpful atm + return new GoalNode(this.getParent(), sequent); + } } diff --git a/src/main/java/edu/kit/formal/interpreter/Interpreter.java b/src/main/java/edu/kit/formal/interpreter/Interpreter.java index 5c44719d..de94fe36 100644 --- a/src/main/java/edu/kit/formal/interpreter/Interpreter.java +++ b/src/main/java/edu/kit/formal/interpreter/Interpreter.java @@ -11,6 +11,7 @@ import java.util.*; * @author S.Grebing */ public class Interpreter extends DefaultASTVisitor { + //TODO later also inclulde information about source line for each state (for debugging purposes and rewind purposes) public Stack stateStack; public HashMap localCommands; @@ -38,7 +39,28 @@ public class Interpreter extends DefaultASTVisitor { } + /** + * If new Block is entered, a new state has to be created (copy of current state) and opushed to the stack + */ + private void enterScope() { + } + + /** + * If block is extied the top state on the stack has to be removed + */ + private void exitScope() { + + } + + /** + * Visit a proof script (context is handled by the call of the script noch by visiting the script itself) + * 1) visit its signature + * 2) visit its body + * + * @param proofScript + * @return + */ @Override public T visit(ProofScript proofScript) { //AbstractState currentState = stateStack.pop(); @@ -50,6 +72,11 @@ public class Interpreter extends DefaultASTVisitor { return null; } + /** + * Visiting an assignment results in changing the variables of the current selected goalnode + * @param assignmentStatement + * @return + */ @Override public T visit(AssignmentStatement assignmentStatement) { System.out.println("Visiting Assignment " + assignmentStatement.toString()); @@ -71,18 +98,24 @@ public class Interpreter extends DefaultASTVisitor { return null; } - + /** + * Visiting a statement list results in visiting each statement + * @param statements + * @return + */ @Override public T visit(Statements statements) { - Iterator iterator = statements.iterator(); - - while (iterator.hasNext()) { - Statement s = iterator.next(); + for (Statement s : statements) { s.accept(this); } return null; } + /** + * + * @param casesStatement + * @return + */ @Override public T visit(CasesStatement casesStatement) { //neuerScope @@ -91,36 +124,61 @@ public class Interpreter extends DefaultASTVisitor { return null; } + /** + * + * @param caseStatement + * @return + */ @Override public T visit(CaseStatement caseStatement) { return null; } + /** + * Visiting a call statement results in: + * 0) searching for the handler of the called command + * 1) saving the context onto the stack and creating a copy of the state and push it onto the stack + * 2) adding new Variable Assignments to te selected goal + * 3) adding the assigned parameters to the variable assignments + * 4) visting the body respec. letting the handler take over + * 5) removing the top element form the stack + * @param call + * @return + */ @Override public T visit(CallStatement call) { //neuer scope State newState = stateStack.peek().copy(); + Evaluator eval = new Evaluator(newState.getSelectedGoalNode()); String commandName = call.getCommand(); Parameters parameters = call.getParameters(); - ProofScript commandScript; - //find body if local script command + //TODO refactor into own interface/facade for proof commands if (localCommands.containsKey(commandName)) { commandScript = localCommands.get(commandName); + Signature sig = commandScript.getSignature(); + Iterator> paramIterator = parameters.entrySet().iterator(); + //Iterator> sigIter = sig.entrySet().iterator(); + while (paramIterator.hasNext()) { + Map.Entry nextP = paramIterator.next(); + Expression expr = nextP.getValue(); + Variable var = nextP.getKey(); + Value val = (Value) expr.accept(eval); + newState.getSelectedGoalNode().setVarValue(var.getIdentifier(), val); + + } + newState.getSelectedGoalNode().enterNewVarScope(); + stateStack.push(newState); + visit(commandScript.getBody()); + stateStack.pop().getSelectedGoalNode().exitNewVarScope(); } else { throw new RuntimeException("Command " + commandName + " is not known"); } return null; - //call.getCommand(); on signatur body suchen - //state map mit commands die name nach body+parameter - //nach schauen - //call.getParameters(); - //ProofScript aktuell; - //interpret(aktuell.getBody()); } @Override @@ -129,10 +187,31 @@ public class Interpreter extends DefaultASTVisitor { return null; } + /** + * Visiting foreach: + * 1) foreach goal in state create a new state with exact this goal + * 2) foreach of these goals visit body of foreach + * 3) collect all results after foreach + * @param foreach + * @return + */ @Override public T visit(ForeachStatement foreach) { - //neue zustände auf den stack mit jeweils anderem Ziel ausgewählt - foreach.getBody(); + State currentState = (State) stateStack.pop(); + List allGoals = currentState.getGoals(); + List goalsAfterForeach = new ArrayList<>(); + Statements body = foreach.getBody(); + for (GoalNode goal : allGoals) { + List goals = new ArrayList<>(); + goals.add(goal); + State single = new State(goals, goal); + stateStack.push(single); + visit(body); + State afterForeach = (State) stateStack.pop(); + goalsAfterForeach.addAll(afterForeach.getGoals()); + } + State afterForeach = new State(goalsAfterForeach, null); + stateStack.push(afterForeach); return null; } diff --git a/src/main/java/edu/kit/formal/interpreter/State.java b/src/main/java/edu/kit/formal/interpreter/State.java index 8648cbfa..1108812d 100644 --- a/src/main/java/edu/kit/formal/interpreter/State.java +++ b/src/main/java/edu/kit/formal/interpreter/State.java @@ -1,5 +1,6 @@ package edu.kit.formal.interpreter; +import java.util.ArrayList; import java.util.List; /** @@ -51,5 +52,19 @@ public class State extends AbstractState { this.selectedGoalNode = selectedGoalNode; } + /** + * TODO correct this method, atm does nothing helpful! + * + * @return + */ + @Override + public State copy() { + List copiedGoals = new ArrayList<>(); + GoalNode refToSelGoal = selectedGoalNode; + + + return new State(copiedGoals, refToSelGoal); + } + } diff --git a/src/main/java/edu/kit/formal/interpreter/Value.java b/src/main/java/edu/kit/formal/interpreter/Value.java index 0ccbdf24..70177e32 100644 --- a/src/main/java/edu/kit/formal/interpreter/Value.java +++ b/src/main/java/edu/kit/formal/interpreter/Value.java @@ -13,6 +13,7 @@ import java.math.BigInteger; * Class representing the values our variables may have * * @author S.Grebing + * @author A. Weigl * //TODO alle restlichen typen ergaenzen */ @RequiredArgsConstructor -- GitLab