Implemented Subst and rework on types

now Term<KeyType> ist possible!

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

@@ -49,10 +49,7 @@ assignment
 
 expression
     :
-        MINUS expression   #exprNegate
-    |   NOT expression  #exprNot
-    |   expression '[' substExpressionList ']'  #exprSubst
-    |   expression MUL expression #exprMultiplication
+      expression MUL expression #exprMultiplication
     | <assoc=right> expression DIV expression #exprDivision
     | expression op=(PLUS|MINUS) expression #exprLineOperators
     | expression op=(LE|GE|LEQ|GEQ) expression #exprComparison
@@ -61,6 +58,9 @@ expression
     | expression OR expression    #exprOr
     | expression IMP expression   #exprIMP
     //|   expression EQUIV expression already covered by EQ/NEQ
+    | expression LBRACKET substExpressionList RBRACKET #exprSubst
+    | MINUS expression   #exprNegate
+    | NOT expression  #exprNot
     | '(' expression ')' #exprParen
     | literals             #exprLiterals
     | matchPattern         #exprMatch
@@ -69,7 +69,9 @@ expression
 
 substExpressionList
     :
-    scriptVar '/' expression (',' substExpressionList)*
+    (scriptVar '/' expression
+        (',' scriptVar '/' expression)*
+    )?
     ;
 
 literals :
@@ -205,4 +207,4 @@ EXE_MARKER: '\u2316' -> channel(HIDDEN);
 
 DIGITS : DIGIT+ ;
 fragment DIGIT : [0-9] ;
-ID : [a-zA-Z] ([_a-zA-Z0-9] | '.' | '\\' | '[]' | '-')* ;
+ID : [a-zA-Z] ([_a-zA-Z0-9] | '.' | '\\')*;
\ No newline at end of file

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

@@ -6,11 +6,16 @@ import edu.kit.formal.interpreter.data.VariableAssignment;
 import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
 import edu.kit.formal.proofscriptparser.Visitor;
 import edu.kit.formal.proofscriptparser.ast.*;
+import edu.kit.formal.proofscriptparser.types.SimpleType;
+import edu.kit.formal.proofscriptparser.types.TermType;
+import edu.kit.formal.proofscriptparser.types.TypeFacade;
 import lombok.Getter;
 import lombok.Setter;
 
 import java.util.ArrayList;
 import java.util.List;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
 
 /**
  * Class handling evaluation of expressions (visitor for expressions)
@@ -68,9 +73,9 @@ public class Evaluator<T> extends DefaultASTVisitor<Value> implements ScopeObser
         Value pattern = (Value) match.getPattern().accept(this);
         if (match.isDerivable()) {
         } else {
-            if (pattern.getType() == Type.STRING) {
+            if (pattern.getType() == SimpleType.STRING) {
                 va = matcher.matchLabel(goal, (String) pattern.getData());
-            } else if (pattern.getType() == Type.TERM) {
+            } else if (TypeFacade.isTerm(pattern.getType())) {
                 va = matcher.matchSeq(goal, (String) pattern.getData(), match.getSignature());
             }
         }
@@ -127,5 +132,29 @@ public class Evaluator<T> extends DefaultASTVisitor<Value> implements ScopeObser
         return op.evaluate(exValue);
     }
 
-
+    public Value visit(SubstituteExpression expr) {
+        Value term = (Value) expr.getSub().accept(this);
+        if (term.getType() instanceof TermType) {
+            Pattern pattern = Pattern.compile("\\?[a-zA-Z_]+");
+            String termstr = term.getData().toString();
+            Matcher m = pattern.matcher(termstr);
+            StringBuffer newTerm = new StringBuffer();
+            while (m.find()) {
+                String name = m.group().substring(1); // remove trailing '?'
+                Expression t = expr.getSubstitution().get(m.group());
+
+                //either evalute the substitent or find ?X in the
+                String newVal = "";
+                if (t != null)
+                    newVal = ((Value) t.accept(this)).getData().toString();
+                else
+                    newVal = state.getValue(new Variable(name)).getData().toString();
+                m.appendReplacement(newTerm, newVal);
+            }
+            m.appendTail(newTerm);
+            return new Value<>(TypeFacade.ANY_TERM, newTerm.toString());
+        } else {
+            throw new IllegalStateException("Try to apply substitute on a non-term value.");
+        }
+    }
 }

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

@@ -14,6 +14,8 @@ 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 edu.kit.formal.proofscriptparser.types.SimpleType;
+import edu.kit.formal.proofscriptparser.types.Type;
 import lombok.Getter;
 import lombok.Setter;
 import org.key_project.util.collection.ImmutableList;
@@ -33,15 +35,15 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
         implements ScopeObservable {
     private static final int MAX_ITERATIONS = 5;
     @Getter
-    private static final BiMap<Type, VariableAssignments.VarType> typeConversionBiMap =
-            new ImmutableBiMap.Builder<Type, VariableAssignments.VarType>()
-                    .put(Type.ANY, VariableAssignments.VarType.ANY)
-                    .put(Type.BOOL, VariableAssignments.VarType.BOOL)
-                    .put(Type.TERM, VariableAssignments.VarType.FORMULA) //TODO: parametrisierte Terms
-                    .put(Type.INT, VariableAssignments.VarType.INT)
-                    .put(Type.STRING, VariableAssignments.VarType.OBJECT)
-                    .put(Type.INT_ARRAY, VariableAssignments.VarType.INT_ARRAY)
-                    .put(Type.SEQ, VariableAssignments.VarType.SEQ)
+    private static final BiMap<SimpleType, VariableAssignments.VarType> typeConversionBiMap =
+            new ImmutableBiMap.Builder<SimpleType, VariableAssignments.VarType>()
+                    .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.SEQ, VariableAssignments.VarType.SEQ)
                     .build();
     private static Logger logger = Logger.getLogger("interpreter");
     //TODO later also include information about source line for each state (for debugging purposes and rewind purposes)
@@ -114,7 +116,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
         if (expr != null) {
             Type type = node.getVariableType(var);
             if (type == null) {
-                throw new RuntimeException("Type of Variable " + var + " is not declared yet");
+                throw new RuntimeException("SimpleType of Variable " + var + " is not declared yet");
             } else {
                 Value v = evaluate(expr);
                 node.setVariableValue(var, v);

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

@@ -18,8 +18,9 @@ import edu.kit.formal.interpreter.data.Value;
 import edu.kit.formal.interpreter.data.VariableAssignment;
 import edu.kit.formal.proofscriptparser.ast.Signature;
 import edu.kit.formal.proofscriptparser.ast.TermLiteral;
-import edu.kit.formal.proofscriptparser.ast.Type;
+import edu.kit.formal.proofscriptparser.types.SimpleType;
 import edu.kit.formal.proofscriptparser.ast.Variable;
+import edu.kit.formal.proofscriptparser.types.Type;
 import org.key_project.util.collection.ImmutableList;
 
 import java.util.ArrayList;
@@ -114,7 +115,7 @@ public class KeYMatcher implements MatcherApi<KeyData> {
 
         if (branchLabelMatcher.matches()) {
             VariableAssignment va = new VariableAssignment(null);
-            va.declare("$$branchLabel_", Type.STRING);
+            va.declare("$$branchLabel_", SimpleType.STRING);
             va.assign("$$branchLabel_", Value.from(branchLabelMatcher.group()));
             assignments.add(va);
             resultsFromLabelMatch.add(branchLabelMatcher.toMatchResult());
@@ -124,7 +125,7 @@ public class KeYMatcher implements MatcherApi<KeyData> {
         Matcher linesMatcher = regexpForLabel.matcher(controlFlowLines);
         if (linesMatcher.matches()) {
             VariableAssignment va = new VariableAssignment(null);
-            va.declare("$$CtrlLinesLabel_", Type.STRING);
+            va.declare("$$CtrlLinesLabel_", SimpleType.STRING);
             va.assign("$$CtrlLinesLabel_", Value.from(linesMatcher.group()));
             assignments.add(va);
             resultsFromLabelMatch.add(linesMatcher.toMatchResult());
@@ -134,7 +135,7 @@ public class KeYMatcher implements MatcherApi<KeyData> {
         Matcher flowStmtsMatcher = regexpForLabel.matcher(controlFlowLines);
         if (flowStmtsMatcher.matches()) {
             VariableAssignment va = new VariableAssignment(null);
-            va.declare("$$FlowStmtsLabel_", Type.STRING);
+            va.declare("$$FlowStmtsLabel_", SimpleType.STRING);
             va.assign("$$FlowStmtsLabel_", Value.from(flowStmtsMatcher.group()));
             assignments.add(va);
             resultsFromLabelMatch.add(flowStmtsMatcher.toMatchResult());
@@ -144,7 +145,7 @@ public class KeYMatcher implements MatcherApi<KeyData> {
         Matcher ruleMatcher = regexpForLabel.matcher(ruleLabel);
         if (ruleMatcher.matches()) {
             VariableAssignment va = new VariableAssignment(null);
-            va.declare("$$RuleLabel_", Type.STRING);
+            va.declare("$$RuleLabel_", SimpleType.STRING);
             va.assign("$$RuleLabel_", Value.from(ruleMatcher.group()));
             assignments.add(va);
             resultsFromLabelMatch.add(ruleMatcher.toMatchResult());

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

@@ -6,6 +6,8 @@ import edu.kit.formal.interpreter.data.VariableAssignment;
 import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
 import edu.kit.formal.proofscriptparser.Visitor;
 import edu.kit.formal.proofscriptparser.ast.*;
+import edu.kit.formal.proofscriptparser.types.SimpleType;
+import edu.kit.formal.proofscriptparser.types.TypeFacade;
 import lombok.Getter;
 import org.apache.commons.lang.NotImplementedException;
 
@@ -156,10 +158,10 @@ public class MatchEvaluator extends DefaultASTVisitor<List<VariableAssignment>>
         // Value pattern = (Value) match.getPattern().accept(this);
 
         List<VariableAssignment> va = null;
-        if (pattern.getType() == Type.STRING) {
+        if (pattern.getType() == SimpleType.STRING) {
             va = getMatcher().matchLabel(goal, (String) pattern.getData());
             //TODO extract the results form the matcher in order to retrieve the selection results
-        } else if (pattern.getType() == Type.TERM) {
+        } else if (TypeFacade.isTerm(pattern.getType())) {
             va = getMatcher().matchSeq(goal, (String) pattern.getData(), sig);
         }
         return va != null ? va : Collections.emptyList();
@@ -203,7 +205,7 @@ public class MatchEvaluator extends DefaultASTVisitor<List<VariableAssignment>>
      */
     public List<VariableAssignment> transformTruthValue(Value v) {
 
-        if (v.getType().equals(Type.BOOL)) {
+        if (v.getType().equals(SimpleType.BOOL)) {
             List<VariableAssignment> transformedValue = new ArrayList<>();
             if (v.getData().equals(Value.TRUE)) {
                 transformedValue.add(new VariableAssignment(null));

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

 package edu.kit.formal.interpreter.data;
 
-import edu.kit.formal.proofscriptparser.ast.Type;
+import edu.kit.formal.proofscriptparser.types.SimpleType;
 import edu.kit.formal.proofscriptparser.ast.Variable;
+import edu.kit.formal.proofscriptparser.types.Type;
 import lombok.Getter;
 import lombok.ToString;
 

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

 package edu.kit.formal.interpreter.data;
 
 import edu.kit.formal.proofscriptparser.ast.*;
+import edu.kit.formal.proofscriptparser.types.SimpleType;
+import edu.kit.formal.proofscriptparser.types.Type;
+import edu.kit.formal.proofscriptparser.types.TypeFacade;
 import lombok.Getter;
 import lombok.RequiredArgsConstructor;
 
@@ -15,8 +18,8 @@ import java.math.BigInteger;
  */
 @RequiredArgsConstructor
 public class Value<T> {
-    public static final Value TRUE = new Value<>(Type.BOOL, true);
-    public static final Value FALSE = new Value<>(Type.BOOL, false);
+    public static final Value TRUE = new Value<>(SimpleType.BOOL, true);
+    public static final Value FALSE = new Value<>(SimpleType.BOOL, false);
 
     @Getter
     private final Type type;
@@ -25,35 +28,35 @@ public class Value<T> {
 
 
     public static Value<BigInteger> from(IntegerLiteral i) {
-        return new Value<>(Type.INT, i.getValue());
+        return new Value<>(SimpleType.INT, i.getValue());
     }
 
     public static Value<BigInteger> from(Integer i) {
-        return new Value<>(Type.INT, BigInteger.valueOf(i));
+        return new Value<>(SimpleType.INT, BigInteger.valueOf(i));
     }
 
     public static Value<String> from(StringLiteral s) {
-        return new Value<>(Type.STRING, s.getText());
+        return new Value<>(SimpleType.STRING, s.getText());
     }
 
     public static Value<Boolean> from(BooleanLiteral b) {
-        return new Value(Type.BOOL, b.isValue());
+        return new Value<>(SimpleType.BOOL, b.isValue());
     }
 
     public static Value<Boolean> from(boolean equals) {
-        return new Value(Type.BOOL, equals);
+        return new Value<>(SimpleType.BOOL, equals);
     }
 
     public static Value<BigInteger> from(BigInteger apply) {
-        return new Value<>(Type.INT, apply);
+        return new Value<>(SimpleType.INT, apply);
     }
 
     public static Value<String> from(String s) {
-        return new Value<>(Type.STRING, s);
+        return new Value<>(SimpleType.STRING, s);
     }
 
     public static Value<String> from(TermLiteral term) {
-        return new Value<>(Type.TERM, term.getText());
+        return new Value<>(TypeFacade.ANY_TERM, term.getText());
     }
 
     @Override

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

 package edu.kit.formal.interpreter.data;
 
 import edu.kit.formal.interpreter.exceptions.VariableNotDefinedException;
-import edu.kit.formal.proofscriptparser.ast.Type;
+import edu.kit.formal.proofscriptparser.types.SimpleType;
 import edu.kit.formal.proofscriptparser.ast.Variable;
+import edu.kit.formal.proofscriptparser.types.Type;
 import lombok.ToString;
 
 import java.util.HashMap;

src/main/java/edu/kit/formal/interpreter/dbg/PseudoMatcher.java

@@ -5,8 +5,9 @@ import edu.kit.formal.interpreter.data.GoalNode;
 import edu.kit.formal.interpreter.data.Value;
 import edu.kit.formal.interpreter.data.VariableAssignment;
 import edu.kit.formal.proofscriptparser.ast.Signature;
-import edu.kit.formal.proofscriptparser.ast.Type;
+import edu.kit.formal.proofscriptparser.types.SimpleType;
 import edu.kit.formal.proofscriptparser.ast.Variable;
+import edu.kit.formal.proofscriptparser.types.Type;
 
 import java.util.Collections;
 import java.util.List;

src/main/java/edu/kit/formal/interpreter/funchdl/MacroCommandHandler.java

@@ -5,6 +5,7 @@ import edu.kit.formal.interpreter.Interpreter;
 import edu.kit.formal.interpreter.data.Value;
 import edu.kit.formal.interpreter.data.VariableAssignment;
 import edu.kit.formal.proofscriptparser.ast.*;
+import edu.kit.formal.proofscriptparser.types.SimpleType;
 import lombok.Getter;
 import lombok.RequiredArgsConstructor;
 
@@ -39,7 +40,7 @@ public class MacroCommandHandler implements CommandHandler {
         CallStatement macroCall = new CallStatement("macro", p);
         macroCall.setRuleContext(call.getRuleContext());
         VariableAssignment newParam = new VariableAssignment(null);
-        newParam.declare("#2", Type.STRING);
+        newParam.declare("#2", SimpleType.STRING);
         newParam.assign("#2", Value.from(call.getCommand()));
         //macro proofscript command
         interpreter.getFunctionLookup().callCommand(interpreter, macroCall, newParam);

src/main/java/edu/kit/formal/interpreter/graphs/EdgeTypes.java

 package edu.kit.formal.interpreter.graphs;
 
 /**
- * Edge Types a state graph and control flow graph may have
+ * Edge Type a state graph and control flow graph may have
  */
 public enum EdgeTypes {
     STEP_INTO, STEP_OVER, STEP_BACK, STEP_RETURN, STEP_OVER_COND, STATE_FLOW;

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

@@ -24,6 +24,8 @@ package edu.kit.formal.proofscriptparser;
 
 
 import edu.kit.formal.proofscriptparser.ast.*;
+import edu.kit.formal.proofscriptparser.types.SimpleType;
+import edu.kit.formal.proofscriptparser.types.Type;
 
 import java.util.ArrayList;
 import java.util.Map;

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

@@ -24,6 +24,7 @@ package edu.kit.formal.proofscriptparser;
 
 
 import edu.kit.formal.proofscriptparser.ast.*;
+import edu.kit.formal.proofscriptparser.types.Type;
 
 import java.util.Map;
 
@@ -171,4 +172,13 @@ public interface ASTTraversal<T> extends Visitor<T> {
         simpleCaseStatement.getBody().accept(this);
         return null;
     }
+
+    @Override
+    default T visit(SubstituteExpression subst) {
+        subst.getSub().accept(this);
+        for (Expression e : subst.getSubstitution().values()) {
+            e.accept(this);
+        }
+        return null;
+    }
 }

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

@@ -94,6 +94,11 @@ public class DefaultASTVisitor<T> implements Visitor<T> {
         return defaultVisit(caseStatement);
     }
 
+    @Override
+    public T visit(SubstituteExpression subst) {
+        return defaultVisit(subst);
+    }
+
     @Override
     public T visit(CallStatement call) {
         return defaultVisit(call);
@@ -138,5 +143,6 @@ public class DefaultASTVisitor<T> implements Visitor<T> {
     public T visit(SimpleCaseStatement simpleCaseStatement) {
         return defaultVisit(simpleCaseStatement);
     }
+
 }
 

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

@@ -24,6 +24,8 @@ package edu.kit.formal.proofscriptparser;
 
 
 import edu.kit.formal.proofscriptparser.ast.*;
+import edu.kit.formal.proofscriptparser.types.SimpleType;
+import edu.kit.formal.proofscriptparser.types.Type;
 import lombok.Getter;
 import lombok.Setter;
 

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

@@ -24,6 +24,7 @@ package edu.kit.formal.proofscriptparser;
 
 
 import edu.kit.formal.proofscriptparser.ast.*;
+import edu.kit.formal.proofscriptparser.types.TypeFacade;
 import org.antlr.v4.runtime.ParserRuleContext;
 import org.antlr.v4.runtime.tree.ErrorNode;
 import org.antlr.v4.runtime.tree.ParseTree;
@@ -31,7 +32,9 @@ import org.antlr.v4.runtime.tree.RuleNode;
 import org.antlr.v4.runtime.tree.TerminalNode;
 
 import java.util.ArrayList;
+import java.util.LinkedHashMap;
 import java.util.List;
+import java.util.Map;
 
 /**
  * @author Alexander Weigl
@@ -66,7 +69,8 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
     public Signature visitArgList(ScriptLanguageParser.ArgListContext ctx) {
         Signature signature = new Signature();
         for (ScriptLanguageParser.VarDeclContext decl : ctx.varDecl()) {
-            signature.put(new Variable(decl.name), Type.findType(decl.type.getText()));
+            signature.put(new Variable(decl.name),
+                    TypeFacade.findType(decl.type.getText()));
         }
         return signature;
     }
@@ -80,7 +84,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
     public Object visitVarDecl(ScriptLanguageParser.VarDeclContext ctx) {
        /* VariableDeclaration varDecl = new VariableDeclaration();
         varDecl.setIdentifier(new Variable(ctx.name));
-        varDecl.setType(Type.findType(ctx.type.getText()));
+        varDecl.setType(SimpleType.findType(ctx.type.getText()));
         return varDecl;*/
         return null;
 
@@ -90,7 +94,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
     public Statements visitStmtList(ScriptLanguageParser.StmtListContext ctx) {
         Statements statements = new Statements();
         for (ScriptLanguageParser.StatementContext stmt : ctx.statement()) {
-            statements.add((Statement) stmt.accept(this));
+            statements.add((Statement<ParserRuleContext>) stmt.accept(this));
         }
         return statements;
     }
@@ -107,10 +111,10 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
         assign.setRuleContext(ctx);
         assign.setLhs(new Variable(ctx.variable));
         if (ctx.type != null) {
-            assign.setType(Type.findType(ctx.type.getText()));
+            assign.setType(TypeFacade.findType(ctx.type.getText()));
         }
         if (ctx.expression() != null) {
-            assign.setRhs((Expression) ctx.expression().accept(this));
+            assign.setRhs((Expression<ParserRuleContext>) ctx.expression().accept(this));
         }
         return assign;
     }
@@ -123,8 +127,8 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
     private BinaryExpression createBinaryExpression(ParserRuleContext ctx,
                                                     List<ScriptLanguageParser.ExpressionContext> expression, Operator op) {
         BinaryExpression be = new BinaryExpression();
-        be.setLeft((Expression) expression.get(0).accept(this));
-        be.setRight((Expression) expression.get(1).accept(this));
+        be.setLeft((Expression<ParserRuleContext>) expression.get(0).accept(this));
+        be.setRight((Expression<ParserRuleContext>) expression.get(1).accept(this));
         be.setOperator(op);
         return be;
     }
@@ -132,7 +136,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
     private UnaryExpression createUnaryExpression(ParserRuleContext ctx, ScriptLanguageParser.ExpressionContext expression, Operator op) {
         UnaryExpression ue = new UnaryExpression();
         ue.setRuleContext(ctx);
-        ue.setExpression((Expression) expression.accept(this));
+        ue.setExpression((Expression<ParserRuleContext>) expression.accept(this));
         ue.setOperator(op);
         return ue;
     }
@@ -153,7 +157,6 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
     }
 
 
-
     private Operator findOperator(String n) {
         return findOperator(n, 2);
     }
@@ -222,12 +225,21 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
 
     @Override
     public Object visitExprSubst(ScriptLanguageParser.ExprSubstContext ctx) {
-        return null;
+        SubstituteExpression se = new SubstituteExpression();
+        se.setSub((Expression) ctx.expression().accept(this));
+        se.setSubstitution(
+                (Map<String, Expression>) ctx.substExpressionList().accept(this));
+        return se;
     }
 
     @Override
-    public Object visitSubstExpressionList(ScriptLanguageParser.SubstExpressionListContext ctx) {
-        return null;
+    public Map<String, Expression> visitSubstExpressionList(ScriptLanguageParser.SubstExpressionListContext ctx) {
+        Map<String, Expression> map = new LinkedHashMap<>();
+        for (int i = 0; i < ctx.scriptVar().size(); i++) {
+            map.put(ctx.scriptVar(i).getText(),
+                    (Expression) ctx.expression(i).accept(this));
+        }
+        return map;
     }
 
     @Override
@@ -267,11 +279,11 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
 
         if (ctx.derivable != null) {
             match.setDerivable(true);
-            match.setDerivableTerm((Expression) ctx.derivableExpression.accept(this));
+            match.setDerivableTerm((Expression<ParserRuleContext>) ctx.derivableExpression.accept(this));
         } else {
             if (ctx.argList() != null)
                 match.setSignature((Signature) ctx.argList().accept(this));
-            match.setPattern((Expression) ctx.pattern.accept(this));
+            match.setPattern((Expression<ParserRuleContext>) ctx.pattern.accept(this));
         }
 
         return match;
@@ -314,7 +326,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
         } else {
             SimpleCaseStatement caseStatement = new SimpleCaseStatement();
             caseStatement.setRuleContext(ctx);
-            caseStatement.setGuard((Expression) ctx.expression().accept(this));
+            caseStatement.setGuard((Expression<ParserRuleContext>) ctx.expression().accept(this));
             caseStatement.setBody((Statements) ctx.stmtList().accept(this));
             return caseStatement;
         }

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

@@ -75,4 +75,6 @@ public interface Visitor<T> {
     T visit(SimpleCaseStatement simpleCaseStatement);
 
     T visit(CaseStatement caseStatement);
+
+    T visit(SubstituteExpression subst);
 }

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

@@ -26,6 +26,8 @@ package edu.kit.formal.proofscriptparser.ast;
 
 import edu.kit.formal.proofscriptparser.ScriptLanguageParser;
 import edu.kit.formal.proofscriptparser.Visitor;
+import edu.kit.formal.proofscriptparser.types.SimpleType;
+import edu.kit.formal.proofscriptparser.types.Type;
 import lombok.*;
 
 /**

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

@@ -25,6 +25,8 @@ package edu.kit.formal.proofscriptparser.ast;
 
 import edu.kit.formal.proofscriptparser.NotWelldefinedException;
 import edu.kit.formal.proofscriptparser.Visitor;
+import edu.kit.formal.proofscriptparser.types.SimpleType;
+import edu.kit.formal.proofscriptparser.types.Type;
 import lombok.Data;
 import org.antlr.v4.runtime.ParserRuleContext;
 

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

@@ -26,6 +26,7 @@ package edu.kit.formal.proofscriptparser.ast;
 
 import edu.kit.formal.proofscriptparser.NotWelldefinedException;
 import edu.kit.formal.proofscriptparser.Visitor;
+import edu.kit.formal.proofscriptparser.types.SimpleType;
 import lombok.Data;
 import lombok.EqualsAndHashCode;
 import lombok.Getter;
@@ -82,7 +83,7 @@ public class BooleanLiteral extends Literal {
      * {@inheritDoc}
      */
     @Override
-    public Type getType(Signature signature) throws NotWelldefinedException {
-        return Type.BOOL;
+    public SimpleType getType(Signature signature) throws NotWelldefinedException {
+        return SimpleType.BOOL;
     }
 }

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

@@ -25,6 +25,8 @@ package edu.kit.formal.proofscriptparser.ast;
 
 
 import edu.kit.formal.proofscriptparser.NotWelldefinedException;
+import edu.kit.formal.proofscriptparser.types.SimpleType;
+import edu.kit.formal.proofscriptparser.types.Type;
 import org.antlr.v4.runtime.ParserRuleContext;
 
 /**

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

@@ -26,6 +26,8 @@ package edu.kit.formal.proofscriptparser.ast;
 
 import edu.kit.formal.proofscriptparser.NotWelldefinedException;
 import edu.kit.formal.proofscriptparser.Visitor;
+import edu.kit.formal.proofscriptparser.types.SimpleType;
+import edu.kit.formal.proofscriptparser.types.Type;
 import lombok.Data;
 import org.antlr.v4.runtime.Token;
 
@@ -78,7 +80,7 @@ public class IntegerLiteral extends Literal {
      */
     @Override
     public Type getType(Signature signature) throws NotWelldefinedException {
-        return Type.INT;
+        return SimpleType.INT;
     }
 
 

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

@@ -26,6 +26,9 @@ package edu.kit.formal.proofscriptparser.ast;
 import edu.kit.formal.proofscriptparser.NotWelldefinedException;
 import edu.kit.formal.proofscriptparser.ScriptLanguageParser;
 import edu.kit.formal.proofscriptparser.Visitor;
+import edu.kit.formal.proofscriptparser.types.SimpleType;
+import edu.kit.formal.proofscriptparser.types.TermType;
+import edu.kit.formal.proofscriptparser.types.Type;
 import lombok.Data;
 import lombok.Getter;
 import lombok.Setter;
@@ -73,15 +76,10 @@ public class MatchExpression extends Expression<ScriptLanguageParser.MatchPatter
     @Override
     public Type getType(Signature signature) throws NotWelldefinedException {
         Type patternType = pattern.getType(signature);
-        switch (patternType) {
-            case TERM:
-            case STRING:
-                break;
-            default:
+        if (!(patternType instanceof TermType || patternType == SimpleType.STRING)) {
             throw new NotWelldefinedException("Missing parameter", this);
         }
-
-        return Type.BOOL;
+        return SimpleType.BOOL;
     }
 
     @Override

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

@@ -23,14 +23,18 @@ package edu.kit.formal.proofscriptparser.ast;
  */
 
 
+import de.uka.ilkd.key.logic.TermFactory;
 import edu.kit.formal.interpreter.data.Value;
+import edu.kit.formal.proofscriptparser.types.SimpleType;
+import edu.kit.formal.proofscriptparser.types.Type;
+import edu.kit.formal.proofscriptparser.types.TypeFacade;
 
 import java.math.BigInteger;
 import java.util.function.BiFunction;
 import java.util.function.UnaryOperator;
 
-import static edu.kit.formal.proofscriptparser.ast.Type.BOOL;
-import static edu.kit.formal.proofscriptparser.ast.Type.INT;
+import static edu.kit.formal.proofscriptparser.types.SimpleType.BOOL;
+import static edu.kit.formal.proofscriptparser.types.SimpleType.INT;
 
 /**
  * An enum which contains meta-data to all operators.
@@ -53,6 +57,15 @@ public enum Operator {
             return null;
         }
     },
+    /**
+     *
+     */
+    SUBST("<subst>", "[]", 10, TypeFacade.ANY_TERM, TypeFacade.ANY_TERM) {
+        @Override