First Part of Interpreter

src/main/antlr4/edu/kit/formal/proofscriptparser/ScriptLanguage.g4

 grammar ScriptLanguage;
+//TODO There is still sth. missing:import statements at the beginning to allow scripts from other files
 
+/*start
+    : stmtList
+    ;
+*/
 start
     :   (SCRIPT name=ID '(' signature=argList? ')' INDENT body=stmtList DEDENT)*
     ;
@@ -17,7 +22,9 @@ stmtList
     ;
 
 statement
-    :   assignment
+    :   //scriptDecl
+       varDecl
+    |   assignment
     |   repeatStmt
     |   casesStmt
     |   forEachStmt
@@ -26,6 +33,11 @@ statement
   //  |   callStmt
     ;
 
+/*scriptDecl
+    :
+    SCRIPT name=ID '(' signature=argList? ')' INDENT body=stmtList DEDENT
+    ;
+*/
 assignment
     :   variable=ID (COLON type=ID)? ASSIGN expression SEMICOLON
     ;
@@ -166,62 +178,8 @@ IMP : '==>' ;
 EQUIV : '<=>' ;
 NOT: 'not';
 
-//options {...}
-//import ... ;
 
-//tokens {...}
-//channels {...} // lexer only
-//@actionName {...}
 
-/*
-//Script ::= 'script' ID (ARGLIST)? NEWLINE INDENT Cmd DEDENT | Cmd
 
-Cmd ::= //Cmd ';' Cmd |
-        VarAssign |
-        //'repeat' NEWLINE INDENT Cmd+ DEDENT |
-        'cases' NEWLINE DEDENT Case+ ('default:' NEWLINE INDENT Cmd DEDENT)? DEDENT |
-        'foreach' NEWLINE INDENT Cmd+ DEDENT |
-        'theonly'NEWLINE INDENT cmd DEDENT |
-       // Cmd 'on' (ShemaTerm | ShemaVar)+ ('with' (ShemaVar| ShemaTerm))? |
-       'call' scriptCommand;
-
-Case ::= 'case' BoolExpr ':' NEWLINE INDENT Cmd+ DEDENT
-
-VarAssign ::= ID ':' TYPE  |
-              ID ':=' (AExpr| BExpr | ///PosExpr) //PosExp evtl. das matchpattern für Sequents?
-
-//MatchPattern ::= 'match' ('Seq'? ShemaSeq) |
-//                ('matchLabel'| 'matchRule') RegExpr
-
-//                'match' ( `~[`]` | '~[\']' | ID)
-*/
 
 
-
-/*arithExpr
-    :   ID
-    |   DIGITS
-    |   arithExpr arithOp arithExpr
-    ;
-
-arithOp
-    :   '+' | '-' | '*' | '/'
-    ;
-
-boolExpr
-    :   TRUE
-    |   FALSE
-    |   matchPattern
-    |   'not' boolExpr
-    |   boolExpr boolOp boolExpr
-    |   arithExpr relOp arithExpr
-    ;
-
-boolOp
-    :   'and' | 'or'
-    ;
-
-relOp
-    :   '<' | '<=' | '=' | '>' | '>='
-    ;
-*/
\ No newline at end of file

src/main/java/edu/kit/formal/interpreter/AbstractState.java

+package edu.kit.formal.interpreter;
+
+import java.util.List;
+
+/**
+ * Represents a script state
+ */
+public abstract class AbstractState {
+    /**
+     * Returns whether the state is an ErrorState
+     *
+     * @return
+     */
+    public abstract boolean isErrorState();
+
+    /**
+     * Returns all GoalNodes in a state
+     *
+     * @return
+     */
+    public abstract List<GoalNode> getGoals();
+
+    /**
+     * Returns the selected GoalNode to which the next statement should be applied
+     * Can be null if no selector was applied or state is an ErrorState
+     *
+     * @return GoalNode or null
+     */
+    public abstract GoalNode getSelectedGoalNode();
+
+
+    public State copy() {
+        // return new State();
+        return null;
+    }
+}

src/main/java/edu/kit/formal/interpreter/ErrorState.java

+package edu.kit.formal.interpreter;
+
+import java.util.List;
+
+/**
+ * State representing error states
+ *
+ * @author S.Grebing
+ */
+public class ErrorState extends AbstractState {
+    @Override
+    public boolean isErrorState() {
+        return true;
+    }
+
+    @Override
+    public List<GoalNode> getGoals() {
+        return null;
+    }
+
+    @Override
+    public GoalNode getSelectedGoalNode() {
+        return null;
+    }
+}

src/main/java/edu/kit/formal/interpreter/Evaluator.java

+package edu.kit.formal.interpreter;
+
+import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
+import edu.kit.formal.proofscriptparser.ast.*;
+
+/**
+ * Class handling evaluation of expressions (visitor for expressions)
+ *
+ * @author S.Grebing
+ */
+public class Evaluator extends DefaultASTVisitor<Value> {
+    State currentState;
+
+    public Evaluator(State s) {
+        this.currentState = s;
+    }
+
+
+    @Override
+    public Value visit(BinaryExpression e) {
+        Value v1 = (Value) e.getLeft().accept(this);
+        Value v2 = (Value) e.getLeft().accept(this);
+        Operator op = e.getOperator();
+        return op.evaluate(v1, v2);
+
+    }
+
+    /**
+     * TODO Connect with KeY
+     *
+     * @param match
+     * @return
+     */
+    @Override
+    public Value visit(MatchExpression match) {
+        return null;
+    }
+
+    /**
+     * 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();
+        GoalNode n = currentState.getSelectedGoalNode();
+        Value v = n.lookupVarValue(id);
+        if (v != null) {
+            return v;
+        } else {
+            throw new RuntimeException("Variable " + variable + " was not initialized");
+        }
+
+    }
+
+    @Override
+    public Value visit(BooleanLiteral bool) {
+        return Value.from(bool);
+    }
+
+
+    @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);
+    }
+
+
+}

src/main/java/edu/kit/formal/interpreter/GoalNode.java

+package edu.kit.formal.interpreter;
+
+import edu.kit.formal.proofscriptparser.ast.Type;
+
+/**
+ * Objects of this class represent a GoalNode in a script state
+ * If parent is null, this is the root
+ *
+ * @author S.Grebing
+ */
+public class GoalNode {
+
+    //TODO this is only for testing, later Sequent object or similar
+    private String sequent;
+
+    private VariableAssignment assignments;
+
+    private GoalNode parent;
+
+    public GoalNode(GoalNode parent, String seq) {
+        if (parent == null) {
+            this.assignments = new VariableAssignment(null);
+        }
+        this.parent = parent;
+        this.sequent = seq;
+    }
+
+    public VariableAssignment getAssignments() {
+        return assignments;
+    }
+
+    public GoalNode setAssignments(VariableAssignment assignments) {
+        this.assignments = assignments;
+        return this;
+    }
+
+    public GoalNode getParent() {
+        return parent;
+    }
+
+    public String toString() {
+        return sequent;
+    }
+
+    /**
+     * @param varname
+     * @return value of variable if it exists
+     */
+    public Value lookupVarValue(String varname) {
+
+        Value v = assignments.getValue(varname);
+        if (v != null) {
+            return v;
+        } else {
+            throw new RuntimeException("Value of variable " + varname + " is not defined in goal node " + this.toString());
+
+        }
+
+    }
+
+    /**
+     * Lookup the type of the variable in the type map
+     *
+     * @param id
+     * @return
+     */
+
+    public Type lookUpType(String id) {
+        Type t = this.getAssignments().getTypes().get(id);
+        if (t == null) {
+            //TODO lookup parent and outer Scope
+            // this.getAssignments().
+        } else {
+            return t;
+        }
+        return null;
+    }
+
+
+    /**
+     * Add a variable declaration to the type map
+     * TODO default value in valuemap?
+     *
+     * @param name
+     * @param t
+     */
+    public void addVarDecl(String name, Type t) {
+        this.assignments = getAssignments().addVariable(name, t);
+
+    }
+
+    /**
+     * Set the value of a variable in the value map
+     *
+     * @param name
+     * @param v
+     */
+    public void setVarValue(String name, Value v) {
+        VariableAssignment assignments = getAssignments();
+        if (assignments.getTypes().containsKey(name)) {
+            assignments.setVar(name, v);
+        } else {
+            throw new RuntimeException("Variable " + name + " has to be declared first");
+        }
+    }
+
+    /**
+     * Enter new variable scope and push onto stack
+     */
+    public void enterNewVarScope() {
+        this.assignments = this.assignments.push();
+    }
+
+    public void exitNewVarScope() {
+        this.assignments = this.assignments.pop();
+    }
+
+    public VariableAssignment peek() {
+        return null;
+    }
+
+}

src/main/java/edu/kit/formal/interpreter/Main.java

+package edu.kit.formal.interpreter;
+
+import edu.kit.formal.proofscriptparser.Facade;
+import edu.kit.formal.proofscriptparser.ast.ProofScript;
+
+import java.io.File;
+import java.io.IOException;
+import java.util.List;
+
+/**
+ * Test Main, will be replaced
+ */
+public class Main {
+    //This hard coded link is only for the first testing will be removed later on
+    private static File testFile = new File("/home/sarah/Documents/KIT_Mitarbeiter/ProofScriptingLanguage/src/test/resources/edu/kit/formal/proofscriptparser/scripts/test.txt");
+
+    public static void main(String[] args) {
+        //Erzeuge Parser
+        //lese P ein
+        //Erzeuge Interpreter
+        //rufe interpret(AST) auf interpreter auf
+        Facade f = new Facade();
+        try {
+            List<ProofScript> l = f.getAST(testFile);
+            Interpreter inter = new Interpreter();
+            inter.interpret(l, "TestSeq");
+        } catch (IOException e) {
+            e.printStackTrace();
+        }
+
+
+    }
+
+
+}

src/main/java/edu/kit/formal/interpreter/State.java

+package edu.kit.formal.interpreter;
+
+import java.util.List;
+
+/**
+ * Object representing a state
+ *
+ * @author S.Grebing
+ */
+public class State extends AbstractState {
+
+
+    /**
+     * All goalnodes in this state
+     */
+    private List<GoalNode> goals;
+
+
+    /**
+     * Currently selected GoalNode
+     */
+    private GoalNode selectedGoalNode;
+
+    public State(List<GoalNode> goals, GoalNode selected) {
+        this.goals = goals;
+        this.selectedGoalNode = selected;
+
+
+    }
+
+    @Override
+    public boolean isErrorState() {
+        return false;
+    }
+
+    @Override
+    public List<GoalNode> getGoals() {
+        return goals;
+    }
+
+    @Override
+    public GoalNode getSelectedGoalNode() {
+        if (selectedGoalNode == null) {
+            return null;
+        } else {
+            return selectedGoalNode;
+        }
+    }
+
+    public void setSelectedGoalNode(GoalNode selectedGoalNode) {
+        this.selectedGoalNode = selectedGoalNode;
+    }
+
+}
+

src/main/java/edu/kit/formal/interpreter/Value.java

+package edu.kit.formal.interpreter;
+
+import edu.kit.formal.proofscriptparser.ast.BooleanLiteral;
+import edu.kit.formal.proofscriptparser.ast.IntegerLiteral;
+import edu.kit.formal.proofscriptparser.ast.StringLiteral;
+import edu.kit.formal.proofscriptparser.ast.Type;
+import lombok.Getter;
+import lombok.RequiredArgsConstructor;
+
+import java.math.BigInteger;
+
+/**
+ * Class representing the values our variables may have
+ *
+ * @author S.Grebing
+ *         //TODO alle restlichen typen ergaenzen
+ */
+@RequiredArgsConstructor
+public class Value<T> {
+    @Getter
+    private final Type type;
+    @Getter
+    private final T data;
+
+
+    public static Value<BigInteger> from(IntegerLiteral i) {
+        return new Value<>(Type.INT, i.getValue());
+    }
+
+    public static Value<BigInteger> from(Integer i) {
+        return new Value<>(Type.INT, BigInteger.valueOf(i));
+    }
+
+    public static Value<String> from(StringLiteral s) {
+        return new Value<>(Type.INT, s.getText());
+    }
+
+    public static Value<Boolean> from(BooleanLiteral b) {
+        return new Value<>(Type.BOOL, b.isValue());
+    }
+
+    public static Value<Boolean> from(boolean equals) {
+        return new Value<>(Type.BOOL, equals);
+    }
+
+    public static Value<BigInteger> from(BigInteger apply) {
+        return new Value<>(Type.INT, apply);
+    }
+
+    @Override
+    public String toString() {
+        return "Value{" +
+                "type=" + type +
+                ", data=" + data +
+                '}';
+    }
+}

src/main/java/edu/kit/formal/interpreter/VariableAssignment.java

+package edu.kit.formal.interpreter;
+
+import edu.kit.formal.proofscriptparser.ast.Type;
+
+import java.util.HashMap;
+import java.util.Map;
+
+/**
+ * Variable Assignments for each goal node
+ *
+ * @author S.Grebing
+ */
+public class VariableAssignment {
+
+    private final VariableAssignment parent;
+    Map<String, Value> values;
+    Map<String, Type> types;
+
+    public VariableAssignment(VariableAssignment parent) {
+        values = new HashMap<>();
+        types = new HashMap<>();
+        this.parent = parent;
+    }
+
+    public VariableAssignment getParent() {
+        return parent;
+    }
+
+    public Map<String, Value> getValues() {
+        return values;
+    }
+
+    public Map<String, Type> getTypes() {
+        return types;
+    }
+
+    public VariableAssignment copy() {
+        VariableAssignment copy;
+        if (parent != null) {
+            copy = new VariableAssignment(this.parent.copy());
+
+        } else {
+            copy = new VariableAssignment(null);
+        }
+        //TODO
+        //copy.setValues(deepcopy of values);
+        //deepcopy types
+        return copy;
+    }
+
+
+    /**
+     * Lookup value of variable also in parent assignments
+     *
+     * @param name
+     * @return
+     */
+    //TODO throw exception
+    public Value getValue(String name) {
+        if (parent == null) {
+            return values.getOrDefault(name, null);
+        } else {
+            return values.getOrDefault(name, parent.getValue(name));
+        }
+    }
+
+    public VariableAssignment addVariable(String name, Type type) {
+        this.types.put(name, type);
+        return this;
+    }
+
+    /*
+        public VariableAssignment peek(){
+            TODO?