Changes to jars and commented exceptions

keydeps/README

 # Execute this in this folder.
 
 # Set to key/key/deployment/components/
-COMPONENTS=~/work/key/key/deployment/components/
+COMPONENTS=${COMPONENTS:-~/work/key/key/deployment/components/}
 
 
 mvn install:install-file -Dfile=$COMPONENTS/key.core.jar \

keydeps/README.user

 # Execute this in this folder.
 
 # Set to key/key/deployment/components/
-COMPONENTS=~/work/key/key/deployment/components/
+COMPONENTS=${COMPONENTS:-~/work/key/key/deployment/components/}
 
 
 mvn install:install-file -Dfile=$COMPONENTS/key.core.jar \

keydeps/local-repo/key-project-psdbg/key.core/2.7-SNAPSHOT/maven-metadata-local.xml

@@ -7,17 +7,17 @@
     <snapshot>
       <localCopy>true</localCopy>
     </snapshot>
-    <lastUpdated>20170911152346</lastUpdated>
+      <lastUpdated>20170912105152</lastUpdated>
     <snapshotVersions>
       <snapshotVersion>
         <extension>jar</extension>
         <value>2.7-SNAPSHOT</value>
-        <updated>20170911152346</updated>
+          <updated>20170912105152</updated>
       </snapshotVersion>
       <snapshotVersion>
         <extension>pom</extension>
         <value>2.7-SNAPSHOT</value>
-        <updated>20170911152346</updated>
+          <updated>20170912103022</updated>
       </snapshotVersion>
     </snapshotVersions>
   </versioning>

keydeps/local-repo/key-project-psdbg/key.core/maven-metadata-local.xml

@@ -6,6 +6,6 @@
     <versions>
       <version>2.7-SNAPSHOT</version>
     </versions>
-    <lastUpdated>20170911152346</lastUpdated>
+      <lastUpdated>20170912105152</lastUpdated>
   </versioning>
 </metadata>

keydeps/local-repo/key-project-psdbg/key.ui/2.7-SNAPSHOT/maven-metadata-local.xml

@@ -7,17 +7,17 @@
     <snapshot>
       <localCopy>true</localCopy>
     </snapshot>
-    <lastUpdated>20170911152349</lastUpdated>
+      <lastUpdated>20170912105155</lastUpdated>
     <snapshotVersions>
       <snapshotVersion>
         <extension>jar</extension>
         <value>2.7-SNAPSHOT</value>
-        <updated>20170911152349</updated>
+          <updated>20170912105155</updated>
       </snapshotVersion>
       <snapshotVersion>
         <extension>pom</extension>
         <value>2.7-SNAPSHOT</value>
-        <updated>20170911152349</updated>
+          <updated>20170912103024</updated>
       </snapshotVersion>
     </snapshotVersions>
   </versioning>

keydeps/local-repo/key-project-psdbg/key.ui/maven-metadata-local.xml

@@ -6,6 +6,6 @@
     <versions>
       <version>2.7-SNAPSHOT</version>
     </versions>
-    <lastUpdated>20170911152349</lastUpdated>
+      <lastUpdated>20170912105155</lastUpdated>
   </versioning>
 </metadata>

keydeps/local-repo/key-project-psdbg/key.util/2.7-SNAPSHOT/maven-metadata-local.xml

@@ -7,17 +7,17 @@
     <snapshot>
       <localCopy>true</localCopy>
     </snapshot>
-    <lastUpdated>20170911152351</lastUpdated>
+      <lastUpdated>20170912105158</lastUpdated>
     <snapshotVersions>
       <snapshotVersion>
         <extension>jar</extension>
         <value>2.7-SNAPSHOT</value>
-        <updated>20170911152351</updated>
+          <updated>20170912105158</updated>
       </snapshotVersion>
       <snapshotVersion>
         <extension>pom</extension>
         <value>2.7-SNAPSHOT</value>
-        <updated>20170911152351</updated>
+          <updated>20170912103027</updated>
       </snapshotVersion>
     </snapshotVersions>
   </versioning>

keydeps/local-repo/key-project-psdbg/key.util/maven-metadata-local.xml

@@ -6,6 +6,6 @@
     <versions>
       <version>2.7-SNAPSHOT</version>
     </versions>
-    <lastUpdated>20170911152351</lastUpdated>
+      <lastUpdated>20170912105158</lastUpdated>
   </versioning>
 </metadata>

keydeps/local-repo/key-project-psdbg/recoder/maven-metadata-local.xml

@@ -7,6 +7,6 @@
     <versions>
       <version>2.7</version>
     </versions>
-    <lastUpdated>20170911152354</lastUpdated>
+      <lastUpdated>20170912105201</lastUpdated>
   </versioning>
 </metadata>

keydeps/src/main/java/GenDoc.java

@@ -19,6 +19,23 @@ import java.util.stream.Collectors;
  * @version 1 (11.09.17)
  */
 public class GenDoc {
+    private static final Set<String> FORBBIDEN = new TreeSet<>();
+
+    static {
+        FORBBIDEN.add("exit");
+        FORBBIDEN.add("focus");
+        FORBBIDEN.add("javascript");
+        FORBBIDEN.add("leave");
+        FORBBIDEN.add("let \n");
+        /*TODO
+        script
+                schemaVar
+        select
+                set
+        skip
+              */
+    }
+
     private static File basedir = new File("..");
     private static File propertiesFile = new File(basedir, "rt-key/src/main/resources/edu/kit/iti/formal/psdbg/taclets.properties.xml");
     private static File dummyFile = new File(basedir, "rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/contraposition/contraposition.key");
@@ -58,7 +75,7 @@ public class GenDoc {
                     "\n\nCovering the *default* taclets of [KeY](http://key-project.org).");
 
             for (Taclet t : taclets) {
-                stream.write("\n\n## ${t.displayName()}\n\n");
+                stream.write("\n\n## " + t.displayName() + "\n\n");
                 stream.write("```\n" + t.toString() + "\n```");
             }
 
@@ -143,7 +160,8 @@ public class GenDoc {
             commands.sort(Comparator.comparing(ProofScriptCommand::getName));
 
             for (ProofScriptCommand t : commands) {
-                stream.write(helpForCommand(t) + "\n\n");
+                if (!FORBBIDEN.contains(t.getName()))
+                    stream.write(helpForCommand(t) + "\n\n");
             }
             stream.close();
         } catch (IOException e) {

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

@@ -69,8 +69,8 @@ expression
 
 substExpressionList
     :
-    (scriptVar '/' expression
-        (',' scriptVar '/' expression)*
+    (scriptVar '\\' expression
+        (',' scriptVar '\\' expression)*
     )?
     ;
 

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

@@ -5,6 +5,7 @@ import lombok.Data;
 import lombok.NoArgsConstructor;
 
 import java.util.ArrayList;
+import java.util.Arrays;
 import java.util.List;
 
 /**
@@ -17,6 +18,10 @@ import java.util.List;
 public class TermType implements Type {
     private List<Type> argTypes = new ArrayList<>();
 
+    public TermType(Type... sortType) {
+        this(Arrays.asList(sortType));
+    }
+
     @Override
     public String symbol() {
         return "Term<" +

matcher/src/main/antlr4/edu/kit/formal/psdb/termmatcher/MatchPattern.g4

@@ -26,11 +26,12 @@ termPattern :
     | <assoc=right> termPattern op=(DIV|MOD) termPattern        #divMod
     | termPattern op=(PLUS|MINUS) termPattern                   #plusMinus
     | termPattern op=(LE|GE|LEQ|GEQ) termPattern                #comparison
-    | termPattern op=(NEQ|EQ) termPattern                       #equality
+    | termPattern op=(NEQ|EQ) termPattern                 #equality
     | termPattern AND termPattern                               #and
     | termPattern OR termPattern                                #or
     | termPattern IMP termPattern                               #impl
     | termPattern XOR termPattern                               #xor
+   // | termPattern EQUIV termPattern                             #equivalence
     //|   termPattern EQUIV termPattern already covered by EQ/NEQ
     | MINUS termPattern                                         #exprNegate
     | NOT termPattern                                           #exprNot
@@ -61,6 +62,7 @@ EQ : '=' ;
 NEQ : '!=' ;
 GEQ : '>=' ;
 LEQ : '<=' ;
+EQUIV : '<->';
 GE : '>' ;
 LE : '<' ;
 AND : '&' ;

matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/Utils.java

@@ -12,10 +12,12 @@ public class Utils {
      * @param formula
      * @return parsable Stringversion of Term
      */
+    @Deprecated
     public static String toPrettyTerm(Term formula) {
         StringBuilder sb = new StringBuilder();
 
         Operator op = formula.op();
+
         //ugly if/else
         if (op.equals(Junctor.IMP)) {
             sb.append("(" + toPrettyTerm(formula.sub(0)) + ") -> (" + toPrettyTerm(formula.sub(1)) + ")");

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

@@ -3,9 +3,9 @@ package edu.kit.iti.formal.psdbg.interpreter;
 import de.uka.ilkd.key.api.ScriptApi;
 import de.uka.ilkd.key.api.VariableAssignments;
 import de.uka.ilkd.key.logic.Name;
-import de.uka.ilkd.key.logic.SequentFormula;
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.op.SchemaVariable;
+import de.uka.ilkd.key.pp.LogicPrinter;
 import de.uka.ilkd.key.proof.ApplyStrategy;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Proof;
@@ -15,9 +15,9 @@ import de.uka.ilkd.key.rule.Taclet;
 import de.uka.ilkd.key.rule.TacletApp;
 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.SortType;
 import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
 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.ast.Variable;
 import edu.kit.iti.formal.psdbg.parser.data.Value;
 import edu.kit.iti.formal.psdbg.parser.types.SimpleType;
@@ -25,7 +25,6 @@ import edu.kit.iti.formal.psdbg.parser.types.TermType;
 import edu.kit.iti.formal.psdbg.parser.types.Type;
 import edu.kit.iti.formal.psdbg.termmatcher.MatcherFacade;
 import edu.kit.iti.formal.psdbg.termmatcher.Matchings;
-import edu.kit.iti.formal.psdbg.termmatcher.Utils;
 import edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath;
 import org.key_project.util.collection.ImmutableList;
 
@@ -197,13 +196,46 @@ public class KeYMatcher implements MatcherApi<KeyData> {
         // System.out.println("Matched " + keyMatchResult.size() + " goals from " + currentState.toString() + " with pattern " + term);
         List<VariableAssignment> transformedMatchResults = new ArrayList<>();
         for (VariableAssignments mResult : keyMatchResult) {
-            transformedMatchResults.add(from(mResult));
+            transformedMatchResults.add(from(mResult, currentState.getData()));
         }
         //keyMatchResult.forEach(r -> transformedMatchResults.add(from(r)));
         return transformedMatchResults;
 
     }
 
+    /**
+     * Transforms a KeY Variable Assignment into an assignment for the interpreter
+     *
+     * @param keyAssignments
+     * @param currentState
+     * @return
+     */
+    public VariableAssignment from(VariableAssignments keyAssignments, KeyData currentState) {
+
+        VariableAssignment interpreterAssignments = new VariableAssignment(null);
+
+        Map<String, VariableAssignments.VarType> keyTypeMap = keyAssignments.getTypeMap();
+        keyTypeMap.entrySet().forEach(e -> interpreterAssignments.declare(e.getKey(), interpreter.getTypeConversionBiMap().inverse().get(e.getValue())));
+        keyTypeMap.keySet().forEach(k -> {
+            try {
+                interpreterAssignments.assign(k, toValueTerm(currentState, (Term) keyAssignments.getVarValue(k)));
+                //System.out.println(keyAssignments.getVarValue(k));
+            } catch (Exception e) {
+                e.printStackTrace();
+            }
+        });
+        return interpreterAssignments;
+    }
+
+    private Value<String> toValueTerm(KeyData currentState, Term matched) {
+        String reprTerm = LogicPrinter.quickPrintTerm(matched, currentState.getEnv().getServices());
+
+        return new Value<>(
+                new TermType(new SortType(matched.sort())),
+                reprTerm
+        );
+    }
+
     @Override
     public List<VariableAssignment> matchSeq(GoalNode<KeyData> currentState, String data, Signature sig) {
         System.out.println("State that will be matched " + currentState.getData().getNode().sequent() + " with pattern " + data);
@@ -225,9 +257,10 @@ public class KeYMatcher implements MatcherApi<KeyData> {
                         s = s.replaceFirst("\\?", "");
                     }
 
-                    va.declare(s, new TermType());
-                    va.assign(s, Value.from(from(matched)));
-                    System.out.println("Variable " + s + " : " + Value.from(from(matched)));
+                    Value<String> value = toValueTerm(currentState.getData(), matched);
+                    va.declare(s, value.getType());
+                    va.assign(s, value);
+                    System.out.println("Variable " + s + " : " + value);
                 }
             }
             List<VariableAssignment> retList = new LinkedList();
@@ -237,35 +270,8 @@ public class KeYMatcher implements MatcherApi<KeyData> {
         }
     }
 
-    /**
-     * Transforms a KeY Variable Assignment into an assignment for the interpreter
-     *
-     * @param keyAssignments
-     * @return
-     */
-    public VariableAssignment from(VariableAssignments keyAssignments) {
-
-        VariableAssignment interpreterAssignments = new VariableAssignment(null);
-
-        Map<String, VariableAssignments.VarType> keyTypeMap = keyAssignments.getTypeMap();
-        keyTypeMap.entrySet().forEach(e -> interpreterAssignments.declare(e.getKey(), interpreter.getTypeConversionBiMap().inverse().get(e.getValue())));
-        keyTypeMap.keySet().forEach(k -> {
-            try {
-                interpreterAssignments.assign(k, Value.from(from((Term) keyAssignments.getVarValue(k))));
-                //System.out.println(keyAssignments.getVarValue(k));
-            } catch (Exception e) {
-                e.printStackTrace();
-            }
-        });
-        return interpreterAssignments;
-    }
-
-    private TermLiteral from(Term t) {
-        //TODO rewrite operator
-        return new TermLiteral(Utils.toPrettyTerm(t));
-    }
 
-    private TermLiteral from(SequentFormula sf) {
-        return new TermLiteral(sf.toString());
-    }
+    //private TermLiteral from(SequentFormula sf) {
+    //    return new TermLiteral(sf.toString());
+    //}
 }

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

+package edu.kit.iti.formal.psdbg.interpreter.data;
+
+import de.uka.ilkd.key.logic.sort.Sort;
+import edu.kit.iti.formal.psdbg.parser.types.Type;
+import lombok.Getter;
+import lombok.RequiredArgsConstructor;
+
+@RequiredArgsConstructor
+public class SortType implements Type {
+    @Getter
+    private final Sort sort;
+
+    @Override
+    public String symbol() {
+        return sort.toString();
+    }
+}

rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/ExecuteTest.java

@@ -2,7 +2,9 @@ package edu.kit.iti.formal.psdbg.interpreter;
 
 import static edu.kit.iti.formal.psdbg.TestHelper.getFile;
 import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
+import edu.kit.iti.formal.psdbg.interpreter.data.State;
 import org.apache.commons.cli.ParseException;
+import org.junit.Assert;
 import org.junit.Test;
 
 import java.io.IOException;
@@ -51,7 +53,10 @@ public class ExecuteTest {
                 getFile(getClass(), "contraposition/contraposition.key"),
                 "-s", getFile(getClass(), "contraposition/cutTest.kps"));
         Interpreter<KeyData> i = execute.run();
-        System.out.println(i.getCurrentState());
+        State<KeyData> currentState = i.getCurrentState();
+        System.out.println(currentState);
+        //This reveals a bug in the cases merge
+        Assert.assertEquals("Number of goals has to be two ", 2, i.getCurrentGoals().size());
 
     }
 }
\ No newline at end of file

rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/contraposition/cutTest.kps

 script cutTest(){
-  //auto step=2;
-  //cut `p`;
   cases{
+    //X:TERM :=`p`;
     case match `==>?X -> ?Y`:
-    //auto steps=100;
-    cut `?Y`[];
-     
+        cut `?X`[?X \ Y];
+
   }
-    //cut #2=`p`;
-    //auto steps=100;
 }
\ No newline at end of file

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

@@ -40,7 +40,7 @@ public class ANTLR4LexerHighlighter {
 
             return spansBuilder.create();
         } catch (StringIndexOutOfBoundsException e) {
-            e.printStackTrace();
+            // e.printStackTrace();
         }
         return null;
     }

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

@@ -235,13 +235,4 @@ public class Utils {
         return String.valueOf(t.getData().getNode().serialNr());
     }
 
-    /**
-     * Rewrite toString() representation of Term to a parsable version
-     *
-     * @param formula
-     * @return parsable Stringversion of Term
-     */
-  /*  public static String toPrettyTerm(Term formula) {
-      return KeYUtils.toPrettyTerm(formula);
-    }*/
 }

website/docs/commands.md

@@ -2,7 +2,7 @@
 
 
 
-Generated on: Mon Sep 11 17:22:08 CEST 2017by `gendoc.groovy`.
+Generated on: Tue Sep 12 15:08:55 CEST 2017by `gendoc.groovy`.
 
 Covering the proof script commands of [KeY](http://key-project.org).
 
@@ -18,96 +18,47 @@ a formula #2 to which the command is applied
 
 **Arguments:**
 
-* `#2` :  *TERM* (*R*)
+* `#2` :  *TERM* (*R*)null
 
 ## auto
 > Synopsis: `auto [all=<BOOLEAN>] [steps=<INT>]`
 
 
-The AutoCommand invokes the automatic strategy "Auto"
-
 
 **Arguments:**
 
-* `all` :  *BOOLEAN* 
-* `steps` :  *INT* 
+* `all` :  *BOOLEAN* null
+* `steps` :  *INT* null
 
 ## cut
 > Synopsis: `cut <TERM>`
 
 
-* The command object CutCommand has as scriptcommand name "cut"
-* As parameters:
-* a formula with the id "#2"
-
 
 **Arguments:**
 
-* `#2` :  *TERM* (*R*)
-
-## exit
-> Synopsis: `exit`
-
-
-
-
-
-**Arguments:**
-
-
-## focus
-> Synopsis: `focus <SEQUENT>`
-
-
-
-**Arguments:**
-
-* `#2` :  *SEQUENT* (*R*)
+* `#2` :  *TERM* (*R*)null
 
 ## instantiate
-> Synopsis: `instantiate [formula=<TERM>] [var=<STRING>] [occ=<INT>] [<STRING>] [with=<TERM>]`
+> Synopsis: `instantiate formula=<TERM> var=<STRING> occ=<INT> with=<TERM>`
 
 
-instantiate var=a occ=2 with="a_8" hide
-<p>
-instantiate formula="\forall int a; phi(a)" with="a_8"
-
-
-
-**Arguments:**
-
-* `formula` :  *TERM* 
-* `var` :  *STRING* 
-* `occ` :  *INT* 
-* `#2` :  *STRING* 
-* `with` :  *TERM* 
-
-## javascript
-> Synopsis: `javascript <STRING>`
-
-
-
-**Arguments:**
-
-* `#2` :  *STRING* (*R*)
-
-## leave
-> Synopsis: `leave`
-
 
 
 
 
 **Arguments:**
 
+* `formula` :  *TERM* (*R*)null
+* `var` :  *STRING* (*R*)null
+* `occ` :  *INT* (*R*)null
+* `with` :  *TERM* (*R*)null
 
 ## let
 > Synopsis: `let`
 
 
 
-
-
 **Arguments:**
 
 
@@ -118,31 +69,19 @@ instantiate formula="\forall int a; phi(a)" with="a_8"
 
 **Arguments:**
 
-* `#2` :  *STRING* (*R*)
+* `#2` :  *STRING* (*R*)null
 
 ## rule
 > Synopsis: `rule <STRING> [on=<TERM>] [formula=<TERM>] [occ=<INT>]`
 
 
-* Command that applies a calculus rule
-* All parameters are passed as strings and converted by the command.
-* The parameters are:
-* <ol>
-*     <li>#2 = <String>rule name</String></li>
-*     <li>on= key.core.logic.Term on which the rule should be applied to as String (find part of the rule) </li>
-*     <li>formula= toplevel formula in which term appears in</li>
-*     <li>occ = occurrence number</li>
-*     <li>inst_= instantiation</li>
-* </ol>
-
-
 
 **Arguments:**
 
-* `#2` :  *STRING* (*R*)
-* `on` :  *TERM* 
-* `formula` :  *TERM* 
-* `occ` :  *INT* 
+* `#2` :  *STRING* (*R*)null
+* `on` :  *TERM* null
+* `formula` :  *TERM* null
+* `occ` :  *INT* null