bind statement

lang/src/main/antlr/edu/kit/iti/formal/psdbg/parser/ScriptLanguage.g4

@@ -33,9 +33,18 @@ statement
     | scriptCommand
     | unconditionalBlock
     | conditionalBlock
+    | letStmt
   //  |   callStmt
     ;
 
+letStmt
+    :
+        'bind' expression
+        ( SEMICOLON
+        | 'in' ( statement | INDENT stmtList DEDENT)
+        )
+    ;
+
 /*scriptDecl
     :
     SCRIPT name=ID '(' signature=argList? ')' INDENT body=stmtList DEDENT

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTTraversal.java

@@ -262,4 +262,11 @@ public interface ASTTraversal<T> extends Visitor<T> {
         relaxBlock.getBody().accept(this);
         return null;
     }
+
+    @Override
+    default T visit(LetStatement let) {
+        let.getExpression().accept(this);
+        let.getBody().accept(this);
+        return null;
+    }
 }

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/DefaultASTVisitor.java

@@ -177,5 +177,9 @@ public class DefaultASTVisitor<T> implements Visitor<T> {
         return defaultVisit(relaxBlock);
     }
 
+    @Override
+    public T visit(LetStatement let) {
+        return defaultVisit(let);
+    }
 }
 

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java

@@ -29,6 +29,7 @@ import edu.kit.iti.formal.psdbg.parser.function.ScriptFunction;
 import edu.kit.iti.formal.psdbg.parser.types.TypeFacade;
 import lombok.Getter;
 import lombok.Setter;
+import lombok.val;
 import org.antlr.v4.runtime.ParserRuleContext;
 import org.antlr.v4.runtime.tree.ErrorNode;
 import org.antlr.v4.runtime.tree.ParseTree;
@@ -163,6 +164,26 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
         return ctx.getChild(0).accept(this);
     }
 
+    @Override
+    public Object visitLetStmt(ScriptLanguageParser.LetStmtContext ctx) {
+        LetStatement lst = new LetStatement();
+        lst.setRuleContext(ctx);
+        lst.setExpression((Expression) ctx.expression().accept(this));
+        lst.getExpression().setParent(lst);
+        if (ctx.statement() != null) {
+            val stmt = (Statement) ctx.statement().accept(this);
+            Statements stmts = new Statements();
+            stmts.add(stmt);
+            lst.setBody(stmts);
+            stmts.setParent(lst);
+        }
+        if (ctx.stmtList() != null) {
+            lst.setBody((Statements) ctx.stmtList().accept(this));
+            lst.getBody().setParent(lst);
+        }
+        return lst;
+    }
+
     @Override
     public Object visitAssignment(ScriptLanguageParser.AssignmentContext ctx) {
         AssignmentStatement assign = new AssignmentStatement();

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/Visitor.java

@@ -89,4 +89,6 @@ public interface Visitor<T> {
     T visit(StrictBlock strictBlock);
 
     T visit(RelaxBlock relaxBlock);
+
+    T visit(LetStatement let);
 }

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/LetStatement.java

+package edu.kit.iti.formal.psdbg.parser.ast;
+
+import edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser;
+import edu.kit.iti.formal.psdbg.parser.Visitor;
+import lombok.AllArgsConstructor;
+import lombok.Data;
+import lombok.NoArgsConstructor;
+import lombok.NonNull;
+
+import javax.annotation.Nullable;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (22.05.18)
+ */
+@Data
+@AllArgsConstructor
+@NoArgsConstructor
+public class LetStatement extends Statement<ScriptLanguageParser.LetStmtContext> {
+    @NonNull
+    private Expression expression;
+    @Nullable
+    private Statements body;
+
+    @Override
+    public <T> T accept(Visitor<T> visitor) {
+        return visitor.visit(this);
+    }
+
+    @Override
+    public ASTNode[] getChildren() {
+        return new ASTNode[]{getExpression(), getBody()};
+    }
+
+    @Override
+    public LetStatement copy() {
+        LetStatement ls = new LetStatement();
+        ls.expression = expression.copy();
+        ls.body = body.copy();
+        return ls;
+    }
+
+    public boolean isBindGlobal() {
+        return getBody() != null;
+    }
+}

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Statements.java

@@ -81,6 +81,7 @@ public class Statements extends ASTNode<ScriptLanguageParser.StmtListContext>
     public boolean add(Statement statement) {
         if (statement == null)
             throw new NullPointerException();
+        statement.setParent(this);
         return statements.add(statement);
     }
 

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/data/Value.java

@@ -13,6 +13,7 @@ import java.math.BigInteger;
 /**
  * Class representing the values our variables may have
  *
+ * @param T internal data
  * @author S.Grebing
  * @author A. Weigl
  *         //TODO alle restlichen typen ergaenzen

rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeyInterpreter.java

 package edu.kit.iti.formal.psdbg.interpreter;
 
 import com.google.common.collect.BiMap;
-import com.google.common.collect.HashBiMap;
 import com.google.common.collect.ImmutableBiMap;
 import de.uka.ilkd.key.api.VariableAssignments;
-import de.uka.ilkd.key.logic.sort.Sort;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
 import edu.kit.iti.formal.psdbg.interpreter.data.*;
+import edu.kit.iti.formal.psdbg.interpreter.exceptions.InvalidTypeException;
 import edu.kit.iti.formal.psdbg.interpreter.funchdl.CommandLookup;
 import edu.kit.iti.formal.psdbg.parser.Visitor;
-import edu.kit.iti.formal.psdbg.parser.ast.ClosesCase;
-import edu.kit.iti.formal.psdbg.parser.ast.Statements;
-import edu.kit.iti.formal.psdbg.parser.ast.TermLiteral;
-import edu.kit.iti.formal.psdbg.parser.ast.TryCase;
+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.SimpleType;
 import edu.kit.iti.formal.psdbg.parser.types.TermType;
-import edu.kit.iti.formal.psdbg.parser.types.Type;
 import edu.kit.iti.formal.psdbg.parser.types.TypeFacade;
 import lombok.Getter;
-import lombok.val;
 
 import java.util.List;
 import java.util.function.Function;
@@ -33,17 +27,16 @@ public class KeyInterpreter extends Interpreter<KeyData> {
     @Getter
     private static final BiMap<SimpleType, VariableAssignments.VarType> typeConversionBiMap =
             new ImmutableBiMap.Builder<SimpleType, VariableAssignments.VarType>()
-      //              .put(SimpleType.ANY, VariableAssignments.VarType.ANY)
+                    //              .put(SimpleType.ANY, VariableAssignments.VarType.ANY)
                     .put(SimpleType.BOOL, VariableAssignments.VarType.BOOL)
                     //.put(SimpleType.TERM, VariableAssignments.VarType.FORMULA) //TODO: parametrisierte Terms
                     .put(SimpleType.INT, VariableAssignments.VarType.INT)
                     .put(SimpleType.STRING, VariableAssignments.VarType.OBJECT)
-    //                  .put(SimpleType.INT_ARRAY, VariableAssignments.VarType.INT_ARRAY)
+                    //                  .put(SimpleType.INT_ARRAY, VariableAssignments.VarType.INT_ARRAY)
 //                    .put(SimpleType.SEQ, VariableAssignments.VarType.SEQ)
                     .build();
 
 
-
     public KeyInterpreter(CommandLookup lookup) {
         super(lookup);
     }
@@ -141,9 +134,45 @@ public class KeyInterpreter extends Interpreter<KeyData> {
         eval.setTermValueFactory(new Function<TermLiteral, Value>() {
             @Override
             public Value apply(TermLiteral termLiteral) {
-                return  new Value(TypeFacade.ANY_TERM, new TermValue(termLiteral.getContent()));
+                return new Value(TypeFacade.ANY_TERM, new TermValue(termLiteral.getContent()));
             }
         });
         return eval;
     }
+
+
+    @Override
+    public Object visit(LetStatement let) {
+        enterScope(let);
+        Value value = evaluate(let.getExpression());
+        if (!(value.getType() instanceof TermType)) {
+            return new InvalidTypeException();
+        }
+
+        try {
+            TermValue tv = (TermValue) value.getData();
+            List<VariableAssignment> vas = getMatcherApi().matchSeq(getSelectedNode(), tv.getTermRepr());
+            if (!vas.isEmpty()) {
+                VariableAssignment va = vas.get(0);
+                if (let.isBindGlobal()) {
+                    getSelectedNode().getAssignments().push(va);
+                } else {
+                    //Path new assignments in chan.
+                    va.setParent(getSelectedNode().getAssignments());
+                    getSelectedNode().setAssignments(va);
+
+                    let.getBody().accept(this);
+
+                    //remove variables
+                    // TODO for all goal nodes, travers VariableAssignment hierarchy
+                    // and patch out `va`.
+                }
+            }
+        } catch (ClassCastException e) {
+            return new InvalidTypeException(e);
+        }
+        exitScope(let);
+        return null;
+    }
+
 }

rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/exceptions/InvalidTypeException.java

+package edu.kit.iti.formal.psdbg.interpreter.exceptions;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (23.05.18)
+ */
+public class InvalidTypeException extends InterpreterRuntimeException{
+    public InvalidTypeException() {
+        super();
+    }
+
+    public InvalidTypeException(String message) {
+        super(message);
+    }
+
+    public InvalidTypeException(String message, Throwable cause) {
+        super(message, cause);
+    }
+
+    public InvalidTypeException(Throwable cause) {
+        super(cause);
+    }
+
+    protected InvalidTypeException(String message, Throwable cause, boolean enableSuppression, boolean writableStackTrace) {
+        super(message, cause, enableSuppression, writableStackTrace);
+    }
+}

rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java

@@ -175,7 +175,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
         return variableHooks.size() == 0;
     }
 
-    private Value evaluate(Expression expr) {
+    protected Value evaluate(Expression expr) {
         return evaluate(getSelectedNode(), expr);
     }
 

rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/MatcherApi.java

@@ -11,7 +11,20 @@ import java.util.List;
  * @version 1 (16.05.17)
  */
 public interface MatcherApi<T> {
+    /**
+     *
+     * @param currentState
+     * @param label
+     * @return
+     */
     List<VariableAssignment> matchLabel(GoalNode<T> currentState, String label);
-    List<VariableAssignment> matchSeq(GoalNode<T> currentState, String data);
+
+    /**
+     *
+     * @param currentState
+     * @param pattern
+     * @return
+     */
+    List<VariableAssignment> matchSeq(GoalNode<T> currentState, String pattern);
 
 }

rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/VariableAssignment.java

@@ -4,6 +4,8 @@ import edu.kit.iti.formal.psdbg.interpreter.exceptions.VariableNotDefinedExcepti
 import edu.kit.iti.formal.psdbg.parser.ast.Variable;
 import edu.kit.iti.formal.psdbg.parser.data.Value;
 import edu.kit.iti.formal.psdbg.parser.types.Type;
+import lombok.Getter;
+import lombok.Setter;
 import lombok.ToString;
 
 import java.util.HashMap;
@@ -18,7 +20,9 @@ import java.util.stream.Collectors;
  */
 @ToString
 public class VariableAssignment {
-    private final VariableAssignment parent;
+    @Getter
+    @Setter
+    private VariableAssignment parent;
     private Map<Variable, Value> values = new HashMap<>();
     private Map<Variable, Type> types = new HashMap<>();
 
@@ -30,14 +34,6 @@ public class VariableAssignment {
         this(null);
     }
 
-    /**
-     * returns the parent assignment or null
-     *
-     * @return
-     */
-    public VariableAssignment getParent() {
-        return parent;
-    }
 
     /**
      * returns the map of values in this assignment
@@ -229,6 +225,7 @@ public class VariableAssignment {
     }
 
     /**
+     * push and override
      * @param va
      * @return
      */
@@ -236,7 +233,6 @@ public class VariableAssignment {
         VariableAssignment nva = push();
         nva.types.putAll(va.types);
         nva.values.putAll(va.values);
-
         return nva;
     }
 }