Removal of NamespaceSetExpression

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

@@ -57,7 +57,6 @@ expression
     | expression AND expression   #exprAnd
     | expression OR expression    #exprOr
     | expression IMP expression   #exprIMP
-    | expression USING LBRACKET argList RBRACKET #namespaceset
     //|   expression EQUIV expression already covered by EQ/NEQ
     | expression LBRACKET substExpressionList RBRACKET #exprSubst
     | ID LPAREN  (expression (',' expression)*)? RPAREN  #function

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

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

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

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

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

 package edu.kit.iti.formal.psdbg.parser;
 
-        /*-
-         * #%L
-         * ProofScriptParser
-         * %%
-         * Copyright (C) 2017 Application-oriented Formal Verification
-         * %%
-         * This program is free software: you can redistribute it and/or modify
-         * it under the terms of the GNU General Public License as
-         * published by the Free Software Foundation, either version 3 of the
-         * License, or (at your option) any later version.
-         *
-         * This program is distributed in the hope that it will be useful,
-         * but WITHOUT ANY WARRANTY; without even the implied warranty of
-         * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-         * GNU General Public License for more details.
-         *
-         * You should have received a copy of the GNU General Public
-         * License along with this program.  If not, see
-         * <http://www.gnu.org/licenses/gpl-3.0.html>.
-         * #L%
-         */
+/*-
+ * #%L
+ * ProofScriptParser
+ * %%
+ * Copyright (C) 2017 Application-oriented Formal Verification
+ * %%
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as
+ * published by the Free Software Foundation, either version 3 of the
+ * License, or (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public
+ * License along with this program.  If not, see
+ * <http://www.gnu.org/licenses/gpl-3.0.html>.
+ * #L%
+ */
 
 
 import edu.kit.iti.formal.psdbg.parser.ast.*;
@@ -245,14 +245,6 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
         return ctx.matchPattern().accept(this);
     }
 
-    @Override
-    public Object visitNamespaceset(ScriptLanguageParser.NamespacesetContext ctx) {
-        NamespaceSetExpression nse = new NamespaceSetExpression();
-        nse.setExpression((Expression) ctx.expression().accept(this));
-        nse.setSignature((Signature) ctx.argList().accept(this));
-        return nse;
-    }
-
     @Override
     public Object visitExprIMP(ScriptLanguageParser.ExprIMPContext ctx) {
         return createBinaryExpression(ctx, ctx.expression(), Operator.IMPLICATION);

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

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

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/NamespaceSetExpression.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.types.Type;
-import lombok.Getter;
-import lombok.Setter;
-
-public class NamespaceSetExpression extends Expression<ScriptLanguageParser.NamespacesetContext>{
-
-    @Getter @Setter
-    private Expression expression;
-
-    @Getter @Setter
-    private Signature signature = new Signature();
-
-    @Override
-    public <T> T accept(Visitor<T> visitor) {
-        return visitor.visit(this);
-    }
-
-    @Override
-    public boolean hasMatchExpression() {
-        return expression.hasMatchExpression();
-    }
-
-    @Override
-    public int getPrecedence() {
-        return 5;
-    }
-
-    @Override
-    public NamespaceSetExpression copy() {
-        NamespaceSetExpression nse = new NamespaceSetExpression();
-        nse.expression = expression.copy();
-        nse.signature = signature.copy();
-        return nse;
-    }
-
-    @Override
-    public Type getType(Signature signature) throws NotWelldefinedException {
-        return expression.getType(signature);
-    }
-}

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

@@ -34,7 +34,7 @@ public final class TypeFacade {
 
     public static SimpleType getSimpleType(String n) {
         for (SimpleType t : SimpleType.values()) {
-            if (t.symbol().equals(n))
+            if (t.symbol().equalsIgnoreCase(n))
                 return t;
         }
         throw new IllegalStateException("SimpleType " + n + " is not defined. Valid types are: " + Arrays.toString(SimpleType.values()));

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

 package edu.kit.iti.formal.psdbg.interpreter;
 
-import de.uka.ilkd.key.logic.Name;
 import de.uka.ilkd.key.logic.NamespaceSet;
-import de.uka.ilkd.key.logic.Term;
-import de.uka.ilkd.key.logic.op.LogicVariable;
-import de.uka.ilkd.key.logic.op.QuantifiableVariable;
 import de.uka.ilkd.key.logic.sort.Sort;
 import de.uka.ilkd.key.proof.Goal;
 import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
 import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
-import edu.kit.iti.formal.psdbg.interpreter.data.TermValue;
 import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
 import edu.kit.iti.formal.psdbg.parser.ast.Expression;
-import edu.kit.iti.formal.psdbg.parser.ast.NamespaceSetExpression;
 import edu.kit.iti.formal.psdbg.parser.ast.SubstituteExpression;
-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.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 org.key_project.util.collection.ImmutableArray;
 
 import java.util.regex.Matcher;
 import java.util.regex.Pattern;
@@ -30,21 +21,6 @@ public class KeyEvaluator extends Evaluator<KeyData> {
         super(assignments, g);
     }
 
-    @Override
-    public Value visit(NamespaceSetExpression nss) {
-        Value term = (Value) nss.getExpression().accept(this);
-        if (term.getType() instanceof TermType) {
-            TermValue data = ((TermValue) term.getData()).copy();
-            nss.getSignature().forEach((v,s) -> {
-                Sort sort = asKeySort(s, getGoal().getData().getGoal());
-                QuantifiableVariable gf;
-                data.getNs().variables().add(new LogicVariable(new Name(v.getIdentifier()), sort));
-            });
-            return new Value(term.getType(), data);
-        }else {
-            throw new IllegalStateException("Try to apply substitute on a non-term value.");
-        }
-    }
 
     private Sort asKeySort(Type symbol, Goal g) {
         NamespaceSet global = g.proof().getServices().getNamespaces();

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

@@ -164,9 +164,4 @@ public class Evaluator<T> extends DefaultASTVisitor<Value> implements ScopeObser
     public Value visit(FunctionCall func) {
         return func.getFunction().eval(this, func);
     }
-
-    @Override
-    public Value visit(NamespaceSetExpression nss) {
-        return null;
-    }
 }

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/FindNearestASTNode.java

@@ -199,11 +199,6 @@ public class FindNearestASTNode implements ASTTraversal<ASTNode> {
         return null;
     }
 
-    @Override
-    public ASTNode visit(NamespaceSetExpression nss) {
-        return null;
-    }
-
     public Optional<ASTNode> find(List<ProofScript> ast) {
         return ast.stream().map(a -> a.accept(this))
                 .filter(Objects::nonNull)