Commit 814a7c3e authored by Alexander Weigl's avatar Alexander Weigl
Browse files

Fixing details in Interpreter

* [FEATURE] CommandLookup
* [FEATURE] InterpreterTest for testing the interpreter; includes helper commands like assert/assertEq
* [FEATURE] Listeners for Evaluator and Interpreter
   * including History and Logger listener for the start
* [FEATURE] Interpreter has scrict or non-script mode (exception on not selected goals)
* [FEATURE] Interpreter has a logger instance
* [FEATURE] default ast visitor has defaultVisit method
parent 341605af
Pipeline #10642 passed with stage
in 2 minutes
target/
*.iml
.idea
package edu.kit.formal;
import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
import edu.kit.formal.proofscriptparser.ast.ASTNode;
import lombok.Getter;
import lombok.Setter;
import java.util.logging.Logger;
/**
* @author Alexander Weigl
* @version 1 (21.05.17)
*/
public class ScopeLogger extends DefaultASTVisitor<Void> {
private Logger logger;
@Getter
@Setter
private String suffix = "", prefix = "";
public ScopeLogger(String name) {
logger = Logger.getLogger(name);
}
@Override
public Void defaultVisit(ASTNode node) {
logger.info(suffix + node.getNodeName() + " @" + node.getStartPosition().getCharInLine() + suffix);
logger.info(node.toString());
return null;
}
}
package edu.kit.formal.TestCommands;
import edu.kit.formal.interpreter.State;
/**
* Created by sarah on 5/17/17.
*/
public abstract class AbstractCommand {
public abstract State execute(State s);
}
package edu.kit.formal.TestCommands;
import edu.kit.formal.interpreter.State;
/**
* TestCommand
* Created by sarah on 5/17/17.
*/
public final class PrintCommand extends AbstractCommand {
public State execute(State s) {
System.out.println("Printing state " + s + " " + s.getSelectedGoalNode().toString());
return s;
}
}
package edu.kit.formal.TestCommands;
import edu.kit.formal.interpreter.GoalNode;
import edu.kit.formal.interpreter.State;
import edu.kit.formal.interpreter.Value;
import edu.kit.formal.interpreter.VariableAssignment;
import edu.kit.formal.proofscriptparser.ast.Type;
import java.math.BigInteger;
/**
* Created by sarah on 5/17/17.
*/
public class SplitCommand extends AbstractCommand {
@Override
public State execute(State s) {
GoalNode g = s.getSelectedGoalNode();
VariableAssignment assignments = g.getAssignments();
String seq1 = g.getSequent().concat("1");
String seq2 = g.getSequent().concat("2");
s.getGoals().remove(g);
s.getGoals().add(new GoalNode(g, seq1));
GoalNode g2 = new GoalNode(g, seq2);
g2.setVarValue("z", new Value(Type.INT, BigInteger.valueOf(10)));
s.getGoals().add(g2);
return s;
}
}
package edu.kit.formal.interpreter;
import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
import edu.kit.formal.proofscriptparser.Visitor;
import edu.kit.formal.proofscriptparser.ast.*;
import lombok.Getter;
import lombok.Setter;
......@@ -14,17 +15,27 @@ import java.util.List;
* @author S.Grebing
* @author A. Weigl
*/
public class Evaluator extends DefaultASTVisitor<Value> {
public class Evaluator extends DefaultASTVisitor<Value> implements ScopeObservable {
private GoalNode currentState;
private List<VariableAssignment> matchedVariables = new ArrayList<>();
@Getter
@Setter
private MatcherApi matcher;
@Getter
private List<Visitor> entryListeners = new ArrayList<>(),
exitListeners = new ArrayList<>();
public Evaluator(GoalNode s) {
this.currentState = s;
}
public Evaluator(GoalNode g, MatcherApi matcherApi) {
this(g);
setMatcher(matcherApi);
}
/**
* Evaluation of an expression.
*
......
package edu.kit.formal.interpreter;
import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
import edu.kit.formal.proofscriptparser.ast.*;
import lombok.Getter;
import lombok.Setter;
import java.util.List;
/**
* Class handling evaluation of expressions (visitor for expressions)
*
* @author S.Grebing
*/
public class Evaluator extends DefaultASTVisitor<Value> {
<<<<<<< Updated upstream
private State currentState;
private Stack<List<GoalNode>> matchedGoals = new Stack<>();
private EvaluatorABI abi;
=======
private GoalNode currentState;
private List<VariableAssignment> matchedVariables = new ArrayList<>();
@Getter
@Setter
private MatcherApi matcher;
>>>>>>> Stashed changes
public Evaluator(State s) {
this.currentState = s;
}
/**
* Evaluation of an expression.
*
* @param truth
* @return
*/
public Value eval(Expression truth) {
return (Value) truth.accept(this);
}
@Override
public Value visit(BinaryExpression e) {
Value v1 = (Value) e.getLeft().accept(this);
Value v2 = (Value) e.getRight().accept(this);
Operator op = e.getOperator();
return op.evaluate(v1, v2);
}
/**
* TODO Connect with KeY
*
* @param match
* @return
*/
@Override
public Value visit(MatchExpression match) {
<<<<<<< Updated upstream
=======
Value pattern = (Value) match.getPattern().accept(this);
>>>>>>> Stashed changes
List<VariableAssignment> va = null;
if (pattern.getType() == Type.STRING) {
va = matcher.matchLabel(currentState, (String) pattern.getData());
} else if (pattern.getType() == Type.TERM) {
va = matcher.matchSeq(currentState, (String) pattern.getData());
}
return va != null && va.size() > 0 ? Value.TRUE : Value.FALSE;
}
/**
* TODO Connect with KeY
*
* @param term
* @return
*/
@Override
public Value visit(TermLiteral term) {
return null;
}
@Override
public Value visit(StringLiteral string) {
return Value.from(string);
}
@Override
public Value visit(Variable variable) {
//get variable value
String id = variable.getIdentifier();
Value v = currentState.lookupVarValue(id);
if (v != null) {
return v;
} else {
throw new RuntimeException("Variable " + variable + " was not initialized");
}
}
@Override
public Value visit(BooleanLiteral bool) {
return bool.isValue() ? Value.TRUE : Value.FALSE;
}
@Override
public Value visit(IntegerLiteral integer) {
return Value.from(integer);
}
@Override
public Value visit(UnaryExpression e) {
Operator op = e.getOperator();
Expression expr = e.getExpression();
Value exValue = (Value) expr.accept(this);
return op.evaluate(exValue);
}
}
......@@ -39,7 +39,7 @@ public class GoalNode {
public String toString() {
String s = "Seq: " + sequent + "\n" +
assignments.toString();
assignments.asMap();
return s;
}
......@@ -53,7 +53,6 @@ public class GoalNode {
return v;
} else {
throw new RuntimeException("Value of variable " + varname + " is not defined in goal node " + this.toString());
}
}
......@@ -78,6 +77,7 @@ public class GoalNode {
/**
* Add a variable declaration to the type map (TODO Default value in map?)
*
* @param name
* @param t
*/
......
package edu.kit.formal.interpreter;
import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
import edu.kit.formal.proofscriptparser.ast.ASTNode;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
import java.util.LinkedList;
import java.util.List;
/**
* @author Alexander Weigl
* @version 1 (21.05.17)
*/
@RequiredArgsConstructor
public class HistoryListener extends DefaultASTVisitor<Void> {
@Getter
private final List<ASTNode> queueNode = new LinkedList<>();
private final List<AbstractState> queueState = new LinkedList<>();
private final Interpreter interpreter;
@Override
public Void defaultVisit(ASTNode node) {
queueState.add(interpreter.getCurrentState());
queueNode.add(node);
return null;
}
}
package edu.kit.formal.interpreter;
import edu.kit.formal.TestCommands.AbstractCommand;
import edu.kit.formal.TestCommands.PrintCommand;
import edu.kit.formal.TestCommands.SplitCommand;
import edu.kit.formal.interpreter.funchdl.CommandCall;
import edu.kit.formal.interpreter.funchdl.CommandLookup;
import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
import edu.kit.formal.proofscriptparser.Visitor;
import edu.kit.formal.proofscriptparser.ast.*;
import lombok.Getter;
import lombok.Setter;
import org.antlr.v4.runtime.ParserRuleContext;
import javax.xml.bind.annotation.XmlSeeAlso;
import java.util.*;
import java.util.logging.Logger;
/**
* Main Class for interpreter
*
* @author S.Grebing
*/
public class Interpreter<T> extends DefaultASTVisitor<T> {
public class Interpreter extends DefaultASTVisitor<Void>
implements ScopeObservable {
//TODO later also include information about source line for each state (for debugging purposes and rewind purposes)
public Stack<AbstractState> stateStack;
private Stack<AbstractState> stateStack = new Stack<>();
private static Logger logger = Logger.getLogger("interpreter");
public HashMap<String, ProofScript> localCommands;
public HashMap<String, AbstractCommand> commands = new HashMap<>();
@Getter
private List<Visitor> entryListeners = new ArrayList<>(),
exitListeners = new ArrayList<>();
public Interpreter() {
localCommands = new LinkedHashMap<>();
commands.put("printState", new PrintCommand());
commands.put("splitState", new SplitCommand());
@Getter
@Setter
private MatcherApi matcherApi;
@Getter
private CommandLookup functionLookup;
@Getter
@Setter
private boolean scrictSelectedGoalMode = false;
public Interpreter(CommandLookup lookup) {
functionLookup = lookup;
}
//starting point is a statement list
public void interpret(List<ProofScript> scripts, String sequent) {
stateStack = new Stack<>();
GoalNode startNode = new GoalNode(null, sequent);
List<GoalNode> startNodes = new LinkedList<>();
startNodes.add(startNode);
//copy all local available proof script to hashmap for better lookup
scripts.forEach(p -> localCommands.put(p.getName(), p));
newState(new GoalNode(null, sequent));
//execute first script (RULE: The first script in the file is main script)
ProofScript m = scripts.get(0);
//create new state
State s = new State(startNodes, startNode);
stateStack.push(s);
//later through interface with getMainScript();
visit(m);
m.accept(this);
}
/**
* If new Block is entered, a new state has to be created (copy of current state) and pushed 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)
......@@ -68,69 +62,85 @@ public class Interpreter<T> extends DefaultASTVisitor<T> {
* @return
*/
@Override
public T visit(ProofScript proofScript) {
System.out.println("Visiting " + proofScript.getName());
public Void visit(ProofScript proofScript) {
enterScope(proofScript);
//add vars
visit(proofScript.getSignature());
System.out.println("Visited Signature");
Statements body = proofScript.getBody();
visit(body);
proofScript.getBody().accept(this);
exitScope(proofScript);
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());
AbstractState state = stateStack.pop();
GoalNode node = state.getSelectedGoalNode();
public Void visit(AssignmentStatement assignmentStatement) {
enterScope(assignmentStatement);
GoalNode node = getSelectedNode();
Type t = assignmentStatement.getType();
Variable var = assignmentStatement.getLhs();
Expression expr = assignmentStatement.getRhs();
if (t != null) {
node.addVarDecl(var.getIdentifier(), t);
}
if (expr != null) {
Type type = node.lookUpType(var.getIdentifier());
if (type == null) {
throw new RuntimeException("Type of Variable " + var.getIdentifier() + " is not declared yet");
} else {
Evaluator eval = new Evaluator(state.getSelectedGoalNode());
Value v = (Value) expr.accept(eval);
Value v = evaluate(expr);
node.setVarValue(var.getIdentifier(), v);
}
}
stateStack.push(state);
exitScope(assignmentStatement);
return null;
}
private Value evaluate(Expression expr) {
return evaluate(getSelectedNode(), expr);
}
private Value evaluate(GoalNode g, Expression expr) {
enterScope(expr);
Evaluator evaluator = new Evaluator(g, matcherApi);
evaluator.getEntryListeners().addAll(entryListeners);
evaluator.getExitListeners().addAll(exitListeners);
exitScope(expr);
return evaluator.eval(expr);
}
/**
* Visiting a statement list results in visiting each statement
*
* @param statements
* @return
*/
@Override
public T visit(Statements statements) {
public Void visit(Statements statements) {
enterScope(statements);
for (Statement s : statements) {
s.accept(this);
}
exitScope(statements);
return null;
}
/**
*
* @param casesStatement
* @return
*/
@Override
public T visit(CasesStatement casesStatement) {
public Void visit(CasesStatement casesStatement) {
enterScope(casesStatement);
State beforeCases = (State) stateStack.pop();
//enterscope
List<GoalNode> allGoalsBeforeCases = beforeCases.getGoals();
for (GoalNode node : allGoalsBeforeCases) {
node.enterNewVarScope();
......@@ -158,8 +168,7 @@ public class Interpreter<T> extends DefaultASTVisitor<T> {
//assumption, matchpattern handles varAssignments
while (goalIter.hasNext()) {
GoalNode g = goalIter.next();
Evaluator goalEval = new Evaluator(g);
Value eval = goalEval.eval(guard);
Value eval = evaluate(g, guard);
System.out.println();
if (eval.getData().equals(true)) {
forCase.add(g);
......@@ -216,16 +225,19 @@ public class Interpreter<T> extends DefaultASTVisitor<T> {
stateStack.push(newStateAfterCases);
}
exitScope(casesStatement);
return null;
}
/**
*
* @param caseStatement
* @return
*/
@Override
public T visit(CaseStatement caseStatement) {
public Void visit(CaseStatement caseStatement) {
enterScope(caseStatement);
exitScope(caseStatement);
return null;
}
......@@ -237,59 +249,47 @@ public class Interpreter<T> extends DefaultASTVisitor<T> {
* 3) adding the assigned parameters to the variable assignments
* 4) visiting 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) {
public Void visit(CallStatement call) {
enterScope(call);
//neuer VarScope
State newState = (State) stateStack.pop();
//enter new variable scope
newState.getSelectedGoalNode().enterNewVarScope();
stateStack.push(newState);
Evaluator eval = new Evaluator(newState.getSelectedGoalNode());
String commandName = call.getCommand();
Parameters parameters = call.getParameters();
ProofScript commandScript;
//TODO refactor into own interface/facade for proof commands
if (localCommands.containsKey(commandName)) {
commandScript = localCommands.get(commandName);
Signature sig = commandScript.getSignature();
Iterator<Map.Entry<Variable, Expression>> paramIterator = parameters.entrySet().iterator();
//Iterator<Map.Entry<Variable, Type>> sigIter = sig.entrySet().iterator();
while (paramIterator.hasNext()) {
Map.Entry<Variable, Expression> 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.peek().getSelectedGoalNode().exitNewVarScope();
} else {
if (commands.containsKey(commandName)) {
AbstractCommand com = commands.get(commandName);
State current = (State) stateStack.pop();
State afterCom = com.execute(current);
afterCom.getSelectedGoalNode().exitNewVarScope();
stateStack.push(afterCom);
} else {
throw new RuntimeException("Command " + commandName + " is not known");