multiple enhancements

* Open in Key
* repair matching of updates
* assignment hooks

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

@@ -50,8 +50,17 @@ f(x), f(x,y,g(y)), X, ?Y, _, ..., f(... ?X ...), f(..., ?X), f(..., ...?X...), f
 
 bindClause : ('\\as' | ':') SID;
 
-ARROW : '⇒' | '==>';
 DONTCARE: '?' | '_' | '█';
+DIGITS : DIGIT+ ;
+fragment DIGIT : [0-9] ;
+SID: '?' [_a-zA-Z0-9\\]+ ;
+ID : [a-zA-Z\\_] ([_a-zA-Z0-9\\])*
+   | 'update-application'
+   | 'parallel-upd'
+   | 'elem-update'
+   ;
+
+ARROW : '⇒' | '==>';
 STARDONTCARE: '...' | '…';
 PLUS : '+' ;
 MINUS : '-' ;
@@ -72,10 +81,5 @@ XOR:'^';
 FORALL: '\forall' | '∀';
 EXISTS: '\exists';
 
-DIGITS : DIGIT+ ;
-fragment DIGIT : [0-9] ;
-SID: '?' [_a-zA-Z0-9\\]+ ;
-ID : [a-zA-Z\\_] ([_a-zA-Z0-9\\])*| 'update-application';
-
 COMMENT: '//' ~[\n\r]* -> channel(HIDDEN);
 WS: [\n\f\r\t ] -> channel(HIDDEN);

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

@@ -72,7 +72,7 @@ public class MatcherFacade {
     public static Matchings matches(String pattern, Sequent sequent, boolean catchAll) {
         MatchPatternParser mpp = getParser(pattern);
         MatchPatternParser.SequentPatternContext ctx = mpp.sequentPattern();
-        logger.error("Matching \n" + pattern + "\n" + sequent.toString());
+        logger.info("Matching \n" + pattern + "\n" + sequent.toString());
         if (mpp.getNumberOfSyntaxErrors() != 0) {
             logger.info("Invalid pattern syntax '{}' no matches returned.", pattern);
             return new Matchings();

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

@@ -7,7 +7,6 @@ import de.uka.ilkd.key.logic.Term;
 import edu.kit.formal.psdb.termmatcher.MatchPatternLexer;
 import edu.kit.formal.psdb.termmatcher.MatchPatternParser;
 import edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath;
-import static edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPathFacade.*;
 import lombok.Getter;
 import lombok.Setter;
 import org.antlr.v4.runtime.CommonToken;
@@ -18,6 +17,8 @@ import java.util.stream.Collectors;
 import java.util.stream.IntStream;
 import java.util.stream.Stream;
 
+import static edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPathFacade.*;
+
 /**
  * Matchpattern visitor visits the matchpatterns of case-statements
  *
@@ -26,9 +27,13 @@ import java.util.stream.Stream;
  */
 class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
     static final Matchings NO_MATCH = new Matchings();
+
     static final Matchings EMPTY_MATCH = Matchings.singleton("EMPTY_MATCH", null);
+
     static final Map<String, MatchPath> EMPTY_VARIABLE_ASSIGNMENT = EMPTY_MATCH.first();
+
     Random random = new Random(42L);
+
     /*
      * Reduce two matchinfos
      *
@@ -61,6 +66,7 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
     }
     */
     private List<Integer> currentPosition = new ArrayList<>();
+
     /**
      * If true, we assume every term in the pattern has a binder.
      * The binding names are generated.
@@ -205,9 +211,11 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
         //System.out.format("Match: %25s with %s %n", peek, ctx.toInfoString(new MatchPatternParser(null)));
         String expectedFunction = ctx.func.getText();
         Term peek = ((MatchPath.MPTerm) path).getUnit();
-        if (peek.op().name().toString().equals(expectedFunction)  // same name
-                && ctx.termPattern().size() == peek.arity()       // same arity
-                ) {
+        boolean sameName = expectedFunction.equals("?")
+                || expectedFunction.equals("_")
+                || peek.op().name().toString().equals(expectedFunction);
+        boolean sameArity = ctx.termPattern().size() == peek.arity();
+        if (sameName && sameArity) {
             Matchings m = IntStream.range(0, peek.arity())
                     .mapToObj(i -> (Matchings)
                             accept(ctx.termPattern(i), create(path, i)))

matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/TestUpdateMatch.java

+package edu.kit.iti.formal.psdbg.termmatcher;
+
+import de.uka.ilkd.key.api.KeYApi;
+import de.uka.ilkd.key.api.ProofApi;
+import de.uka.ilkd.key.api.ProofManagementApi;
+import de.uka.ilkd.key.logic.Sequent;
+import de.uka.ilkd.key.proof.init.ProofInputException;
+import de.uka.ilkd.key.proof.io.ProblemLoaderException;
+import org.junit.Assert;
+import org.junit.Test;
+
+import java.io.File;
+import java.util.regex.Pattern;
+
+public class TestUpdateMatch {
+    @Test
+    public void test() throws ProblemLoaderException, ProofInputException {
+        ProofManagementApi a = KeYApi.loadFromKeyFile(new File("src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/javasimple/project.key"));
+        ProofApi pa = a.startProof(a.getProofContracts().get(0));
+        Sequent sequent = pa.getProof().root().sequent();
+        System.out.println(sequent);
+        Matchings result = MatcherFacade.matches("... update-application(_, ?X) ...", sequent, false);
+        System.out.println(result);
+        String exp = normalize("\\<{exc=null;try { result=self.foo(_x)@Test;} catch (java.lang.Throwable e) { exc=e; } }\\> (and(and(and(gt(result,Z(0(#))),java.lang.Object::<inv>(heap,self)),equals(exc,null)),all{f:Field}(all{o:java.lang.Object}(or(or(elementOf(o,f,allLocs),and(not(equals(o,null)),not(equals(boolean::select(heapAtPre,o,java.lang.Object::<created>),TRUE)))),equals(any::select(heap,o,f),any::select(heapAtPre,o,f)))))))");
+        String x = normalize(result.iterator().next().get("?X").getUnit().toString().replace("\n", " "));
+        Assert.assertEquals(exp, x);
+    }
+
+    private String normalize(String s) {
+        Pattern re = Pattern.compile("\\s+");
+        return re.matcher(s).replaceAll(" ");
+    }
+
+
+}

matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/javasimple/Test.java

+public class Test{
+
+
+
+    /*@ public normal_behavior
+      @ requires x >= 0;
+      @ ensures \result >0;
+      @*/
+    public int foo(int x){
+        if(x > 0){
+            x--;
+        }else{
+            x++;
+        }
+        return x++;
+    }
+}
\ No newline at end of file

matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/javasimple/project.key

+\javaSource "";
+\chooseContract
\ No newline at end of file

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

@@ -32,8 +32,6 @@ import java.util.stream.Stream;
  */
 public class Interpreter<T> extends DefaultASTVisitor<Object>
         implements ScopeObservable {
-    private static final int MAX_ITERATIONS = 10000;
-
     protected static Logger logger = LogManager.getLogger(Interpreter.class);
 
     @Getter
@@ -43,6 +41,13 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
     protected List<Visitor> entryListeners = new ArrayList<>(),
             exitListeners = new ArrayList<>();
 
+    /**
+     *
+     */
+    @Getter
+    @Setter
+    private int maxIterationsRepeat = 10000;
+
     private Stack<State<T>> stateStack = new Stack<>();
 
     @Getter
@@ -54,12 +59,13 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
 
     @Getter
     @Setter
-    private boolean scrictSelectedGoalMode = false;
+    private boolean strictMode = false;
 
     @Getter
     @Setter
     private VariableAssignmentHook<T> variableAssignmentHook = null;
 
+
     @Getter
     @Setter
     private boolean suppressListeners = false;
@@ -551,8 +557,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
             //State<T> newErrorState = newState(null, null);
             //newErrorState.setErrorState(true);
             //pushState(newErrorState);
-        }
-        finally {
+        } finally {
             g.exitScope();
             //  System.out.println(stateStack.peek().hashCode());
             exitScope(call);
@@ -627,9 +632,9 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
                 Set<GoalNode<T>> prevNodes = new HashSet<>(prev.getGoals());
                 Set<GoalNode<T>> endNodes = new HashSet<>(end.getGoals());
                 b = prevNodes.equals(endNodes);
-                b = b && counter <= MAX_ITERATIONS;
+                b = b && counter <= maxIterationsRepeat;
             } while (b);
-        }catch (InterpreterRuntimeException e) {
+        } catch (InterpreterRuntimeException e) {
             logger.debug("Catched!", e);
         }
         exitScope(repeatStatement);
@@ -655,7 +660,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
             }
             return selectedGoalNode;
         } catch (IllegalStateException e) {
-            if (scrictSelectedGoalMode)
+            if (strictMode)
                 throw e;
 
             logger.warn("No goal selected. Returning first goal!");

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

+package edu.kit.iti.formal.psdbg.interpreter.assignhook;
+
+import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
+import edu.kit.iti.formal.psdbg.parser.data.Value;
+import lombok.Getter;
+import lombok.Setter;
+
+public class InterpreterOptionsHook<T> extends DefaultAssignmentHook<T> {
+    @Getter
+    @Setter
+    private Interpreter<T> interpreter;
+
+    public InterpreterOptionsHook(Interpreter<T> interpreter) {
+        this.interpreter = interpreter;
+
+
+        register("__MAX_ITERATIONS_REPEAT",
+                (T data, Value v) -> {
+                    interpreter.setMaxIterationsRepeat((Integer) v.getData());
+                    return true;
+                },
+                (T data) -> Value.from(interpreter.getMaxIterationsRepeat())
+        );
+
+
+        register("__STRICT_MODE",
+                (T data, Value v) -> {
+                    interpreter.setStrictMode((boolean) v.getData());
+                    return true;
+                },
+                (T data) -> Value.from(interpreter.isStrictMode())
+        );
+
+    }
+}

ui/src/main/java/de/uka/ilkd/key/macros/TestGenMacro.java

+package de.uka.ilkd.key.macros;
+
+import de.uka.ilkd.key.control.UserInterfaceControl;
+import de.uka.ilkd.key.logic.PosInOccurrence;
+import de.uka.ilkd.key.macros.ProofMacro;
+import de.uka.ilkd.key.proof.Goal;
+import de.uka.ilkd.key.proof.Node;
+import de.uka.ilkd.key.proof.Proof;
+import de.uka.ilkd.key.proof.ProverTaskListener;
+import org.key_project.util.collection.ImmutableList;
+
+public class TestGenMacro implements ProofMacro {
+    @Override
+    public String getName() {
+        return "dummy test gen macro";
+    }
+
+    @Override
+    public String getScriptCommandName() {
+        return null;
+    }
+
+    @Override
+    public String getCategory() {
+        return null;
+    }
+
+    @Override
+    public String getDescription() {
+        return null;
+    }
+
+    @Override
+    public boolean canApplyTo(Proof proof, ImmutableList<Goal> immutableList, PosInOccurrence posInOccurrence) {
+        return false;
+    }
+
+    @Override
+    public boolean canApplyTo(Node node, PosInOccurrence posInOccurrence) {
+        return false;
+    }
+
+    @Override
+    public ProofMacroFinishedInfo applyTo(UserInterfaceControl userInterfaceControl, Proof proof, ImmutableList<Goal> immutableList, PosInOccurrence posInOccurrence, ProverTaskListener proverTaskListener) throws InterruptedException, Exception {
+        return null;
+    }
+
+    @Override
+    public ProofMacroFinishedInfo applyTo(UserInterfaceControl userInterfaceControl, Node node, PosInOccurrence posInOccurrence, ProverTaskListener proverTaskListener) throws InterruptedException, Exception {
+        return null;
+    }
+}

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java

@@ -6,9 +6,11 @@ import com.google.common.eventbus.Subscribe;
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
 import de.uka.ilkd.key.api.ProofApi;
+import de.uka.ilkd.key.gui.MainWindow;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
+import de.uka.ilkd.key.proof.SingleProof;
 import de.uka.ilkd.key.proof.init.ProofInputException;
 import de.uka.ilkd.key.proof.io.ProblemLoaderException;
 import de.uka.ilkd.key.speclang.Contract;
@@ -26,7 +28,6 @@ import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
 import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter;
 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.State;
 import edu.kit.iti.formal.psdbg.interpreter.dbg.*;
 import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
 import javafx.application.Platform;
@@ -55,6 +56,7 @@ import org.reactfx.util.FxTimer;
 import org.reactfx.util.Timer;
 
 import javax.annotation.Nullable;
+import javax.swing.*;
 import java.io.File;
 import java.io.FileWriter;
 import java.io.IOException;
@@ -82,13 +84,13 @@ public class DebuggerMain implements Initializable {
 
     public final ContractLoaderService contractLoaderService = new ContractLoaderService();
 
-    private InspectionViewsController inspectionViewsController;
-
     private final ExecutorService executorService = Executors.newFixedThreadPool(2);
 
     @Getter
     private final DebuggerMainModel model = new DebuggerMainModel();
 
+    private InspectionViewsController inspectionViewsController;
+
     private ScriptController scriptController;
 
     @FXML
@@ -868,7 +870,7 @@ public class DebuggerMain implements Initializable {
             interactiveModeController.start(getFacade().getProof(), getInspectionViewsController().getActiveInspectionViewTab().getModel());
         } else {
             interactiveModeController.stop();
-        } 
+        }
     }
 
     @FXML
@@ -953,6 +955,24 @@ public class DebuggerMain implements Initializable {
         });
     }
 
+    public void openInKey(@Nullable ActionEvent event) {
+        if (FACADE.getProofState() == KeYProofFacade.ProofState.EMPTY) {
+            Alert alert = new Alert(Alert.AlertType.ERROR, "No proof is loaded", ButtonType.OK);
+            alert.show();
+            return;
+        }
+
+        SwingUtilities.invokeLater(() -> {
+            // Swing Thread!
+            MainWindow keyWindow = MainWindow.getInstance();
+            keyWindow.addProblem(new SingleProof(FACADE.getProof(), "script"));
+            //keyWindow.getProofList().getModel().addProof();
+            keyWindow.makePrettyView();
+            keyWindow.setVisible(true);
+        });
+    }
+
+
     public class ContractLoaderService extends Service<List<Contract>> {
         @Override
         protected void succeeded() {

ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml

@@ -60,6 +60,7 @@
                         </Menu>
                         <Menu text="Edit">
                             <items>
+                                <MenuItem text="Open in KeY" onAction="#openInKey"/>
                                 <MenuItem text="Delete"/>
                                 <MenuItem text="Reformat" accelerator="Ctrl+Shift+f" onAction="#reformatCurrentEditor"/>
                                 <MenuItem text="Print Debug Information" onAction="#debugPrintDot"

website/docs/mathjaxhelper.js

+MathJax.Hub.Config({
+    config: ["MMLorHTML.js"],
+    jax: ["input/TeX", "output/HTML-CSS", "output/NativeMML"],
+    extensions: ["MathMenu.js", "MathZoom.js"]
+});

website/docs/mdx_math.py

+# -*- coding: utf-8 -*-
+
+'''
+Math extension for Python-Markdown
+==================================
+
+Adds support for displaying math formulas using
+[MathJax](http://www.mathjax.org/).
+
+Author: 2015-2017, Dmitry Shachnev <mitya57@gmail.com>.
+'''
+
+from markdown.inlinepatterns import Pattern
+from markdown.extensions import Extension
+from markdown.util import AtomicString, etree
+
+
+class MathExtension(Extension):
+    def __init__(self, *args, **kwargs):
+        self.config = {
+            'enable_dollar_delimiter':
+                [False, 'Enable single-dollar delimiter'],
+            'add_preview': [False, 'Add a preview node before each math node'],
+            'use_asciimath':
+                [False, 'Use AsciiMath syntax instead of TeX syntax'],
+        }
+        super(MathExtension, self).__init__(*args, **kwargs)
+
+    def _get_content_type(self):
+        if self.getConfig('use_asciimath'):
+            return 'math/asciimath'
+        return 'math/tex'
+
+    def extendMarkdown(self, md, md_globals):
+        def _wrap_node(node, preview_text, wrapper_tag):
+            if not self.getConfig('add_preview'):
+                return node
+            preview = etree.Element('span', {'class': 'MathJax_Preview'})
+            preview.text = AtomicString(preview_text)
+            wrapper = etree.Element(wrapper_tag)
+            wrapper.extend([preview, node])
+            return wrapper
+
+        def handle_match_inline(m):
+            node = etree.Element('script')
+            node.set('type', self._get_content_type())
+            node.text = AtomicString(m.group(3))
+            return _wrap_node(node, ''.join(m.group(2, 3, 4)), 'span')
+
+        def handle_match(m):
+            node = etree.Element('script')
+            node.set('type', '%s; mode=display' % self._get_content_type())
+            if '\\begin' in m.group(2):
+                node.text = AtomicString(''.join(m.group(2, 4, 5)))
+                return _wrap_node(node, ''.join(m.group(1, 2, 4, 5, 6)), 'div')
+            else:
+                node.text = AtomicString(m.group(3))
+                return _wrap_node(node, ''.join(m.group(2, 3, 4)), 'div')
+
+        inlinemathpatterns = (
+            Pattern(r'(?<!\\|\$)(\$)([^\$]+)(\$)'),   #  $...$
+            Pattern(r'(?<!\\)(\\\()(.+?)(\\\))')      # \(...\)
+        )
+        mathpatterns = (
+            Pattern(r'(?<!\\)(\$\$)([^\$]+)(\$\$)'),  # $$...$$
+            Pattern(r'(?<!\\)(\\\[)(.+?)(\\\])'),     # \[...\]
+            Pattern(r'(?<!\\)(\\begin{([a-z]+?\*?)})(.+?)(\\end{\3})')
+        )
+        if not self.getConfig('enable_dollar_delimiter'):
+            inlinemathpatterns = inlinemathpatterns[1:]
+        for i, pattern in enumerate(mathpatterns):
+            pattern.handleMatch = handle_match
+            md.inlinePatterns.add('math-%d' % i, pattern, '<escape')
+        for i, pattern in enumerate(inlinemathpatterns):
+            pattern.handleMatch = handle_match_inline
+            md.inlinePatterns.add('math-inline-%d' % i, pattern, '<escape')
+        if self.getConfig('enable_dollar_delimiter'):
+            md.ESCAPED_CHARS.append('$')
+
+
+def makeExtension(*args, **kwargs):
+    return MathExtension(*args, **kwargs)
\ No newline at end of file

website/docs/variables.md

+# Variables 
+
+The proof script language supports script variables. 
+These are variables that are managed by the interpreter and are not part of the explicit proof 
+object—in contrast to the variables of the 
+Java program and the logical variables of first oder logic formulas.
+
+As Java or logic variables, we bind the assignments script variables to a sequences.
+If a script variable is not assigned in the current selected goal, 
+we look up its value in the sequence's ancestors, recursively. 
+
+## Types 
+
+Each variables has a type. Following *simple* types are defined: 
+
+* `int`  -- arbitrary precision integers
+* `bool` -- true or false
+* `string` --  string (`""`)
+
+For the interoperability with KeY we allow that parameterized term types `TERM<S>`, 
+where `S` is a KeY sort (already defined by in the KeY namespace).
+The type hierarchy is fixed.
+
+* `TERM` -- for an unknown sort
+* `TERM<S>` -- with sort `S` (e.g. int, locset)
+
+## Special Variables
+
+During the design of our scripting language we arrived at a point, 
+in which we need access to configuration options of the underlying 
+theorem prover. We decided to implement an access to these options via variables. 
+The variable access has advantages over built-in commands. The main advantage is that 
+you can do conditions other these options.
+ 
+Here we give a list of the current special variables 
+
+### Interpreter options
+
+* `__MAX_ITERATIONS_REPEAT : int`
+
+    Sets the the upper limit for iterations in repeat loops. Default value is really high. 
+
+* `__STRICT_MODE : bool` 
+
+    Defines if the interpreter is in strict or relax mode. 
+    
+    In strict mode the interpreter throws an exception in following cases:
+    
+    * access to undeclared or unassigned variable
+    * application of non-applicable rule
+    
+    In non-strict mode these errors are ignored&mdash;a warning is given on the console. 
+    
+### KeY configuration
+
+* `__KEY_AUTO_MAX_STEPS : int`
+
+    Should be a positive number and is the limit for rule application in automatic proof searchs.
+    
+* `__KEY_MATH`
\ No newline at end of file

website/mkdocs.yml

@@ -9,8 +9,16 @@ site_author: Alexander Weigl <weigl@kit.edu>
 theme_dir: kit_theme
 
 markdown_extensions:
+  - fenced_code
+  - codehilite
+  - footnotes
   - smarty
   - toc:
       permalink: True
       separator: "_"
   - sane_lists
+  - mdx_math:
+      enable_dollar_delimiter: True #for use of inline $..$
+
+extra_javascript: ['https://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS_HTML']
+