further bug fixes in variable assignments, added key.core.jar and dependencies

.idea/libraries/Maven__antlr_antlr_2_7_7.xml

+<component name="libraryTable">
+  <library name="Maven: antlr:antlr:2.7.7">
+    <CLASSES>
+      <root url="jar://$MAVEN_REPOSITORY$/antlr/antlr/2.7.7/antlr-2.7.7.jar!/" />
+    </CLASSES>
+    <JAVADOC>
+      <root url="jar://$MAVEN_REPOSITORY$/antlr/antlr/2.7.7/antlr-2.7.7-javadoc.jar!/" />
+    </JAVADOC>
+    <SOURCES>
+      <root url="jar://$MAVEN_REPOSITORY$/antlr/antlr/2.7.7/antlr-2.7.7-sources.jar!/" />
+    </SOURCES>
+  </library>
+</component>
\ No newline at end of file

.idea/libraries/Maven__net_java_dev_javacc_javacc_4_0.xml

+<component name="libraryTable">
+  <library name="Maven: net.java.dev.javacc:javacc:4.0">
+    <CLASSES>
+      <root url="jar://$MAVEN_REPOSITORY$/net/java/dev/javacc/javacc/4.0/javacc-4.0.jar!/" />
+    </CLASSES>
+    <JAVADOC>
+      <root url="jar://$MAVEN_REPOSITORY$/net/java/dev/javacc/javacc/4.0/javacc-4.0-javadoc.jar!/" />
+    </JAVADOC>
+    <SOURCES>
+      <root url="jar://$MAVEN_REPOSITORY$/net/java/dev/javacc/javacc/4.0/javacc-4.0-sources.jar!/" />
+    </SOURCES>
+  </library>
+</component>
\ No newline at end of file

.idea/libraries/Maven__org_antlr_antlr_3_5_2.xml

+<component name="libraryTable">
+  <library name="Maven: org.antlr:antlr:3.5.2">
+    <CLASSES>
+      <root url="jar://$MAVEN_REPOSITORY$/org/antlr/antlr/3.5.2/antlr-3.5.2.jar!/" />
+    </CLASSES>
+    <JAVADOC>
+      <root url="jar://$MAVEN_REPOSITORY$/org/antlr/antlr/3.5.2/antlr-3.5.2-javadoc.jar!/" />
+    </JAVADOC>
+    <SOURCES>
+      <root url="jar://$MAVEN_REPOSITORY$/org/antlr/antlr/3.5.2/antlr-3.5.2-sources.jar!/" />
+    </SOURCES>
+  </library>
+</component>
\ No newline at end of file

.idea/libraries/Maven__org_key_project_key_core_2_7.xml

+<component name="libraryTable">
+  <library name="Maven: org.key-project:key.core:2.7">
+    <CLASSES>
+      <root url="jar://$MAVEN_REPOSITORY$/org/key-project/key.core/2.7/key.core-2.7.jar!/" />
+    </CLASSES>
+    <JAVADOC>
+      <root url="jar://$MAVEN_REPOSITORY$/org/key-project/key.core/2.7/key.core-2.7-javadoc.jar!/" />
+    </JAVADOC>
+    <SOURCES>
+      <root url="jar://$MAVEN_REPOSITORY$/org/key-project/key.core/2.7/key.core-2.7-sources.jar!/" />
+    </SOURCES>
+  </library>
+</component>
\ No newline at end of file

.idea/libraries/Maven__org_key_project_recoderKey_1_0_0.xml

+<component name="libraryTable">
+  <library name="Maven: org.key-project:recoderKey:1.0.0">
+    <CLASSES>
+      <root url="jar://$MAVEN_REPOSITORY$/org/key-project/recoderKey/1.0.0/recoderKey-1.0.0.jar!/" />
+    </CLASSES>
+    <JAVADOC>
+      <root url="jar://$MAVEN_REPOSITORY$/org/key-project/recoderKey/1.0.0/recoderKey-1.0.0-javadoc.jar!/" />
+    </JAVADOC>
+    <SOURCES>
+      <root url="jar://$MAVEN_REPOSITORY$/org/key-project/recoderKey/1.0.0/recoderKey-1.0.0-sources.jar!/" />
+    </SOURCES>
+  </library>
+</component>
\ No newline at end of file

pom.xml

-<project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+<project xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns="http://maven.apache.org/POM/4.0.0"
          xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
     <modelVersion>4.0.0</modelVersion>
 
@@ -118,6 +118,31 @@
             <version>1.16.16</version>
             <scope>provided</scope>
         </dependency>
+        <dependency>
+            <groupId>org.key-project</groupId>
+            <artifactId>key.core</artifactId>
+            <version>2.7</version>
+        </dependency>
+        <dependency>
+            <groupId>org.antlr</groupId>
+            <artifactId>antlr</artifactId>
+            <version>3.5.2</version>
+        </dependency>
+        <dependency>
+            <groupId>antlr</groupId>
+            <artifactId>antlr</artifactId>
+            <version>2.7.7</version>
+        </dependency>
+        <dependency>
+            <groupId>net.java.dev.javacc</groupId>
+            <artifactId>javacc</artifactId>
+            <version>4.0</version>
+        </dependency>
+        <dependency>
+            <groupId>org.key-project</groupId>
+            <artifactId>recoderKey</artifactId>
+            <version>1.0.0</version>
+        </dependency>
     </dependencies>
 
 

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

@@ -5,10 +5,12 @@ grammar ScriptLanguage;
     : stmtList
     ;
 */
+
 start
-    :   (SCRIPT name=ID '(' signature=argList? ')' INDENT body=stmtList DEDENT)*
+    :   (script)*
     ;
 
+script: SCRIPT name=ID '(' signature=argList? ')' INDENT body=stmtList DEDENT;
 argList
     :   varDecl (',' varDecl)*
     ;
@@ -21,10 +23,10 @@ stmtList
     :   statement*
     ;
 
+
 statement
     :   //scriptDecl
-       varDecl
-    |   assignment
+         assignment
     |   repeatStmt
     |   casesStmt
     |   forEachStmt
@@ -39,7 +41,8 @@ statement
     ;
 */
 assignment
-    :   variable=ID (COLON type=ID)? ASSIGN expression SEMICOLON
+    :   variable=ID COLON type=ID SEMICOLON
+    |   variable=ID (COLON type=ID)? ASSIGN expression SEMICOLON
     ;
 
 expression

src/main/java/edu/kit/formal/TestCommands/AbstractCommand.java

+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);
+}

src/main/java/edu/kit/formal/TestCommands/PrintCommand.java

+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;
+    }
+
+}

src/main/java/edu/kit/formal/TestCommands/SplitCommand.java

+package edu.kit.formal.TestCommands;
+
+import edu.kit.formal.interpreter.GoalNode;
+import edu.kit.formal.interpreter.State;
+
+/**
+ * Created by sarah on 5/17/17.
+ */
+public class SplitCommand extends AbstractCommand {
+    @Override
+    public State execute(State s) {
+        GoalNode g = s.getSelectedGoalNode();
+        String seq1 = g.getSequent().concat("1");
+        String seq2 = g.getSequent().concat("2");
+
+        s.getGoals().remove(g);
+        s.getGoals().add(new GoalNode(g, seq1));
+        s.getGoals().add(new GoalNode(g, seq2));
+        return s;
+    }
+}

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

@@ -33,7 +33,9 @@ public class GoalNode {
     }
 
     public String toString() {
-        return sequent;
+        String s = "Seq: " + sequent + "\n" +
+                assignments.toString();
+        return s;
     }
 
     /**
@@ -41,7 +43,7 @@ public class GoalNode {
      * @return value of variable if it exists
      */
     public Value lookupVarValue(String varname) {
-        Value v = assignments.getValue(varname);
+        Value v = assignments.lookupVarValue(varname);
         if (v != null) {
             return v;
         } else {
@@ -59,26 +61,28 @@ public class GoalNode {
      */
 
     public Type lookUpType(String id) {
-        Type t = this.getAssignments().getTypes().get(id);
+        Type t = this.getAssignments().lookupType(id);
         if (t == null) {
-            //TODO lookup parent and outer Scope
-            // this.getAssignments().
+            throw new RuntimeException("Variable " + id + " must be declared first");
         } else {
+
             return t;
         }
-        return null;
     }
 
 
     /**
-     * Add a variable declaration to the type map
-     * TODO default value in valuemap?
-     *
+     * Add a variable declaration to the type map (TODO Default value in map?)
      * @param name
      * @param t
      */
     public void addVarDecl(String name, Type t) {
-        getAssignments().addVariable(name, t);
+        VariableAssignment assignments = this.getAssignments().addVarDecl(name, t);
+        if (assignments == null) {
+            throw new RuntimeException("Could not add var decl " + name);
+        } else {
+            this.assignments = assignments;
+        }
     }
 
     /**
@@ -89,11 +93,8 @@ public class GoalNode {
      */
     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");
-        }
+        assignments.setVarValue(name, v);
+
     }
 
     /**

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

 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.proofscriptparser.DefaultASTVisitor;
 import edu.kit.formal.proofscriptparser.ast.*;
 
@@ -11,13 +14,16 @@ import java.util.*;
  * @author S.Grebing
  */
 public class Interpreter<T> extends DefaultASTVisitor<T> {
-    //TODO later also inclulde information about source line for each state (for debugging purposes and rewind purposes)
+    //TODO later also include information about source line for each state (for debugging purposes and rewind purposes)
     public Stack<AbstractState> stateStack;
 
     public HashMap<String, ProofScript> localCommands;
+    public HashMap<String, AbstractCommand> commands = new HashMap<>();
 
     public Interpreter() {
         localCommands = new LinkedHashMap<>();
+        commands.put("printState", new PrintCommand());
+        commands.put("splitState", new SplitCommand());
     }
 
     //starting point is a statement list
@@ -40,7 +46,7 @@ public class Interpreter<T> extends DefaultASTVisitor<T> {
     }
 
     /**
-     * If new Block is entered, a new state has to be created (copy of current state) and opushed to the stack
+     * If new Block is entered, a new state has to be created (copy of current state) and pushed to the stack
      */
     private void enterScope() {
 
@@ -63,10 +69,11 @@ public class Interpreter<T> extends DefaultASTVisitor<T> {
      */
     @Override
     public T visit(ProofScript proofScript) {
-        //AbstractState currentState = stateStack.pop();
+
         System.out.println("Visiting " + proofScript.getName());
         //add vars
         visit(proofScript.getSignature());
+        System.out.println("Visited Signature");
         Statements body = proofScript.getBody();
         visit(body);
         return null;
@@ -82,16 +89,20 @@ public class Interpreter<T> extends DefaultASTVisitor<T> {
         System.out.println("Visiting Assignment " + assignmentStatement.toString());
         AbstractState state = stateStack.pop();
         GoalNode node = state.getSelectedGoalNode();
+        Type t = assignmentStatement.getType();
         Variable var = assignmentStatement.getLhs();
         Expression expr = assignmentStatement.getRhs();
-        if (node != null) {
-            Type t = node.lookUpType(var.getIdentifier());
-            if (t != null) {
+        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);
-                node.getAssignments().setVar(var.getIdentifier(), v);
-            } else {
-                throw new RuntimeException("Assignment problem");
+                node.setVarValue(var.getIdentifier(), v);
             }
         }
         stateStack.push(state);
@@ -118,9 +129,36 @@ public class Interpreter<T> extends DefaultASTVisitor<T> {
      */
     @Override
     public T visit(CasesStatement casesStatement) {
-        //neuerScope
-        casesStatement.getCases();
+        State beforeCases = (State) stateStack.pop();
+        //enterscope
+        List<GoalNode> allGoalsBeforeCases = beforeCases.getGoals();
+        for (GoalNode node : allGoalsBeforeCases) {
+            node.enterNewVarScope();
+        }
+        //copy the list of goal nodes for keeping track of goals
+        List<GoalNode> copiedList = new ArrayList<>();
+        for (GoalNode goalNode : allGoalsBeforeCases) {
+            copiedList.add(goalNode);
+        }
+
+        //handle cases TODO
+        List<CaseStatement> cases = casesStatement.getCases();
+        Iterator<CaseStatement> casesIter = cases.iterator();
+        while (casesIter.hasNext()) {
+            CaseStatement currentCase = casesIter.next();
+            currentCase.getGuard();
+        }
         casesStatement.getDefaultCase();
+
+
+        //exit scope
+        State aftercases = (State) stateStack.pop();
+        List<GoalNode> goalsAfterCases = aftercases.getGoals();
+        if (!goalsAfterCases.isEmpty()) {
+            for (GoalNode goalAfterCases : goalsAfterCases) {
+                goalAfterCases.exitNewVarScope();
+            }
+        }
         return null;
     }
 
@@ -140,15 +178,18 @@ public class Interpreter<T> extends DefaultASTVisitor<T> {
      * 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
+     * 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) {
-        //neuer scope
-        State newState = stateStack.peek().copy();
+        //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();
@@ -172,9 +213,17 @@ public class Interpreter<T> extends DefaultASTVisitor<T> {
             newState.getSelectedGoalNode().enterNewVarScope();
             stateStack.push(newState);
             visit(commandScript.getBody());
-            stateStack.pop().getSelectedGoalNode().exitNewVarScope();
+            stateStack.peek().getSelectedGoalNode().exitNewVarScope();
         } else {
-            throw new RuntimeException("Command " + commandName + " is not known");
+            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");
+            }
         }
 
         return null;
@@ -236,6 +285,8 @@ public class Interpreter<T> extends DefaultASTVisitor<T> {
 
     @Override
     public T visit(Parameters parameters) {
+
+        System.out.println("Params " + parameters.toString());
         return null;
     }
 

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

@@ -61,8 +61,6 @@ public class State extends AbstractState {
     public State copy() {
         List<GoalNode> copiedGoals = new ArrayList<>();
         GoalNode refToSelGoal = selectedGoalNode;
-
-
         return new State(copiedGoals, refToSelGoal);
     }
 

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

@@ -38,7 +38,15 @@ public class VariableAssignment {
         return types;
     }
 
-    public VariableAssignment copy() {
+    public Type lookupType(String name) {
+        if (parent == null) {
+            return types.getOrDefault(name, null);
+        } else {
+            return types.getOrDefault(name, parent.lookupType(name));
+        }
+    }
+
+/*    public VariableAssignment copy() {
         VariableAssignment copy;
         if (parent != null) {
             copy = new VariableAssignment(this.parent.copy());
@@ -51,7 +59,7 @@ public class VariableAssignment {
         //deepcopy types
         return copy;
     }
-
+*/
 
     /**
      * Lookup value of variable also in parent assignments
@@ -59,24 +67,25 @@ public class VariableAssignment {
      * @param name
      * @return
      */
-    //TODO throw exception
-    public Value getValue(String name) {
+
+    public Value lookupVarValue(String name) {
         if (parent == null) {
             return values.getOrDefault(name, null);
         } else {
-            return values.getOrDefault(name, parent.getValue(name));
+            return values.getOrDefault(name, parent.lookupVarValue(name));
         }
     }
 
-    public VariableAssignment addVariable(String name, Type type) {
-        this.types.put(name, type);
-        return this;
+    public VariableAssignment addVarDecl(String name, Type type) {
+        if (lookupType(name) == null) {
+            this.types.put(name, type);
+            return this;
+        } else {
+            throw new RuntimeException("Variable " + name + " is already declared with type " + type.toString());
+        }
     }
 
-    /*
-        public VariableAssignment peek(){
-            TODO?
-        }*/
+
     //enterscope
     public VariableAssignment push() {
         return new VariableAssignment(this);
@@ -87,8 +96,26 @@ public class VariableAssignment {
         return getParent();
     }
 
-    public VariableAssignment setVar(String name, Value v) {
-        this.getValues().put(name, v);
-        return this;
+    public VariableAssignment setVarValue(String name, Value v) {
+        VariableAssignment temp = this;
+        if (this.getTypes().containsKey(name)) {
+            this.values.put(name, v);
+        } else {
+            if (parent != null) {
+                parent.setVarValue(name, v);
+            } else {
+                throw new RuntimeException("Variable " + name + " needs to be declared first");
+            }
+        }
+        return temp;
+    }
+
+    @Override
+    public String toString() {
+        return "VariableAssignment{" +
+                "parent=" + parent +
+                ", values=" + values +
+                ", types=" + types +
+                '}';
     }
 }

src/main/java/edu/kit/formal/proofscriptparser/TransformAst.java

@@ -45,17 +45,23 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
     }
 
     @Override
-    public ProofScript visitStart(ScriptLanguageParser.StartContext ctx) {
+    public ProofScript visitScript(ScriptLanguageParser.ScriptContext ctx) {
         ProofScript s = new ProofScript();
         s.setName(ctx.name.getText());
         s.setRuleContext(ctx);
         if (ctx.signature != null)
             s.setSignature((Signature) ctx.signature.accept(this));
         s.setBody((Statements) ctx.body.accept(this));
-        scripts.add(s);
         return s;
     }
 
+    @Override
+    public List<ProofScript> visitStart(ScriptLanguageParser.StartContext ctx) {
+        ctx.script().forEach(s ->
+                scripts.add((ProofScript) s.accept(this)));
+        return scripts;
+    }
+
     @Override
     public Signature visitArgList(ScriptLanguageParser.ArgListContext ctx) {
         Signature signature = new Signature();
@@ -89,6 +95,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
         return statements;
     }
 
+
     @Override
     public Object visitStatement(ScriptLanguageParser.StatementContext ctx) {
         return ctx.getChild(0).accept(this);
@@ -99,7 +106,12 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
         AssignmentStatement assign = new AssignmentStatement();
         assign.setRuleContext(ctx);
         assign.setLhs(new Variable(ctx.variable));
-        assign.setRhs((Expression) ctx.expression().accept(this));
+        if (ctx.type != null) {
+            assign.setType(Type.findType(ctx.type.getText()));
+        }
+        if (ctx.expression() != null) {
+            assign.setRhs((Expression) ctx.expression().accept(this));
+        }
         return assign;
     }
 

src/main/java/edu/kit/formal/proofscriptparser/Visitor.java

@@ -68,4 +68,6 @@ public interface Visitor<T> {
     T visit(Parameters parameters);
 
     T visit(UnaryExpression e);
+
+
 }

src/main/java/edu/kit/formal/proofscriptparser/ast/AssignmentStatement.java

@@ -44,7 +44,7 @@ public class AssignmentStatement
         extends Statement<ScriptLanguageParser.AssignmentContext> {
     @NonNull
     private Variable lhs;
-    @NonNull