function: parser, ast, evaluator

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

@@ -151,5 +151,10 @@ public class DefaultASTVisitor<T> implements Visitor<T> {
     public T visit(ClosesCase closesCase) {
         return defaultVisit(closesCase);
     }
+
+    @Override
+    public T visit(FunctionCall func) {
+        return defaultVisit(func);
+    }
 }
 

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

@@ -24,8 +24,11 @@ package edu.kit.iti.formal.psdbg.parser;
 
 
 import edu.kit.iti.formal.psdbg.parser.ast.*;
+import edu.kit.iti.formal.psdbg.parser.function.FunctionRegister;
+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 org.antlr.v4.runtime.ParserRuleContext;
 import org.antlr.v4.runtime.tree.ErrorNode;
 import org.antlr.v4.runtime.tree.ParseTree;
@@ -36,6 +39,7 @@ import java.util.ArrayList;
 import java.util.LinkedHashMap;
 import java.util.List;
 import java.util.Map;
+import java.util.stream.Collectors;
 
 /**
  * @author Alexander Weigl
@@ -47,9 +51,15 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
      * Start index for positional arguments for command calls
      */
     public static final int KEY_START_INDEX_PARAMETER = 2;
-
     @Getter
     private final List<ProofScript> scripts = new ArrayList<>(10);
+    @Getter
+    @Setter
+    private FunctionRegister functionRegister = new FunctionRegister();
+
+    public TransformAst() {
+        functionRegister.loadDefault();
+    }
 
     @Override
     public List<ProofScript> visitStart(ScriptLanguageParser.StartContext ctx) {
@@ -221,10 +231,18 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
 
     }
 
+    @Override
+    public FunctionCall visitFunction(ScriptLanguageParser.FunctionContext ctx) {
+        List<Expression> args = ctx.expression().stream()
+                .map(c -> (Expression) c.accept(this))
+                .collect(Collectors.toList());
+        ScriptFunction func = functionRegister.get(ctx.ID().getText());
+        return new FunctionCall(func, args);
+    }
+
     @Override
     public Object visitExprAnd(ScriptLanguageParser.ExprAndContext ctx) {
         return createBinaryExpression(ctx, ctx.expression(), Operator.AND);
-
     }
 
     @Override

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

@@ -79,4 +79,6 @@ public interface Visitor<T> {
     T visit(SubstituteExpression subst);
 
     T visit(ClosesCase closesCase);
+
+    T visit(FunctionCall func);
 }

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

+package edu.kit.iti.formal.psdbg.parser.ast;
+
+import edu.kit.iti.formal.psdbg.parser.NotWelldefinedException;
+import edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser;
+import edu.kit.iti.formal.psdbg.parser.Visitor;
+import edu.kit.iti.formal.psdbg.parser.data.Value;
+import edu.kit.iti.formal.psdbg.parser.function.ScriptFunction;
+import edu.kit.iti.formal.psdbg.parser.types.Type;
+import lombok.Getter;
+import lombok.NoArgsConstructor;
+import lombok.Setter;
+import lombok.ToString;
+
+import java.util.ArrayList;
+import java.util.List;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (10.11.17)
+ */
+@Getter
+@Setter
+@ToString
+@NoArgsConstructor
+public class FunctionCall extends Expression<ScriptLanguageParser.FunctionContext> {
+    private ScriptFunction function;
+    private List<Expression> arguments = new ArrayList<>(10);
+
+    public FunctionCall(ScriptFunction func, List<Expression> arguments) {
+        this.function = func;
+        arguments.forEach(a -> this.arguments.add(a.copy()));
+    }
+
+    @Override
+    public boolean hasMatchExpression() {
+        return arguments.stream().anyMatch(Expression::hasMatchExpression);
+    }
+
+    @Override
+    public int getPrecedence() {
+        return 0;
+    }
+
+    @Override
+    public <T> T accept(Visitor<T> visitor) {
+        return visitor.visit(this);
+    }
+
+    @Override
+    public Expression copy() {
+        return new FunctionCall(function, arguments);
+    }
+
+    @Override
+    public Type getType(Signature signature)
+            throws NotWelldefinedException {
+        List<Type> argtypes = new ArrayList<>();
+        for (Expression e : arguments) {
+            argtypes.add(e.getType(signature));
+        }
+        return function.getType(argtypes);
+    }
+}

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

+package edu.kit.iti.formal.psdbg.parser.function;
+
+import edu.kit.iti.formal.psdbg.parser.Visitor;
+import edu.kit.iti.formal.psdbg.parser.ast.Expression;
+import edu.kit.iti.formal.psdbg.parser.ast.FunctionCall;
+import edu.kit.iti.formal.psdbg.parser.data.Value;
+
+import java.util.List;
+import java.util.stream.Collectors;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (10.11.17)
+ */
+public abstract class EvaluatedScriptFunction implements ScriptFunction {
+    @Override
+    public Value eval(Visitor<Value> val, FunctionCall call) {
+        List<Value> values = call.getArguments().stream()
+                .map(e -> (Value) e.accept(val))
+                .collect(Collectors.toList());
+        return eval(values, val);
+    }
+
+    protected abstract Value eval(List<Value> values,
+                                  Visitor<Value> val);
+}

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

+package edu.kit.iti.formal.psdbg.parser.function;
+
+import lombok.Getter;
+
+import java.util.HashMap;
+import java.util.Map;
+import java.util.ServiceLoader;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (10.11.17)
+ */
+@Getter
+public class FunctionRegister {
+    private Map<String, ScriptFunction> functions = new HashMap<>();
+
+    /**
+     * Load the default script functions via {@link java.util.ServiceLoader}.
+     */
+    public void loadDefault() {
+        ServiceLoader<ScriptFunction> sf = ServiceLoader.load(ScriptFunction.class);
+        sf.forEach(s -> put(s.getName(), s));
+    }
+
+    public int size() {
+        return functions.size();
+    }
+
+    public boolean isEmpty() {
+        return functions.isEmpty();
+    }
+
+    public boolean containsKey(String key) {
+        return functions.containsKey(key);
+    }
+
+    public boolean containsValue(ScriptFunction value) {
+        return functions.containsValue(value);
+    }
+
+    public ScriptFunction get(String key) {
+        return functions.get(key);
+    }
+
+    public ScriptFunction put(String key, ScriptFunction value) {
+        return functions.put(key, value);
+    }
+
+    public ScriptFunction remove(String key) {
+        return functions.remove(key);
+    }
+}

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

+package edu.kit.iti.formal.psdbg.parser.function;
+
+import edu.kit.iti.formal.psdbg.parser.NotWelldefinedException;
+import edu.kit.iti.formal.psdbg.parser.Visitor;
+import edu.kit.iti.formal.psdbg.parser.ast.FunctionCall;
+import edu.kit.iti.formal.psdbg.parser.data.Value;
+import edu.kit.iti.formal.psdbg.parser.types.Type;
+
+import java.util.List;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (10.11.17)
+ */
+public interface ScriptFunction {
+    String getName();
+
+    Type getType(List<Type> types)
+            throws NotWelldefinedException;
+
+    Value eval(Visitor<Value> val, FunctionCall call);
+}

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

@@ -25,12 +25,14 @@ package edu.kit.iti.formal.psdbg.parser.types;
 
 /**
  * Represents the possible types (including scriptVarTypes).
- *
+ * <p>
  * Created at 30.04.2017
+ *
  * @author Sarah Grebing
  */
 public enum SimpleType implements Type {
     STRING("string"), ANY("any"),
+    PATTERN("pattern"),
     INT("int"), BOOL("bool"), INT_ARRAY("int[]"), OBJECT("object"),
     HEAP("heap"), FIELD("field"), LOCSET("locset"), NULL("null"), FORMULA("formula"), SEQ("Seq");
 

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

+package edu.kit.iti.formal.psdbg.interpreter.functions;
+
+import edu.kit.iti.formal.psdbg.interpreter.Evaluator;
+import edu.kit.iti.formal.psdbg.interpreter.KeYMatcher;
+import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
+import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
+import edu.kit.iti.formal.psdbg.parser.NotWelldefinedException;
+import edu.kit.iti.formal.psdbg.parser.Visitor;
+import edu.kit.iti.formal.psdbg.parser.ast.FunctionCall;
+import edu.kit.iti.formal.psdbg.parser.ast.MatchExpression;
+import edu.kit.iti.formal.psdbg.parser.ast.Signature;
+import edu.kit.iti.formal.psdbg.parser.ast.TermLiteral;
+import edu.kit.iti.formal.psdbg.parser.data.Value;
+import edu.kit.iti.formal.psdbg.parser.function.ScriptFunction;
+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 java.util.Collections;
+import java.util.List;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (10.11.17)
+ */
+public class FindInSequence implements ScriptFunction {
+    public static final List<Type> TYPES =
+            Collections.singletonList(SimpleType.PATTERN);
+
+    @Override
+    public String getName() {
+        return "find";
+    }
+
+    @Override
+    public Type getType(List<Type> types) throws NotWelldefinedException {
+        if (!TYPES.equals(types))
+            throw new NotWelldefinedException("Wrong type of parameter for " + getName(), null);
+        return new TermType();
+    }
+
+    @Override
+    public Value eval(Visitor<Value> val, FunctionCall call)
+            throws IllegalArgumentException {
+        Evaluator<KeyData> e = (Evaluator<KeyData>) val;
+        try {
+            MatchExpression match = (MatchExpression) call.getArguments().get(0);
+            Signature sig = match.getSignature();
+            Value pattern = e.eval(match.getPattern());
+            List<VariableAssignment> va = null;
+            KeYMatcher matcher = (KeYMatcher) e.getMatcher();
+            if (pattern.getType() == SimpleType.STRING) {
+                va = matcher.matchLabel(e.getGoal(), (String) pattern.getData());
+                //TODO extract the results form the matcher in order to retrieve the selection results
+            } else if (TypeFacade.isTerm(pattern.getType())) {
+                va = matcher.matchSeq(e.getGoal(), (String) pattern.getData(), sig);
+            }
+
+            //TODO capture top level term
+            return Value.from(new TermLiteral(""));
+        } catch (ClassCastException exc) {
+            throw new IllegalStateException("Excepted a match expression as first argument found: " + call.getArguments().get(0),
+                    exc);
+        }
+    }
+
+}

rt-key/src/main/resources/services/edu.kit.iti.formal.psdbg.parser.function.ScriptFunction

+edu.kit.iti.formal.psdbg.interpreter.functions.FindInSequence
\ No newline at end of file

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

@@ -158,4 +158,9 @@ public class Evaluator<T> extends DefaultASTVisitor<Value> implements ScopeObser
             throw new IllegalStateException("Try to apply substitute on a non-term value.");
         }
     }
+
+    @Override
+    public Value visit(FunctionCall func) {
+        return func.getFunction().eval(this, func);
+    }
 }