Merge remote-tracking branch 'origin/master'

# Conflicts:
#	rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Evaluator.java
#	ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java

build.gradle

@@ -27,6 +27,13 @@ subprojects {
         maven { url "https://oss.sonatype.org/content/repositories/snapshots/" }
     }
 
+    task printClasspath {
+        doLast {//            sourceSets.test.runtimeClasspath.
+
+            sourceSets.test.runtimeClasspath.each {println it}
+
+        }
+    }
 
     dependencies {
         compile group: 'commons-cli', name: 'commons-cli', version: '1.4'

doc @ fb865a83

+Subproject commit fb865a833c618c3a24dddfe08b2e05d76b7a450e

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
@@ -57,7 +66,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/ASTChanger.java

@@ -59,10 +59,6 @@ public class ASTChanger extends DefaultASTVisitor<ASTNode> {
 
     @Override
     public MatchExpression visit(MatchExpression match) {
-        if (match.getSignature() != null)
-            match.setSignature((Signature)
-                    match.getSignature().accept(this));
-
         match.setPattern((Expression) match.getPattern().accept(this));
         return match;
     }

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

@@ -95,7 +95,6 @@ public interface ASTTraversal<T> extends Visitor<T> {
     @Override
     default T visit(MatchExpression match) {
         match.getPattern().accept(this);
-        match.getSignature().accept(this);
         return null;
     }
 
@@ -265,9 +264,9 @@ public interface ASTTraversal<T> extends Visitor<T> {
     }
 
     @Override
-    default T visit(NamespaceSetExpression nss) {
-        nss.getExpression().accept(this);
-        nss.getSignature().accept(this);
+    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

@@ -178,8 +178,8 @@ public class DefaultASTVisitor<T> implements Visitor<T> {
     }
 
     @Override
-    public T visit(NamespaceSetExpression nss) {
-        return defaultVisit(nss);
+    public T visit(LetStatement let) {
+        return defaultVisit(let);
     }
 }
 

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

@@ -123,7 +123,7 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
         s.append("match ");
         String prefix = getWhitespacePrefix();
         match.getPattern().accept(this);
-        if (!match.getSignature().isEmpty()) {
+        /*if (!match.getSignature().isEmpty()) {
 
             if (getCurrentLineLength() > maxWidth) {
                 s.append("\n").append(prefix);
@@ -134,7 +134,7 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
             s.append("using [");
             match.getSignature().accept(this);
             s.append("]");
-        }
+        }*/
 
         return null;
     }

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

 package edu.kit.iti.formal.psdbg.parser;
 
-import edu.kit.iti.formal.psdbg.parser.ast.*;
-import javafx.util.Pair;
+import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
+import edu.kit.iti.formal.psdbg.parser.ast.Parameters;
 
 
 

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.*;
@@ -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();
@@ -245,14 +266,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);
@@ -363,11 +376,6 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
             e.setParent(match);
             match.setDerivableTerm(e);
         } else {
-            if (ctx.argList() != null) {
-                Signature signature = (Signature) ctx.argList().accept(this);
-                match.setSignature(signature);
-                signature.setParent(match);
-            }
             Expression<ParserRuleContext> e = (Expression<ParserRuleContext>) ctx.pattern.accept(this);
             match.setPattern(e);
             e.setParent(match);

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

@@ -90,5 +90,5 @@ public interface Visitor<T> {
 
     T visit(RelaxBlock relaxBlock);
 
-    T visit(NamespaceSetExpression nss);
+    T visit(LetStatement let);
 }

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

@@ -10,12 +10,12 @@ package edu.kit.iti.formal.psdbg.parser.ast;
  * 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>.
@@ -25,12 +25,13 @@ package edu.kit.iti.formal.psdbg.parser.ast;
 
 import edu.kit.iti.formal.psdbg.parser.Visitable;
 import edu.kit.iti.formal.psdbg.parser.Visitor;
-import lombok.EqualsAndHashCode;
 import lombok.Getter;
 import lombok.Setter;
+import lombok.val;
 import org.antlr.v4.runtime.ParserRuleContext;
 
 import javax.annotation.Nullable;
+import java.util.Arrays;
 import java.util.Objects;
 
 /**
@@ -47,7 +48,9 @@ public abstract class ASTNode<T extends ParserRuleContext>
     /**
      *
      */
-    @Getter @Setter @Nullable
+    @Getter
+    @Setter
+    @Nullable
     protected ASTNode parent;
 
     /**
@@ -116,7 +119,7 @@ public abstract class ASTNode<T extends ParserRuleContext>
     @Override
     public abstract ASTNode<T> copy();
 
-    public boolean isAncestor(ASTNode node){
+    public boolean isAncestor(ASTNode node) {
         ASTNode n = this;
         do {
             if (n.equals(node))
@@ -140,6 +143,17 @@ public abstract class ASTNode<T extends ParserRuleContext>
         return depth;
     }
 
+    public ASTNode[] getChildren() {
+        return new ASTNode[0];
+    }
+
+    public final ASTNode[] asList() {
+        val ary = getChildren();
+        val nry = Arrays.copyOf(ary, ary.length + 1);
+        nry[nry.length - 1] = this;
+        return nry;
+    }
+
     @Override
     public boolean equals(Object o) {
         if (this == o) return true;
@@ -152,4 +166,12 @@ public abstract class ASTNode<T extends ParserRuleContext>
     public int hashCode() {
         return Objects.hash(getRuleContext());
     }
+
+    public int getSyntaxWidth() {
+        if (ruleContext != null) {
+            return ruleContext.stop.getStopIndex()
+                    - ruleContext.start.getStartIndex();
+        }
+        return -1;
+    }
 }

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

@@ -10,12 +10,12 @@ package edu.kit.iti.formal.psdbg.parser.ast;
  * 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>.
@@ -23,7 +23,6 @@ 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 edu.kit.iti.formal.psdbg.parser.types.Type;
@@ -74,6 +73,10 @@ public class AssignmentStatement
         return type != null;
     }
 
+    @Override
+    public ASTNode[] getChildren() {
+        return new ASTNode[]{getLhs(), getRhs()};
+    }
 
     @Override
     public boolean eq(ASTNode o) {

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

@@ -10,12 +10,12 @@ package edu.kit.iti.formal.psdbg.parser.ast;
  * 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>.
@@ -47,6 +47,11 @@ public class BinaryExpression extends Expression<ParserRuleContext> {
         this.right = right;
     }
 
+    @Override
+    public ASTNode[] getChildren() {
+        return new ASTNode[]{getLeft(), getRight()};
+    }
+
     @Override
     public <T> T accept(Visitor<T> visitor) {
         return visitor.visit(this);

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

@@ -10,12 +10,12 @@ package edu.kit.iti.formal.psdbg.parser.ast;
  * 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>.
@@ -23,7 +23,6 @@ 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.*;
@@ -58,6 +57,11 @@ public class CallStatement extends Statement<ScriptLanguageParser.ScriptCommandC
         return visitor.visit(this);
     }
 
+    @Override
+    public ASTNode[] getChildren() {
+        return new ASTNode[]{getParameters()};
+    }
+
     /**
      * {@inheritDoc}
      */

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

@@ -10,12 +10,12 @@ package edu.kit.iti.formal.psdbg.parser.ast;
  * 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>.
@@ -44,14 +44,21 @@ public abstract class CaseStatement extends Statement<ScriptLanguageParser.Cases
     /**
      * {@inheritDoc}
      */
-    @Override public <T> T accept(Visitor<T> visitor) {
+    @Override
+    public <T> T accept(Visitor<T> visitor) {
         return visitor.visit(this);
     }
 
     /**
      * {@inheritDoc}
      */
-    @Override public abstract CaseStatement copy();
+    @Override
+    public abstract CaseStatement copy();
+
+    @Override
+    public ASTNode[] getChildren() {
+        return new ASTNode[]{getBody()};
+    }
 
     @Override
     public boolean equals(Object o) {
@@ -63,5 +70,4 @@ public abstract class CaseStatement extends Statement<ScriptLanguageParser.Cases
 
         return getBody().eq(that.getBody());
     }
-
 }

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

@@ -10,12 +10,12 @@ package edu.kit.iti.formal.psdbg.parser.ast;
  * 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>.
@@ -25,10 +25,7 @@ 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.Getter;
-import lombok.NonNull;
-import lombok.RequiredArgsConstructor;
-import lombok.Setter;
+import lombok.*;
 
 import java.util.ArrayList;
 import java.util.List;
@@ -41,22 +38,37 @@ import java.util.List;
 @Getter
 @RequiredArgsConstructor
 public class CasesStatement extends Statement<ScriptLanguageParser.CasesStmtContext> {
-    @NonNull private final List<CaseStatement> cases = new ArrayList<>();
+    @NonNull
+    private final List<CaseStatement> cases = new ArrayList<>();
     // @NonNull private Statements defaultCase = new Statements();
     @NonNull
     private DefaultCaseStatement defCaseStmt = new DefaultCaseStatement();
 
+    @Override
+    public ASTNode[] getChildren() {
+        if (defCaseStmt == null)
+            return (ASTNode[]) cases.toArray();
+        else {
+            val ret = new ASTNode[cases.size() + (defCaseStmt != null ? 1 : 0)];
+            System.arraycopy(cases.toArray(), 0, ret, 0, cases.size());
+            ret[ret.length - 1] = defCaseStmt;
+            return ret;
+        }
+    }
+
     /**
      * {@inheritDoc}
      */
-    @Override public <T> T accept(Visitor<T> visitor) {
+    @Override
+    public <T> T accept(Visitor<T> visitor) {
         return visitor.visit(this);
     }
 
     /**
      * {@inheritDoc}
      */
-    @Override public CasesStatement copy() {
+    @Override
+    public CasesStatement copy() {
         CasesStatement c = new CasesStatement();
         cases.forEach(caseStatement -> c.cases.add(caseStatement.copy()));
         //  if (defaultCase != null)
@@ -76,7 +88,7 @@ public class CasesStatement extends Statement<ScriptLanguageParser.CasesStmtCont
         CasesStatement that = (CasesStatement) o;
 
         for (int i = 0; i < cases.size(); i++) {
-            if(!cases.get(i).eq(that.cases.get(i)))
+            if (!cases.get(i).eq(that.cases.get(i)))
                 return false;
         }
 

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

@@ -19,7 +19,7 @@ public class ClosesCase extends CaseStatement {
      * A close subscript() {bodyscript} expression
      *
      * @param closesGuard the script that is exectued in order to determine whether goal would clos. This proof is pruned afterwards
-     * @param body         the actual script that is then executed when closesscript was successful and pruned
+     * @param body        the actual script that is then executed when closesscript was successful and pruned
      */
     public ClosesCase(Statements closesGuard, Statements body) {
         this.body = body;
@@ -55,4 +55,9 @@ public class ClosesCase extends CaseStatement {
         return getClosesGuard() != null ? getClosesGuard().eq(that.getClosesGuard()) : that.getClosesGuard() == null;
     }
 
+
+    @Override
+    public ASTNode[] getChildren() {
+        return new ASTNode[]{getClosesGuard(), getBody()};
+    }
 }

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

 package edu.kit.iti.formal.psdbg.parser.ast;
 
-        /*-
-         * #%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.ScriptLanguageParser;
 import lombok.*;
-import org.antlr.v4.runtime.ParserRuleContext;
 
 /**
  * @author Alexander Weigl
@@ -39,11 +38,13 @@ public abstract class ConditionalBlock
         extends Statement<ScriptLanguageParser.ConditionalBlockContext> {
     @Getter
     @Setter
-    @NonNull protected Statements body = new Statements();
+    @NonNull
+    protected Statements body = new Statements();
 
     @Getter
     @Setter
-    @NonNull protected Expression condition = BooleanLiteral.TRUE;
+    @NonNull
+    protected Expression condition = BooleanLiteral.TRUE;
 
     @Override
     public boolean eq(ASTNode o) {
@@ -56,4 +57,8 @@ public abstract class ConditionalBlock
         return getBody() != null ? getBody().eq(that.getBody()) : that.getBody() == null;
     }
 
+    @Override
+    public ASTNode[] getChildren() {
+        return new ASTNode[]{getCondition(), getBody()};
+    }
 }

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

@@ -8,7 +8,6 @@ import lombok.Setter;
 @Getter
 @Setter
 public class DefaultCaseStatement extends Statement<ScriptLanguageParser.StmtListContext> {
-
     protected Statements body;