Merge branch 'master' into '55-add-variable-view-to-goaloptionsview'

Reverse Merge Request

See merge request !25

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

@@ -12,7 +12,9 @@ import edu.kit.iti.formal.psdbg.parser.Visitor;
 import edu.kit.iti.formal.psdbg.parser.ast.*;
 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 lombok.Getter;
 import lombok.Setter;
 import org.antlr.v4.runtime.ParserRuleContext;
@@ -209,6 +211,35 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
         return null;
     }
 
+    @Override
+    public Object visit(DerivableCase derivableCase) {
+        Expression pattern = derivableCase.getExpression();
+        State<T> currentStateToMatch = peekState();
+        GoalNode<T> selectedGoal = currentStateToMatch.getSelectedGoalNode();
+        assert currentStateToMatch.getGoals().contains(selectedGoal);
+        Value v = evaluate(pattern);
+        if(v.getType() == TypeFacade.ANY_TERM){
+            GoalNode<T> newGoalNode= matcherApi.isDerivable(selectedGoal, v);
+            try {
+                enterScope(derivableCase);
+
+                if (newGoalNode != null) {
+                    currentStateToMatch.getGoals().remove(selectedGoal);
+                    currentStateToMatch.getGoals().add(newGoalNode);
+                    currentStateToMatch.setSelectedGoalNode(newGoalNode);
+                    executeBody(derivableCase.getBody(), newGoalNode, new VariableAssignment());
+                    return true;
+                } else {
+                    return false;
+                }
+            } finally {
+                exitScope(derivableCase);
+            }
+        } else {
+            throw new RuntimeException("A derivable expression must contain a term. Received a"+v.getType());
+        }
+    }
+
     /**
      * @param casesStatement
      * @return
@@ -303,7 +334,6 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
         GoalNode<T> selectedGoal = currentStateToMatch.getSelectedGoalNode();
         assert currentStateToMatch.getGoals().contains(selectedGoal);
         VariableAssignment va = evaluateMatchInGoal(matchExpression, selectedGoal);
-
         try {
             enterScope(guardedCaseStatement);
             if (va != null) {

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

@@ -16,7 +16,7 @@ import java.util.Collections;
 import java.util.List;
 
 /**
- * Evaluator specially for Expressions in a case "declaration".
+ * Evaluator especially for Expressions in a case "declaration".
  * Created by sarah on 5/22/17.
  */
 public class MatchEvaluator extends DefaultASTVisitor<List<VariableAssignment>> implements ScopeObservable {
@@ -190,9 +190,13 @@ public class MatchEvaluator extends DefaultASTVisitor<List<VariableAssignment>>
     public List<VariableAssignment> visit(UnaryExpression e) {
         Operator op = e.getOperator();
         Expression expr = e.getExpression();
-        Value exValue = (Value) expr.accept(this);
-        Value ret = op.evaluate(exValue);
-        return null;
+        List<VariableAssignment> exValue = (List<VariableAssignment>) expr.accept(this);
+        if(exValue.isEmpty()){
+            return transformTruthValue(Value.TRUE);
+        }else{
+            return transformTruthValue(Value.FALSE);
+
+        }
     }
 
 

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

@@ -3,6 +3,7 @@ package edu.kit.iti.formal.psdbg.interpreter;
 import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
 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.data.Value;
 
 import java.util.List;
 
@@ -27,4 +28,6 @@ public interface MatcherApi<T> {
      */
     List<VariableAssignment> matchSeq(GoalNode<T> currentState, String pattern);
 
+    GoalNode<T> isDerivable(GoalNode<T> currentState, Value v);
+
 }

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

@@ -54,6 +54,11 @@ public class GoalNode<T> {
         this.id = id;
     }
 
+    private GoalNode(int id, GoalNode<T> parent, VariableAssignment ass, T data, boolean isClosed) {
+        this(parent, ass, data, isClosed);
+        this.id = id;
+    }
+
     private GoalNode(int id, T data, boolean isClosed) {
         this(data);
         this.isClosed = isClosed;
@@ -129,7 +134,8 @@ public class GoalNode<T> {
      */
     public GoalNode<T> deepCopy() {
         if (parent != null) {
-            return new GoalNode<T>(id, parent.deepCopy(), data, isClosed);
+            VariableAssignment deepCopy = parent.assignments.deepCopy();
+            return new GoalNode<T>(id, parent.deepCopy(), deepCopy, data, isClosed);
         } else {
             return new GoalNode<T>(id, data, isClosed);
         }

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

@@ -49,6 +49,13 @@ public class PseudoMatcher implements MatcherApi<String> {
         }
         return Collections.singletonList(va);
     }
+
+    @Override
+    public GoalNode<String> isDerivable(GoalNode<String> currentState, Value v) {
+        return null;
+    }
+
+
 }
 
    
\ No newline at end of file

ui/src/main/java/edu/kit/iti/formal/psdbg/examples/Example.java

@@ -4,6 +4,7 @@ import edu.kit.iti.formal.psdbg.gui.controller.DebuggerMain;
 import edu.kit.iti.formal.psdbg.gui.model.MainScriptIdentifier;
 import lombok.*;
 import org.apache.commons.io.FileUtils;
+import org.apache.commons.io.FilenameUtils;
 import org.apache.commons.io.IOUtils;
 
 import java.io.File;
@@ -24,7 +25,12 @@ public abstract class Example {
     protected MainScriptIdentifier mainScriptIdentifier;
 
     public static File newTempFile(URL url, String filename) throws IOException {
-        File f = new File(FileUtils.getTempDirectoryPath(), filename);
+
+
+        File psdbg = new File(FileUtils.getTempDirectoryPath(), "psdbg");
+        File examplefolder = new File(psdbg.getPath(), FilenameUtils.removeExtension(filename));
+
+        File f = new File(examplefolder, filename);
         FileUtils.copyURLToFile(url, f);
         return f;
     }

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

@@ -807,6 +807,7 @@ public class DebuggerMain implements Initializable {
         if (javaFile != null) {
             model.setJavaFile(javaFile);
             model.setInitialDirectory(javaFile.getParentFile());
+            contractLoaderService.reset();
             contractLoaderService.start();
         }
     }
@@ -1166,7 +1167,6 @@ public class DebuggerMain implements Initializable {
         } else {
             throw new RuntimeException("Something went wrong when reloading");
         }
-
     }
 
   /*  public void handle(Events.TacletApplicationEvent tap){
@@ -1408,7 +1408,31 @@ public class DebuggerMain implements Initializable {
         protected void succeeded() {
             statusBar.publishMessage("Contract loaded");
             List<Contract> contracts = getValue();
-            ContractChooser cc = new ContractChooser(FACADE.getService(), contracts);
+
+            /*
+            String javaFile = model.getJavaFile().getName();
+
+            List<Contract> filteredContracts = new ArrayList<>();
+            for (Contract contract : contracts) {
+                String contractFile = contract.getKJT().getFullName();
+                if (javaFile == contractFile) {
+                    filteredContracts.add(contract);
+                }
+            }
+
+            if (filteredContracts.size() == 0) {
+               Utils.showInfoDialog("No loadable contract", "No loadable contract",
+                       "There's no loadable contract for the chosen java file.");
+                return;
+            }
+            */
+
+            ContractChooser cc = null;
+            try {
+                cc = new ContractChooser(FACADE.getService(), FACADE.getContractsForJavaFile(model.getJavaFile()));
+            } catch (ProblemLoaderException e) {
+                e.printStackTrace();
+            }
 
             cc.showAndWait().ifPresent(result -> {
                 model.setChosenContract(result);

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

 package edu.kit.iti.formal.psdbg.gui.controller;
 
 import com.google.common.eventbus.Subscribe;
+import de.uka.ilkd.key.api.KeYApi;
 import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
 import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.Sequent;
 import de.uka.ilkd.key.logic.SequentFormula;
-import de.uka.ilkd.key.macros.ProofMacro;
 import de.uka.ilkd.key.macros.scripts.*;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Node;
@@ -26,7 +26,7 @@ import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
 import edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerFramework;
 import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
 import edu.kit.iti.formal.psdbg.interpreter.exceptions.ScriptCommandNotApplicableException;
-import edu.kit.iti.formal.psdbg.interpreter.funchdl.MacroCommandHandler;
+import edu.kit.iti.formal.psdbg.interpreter.funchdl.ProofScriptCommandBuilder;
 import edu.kit.iti.formal.psdbg.parser.PrettyPrinter;
 import edu.kit.iti.formal.psdbg.parser.ast.*;
 import edu.kit.iti.formal.psdbg.parser.data.Value;
@@ -43,6 +43,7 @@ import org.key_project.util.collection.ImmutableList;
 import recoder.util.Debug;
 
 import javax.annotation.Nullable;
+import java.lang.reflect.Method;
 import java.math.BigInteger;
 import java.util.*;
 import java.util.stream.Collectors;
@@ -66,8 +67,8 @@ public class InteractiveModeController {
     private PTreeNode<KeyData> nodeAtInteractionStart;
 
     //needed for Undo-Operation
-    private ArrayList<CallStatement> savepointsstatement;
-    private ArrayList<Node> savepointslist;
+    private ArrayList<CallStatement> laststatementlist;
+    private ArrayList<Node> lastnodeslist;
 
     private Proof currentProof;
     private Services keYServices;
@@ -99,8 +100,8 @@ public class InteractiveModeController {
             gcs.setBody(v);
             casesStatement.getCases().add(gcs);
         });
-        savepointslist = new ArrayList<>();
-        savepointsstatement = new ArrayList<>();
+        lastnodeslist = new ArrayList<>();
+        laststatementlist = new ArrayList<>();
         nodeAtInteractionStart = debuggerFramework.getStatePointer();
 
     }
@@ -110,13 +111,14 @@ public class InteractiveModeController {
      * Undo the application of the last rule
      */
     public void undo(javafx.event.ActionEvent actionEvent) {
-        if (savepointslist.isEmpty()) {
+        if (lastnodeslist.isEmpty()) {
             Debug.log("Kein vorheriger Zustand.");
             return;
         }
 
-        val pruneNode = savepointslist.get(savepointslist.size() - 1);
-        savepointslist.remove(pruneNode);
+        val pruneNode = lastnodeslist.get(lastnodeslist.size() - 1);
+        lastnodeslist.remove(pruneNode);
+
         ImmutableList<Goal> goalsbeforePrune = currentProof.getSubtreeGoals(pruneNode);
 
         currentProof.pruneProof(pruneNode);
@@ -127,19 +129,55 @@ public class InteractiveModeController {
                 .filter(keyDataGoalNode -> goalsbeforePrune.contains(keyDataGoalNode.getData().getGoal()))
                 .collect(Collectors.toList());
 
+        if(prunedChildren.size() == 0) {
+            //TODO: add Utils.showInfoD
+            return;
+        }
         KeyData kd = prunedChildren.get(0).getData();
         goals.removeAll(prunedChildren);
+
+
+        //Set selected goal after prune
+
         GoalNode<KeyData> lastGoalNode = null;
-        for (Goal newGoalNode : goalsafterPrune) {
-            KeyData kdn = new KeyData(kd, newGoalNode.node());
+        KeyData kdn;
+        if (lastnodeslist.size() == 0) {
+            kdn = new KeyData(kd, goalsafterPrune.get(0).node());
             goals.add(
-                    lastGoalNode = new GoalNode<>(prunedChildren.get(0).getParent().getParent(), kdn, kdn.getNode().isClosed()));
+                    lastGoalNode = new GoalNode<>(prunedChildren.get(0).getParent(), kdn, kdn.getNode().isClosed()));
+        } else {
+            for (Goal newGoalNode : goalsafterPrune) {
+                kdn = new KeyData(kd, newGoalNode.node());
+                goals.add(
+                        lastGoalNode = new GoalNode<>(prunedChildren.get(0).getParent().getParent(), kdn, kdn.getNode().isClosed()));
+            }
         }
 
         model.setSelectedGoalNodeToShow(lastGoalNode);
 
-        val pruneStatement = savepointsstatement.get(savepointsstatement.size() - 1);
-        cases.forEach((k, v) -> v.remove(pruneStatement));
+
+        val pruneStatement = laststatementlist.get(laststatementlist.size() - 1);
+        laststatementlist.remove(laststatementlist.size() - 1);
+
+        //TODO: buggy cuz allstatements of same node removed
+
+        //remove statement from cases / script
+        Statements statements = (cases.get(pruneNode.parent()) == null)? cases.get(pruneNode) : cases.get(pruneNode.parent());
+        int i = statements.size()-1;
+
+        while(statements.get(i) != pruneStatement && i >= 0) {
+            statements.remove(i);
+            i--;
+        }
+        statements.remove(i);
+
+
+        /*
+        cases.forEach((k, v) -> {
+                v.remove(pruneStatement);
+
+        });
+        */
 
         String c = getCasesAsString();
         scriptArea.setText("" +
@@ -260,11 +298,39 @@ public class InteractiveModeController {
         }
     }
 
+    @Subscribe
+    public void handle(Events.CommandApplicationEvent map) {
+
+        LOGGER.debug("Handling {}", map);
+        Goal g = map.getCurrentGoal();
+
+        Parameters callp = new Parameters();
+        CallStatement call = new CallStatement(map.getCommandName().getName(), callp);
+        try {
+            applyRuleHelper(call, g, Type.SCRIPT_COMMAND);
+            String c = getCasesAsString();
+            scriptArea.setText("" +
+                    "//Preview \n" + c);
+
+
+        } catch (ScriptCommandNotApplicableException e) {
+            StringBuilder sb = new StringBuilder("The script command ");
+            sb.append(call.getCommand()).append(" was not applicable.");
+            System.out.println("e = " + e);
+            //sb.append("\nSequent Formula: formula=").append(sfTerm);
+            //sb.append("\nOn Sub Term: on=").append(onTerm);
+
+            Utils.showWarningDialog("Proof Command was not applicable",
+                    "Proof Command was not applicable.",
+                    sb.toString(), e);
+        }
+    }
+
 
     private void applyRuleHelper(CallStatement call, Goal g, Type t) throws ScriptCommandNotApplicableException {
 
-        savepointslist.add(g.node());
-        savepointsstatement.add(call);
+        lastnodeslist.add(g.node());
+        laststatementlist.add(call);
 
         ObservableList<GoalNode<KeyData>> goals = model.getGoals();
         GoalNode<KeyData> expandedNode;
@@ -312,10 +378,11 @@ public class InteractiveModeController {
                     postStateHandler(call, g, goals, expandedNode, kd);
                     break;
                 case SCRIPT_COMMAND:
-                    ScriptCommand.Parameters ccS = new ScriptCommand.Parameters();
-                    ScriptCommand cS = new ScriptCommand();
-                    ccS = valueInjector.inject(cS, ccS, map);
-                    cS.execute(uiControl, ccS, estate);
+                    ProofScriptCommandBuilder psb = new ProofScriptCommandBuilder(KeYApi.getScriptCommandApi().getScriptCommands());
+                    ProofScriptCommand ps = psb.getCommands().get(call.getCommand());
+
+                    Object temp = valueInjector.inject(ps, getParameterInstance(ps), map);
+                    ps.execute(uiControl, temp, estate);
                     postStateHandler(call, g, goals, expandedNode, kd);
                     break;
                 default:
@@ -335,6 +402,12 @@ public class InteractiveModeController {
 
     }
 
+    private <T> T getParameterInstance(ProofScriptCommand c) throws NoSuchMethodException, IllegalAccessException,
+            InstantiationException {
+        Method method = c.getClass().getMethod("evaluateArguments", EngineState.class, Map.class);
+        Class rtclazz = method.getReturnType();
+        return (T) rtclazz.newInstance();
+    }
     private void postStateHandler(CallStatement call, Goal g, ObservableList<GoalNode<KeyData>> goals, GoalNode<KeyData> expandedNode, KeyData kd) {
         ImmutableList<Goal> ngoals = g.proof().getSubtreeGoals(expandedNode.getData().getNode());
 
@@ -391,8 +464,8 @@ public class InteractiveModeController {
     }
 /*
     private void applyRule(CallStatement call, Goal g) throws ScriptCommandNotApplicableException {
-        savepointslist.add(g.node());
-        savepointsstatement.add(call);
+        lastnodeslist.add(g.node());
+        laststatementlist.add(call);
 
         ObservableList<GoalNode<KeyData>> goals = model.getGoals();
         GoalNode<KeyData> expandedNode;

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

@@ -66,9 +66,8 @@ public class ScriptExecutionController {
                 mainCtrl.FACADE.reload(mainCtrl.getModel().getKeyFile());
             } catch (ProofInputException | ProblemLoaderException e) {
                 LOGGER.error(e);
-                Utils.showExceptionDialog("Loading Error", "Could not clear Environment", "There was an error when clearing old environment",
-                        e
-                );
+
+                // Utils.showExceptionDialog("Loading Error", "Could not clear Environment", "There was an error when clearing old environment", e  );
             }
         }
 

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

@@ -10,8 +10,10 @@ import edu.kit.iti.formal.psdbg.gui.actions.acomplete.Suggestion;
 import edu.kit.iti.formal.psdbg.gui.actions.inline.InlineActionSupplier;
 import edu.kit.iti.formal.psdbg.gui.controller.Events;
 import edu.kit.iti.formal.psdbg.gui.model.MainScriptIdentifier;
+import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
 import edu.kit.iti.formal.psdbg.interpreter.data.SavePoint;
 import edu.kit.iti.formal.psdbg.interpreter.dbg.Breakpoint;
+import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
 import edu.kit.iti.formal.psdbg.lint.LintProblem;
 import edu.kit.iti.formal.psdbg.lint.LinterStrategy;
 import edu.kit.iti.formal.psdbg.parser.Facade;
@@ -89,7 +91,6 @@ import static org.fxmisc.wellbehaved.event.InputMap.*;
 public class ScriptArea extends BorderPane {
     public static final Logger LOGGER = LogManager.getLogger(ScriptArea.class);
     public static final Logger CONSOLE_LOGGER = LogManager.getLogger(ScriptArea.class);
-
     public static final String EXECUTION_MARKER = "\u2316";
 
     public static final FileReloadingService FILE_RELOADING_SERVICE = new FileReloadingService();
@@ -489,10 +490,12 @@ public class ScriptArea extends BorderPane {
     }
 
 
+    @Deprecated
     private boolean hasExecutionMarker() {
         return getText().contains(EXECUTION_MARKER);
     }
 
+    @Deprecated
     public int getExecutionMarkerPosition() {
         return getText().lastIndexOf(EXECUTION_MARKER);
     }
@@ -608,11 +611,13 @@ public class ScriptArea extends BorderPane {
         return dirty;
     }
 
+    @Deprecated
     public void removeExecutionMarker() {
         setText(getTextWithoutMarker());
         //Events.unregister(this);
     }
 
+    @Deprecated
     private String getTextWithoutMarker() {
         return getText().replace("" + EXECUTION_MARKER, "");
     }
@@ -622,6 +627,7 @@ public class ScriptArea extends BorderPane {
      *
      * @param pos
      */
+    @Deprecated
     public void insertExecutionMarker(int pos) {
         LOGGER.debug("ScriptArea.insertExecutionMarker");
         Events.register(this);
@@ -992,6 +998,7 @@ public class ScriptArea extends BorderPane {
             }*/
         }
 
+        @Deprecated
         public void setExecutionMarker(ActionEvent event) {
             LOGGER.debug("ScriptAreaContextMenu.setExecutionMarker");
             int pos = codeArea.getCaretPosition();

ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps

+script empty(){
+
+}
+
+script full(){
+  impRight;
+  impRight;
+  impLeft;
+  cases {
+	case derivable `p`:
+   }
+}
+
+
 script full(){
   impRight;
   impRight;

ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/ScriptAreaContextMenu.fxml

@@ -10,7 +10,8 @@
     <MenuItem text="Show post mortem" onAction="#showPostMortem"/>
     <SeparatorMenuItem/>
     <MenuItem text="Set Main Script" onAction="#setMainScript"/>
-    <MenuItem text="Set Execution Marker" onAction="#setExecutionMarker" accelerator="Ctrl+m"/>
+    <!--<MenuItem text="Set Execution Marker" onAction="#setExecutionMarker" accelerator="Ctrl+m"/>
+    -->
 </items>
 
 </fx:root>