First version for applying rule after interpreting script

src/main/antlr4/edu/kit/formal/proofscriptparser/ScriptLanguage.g4

@@ -205,4 +205,4 @@ EXE_MARKER: '\u2316' -> channel(HIDDEN);
 
 DIGITS : DIGIT+ ;
 fragment DIGIT : [0-9] ;
-ID : [a-zA-Z] ([_a-zA-Z0-9] | '.' | '\\' | '[]')* ;
+ID : [a-zA-Z] ([_a-zA-Z0-9] | '.' | '\\' | '[]' | '-')* ;

src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java

@@ -230,14 +230,13 @@ public class DebuggerMainWindowController implements Initializable {
     @FXML
     public void executeScriptFromCursor() {
         InterpreterBuilder ib = FACADE.buildInterpreter();
-//        ib.inheritState(interpreterService.interpreterProperty().get());
-///*
-//        LineMapping lm = new LineMapping(scriptArea.getText());
-//        int line = lm.getLine(scriptArea.getCaretPosition());
-//        int inLine = lm.getCharInLine(scriptArea.getCaretPosition());
-//*/
-//        ib.ignoreLinesUntil(scriptController.getSelectedScriptArea().getCaretPosition());
-//        executeScript(ib, true);
+        //  ib.inheritState(interpreterService.interpreterProperty().get());
+        /*LineMapping lm = new LineMapping(scriptArea.getText());
+        int line = lm.getLine(scriptArea.getCaretPosition());
+        int inLine = lm.getCharInLine(scriptArea.getCaretPosition());
+
+        ib.ignoreLinesUntil(scriptController.getSelectedScriptArea().getCaretPosition());
+        executeScript(ib, true);*/
     }
 
     @FXML
@@ -271,6 +270,7 @@ public class DebuggerMainWindowController implements Initializable {
         }
     }
 
+
     //region Actions: Menu
     @FXML
     public void closeProgram() {

src/main/java/edu/kit/formal/gui/controller/Events.java

@@ -4,6 +4,7 @@ import com.google.common.eventbus.EventBus;
 import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.rule.TacletApp;
 import edu.kit.formal.gui.controls.ScriptArea;
+import edu.kit.formal.proofscriptparser.ast.CallStatement;
 import lombok.Data;
 import lombok.RequiredArgsConstructor;
 
@@ -40,4 +41,11 @@ public class Events {
         private final TacletApp app;
         private final PosInOccurrence pio;
     }
+
+    @Data
+    @RequiredArgsConstructor
+    public static class ScriptModificationEvent {
+        private final int line;
+        private final CallStatement cs;
+    }
 }

src/main/java/edu/kit/formal/gui/controls/ScriptArea.java

@@ -9,7 +9,7 @@ import edu.kit.formal.gui.model.Breakpoint;
 import edu.kit.formal.gui.model.MainScriptIdentifier;
 import edu.kit.formal.proofscriptparser.Facade;
 import edu.kit.formal.proofscriptparser.ScriptLanguageLexer;
-import edu.kit.formal.proofscriptparser.ast.ProofScript;
+import edu.kit.formal.proofscriptparser.ast.*;
 import edu.kit.formal.proofscriptparser.lint.LintProblem;
 import edu.kit.formal.proofscriptparser.lint.LinterStrategy;
 import javafx.beans.InvalidationListener;
@@ -399,17 +399,31 @@ public class ScriptArea extends CodeArea {
 
     @Subscribe
     public void handle(Events.TacletApplicationEvent tap) {
-
+        LOGGER.debug("ScriptArea.handleTacletApplication");
         String tapName = tap.getApp().taclet().displayName();
 
         SequentFormula seqForm = tap.getPio().sequentFormula();
+        //transofrm term to parsable string representation
+        String term = Utils.toPrettyTerm(seqForm.formula());
+
 
-        System.out.println(tap.getPio().sequentFormula());
-        //String on = tap.getApp().ifFormulaInstantiations().toString();
         String text = getText();
-        System.out.println(text);
+
+        //set new Command on position of execution marker
         int posExecMarker = this.getExecutionMarkerPosition();
-        setText(text.substring(0, posExecMarker) + "\n" + tapName + " on=\"" + seqForm + "\";\n" + text.substring(posExecMarker + 1));
+        setText(text.substring(0, posExecMarker) + "\n" + tapName + " formula=`" + term + "`;\n" + text.substring(posExecMarker + 1));
+
+        LineMapping lm = new LineMapping(text);
+        int line = lm.getLine(getCaretPosition());
+        //System.out.println(line);
+
+        setDirty(true);
+
+        //create Call Statement
+        Parameters params = new Parameters();
+        params.put(new Variable("formula"), new TermLiteral(term));
+        CallStatement call = new CallStatement(tapName, params);
+        Events.fire(new Events.ScriptModificationEvent(posExecMarker, call));
         Events.unregister(this);
         //this.getMainScript().getScriptArea().insertText(this.getExecutionMarkerPosition(), tapName+" "+on+ ";");
 

src/main/java/edu/kit/formal/gui/controls/TacletContextMenu.java

@@ -317,6 +317,7 @@ public class TacletContextMenu extends ContextMenu {
                 pos.getPosInOccurrence());*/
 
         //System.out.println("event = [" + event + "]");
+
         Events.fire(new Events.TacletApplicationEvent(event, pos.getPosInOccurrence()));
     }
 

src/main/java/edu/kit/formal/gui/controls/Utils.java

 package edu.kit.formal.gui.controls;
 
+import de.uka.ilkd.key.logic.Term;
+import de.uka.ilkd.key.logic.op.Equality;
 import de.uka.ilkd.key.logic.op.IProgramMethod;
+import de.uka.ilkd.key.logic.op.Junctor;
+import de.uka.ilkd.key.logic.op.Operator;
 import de.uka.ilkd.key.pp.ProgramPrinter;
 import de.uka.ilkd.key.speclang.Contract;
 import edu.kit.formal.interpreter.data.GoalNode;
@@ -231,4 +235,44 @@ public class Utils {
     public static <T> String reprKeyData(GoalNode<KeyData> t) {
         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) {
+        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)) + ")");
+        } else {
+            if (op.equals(Junctor.AND)) {
+                sb.append("(" + toPrettyTerm(formula.sub(0)) + ") && (" + toPrettyTerm(formula.sub(1)) + ")");
+            } else {
+                if (op.equals(Junctor.OR)) {
+                    sb.append("(" + toPrettyTerm(formula.sub(0)) + ") || (" + toPrettyTerm(formula.sub(1)) + ")");
+                } else {
+                    if (op.equals(Equality.EQV)) {
+                        sb.append("(" + toPrettyTerm(formula.sub(0)) + ") <-> (" + toPrettyTerm(formula.sub(1)) + ")");
+                    } else {
+                        if (op.equals(Equality.EQUALS)) {
+                            sb.append("(" + toPrettyTerm(formula.sub(0)) + ") == (" + toPrettyTerm(formula.sub(1)) + ")");
+                        } else {
+                            if (op.equals(Junctor.NOT)) {
+                                sb.append("(!" + toPrettyTerm(formula.sub(0)) + ")");
+                            } else {
+                                sb.append(formula.toString());
+                            }
+                        }
+                    }
+                }
+            }
+        }
+
+        return sb.toString();
+    }
 }

src/main/java/edu/kit/formal/interpreter/graphs/ProofTreeController.java

 package edu.kit.formal.interpreter.graphs;
 
+import com.google.common.eventbus.Subscribe;
+import edu.kit.formal.gui.controller.Events;
 import edu.kit.formal.gui.controller.PuppetMaster;
 import edu.kit.formal.interpreter.Interpreter;
 import edu.kit.formal.interpreter.InterpretingService;
@@ -213,6 +215,7 @@ public class ProofTreeController {
      * @param debugMode
      */
     public void executeScript(boolean debugMode) {
+        Events.register(this);
         blocker.deinstall();
         blocker.install(currentInterpreter);
         if (!debugMode) {
@@ -255,6 +258,16 @@ public class ProofTreeController {
                 this.statePointer.getScriptstmt().getStartPosition());
     }
 
+    @Subscribe
+    public void handle(Events.ScriptModificationEvent mod) {
+        LOGGER.debug("ProofTreeController.handleScriptModificationEvent");
+        System.out.println("Handling ScriptCommand");
+        currentInterpreter.visit(mod.getCs());
+        this.setCurrentSelectedGoal(currentInterpreter.getSelectedNode());
+        this.setCurrentGoals(currentInterpreter.getCurrentGoals());
+    }
+
+
     /**************************************************************************************************************
      *
      *                                              Getter and Setter

src/test/resources/edu/kit/formal/interpreter/paperExample/test2.kps

+script prove_transitive(){
+ symbex;
+ simp-heap;
+ simp-upd;
+ cases{
+   case match
+    `seqPerm(Res0Copy, Arr),
+    seqPerm(Res0Sort, Res0Copy),
+    seqPerm(Res1Copy0, Res0Sort),
+    seqPerm(Res2Copy1, Res0Sort) ==>
+        seqPerm(Res2Copy1, Arr)` using [ ?Res0Copy: Seq, ?Arr: Seq,?Res0Sort: Seq, ?Res1Copy0: Seq, ?Res2Copy1: Seq, ?Res0Sort: Seq  ]:
+   {
+        assume `self==null`;
+   }
+   case match
+    `seqPerm(Res0Copy, Arr),
+    seqPerm(Res0Sort, Res0Copy),
+    seqPerm(Res1Copy0, Res0Sort) ==>
+             seqPerm(Res1Copy0, Arr)`  using [ ?Res0Copy: Seq, ?Arr: Seq,?Res0Sort: Seq, ?Res1Copy0: Seq, ?Res0Sort: Seq ]:
+    {
+        assume `self==null`;
+     }
+     default:{
+        assume `self != null`;
+    }
+  }
+}
\ No newline at end of file