Commit 8b850649 authored by Sarah Grebing's avatar Sarah Grebing

Bigfix in rule menu and first steps twoard interactive proof commands

parent 21d8894d
...@@ -1454,7 +1454,7 @@ public class DebuggerMain implements Initializable { ...@@ -1454,7 +1454,7 @@ public class DebuggerMain implements Initializable {
ptree.setProof(proof); ptree.setProof(proof);
ptree.setRoot(pnode); ptree.setRoot(pnode);
ptree.setNodeColor(pnode, "blueviolet"); ptree.setNodeColor(pnode, "blueviolet");
ptree.setDeactivateRefresh(true); ptree.setDeactivateRefresh(false);
if (stateAfterStmt.size() > 0) { if (stateAfterStmt.size() > 0) {
Set<Node> sentinels = proof.getSubtreeGoals(pnode) Set<Node> sentinels = proof.getSubtreeGoals(pnode)
...@@ -1478,6 +1478,7 @@ public class DebuggerMain implements Initializable { ...@@ -1478,6 +1478,7 @@ public class DebuggerMain implements Initializable {
ptree.expandRootToSentinels(); ptree.expandRootToSentinels();
System.out.println("ptree = " + ptree.getRoot());
DockNode node = new DockNode(ptree, "Proof Tree for Step Into: " + DockNode node = new DockNode(ptree, "Proof Tree for Step Into: " +
original.getStatement().accept(new ShortCommandPrinter()) original.getStatement().accept(new ShortCommandPrinter())
); );
......
...@@ -2,6 +2,9 @@ package edu.kit.iti.formal.psdbg.gui.controller; ...@@ -2,6 +2,9 @@ package edu.kit.iti.formal.psdbg.gui.controller;
import com.google.common.eventbus.EventBus; import com.google.common.eventbus.EventBus;
import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.logic.PosInOccurrence;
import de.uka.ilkd.key.macros.ProofMacro;
import de.uka.ilkd.key.macros.scripts.ProofScriptCommand;
import de.uka.ilkd.key.macros.scripts.ScriptCommand;
import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.rule.TacletApp; import de.uka.ilkd.key.rule.TacletApp;
...@@ -59,7 +62,7 @@ public class Events { ...@@ -59,7 +62,7 @@ public class Events {
@Data @Data
@RequiredArgsConstructor @RequiredArgsConstructor
public static class CommandApplicationEvent { public static class CommandApplicationEvent {
private final String commandName; private final ProofScriptCommand commandName;
private final PosInOccurrence pio; private final PosInOccurrence pio;
private final Goal currentGoal; private final Goal currentGoal;
...@@ -153,4 +156,12 @@ public class Events { ...@@ -153,4 +156,12 @@ public class Events {
private final int position; private final int position;
} }
@Data
@RequiredArgsConstructor
public static class MacroApplicationEvent {
private final ProofMacro macroName;
private final PosInOccurrence posInOccurrence;
private final Goal goal;
}
} }
...@@ -231,6 +231,62 @@ public class InteractiveModeController { ...@@ -231,6 +231,62 @@ public class InteractiveModeController {
} }
@Subscribe
public void handle(Events.MacroApplicationEvent map) {
/* LOGGER.debug("Handling {}", map);
moreThanOneMatch = false;
String tapName = map.getApp().taclet().name().toString();
Goal g = tap.getCurrentGoal();
SequentFormula seqForm = tap.getPio().sequentFormula();
//transform term to parsable string representation
Sequent seq = g.sequent();
String sfTerm = Utils.printParsableTerm(seqForm.formula(), keYServices);
String onTerm = Utils.printParsableTerm(tap.getPio().subTerm(), keYServices);
RuleCommand.Parameters params = new RuleCommand.Parameters();
params.formula = seqForm.formula();
params.rulename = tap.getApp().taclet().name().toString();
params.on = tap.getPio().subTerm();
RuleCommandHelper rch = new RuleCommandHelper(g, params);
int occ = rch.getOccurence(tap.getApp());
Parameters callp = new Parameters();
callp.put(new Variable("formula"), TermLiteral.from(sfTerm));
callp.put(new Variable("occ"), new IntegerLiteral(BigInteger.valueOf(occ)));
callp.put(new Variable("on"), TermLiteral.from(onTerm));
VariableAssignment va = new VariableAssignment(null);
CallStatement call = new CallStatement(tapName, callp);
try {
applyRule(call, g);
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.");
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 Node findRoot(Node cur) { private Node findRoot(Node cur) {
while (cur != null) { while (cur != null) {
if (cases.keySet().contains(cur)) if (cases.keySet().contains(cur))
......
package edu.kit.iti.formal.psdbg.gui.controls; package edu.kit.iti.formal.psdbg.gui.controls;
import de.uka.ilkd.key.api.KeYApi;
import de.uka.ilkd.key.control.ProofControl; import de.uka.ilkd.key.control.ProofControl;
import de.uka.ilkd.key.gui.nodeviews.TacletMenu.TacletAppComparator; import de.uka.ilkd.key.gui.nodeviews.TacletMenu.TacletAppComparator;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.Name; import de.uka.ilkd.key.logic.Name;
import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.logic.PosInOccurrence;
import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.macros.ProofMacro;
import de.uka.ilkd.key.macros.scripts.ProofScriptCommand;
import de.uka.ilkd.key.pp.*; import de.uka.ilkd.key.pp.*;
import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.rule.*; import de.uka.ilkd.key.rule.*;
...@@ -25,7 +27,6 @@ import javafx.scene.text.Text; ...@@ -25,7 +27,6 @@ import javafx.scene.text.Text;
import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList; import org.key_project.util.collection.ImmutableSLList;
import java.io.IOException;
import java.util.*; import java.util.*;
import java.util.stream.Collectors; import java.util.stream.Collectors;
...@@ -43,7 +44,7 @@ public class TacletContextMenu extends ContextMenu { ...@@ -43,7 +44,7 @@ public class TacletContextMenu extends ContextMenu {
private static final Set<Name> CLUTTER_RULESETS = new LinkedHashSet<Name>(); private static final Set<Name> CLUTTER_RULESETS = new LinkedHashSet<Name>();
private static final Set<Name> CLUTTER_RULES = new LinkedHashSet<Name>(); private static final Set<Name> CLUTTER_RULES = new LinkedHashSet<Name>();
private static final Set<String> FILTER_SCRIPT_COMMANDS = new LinkedHashSet<>();
static { static {
CLUTTER_RULESETS.add(new Name("notHumanReadable")); CLUTTER_RULESETS.add(new Name("notHumanReadable"));
CLUTTER_RULESETS.add(new Name("obsolete")); CLUTTER_RULESETS.add(new Name("obsolete"));
...@@ -51,6 +52,18 @@ public class TacletContextMenu extends ContextMenu { ...@@ -51,6 +52,18 @@ public class TacletContextMenu extends ContextMenu {
CLUTTER_RULESETS.add(new Name("pullOutQuantifierEx")); CLUTTER_RULESETS.add(new Name("pullOutQuantifierEx"));
} }
static {
FILTER_SCRIPT_COMMANDS.add("exit");
FILTER_SCRIPT_COMMANDS.add("leave");
FILTER_SCRIPT_COMMANDS.add("javascript");
FILTER_SCRIPT_COMMANDS.add("skip");
FILTER_SCRIPT_COMMANDS.add("macro");
FILTER_SCRIPT_COMMANDS.add("rule");
FILTER_SCRIPT_COMMANDS.add("script");
}
static { static {
CLUTTER_RULES.add(new Name("cut_direct_r")); CLUTTER_RULES.add(new Name("cut_direct_r"));
CLUTTER_RULES.add(new Name("cut_direct_l")); CLUTTER_RULES.add(new Name("cut_direct_l"));
...@@ -83,6 +96,8 @@ public class TacletContextMenu extends ContextMenu { ...@@ -83,6 +96,8 @@ public class TacletContextMenu extends ContextMenu {
@FXML @FXML
private Menu insertHidden; private Menu insertHidden;
@FXML @FXML
private Menu scriptCommands;
@FXML
private MenuItem copyToClipboard; private MenuItem copyToClipboard;
@FXML @FXML
private MenuItem createAbbr; private MenuItem createAbbr;
...@@ -115,6 +130,7 @@ public class TacletContextMenu extends ContextMenu { ...@@ -115,6 +130,7 @@ public class TacletContextMenu extends ContextMenu {
occ = pos.getPosInOccurrence(); occ = pos.getPosInOccurrence();
//MediatorProofControl c = new MediatorProofControl(new DefaultAbstractMediatorUserInterfaceControlAdapter()); //MediatorProofControl c = new MediatorProofControl(new DefaultAbstractMediatorUserInterfaceControlAdapter());
ProofControl c = DebuggerMain.FACADE.getEnvironment().getUi().getProofControl(); ProofControl c = DebuggerMain.FACADE.getEnvironment().getUi().getProofControl();
c.setMinimizeInteraction(true);
final ImmutableList<BuiltInRule> builtInRules = c.getBuiltInRule(goal, occ); final ImmutableList<BuiltInRule> builtInRules = c.getBuiltInRule(goal, occ);
try { try {
...@@ -123,6 +139,9 @@ public class TacletContextMenu extends ContextMenu { ...@@ -123,6 +139,9 @@ public class TacletContextMenu extends ContextMenu {
removeRewrites(findTaclet) removeRewrites(findTaclet)
.prepend(c.getRewriteTaclet(goal, occ)), .prepend(c.getRewriteTaclet(goal, occ)),
c.getNoFindTaclet(goal), builtInRules); c.getNoFindTaclet(goal), builtInRules);
createMacroMenu(KeYApi.getScriptCommandApi().getScriptCommands(), KeYApi.getMacroApi().getMacros());
} catch (NullPointerException e) { } catch (NullPointerException e) {
createDummyMenuItem(); createDummyMenuItem();
} }
...@@ -136,6 +155,31 @@ public class TacletContextMenu extends ContextMenu { ...@@ -136,6 +155,31 @@ public class TacletContextMenu extends ContextMenu {
//proofMacroMenuController.init(occ); //proofMacroMenuController.init(occ);
} }
private void createMacroMenu(Collection<ProofScriptCommand> scriptCommandList, Collection<ProofMacro> macros) {
for(ProofMacro macro : macros){
final MenuItem item = new MenuItem(macro.getScriptCommandName());
item.setOnAction(event -> {
handleMacroCommandApplication(macro);
});
this.scriptCommands.getItems().add(item);
}
for(ProofScriptCommand com : scriptCommandList){
if(!FILTER_SCRIPT_COMMANDS.contains(com.getName())) {
final MenuItem item = new MenuItem(com.getName());
item.setOnAction(event -> {
handleCommandApplication(com);
});
this.scriptCommands.getItems().add(item);
}
}
rootMenu.getItems().add(scriptCommands);
}
/** /**
* Removes RewriteTaclet from the list. * Removes RewriteTaclet from the list.
* *
...@@ -199,16 +243,17 @@ public class TacletContextMenu extends ContextMenu { ...@@ -199,16 +243,17 @@ public class TacletContextMenu extends ContextMenu {
//compare by name //compare by name
Comparator.comparing(o -> o.taclet().name()) Comparator.comparing(o -> o.taclet().name())
); );
//findTaclets = replaceCutOccurrence(findTaclets);
List<TacletApp> toAdd = new ArrayList<>(findTaclets.size() + noFindTaclets.size()); List<TacletApp> toAdd = new ArrayList<>(findTaclets.size() + noFindTaclets.size());
toAdd.addAll(findTaclets); toAdd.addAll(findTaclets);
boolean rulesAvailable = find.size() > 0; boolean rulesAvailable = find.size() > 0;
//remove all cut rules from menu and add cut command for that //remove all cut rules from menu and add cut command for that
if (pos.isSequent()) { if (pos.isSequent()) {
rulesAvailable |= noFind.size() > 0; rulesAvailable |= noFind.size() > 0;
toAdd.addAll(noFindTaclets); toAdd.addAll(replaceCutOccurrence(noFindTaclets));
} }
...@@ -223,40 +268,39 @@ public class TacletContextMenu extends ContextMenu { ...@@ -223,40 +268,39 @@ public class TacletContextMenu extends ContextMenu {
if (rulesAvailable) { if (rulesAvailable) {
createMenuItems(toAdd); createMenuItems(toAdd);
// createCommandMenuItems();
} else { } else {
noRules.setVisible(true); noRules.setVisible(true);
} }
if (occ != null) if (occ != null)
createAbbrevSection(pos.getPosInOccurrence().subTerm()); createAbbrevSection(pos.getPosInOccurrence().subTerm());
} }
private void createCommandMenuItems() { /* private void createCommandMenuItems() {
Text t = new Text("Cut Command"); Text t = new Text("Cut Command");
MenuItem item = new MenuItem(); MenuItem item = new MenuItem();
item.setGraphic(t); item.setGraphic(t);
item.setOnAction(event -> { item.setOnAction(event -> {
handleCommandApplication("cut");
handleCommandApplication(KeYApi.getScriptCommandApi().getScriptCommands("cut"));
}); });
rootMenu.getItems().add(0, item); rootMenu.getItems().add(0, item);
} }*/
private List<TacletApp> replaceCutOccurrence(List<TacletApp> findTaclets) { private List<TacletApp> replaceCutOccurrence(List<TacletApp> findTaclets) {
boolean foundCut = false; //boolean foundCut = false;
List<TacletApp> toReturn = new ArrayList<>();
for (int i = 0; i < findTaclets.size(); i++) { for (int i = 0; i < findTaclets.size(); i++) {
TacletApp tacletApp = findTaclets.get(i); TacletApp tacletApp = findTaclets.get(i);
if(tacletApp.rule().displayName().startsWith("cut")){ if(!tacletApp.rule().displayName().startsWith("cut")){
findTaclets.remove(tacletApp); //findTaclets.remove(tacletApp);
foundCut = true; // foundCut = true;
toReturn.add(tacletApp);
} }
} }
return findTaclets; return toReturn;
// return findTaclets;
} }
private void createDummyMenuItem() { private void createDummyMenuItem() {
...@@ -381,11 +425,15 @@ public class TacletContextMenu extends ContextMenu { ...@@ -381,11 +425,15 @@ public class TacletContextMenu extends ContextMenu {
//System.out.println("event = [" + event + "]"); //System.out.println("event = [" + event + "]");
Events.fire(new Events.TacletApplicationEvent(event, pos.getPosInOccurrence(), goal)); Events.fire(new Events.TacletApplicationEvent(event, pos.getPosInOccurrence(), goal));
} }
private void handleCommandApplication(String event) { private void handleCommandApplication(ProofScriptCommand event) {
Events.fire(new Events.CommandApplicationEvent(event, pos.getPosInOccurrence(), goal)); Events.fire(new Events.CommandApplicationEvent(event, pos.getPosInOccurrence(), goal));
} }
private void handleMacroCommandApplication(ProofMacro event) {
Events.fire(new Events.MacroApplicationEvent(event, pos.getPosInOccurrence(), goal));
}
/** /**
* Handles rule application for automode. * Handles rule application for automode.
* *
......
script full(){
impRight;
impRight;
impLeft;
cases {
case match `!q ==> p`:
notLeft;
notRight;
closeAntec;
case match `q==>!p`:
auto;
}
}
\ No newline at end of file
...@@ -10,7 +10,7 @@ ...@@ -10,7 +10,7 @@
<!-- <fx:include fx:id="insertHidden" visible="false" source="InsertHiddenMenuView.fxml"/>--> <!-- <fx:include fx:id="insertHidden" visible="false" source="InsertHiddenMenuView.fxml"/>-->
<Menu fx:id="moreRules" visible="false" text="More rules"/> <Menu fx:id="moreRules" visible="false" text="More rules"/>
<Menu fx:id="scriptCommands" visible="true" text="Script Commands"/>
<!-- <SeparatorMenuItem/> --> <!-- <SeparatorMenuItem/> -->
<!-- <MenuItem mnemonicParsing="false" onAction="#handleFocussedRuleApplication" <!-- <MenuItem mnemonicParsing="false" onAction="#handleFocussedRuleApplication"
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment