diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/MacroCommandHandler.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/MacroCommandHandler.java index 0efcb2b767036ef18a6bfeee3348ac088aabea84..6706c651814bfde30ab60a6aacb6d76acc6203de 100644 --- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/MacroCommandHandler.java +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/MacroCommandHandler.java @@ -1,16 +1,20 @@ package edu.kit.iti.formal.psdbg.interpreter.funchdl; +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.macros.ProofMacro; +import de.uka.ilkd.key.macros.ProofMacroFinishedInfo; +import de.uka.ilkd.key.proof.Goal; import edu.kit.iti.formal.psdbg.interpreter.Interpreter; -import edu.kit.iti.formal.psdbg.parser.ast.CallStatement; -import edu.kit.iti.formal.psdbg.parser.ast.Parameters; -import edu.kit.iti.formal.psdbg.parser.ast.StringLiteral; -import edu.kit.iti.formal.psdbg.parser.ast.Variable; -import edu.kit.iti.formal.psdbg.parser.data.Value; +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.data.VariableAssignment; -import edu.kit.iti.formal.psdbg.parser.types.SimpleType; +import edu.kit.iti.formal.psdbg.parser.ast.CallStatement; import lombok.Getter; import lombok.RequiredArgsConstructor; +import org.key_project.util.collection.ImmutableList; import java.util.Collection; import java.util.HashMap; @@ -21,8 +25,9 @@ import java.util.Map; * @version 1 (21.05.17) */ @RequiredArgsConstructor -public class MacroCommandHandler implements CommandHandler { - @Getter private final Map macros; +public class MacroCommandHandler implements CommandHandler { + @Getter + private final Map macros; public MacroCommandHandler() { macros = new HashMap<>(); @@ -40,20 +45,35 @@ public class MacroCommandHandler implements CommandHandler { } @Override - public void evaluate(Interpreter interpreter, + public void evaluate(Interpreter interpreter, CallStatement call, VariableAssignment params) { //ProofMacro m = macros.get(call.getCommand()); - Parameters p = new Parameters(); - p.put(new Variable("#2"), new StringLiteral(call.getCommand())); - CallStatement macroCall = new CallStatement("macro", p); - macroCall.setRuleContext(call.getRuleContext()); - VariableAssignment newParam = new VariableAssignment(null); - newParam.declare("#2", SimpleType.STRING); - newParam.assign("#2", Value.from(call.getCommand())); - //macro proofscript command - interpreter.getFunctionLookup().callCommand(interpreter, macroCall, newParam); - - //TODO change MacroCommand.Parameters to public + ProofMacro macro = KeYApi.getMacroApi().getMacro(call.getCommand()); + ProofMacroFinishedInfo info = ProofMacroFinishedInfo.getDefaultInfo(macro, + interpreter.getCurrentState().getSelectedGoalNode().getData().getProof()); + + State state = interpreter.getCurrentState(); + GoalNode expandedNode = state.getSelectedGoalNode(); + + + try { + //uiControl.taskStarted(new DefaultTaskStartedInfo(TaskStartedInfo.TaskKind.Macro, macro.getName(), 0)); + synchronized (macro) { + AbstractUserInterfaceControl uiControl = new DefaultUserInterfaceControl(); + info = macro.applyTo(uiControl, expandedNode.getData().getNode(), null, uiControl); + ImmutableList ngoals = expandedNode.getData().getProof().getSubtreeGoals(expandedNode.getData().getNode()); + + state.getGoals().remove(expandedNode); + for (Goal g : ngoals) { + KeyData kdn = new KeyData(expandedNode.getData(), g.node()); + state.getGoals().add(new GoalNode<>(expandedNode, kdn, kdn.isClosedNode())); + } + } + } catch (InterruptedException e) { + e.printStackTrace(); + } catch (Exception e) { + e.printStackTrace(); + } } } diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/WelcomePane.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/WelcomePane.java index 62e8a2e47212172d469eeeaad4ae60d7315eb004..6e7968938285eef41d4b37cbaab638915fe987eb 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/WelcomePane.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/WelcomePane.java @@ -48,7 +48,9 @@ public class WelcomePane extends AnchorPane { proofScriptDebugger.getWelcomePaneDock().close(); proofScriptDebugger.showActiveInspector(null); Examples.loadExamples().forEach(example -> { - if (example.getName().equals("Transitive Permutation")) + // if (example.getName().equals("Transitive Permutation")) + if (example.getName().equals("Simple Java Example")) + example.open(proofScriptDebugger); }); diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/simple/script.kps b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/simple/script.kps index 77e45a6c02d276621d8bb0aa52c0d02d460ac276..9671b63e8faf58984eb445eca03ace38b71b67d6 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/simple/script.kps +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/simple/script.kps @@ -2,7 +2,7 @@ script t(){ symbex; cases{ case match `?X = 0 ==>`: - eqSymm on=`?X=0`[?X/?X]; + eqSymm on=`?X=0`[]; } diff --git a/website/docs/img/ruleApp.png b/website/docs/img/ruleApp.png new file mode 100644 index 0000000000000000000000000000000000000000..a8a54fce650c7bd9e919dea5f9074c7bf4ba9cd3 Binary files /dev/null and b/website/docs/img/ruleApp.png differ diff --git a/website/docs/img/simpleJava2.png b/website/docs/img/simpleJava2.png new file mode 100644 index 0000000000000000000000000000000000000000..538e71aad496dc351255982634a1bc3b81a4bc94 Binary files /dev/null and b/website/docs/img/simpleJava2.png differ diff --git a/website/docs/img/simpleJavaGoalList.png b/website/docs/img/simpleJavaGoalList.png new file mode 100644 index 0000000000000000000000000000000000000000..c02fcb037e2f4d9c80c6c965df49cf7729b0313d Binary files /dev/null and b/website/docs/img/simpleJavaGoalList.png differ diff --git a/website/docs/img/simpleJavaPath.png b/website/docs/img/simpleJavaPath.png new file mode 100644 index 0000000000000000000000000000000000000000..f6e4ea05846148c43dd270287b3f377432286885 Binary files /dev/null and b/website/docs/img/simpleJavaPath.png differ diff --git a/website/docs/img/simpleJavaStep.png b/website/docs/img/simpleJavaStep.png new file mode 100644 index 0000000000000000000000000000000000000000..0e77c803376e25e5b94e2509750bd947dc20bb91 Binary files /dev/null and b/website/docs/img/simpleJavaStep.png differ diff --git a/website/docs/index.md b/website/docs/index.md index 8712426806a4040b80ab7c6f8de9e9ba932cbc24..c32a9a66061580afea1b38f59b49f5e05989ca07 100644 --- a/website/docs/index.md +++ b/website/docs/index.md @@ -13,7 +13,7 @@ .column>div{ float: left; width: 33%; - text-align: center; + text-align: left; } .column img { @@ -63,63 +63,44 @@ A full description of the language and debugging-concept is published at
- -

Stepping back and forth in Proof Script

+

Inspection of different parts of the proof state

-

+ The different parts of the proof state can be inspected: +
    +
  • list of open goals
    • +
  • sequent of selected open goal
    • +
  • path through program (if existing) for selected open goal
    • +
+

-
- -

Different views onto one proof state

+

Adjustable view on list of open goals

+
-
- \ No newline at end of file diff --git a/website/push.sh b/website/push.sh index a5c8e6ae90e4ed9a344de4ea2a1127d5f3753baf..3aaba8f7058dc7e4e7a6675744555e0bc987c398 100755 --- a/website/push.sh +++ b/website/push.sh @@ -2,4 +2,4 @@ mkdocs build --clean -rsync --delete -vr site/ i57adm.ira.uka.de:htdocs/grebing/psdbg/ +#rsync --delete -vr site/ i57adm.ira.uka.de:htdocs/grebing/psdbg/