Taclet apps in rule context menu

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

@@ -55,8 +55,8 @@ public class DebuggerMainWindowController implements Initializable {
     private final ProofTreeController proofTreeController = new ProofTreeController();
     private final InspectionViewsController inspectionViewsController = new InspectionViewsController();
     private final ExecutorService executorService = Executors.newFixedThreadPool(2);
-    private final KeYProofFacade facade = new KeYProofFacade();
-    private final ContractLoaderService contractLoaderService = new ContractLoaderService();
+    public static final KeYProofFacade FACADE = new KeYProofFacade();
+    public final ContractLoaderService contractLoaderService = new ContractLoaderService();
     /**
      * Property: current loaded javaFile
      */
@@ -89,7 +89,7 @@ public class DebuggerMainWindowController implements Initializable {
     /**
      * True, iff the execution is not possible
      */
-    private ObservableBooleanValue executeNotPossible = proofTreeController.executeNotPossibleProperty().or(facade.readyToExecuteProperty().not());
+    private ObservableBooleanValue executeNotPossible = proofTreeController.executeNotPossibleProperty().or(FACADE.readyToExecuteProperty().not());
 
     /**
      *
@@ -117,7 +117,6 @@ public class DebuggerMainWindowController implements Initializable {
         //statusBar.publishMessage("File: " + (newValue != null ? newValue.getAbsolutePath() : "n/a"));
 
 
-
         //Debugging
         Utils.addDebugListener(javaCode);
         Utils.addDebugListener(executeNotPossible, "executeNotPossible");
@@ -186,12 +185,12 @@ public class DebuggerMainWindowController implements Initializable {
     //region Actions: Execution
     @FXML
     public void executeScript() {
-        executeScript(facade.buildInterpreter(), false);
+        executeScript(FACADE.buildInterpreter(), false);
     }
 
     @FXML
     public void executeScriptFromCursor() {
-        InterpreterBuilder ib = facade.buildInterpreter();
+        InterpreterBuilder ib = FACADE.buildInterpreter();
 //        ib.inheritState(interpreterService.interpreterProperty().get());
 ///*
 //        LineMapping lm = new LineMapping(scriptArea.getText());
@@ -204,7 +203,7 @@ public class DebuggerMainWindowController implements Initializable {
 
     @FXML
     public void executeInDebugMode() {
-        executeScript(facade.buildInterpreter(), true);
+        executeScript(FACADE.buildInterpreter(), true);
     }
     //endregion
 
@@ -271,7 +270,7 @@ public class DebuggerMainWindowController implements Initializable {
 
     public void openScript(File scriptFile) {
         assert scriptFile != null;
-        setInitialDirectory(scriptFile.getParentFile() );
+        setInitialDirectory(scriptFile.getParentFile());
         try {
             String code = FileUtils.readFileToString(scriptFile, Charset.defaultCharset());
             ScriptArea area = scriptController.createNewTab(scriptFile);
@@ -291,10 +290,10 @@ public class DebuggerMainWindowController implements Initializable {
         if (keyFile != null) {
             setKeyFile(keyFile);
             setInitialDirectory(keyFile.getParentFile());
-            Task<Void> task = facade.loadKeyFileTask(keyFile);
+            Task<Void> task = FACADE.loadKeyFileTask(keyFile);
             task.setOnSucceeded(event -> {
                 statusBar.publishMessage("Loaded key sourceName: %s", keyFile);
-                getInspectionViewsController().getActiveInspectionViewTab().getModel().getGoals().setAll(facade.getPseudoGoals());
+                getInspectionViewsController().getActiveInspectionViewTab().getModel().getGoals().setAll(FACADE.getPseudoGoals());
             });
 
             task.setOnFailed(event -> {
@@ -335,6 +334,7 @@ public class DebuggerMainWindowController implements Initializable {
         loadJavaFile();
         showCodeDock(null);
     }
+
     /**
      * Creates a filechooser dialog
      *
@@ -385,7 +385,7 @@ public class DebuggerMainWindowController implements Initializable {
 
 
     public KeYProofFacade getFacade() {
-        return facade;
+        return FACADE;
     }
 
     //region Property
@@ -552,7 +552,7 @@ public class DebuggerMainWindowController implements Initializable {
     public class ContractLoaderService extends Service<List<Contract>> {
         @Override
         protected Task<List<Contract>> createTask() {
-            return facade.getContractsForJavaFileTask(getJavaFile());
+            return FACADE.getContractsForJavaFileTask(getJavaFile());
         }
 
         @Override
@@ -564,13 +564,13 @@ public class DebuggerMainWindowController implements Initializable {
         protected void succeeded() {
             statusBar.publishMessage("Contract loaded");
             List<Contract> contracts = getValue();
-            ContractChooser cc = new ContractChooser(facade.getService(), contracts);
+            ContractChooser cc = new ContractChooser(FACADE.getService(), contracts);
 
             cc.showAndWait().ifPresent(result -> {
                 setChosenContract(result);
                 try {
-                    facade.activateContract(result);
-                    getInspectionViewsController().getActiveInspectionViewTab().getModel().getGoals().setAll(facade.getPseudoGoals());
+                    FACADE.activateContract(result);
+                    getInspectionViewsController().getActiveInspectionViewTab().getModel().getGoals().setAll(FACADE.getPseudoGoals());
                 } catch (ProofInputException e) {
                     Utils.showExceptionDialog("", "", "", e);
                 }

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

@@ -43,7 +43,7 @@ public class InspectionView extends BorderPane {
                 (observable, oldValue, newValue) -> {
                     goalView.getSelectionModel().select(newValue);
                     if (newValue != null && newValue.getData() != null) {
-                        getSequentView().setNode(newValue.getData().getNode());
+                        getSequentView().setNode(newValue.getData().getGoal());
                         // TODO weigl: get marked lines of the program, and set it
                         model.get().highlightedJavaLinesProperty().get()
                                 .clear();

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

@@ -4,10 +4,12 @@ import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.NamespaceSet;
 import de.uka.ilkd.key.logic.Sequent;
 import de.uka.ilkd.key.pp.*;
-import de.uka.ilkd.key.proof.Node;
+import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
+import edu.kit.formal.interpreter.KeYProofFacade;
 import javafx.beans.Observable;
 import javafx.beans.property.SimpleObjectProperty;
+import javafx.scene.input.MouseButton;
 import javafx.scene.input.MouseEvent;
 import javafx.scene.layout.*;
 import javafx.scene.paint.Color;
@@ -26,7 +28,9 @@ public class SequentView extends CodeArea {
     private LogicPrinter lp;
     private IdentitySequentPrintFilter filter;
     private LogicPrinter.PosTableStringBackend backend;
-    private SimpleObjectProperty<de.uka.ilkd.key.proof.Node> node = new SimpleObjectProperty<>();
+    private SimpleObjectProperty<de.uka.ilkd.key.proof.Goal> node = new SimpleObjectProperty<>();
+    private KeYProofFacade keYProofFacade;
+    private TacletContextMenu menu;
 
 
     public SequentView() {
@@ -34,11 +38,11 @@ public class SequentView extends CodeArea {
         setEditable(false);
         node.addListener(this::update);
         setOnMouseMoved(this::hightlight);
+        setOnMouseClicked(this::onMouseClick);
     }
 
     private void hightlight(MouseEvent mouseEvent) {
         if (backend == null) return;
-
         CharacterHit hit = hit(mouseEvent.getX(), mouseEvent.getY());
         int insertionPoint = hit.getInsertionIndex();
         PosInSequent pis = backend.getInitialPositionTable().getPosInSequent(insertionPoint, filter);
@@ -51,14 +55,26 @@ public class SequentView extends CodeArea {
         mouseEvent.consume();
     }
 
-    public void mouseClick(MouseEvent e) {
+    public void onMouseClick(MouseEvent e) {
+        if (menu != null && menu.isShowing()) {
+            menu.hide();
+        }
+
         if (backend == null) {
             return;
         }
-        CharacterHit hit = hit(e.getX(), e.getY());
-        int insertionPoint = hit.getInsertionIndex();
-        PosInSequent pis = backend.getInitialPositionTable().getPosInSequent(insertionPoint, filter);
-
+        if (e.getButton() == MouseButton.SECONDARY) {
+            CharacterHit hit = hit(e.getX(), e.getY());
+            int insertionPoint = hit.getInsertionIndex();
+            PosInSequent pis = backend.getInitialPositionTable().getPosInSequent(insertionPoint, filter);
+            if (pis == null) return;
+
+            menu = new TacletContextMenu(keYProofFacade, pis, node.get());
+            menu.setAutoFix(true);
+            menu.setAutoHide(true);
+            menu.show(this, e.getScreenX(), e.getScreenY());
+            e.consume();
+        }
 /*
         Goal g = new Goal(node, null);
         ImmutableList<NoPosTacletApp> rules = g.ruleAppIndex().getFindTaclet(new TacletFilter() {
@@ -109,21 +125,29 @@ public class SequentView extends CodeArea {
 
         clear();
         insertText(0, backend.getString());
-        if (node.get().isClosed()) {
+        if (node.get().node().isClosed()) {
             this.setBorder(new Border(new BorderStroke(Color.RED, BorderStrokeStyle.SOLID, CornerRadii.EMPTY, BorderWidths.DEFAULT)));
             this.getStyleClass().add("closed-sequent-view");
         }
     }
 
-    public Node getNode() {
+    public Goal getNode() {
         return node.get();
     }
 
-    public void setNode(Node node) {
+    public SimpleObjectProperty<Goal> nodeProperty() {
+        return node;
+    }
+
+    public void setNode(Goal node) {
         this.node.set(node);
     }
 
-    public SimpleObjectProperty<Node> nodeProperty() {
-        return node;
+    public KeYProofFacade getKeYProofFacade() {
+        return keYProofFacade;
+    }
+
+    public void setKeYProofFacade(KeYProofFacade keYProofFacade) {
+        this.keYProofFacade = keYProofFacade;
     }
 }

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

+package edu.kit.formal.gui.controls;
+
+import de.uka.ilkd.key.control.ProofControl;
+import de.uka.ilkd.key.gui.nodeviews.TacletMenu.TacletAppComparator;
+import de.uka.ilkd.key.logic.Name;
+import de.uka.ilkd.key.logic.PosInOccurrence;
+import de.uka.ilkd.key.logic.Term;
+import de.uka.ilkd.key.pp.AbbrevMap;
+import de.uka.ilkd.key.pp.NotationInfo;
+import de.uka.ilkd.key.pp.PosInSequent;
+import de.uka.ilkd.key.proof.Goal;
+import de.uka.ilkd.key.rule.*;
+import edu.kit.formal.gui.controller.DebuggerMainWindowController;
+import edu.kit.formal.interpreter.KeYProofFacade;
+import javafx.event.ActionEvent;
+import javafx.fxml.FXML;
+import javafx.scene.control.ContextMenu;
+import javafx.scene.control.Menu;
+import javafx.scene.control.MenuItem;
+import javafx.scene.control.TextInputDialog;
+import javafx.scene.input.Clipboard;
+import javafx.scene.input.ClipboardContent;
+import org.key_project.util.collection.ImmutableList;
+import org.key_project.util.collection.ImmutableSLList;
+
+import java.util.*;
+import java.util.stream.Collectors;
+
+/**
+ * Copied from TacletMenu and adapted to JavaFX style. This is NOT a menu
+ * anymore but a view controller. There is a field rootMenu to access the actual
+ * menu.
+ *
+ * @author Victor Schuemmer
+ * @author Alexander Weigl
+ * @version 1.0
+ * @see de.uka.ilkd.key.gui.nodeviews.TacletMenu
+ */
+public class TacletContextMenu extends ContextMenu {
+
+    private static final Set<Name> CLUTTER_RULESETS = new LinkedHashSet<Name>();
+
+    static {
+        CLUTTER_RULESETS.add(new Name("notHumanReadable"));
+        CLUTTER_RULESETS.add(new Name("obsolete"));
+        CLUTTER_RULESETS.add(new Name("pullOutQuantifierAll"));
+        CLUTTER_RULESETS.add(new Name("pullOutQuantifierEx"));
+    }
+
+    private static final Set<Name> CLUTTER_RULES = new LinkedHashSet<Name>();
+
+    static {
+        CLUTTER_RULES.add(new Name("cut_direct_r"));
+        CLUTTER_RULES.add(new Name("cut_direct_l"));
+        CLUTTER_RULES.add(new Name("case_distinction_r"));
+        CLUTTER_RULES.add(new Name("case_distinction_l"));
+        CLUTTER_RULES.add(new Name("local_cut"));
+        CLUTTER_RULES.add(new Name("commute_and_2"));
+        CLUTTER_RULES.add(new Name("commute_or_2"));
+        CLUTTER_RULES.add(new Name("boxToDiamond"));
+        CLUTTER_RULES.add(new Name("pullOut"));
+        CLUTTER_RULES.add(new Name("typeStatic"));
+        CLUTTER_RULES.add(new Name("less_is_total"));
+        CLUTTER_RULES.add(new Name("less_zero_is_total"));
+        CLUTTER_RULES.add(new Name("applyEqReverse"));
+
+        // the following are used for drag'n'drop interactions
+        CLUTTER_RULES.add(new Name("eqTermCut"));
+        CLUTTER_RULES.add(new Name("instAll"));
+        CLUTTER_RULES.add(new Name("instEx"));
+    }
+
+    private PosInSequent pos;
+
+    @FXML
+    private ContextMenu rootMenu;
+    @FXML
+    private MenuItem noRules;
+    @FXML
+    private Menu moreRules;
+    @FXML
+    private Menu insertHidden;
+    @FXML
+    private MenuItem copyToClipboard;
+    @FXML
+    private MenuItem createAbbr;
+    @FXML
+    private MenuItem enableAbbr;
+    @FXML
+    private MenuItem disableAbbr;
+    @FXML
+    private MenuItem changeAbbr;
+
+
+    private Goal goal;
+    private PosInOccurrence occ;
+    private NotationInfo notationInfo = new NotationInfo();
+
+    public TacletContextMenu(KeYProofFacade keYProofFacade, PosInSequent pos, Goal goal) {
+        Utils.createWithFXML(this);
+
+        /*mediator = getContext().getKeYMediator();
+        comp = new TacletAppComparator();
+        insertHiddenController.initViewController(getMainApp(), getContext());
+    */
+        if (pos == null)
+            throw new IllegalArgumentException(
+                    "Argument pos must not be null.");
+        this.pos = pos;
+        this.goal = goal;
+
+        occ = pos.getPosInOccurrence();
+        //MediatorProofControl c = new MediatorProofControl(new DefaultAbstractMediatorUserInterfaceControlAdapter());
+        ProofControl c = DebuggerMainWindowController.FACADE.getEnvironment().getUi().getProofControl();
+
+        final ImmutableList<BuiltInRule> builtInRules = c.getBuiltInRule(goal, occ);
+        createTacletMenu(
+                removeRewrites(c.getFindTaclet(goal, occ))
+                        .prepend(c.getRewriteTaclet(goal, occ)),
+                c.getNoFindTaclet(goal), builtInRules);
+
+        //proofMacroMenuController.initViewController(getMainApp(), getContext());
+        //proofMacroMenuController.init(occ);
+    }
+
+    /**
+     * Removes RewriteTaclet from the list.
+     *
+     * @param list the IList<Taclet> from where the RewriteTaclet are removed
+     * @return list without RewriteTaclets
+     */
+    private static ImmutableList<TacletApp> removeRewrites(
+            ImmutableList<TacletApp> list) {
+        ImmutableList<TacletApp> result = ImmutableSLList.<TacletApp>nil();
+        Iterator<TacletApp> it = list.iterator();
+
+        while (it.hasNext()) {
+            TacletApp tacletApp = it.next();
+            Taclet taclet = tacletApp.taclet();
+            result = (taclet instanceof RewriteTaclet ? result
+                    : result.prepend(tacletApp));
+        }
+        return result;
+    }
+
+    /**
+     * Creates the menu by adding all submenus and items.
+     */
+    private void createTacletMenu(ImmutableList<TacletApp> find,
+                                  ImmutableList<TacletApp> noFind,
+                                  ImmutableList<BuiltInRule> builtInList) {
+
+        List<TacletApp> findTaclets = find.stream().collect(Collectors.toList());
+        List<TacletApp> noFindTaclets = noFind.stream().collect(Collectors.toList());
+
+        Collections.sort(findTaclets,
+                //compare by name
+                Comparator.comparing(o -> o.taclet().name())
+        );
+
+        List<TacletApp> toAdd = new ArrayList<>(findTaclets.size() + noFindTaclets.size());
+        toAdd.addAll(findTaclets);
+
+        boolean rulesAvailable = find.size() > 0;
+
+        if (pos.isSequent()) {
+            rulesAvailable |= noFind.size() > 0;
+            toAdd.addAll(noFindTaclets);
+        }
+
+        if (rulesAvailable) {
+            createMenuItems(toAdd);
+        } else {
+            noRules.setVisible(true);
+        }
+
+        if (occ != null)
+            createAbbrevSection(pos.getPosInOccurrence().subTerm());
+
+    }
+
+    /**
+     * Creates menu items for all given taclets. A submenu for insertion of
+     * hidden terms will be created if there are any, and rare rules will be in
+     * a 'More rules' submenu.
+     *
+     * @param taclets the list of taclets to create menu items for
+     */
+    private void createMenuItems(List<TacletApp> taclets) {
+        int idx = 0;
+        for (final TacletApp app : taclets) {
+            final Taclet taclet = app.taclet();
+
+       /*     if (!mediator.getFilterForInteractiveProving().filter(taclet)) {
+                continue;
+            }*/
+
+            final MenuItem item = new MenuItem(app.taclet().name().toString());
+            item.setOnAction(event -> {
+                handleRuleApplication(app);
+            });
+
+
+            // Items for insertion of hidden terms appear in a submenu.
+            /*if (insertHiddenController.isResponsible(item)) {
+                insertHiddenController.add(item);
+            } else */
+            {
+                // If one of the sets contains the rule it is considered rare
+                // and moved to a 'More rules' submenu.
+                boolean rareRule = false;
+                for (RuleSet rs : taclet.getRuleSets()) {
+                    if (CLUTTER_RULESETS.contains(rs.name()))
+                        rareRule = true;
+                }
+                if (CLUTTER_RULES.contains(taclet.name()))
+                    rareRule = true;
+
+                if (rareRule)
+                    moreRules.getItems().add(item);
+                else
+                    rootMenu.getItems().add(idx++, item);
+            }
+        }
+        // Make submenus visible iff they are not empty.
+        if (moreRules.getItems().size() > 0)
+            moreRules.setVisible(true);
+        /*if (!insertHiddenController.isEmpty())
+            insertHiddenController.setVisible(true);
+            */
+
+    }
+
+    /**
+     public TacletFilter getFilterForInteractiveProving() {
+     if(this.filterForInteractiveProving == null) {
+     this.filterForInteractiveProving = new TacletFilter() {
+     protected boolean filter(Taclet taclet) {
+     String[] var2 = JoinProcessor.SIMPLIFY_UPDATE;
+     int var3 = var2.length;
+
+     for(int var4 = 0; var4 < var3; ++var4) {
+     String name = var2[var4];
+     if(name.equals(taclet.name().toString())) {
+     return false;
+     }
+     }
+
+     return true;
+     }
+     };
+     }
+
+     return this.filterForInteractiveProving;
+     }*/
+
+    /**
+     * Manages the visibility of all menu items dealing with abbreviations based
+     * on if the given term already is abbreviated and if the abbreviation is
+     * enabled.
+     *
+     * @param t the term to check if there already is an abbreviation of
+     */
+
+    private void createAbbrevSection(Term t) {
+        AbbrevMap scm = notationInfo.getAbbrevMap();
+        if (scm.containsTerm(t)) {
+            changeAbbr.setVisible(true);
+            if (scm.isEnabled(t)) {
+                disableAbbr.setVisible(true);
+            } else {
+                enableAbbr.setVisible(true);
+            }
+        } else {
+            createAbbr.setVisible(true);
+        }
+    }
+
+    /**
+     * Handles the application of an 'ordinary' rule.
+     *
+     * @param event
+     */
+    private void handleRuleApplication(TacletApp event) {
+        // Synchronization for StaticSequentView
+     /*   parentController.setLastTacletActionID(parentController.getOwnID());
+        mediator.getUI().getProofControl().selectedTaclet(
+                ((TacletMenuItem) event.getSource()).getTaclet(), goal,
+                pos.getPosInOccurrence());*/
+    }
+
+    /**
+     * Handles rule application for automode.
+     *
+     * @param event
+     */
+    @FXML
+    private void handleFocussedRuleApplication(ActionEvent event) {
+        // Synchronization for StaticSequentView
+        // parentController.setLastTacletActionID(parentController.getOwnID());
+        //mediator.getUI().getProofControl()
+//                .startFocussedAutoMode(pos.getPosInOccurrence(), goal);
+    }
+
+    /**
+     * Handles action of the 'Copy to clipboard' menu item.
+     *
+     * @param event
+     */
+    @FXML
+    private void handleCopyToClipboard(ActionEvent event) {
+        final Clipboard clipboard = Clipboard.getSystemClipboard();
+        final ClipboardContent content = new ClipboardContent();
+        //content.putString(parentController.getProofString()
+        //        .substring(pos.getBounds().start(), pos.getBounds().end()));
+        clipboard.setContent(content);
+    }
+
+    /**
+     * Checks whether a string is a valid term abbreviation (is not empty and
+     * only contains 0-9, a-z, A-Z and underscore (_)).
+     *
+     * @param s the string to check
+     * @return true iff the string is a valid term abbreviation
+     */
+    private boolean validateAbbreviation(String s) {
+        if (s == null || s.length() == 0)
+            return false;
+        for (int i = 0; i < s.length(); i++) {
+            if (!((s.charAt(i) <= '9' && s.charAt(i) >= '0')
+                    || (s.charAt(i) <= 'z' && s.charAt(i) >= 'a')
+                    || (s.charAt(i) <= 'Z' && s.charAt(i) >= 'A')
+                    || s.charAt(i) == '_'))
+                return false;
+        }
+        return true;
+    }
+
+    /**
+     * Handles the creation of a term abbreviation.
+     *
+     * @param event
+     */
+    @FXML
+    private void handleCreateAbbreviation(ActionEvent event) {
+        if (occ.posInTerm() != null) {
+            final String oldTerm = occ.subTerm().toString();
+            final String term = oldTerm.length() > 200
+                    ? oldTerm.substring(0, 200) : oldTerm;
+            abbreviationDialog("Create Abbreviation",
+                    "Enter abbreviation for term: \n" + term + "\n", null);
+        }
+    }
+
+    /**
+     * Handles the change of a term abbreviation.
+     *
+     * @param event
+     */
+    @FXML
+    private void handleChangeAbbreviation(ActionEvent event) {
+        if (occ.posInTerm() != null) {