diff --git a/keyext.rusty.gui/build.gradle b/keyext.rusty.gui/build.gradle new file mode 100644 index 00000000000..72235a23563 --- /dev/null +++ b/keyext.rusty.gui/build.gradle @@ -0,0 +1,34 @@ +plugins { + id 'application' + id 'com.gradleup.shadow' version "9.4.1" +} + +description = "A minimal Swing GUI for the Rusty prover (MVP)" + +repositories { + mavenCentral() +} + +dependencies { + api project(':keyext.rusty') + + implementation 'org.jspecify:jspecify:1.0.0' + implementation 'ch.qos.logback:logback-classic:1.5.32' + implementation 'com.formdev:flatlaf:3.7.1' + + testImplementation(platform('org.junit:junit-bom:5.10.0')) + testImplementation('org.junit.jupiter:junit-jupiter') +} + +application { + mainClass = "org.key_project.rusty.gui.RustyMain" +} + +test { + useJUnitPlatform() +} + +shadowJar { + archiveClassifier = "exe" + archiveBaseName = "keyext.rusty.gui" +} diff --git a/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/EditorArea.java b/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/EditorArea.java new file mode 100644 index 00000000000..8317b2704ce --- /dev/null +++ b/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/EditorArea.java @@ -0,0 +1,283 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package org.key_project.rusty.gui; + +import java.awt.BorderLayout; +import java.awt.Cursor; +import java.awt.FlowLayout; +import java.awt.Font; +import java.awt.event.MouseAdapter; +import java.awt.event.MouseEvent; +import java.util.ArrayList; +import java.util.List; +import javax.swing.BorderFactory; +import javax.swing.JComponent; +import javax.swing.JLabel; +import javax.swing.JMenuItem; +import javax.swing.JPanel; +import javax.swing.JPopupMenu; +import javax.swing.JSplitPane; +import javax.swing.JTabbedPane; +import javax.swing.SwingUtilities; + +import org.key_project.rusty.proof.Goal; +import org.key_project.rusty.proof.Node; +import org.key_project.rusty.proof.Proof; + +import org.jspecify.annotations.Nullable; + +/// The central editor: a tabbed area of sequent views. One non-closable main tab follows the +/// selected node (its title says whether that node is an open goal or an inner node); further nodes +/// open as closable, pinned tabs (from the proof tree's right-click menu). A node can open *to the +/// side*, which splits the editor into two tab groups, and any pinned view can be moved between the +/// group and the split (or closed) from its tab menu. +public final class EditorArea extends JPanel implements ProofContext.Listener { + + private final ProofContext context; + private final Runnable runProverAction; + private final List views = new ArrayList<>(); + private final SequentView mainView; + private final JLabel mainTabLabel = new JLabel("Sequent"); + + private final JTabbedPane leftTabs = new JTabbedPane(); + private @Nullable JTabbedPane rightTabs; + private @Nullable JSplitPane split; + private JTabbedPane activeTabs; + private Font contentFont = new Font(Font.MONOSPACED, Font.PLAIN, 13); + + public EditorArea(ProofContext context, Runnable runProverAction) { + super(new BorderLayout()); + this.context = context; + this.runProverAction = runProverAction; + // A hairline on the editor's left edge so its tab strip does not meld into the proof-tree + // column across the thin split divider. + setBorder(BorderFactory.createMatteBorder(0, 1, 0, 0, Theme.hairline())); + + // Mark the live (selection-following) tab with the accent colour + bold + a dot, so it is + // obvious which pane tracks the proof-tree selection and which are pinned to a fixed node. + mainTabLabel.setForeground(Theme.accent()); + mainTabLabel.setFont(mainTabLabel.getFont().deriveFont(Font.BOLD)); + mainTabLabel.setToolTipText("This pane follows the selected proof node"); + + mainView = newView(); + leftTabs.addTab("", mainView); + leftTabs.setTabComponentAt(0, tabComponent(mainTabLabel, null)); + wireGroup(leftTabs); + activeTabs = leftTabs; + add(leftTabs, BorderLayout.CENTER); + + context.addListener(this); + updateMainTab(); + } + + @Override + public void proofLoaded() { + updateMainTab(); + } + + @Override + public void proofChanged() { + updateMainTab(); + } + + @Override + public void selectedNodeChanged() { + updateMainTab(); + } + + /// Labels the main tab by what it currently shows: an open goal or an inner node. A leading dot + /// marks it as the live, selection-following pane. + private void updateMainTab() { + Node node = context.getSelectedNode(); + mainTabLabel.setText("● " + (node == null ? "Sequent" : nodeLabel(node))); + } + + /// A node's tab/title label, using the same vocabulary everywhere (goal vs. inner node). + private String nodeLabel(Node node) { + return (isGoal(node) ? "Open goal " : "Inner node ") + node.getSerialNr(); + } + + private boolean isGoal(Node node) { + Proof proof = context.getProof(); + if (proof != null) { + for (Goal goal : proof.openGoals()) { + if (goal.getNode() == node) { + return true; + } + } + } + return false; + } + + /// Opens `node` in a pinned editor tab — in a new split to the side when `toSide`, otherwise as + /// a tab in the active group. + public void openNode(Node node, boolean toSide) { + JTabbedPane target; + if (toSide) { + ensureSplit(); + target = rightTabs; + } else { + target = activeTabs; + } + SequentView view = newView(); + view.pinTo(node); + addClosableTab(target, view); + target.setSelectedComponent(view); + activeTabs = target; + } + + /// Sets the font (family + size) of every editor view. + public void applyFont(Font font) { + this.contentFont = font; + for (SequentView view : views) { + view.applyFont(font); + } + } + + private SequentView newView() { + SequentView view = new SequentView(context); + view.setRunProverAction(runProverAction); + view.applyFont(contentFont); + views.add(view); + return view; + } + + // ── tab groups ────────────────────────────────────────────────────────── + + private void wireGroup(JTabbedPane tabs) { + // Left-align tabs (Aqua centres a lone tab) and scroll, rather than wrap, when there are + // many. + tabs.setTabLayoutPolicy(JTabbedPane.SCROLL_TAB_LAYOUT); + // A slimmer tab strip (FlatLaf's default is fairly tall). + tabs.putClientProperty("JTabbedPane.tabHeight", 26); + tabs.addChangeListener(e -> activeTabs = tabs); + tabs.addMouseListener(new MouseAdapter() { + @Override + public void mousePressed(MouseEvent e) { + onTabMouse(tabs, e); + } + + @Override + public void mouseReleased(MouseEvent e) { + onTabMouse(tabs, e); + } + }); + } + + private void onTabMouse(JTabbedPane tabs, MouseEvent e) { + activeTabs = tabs; + if (!e.isPopupTrigger()) { + return; + } + int idx = tabs.indexAtLocation(e.getX(), e.getY()); + if (idx < 0 || !(tabs.getComponentAt(idx) instanceof SequentView view) + || view == mainView) { + return; + } + JPopupMenu menu = new JPopupMenu(); + JMenuItem move = new JMenuItem(tabs == leftTabs && split == null + ? "Move to a new split" + : "Move to other split"); + move.addActionListener(ev -> moveToOtherSide(tabs, view)); + JMenuItem close = new JMenuItem("Close"); + close.addActionListener(ev -> closeTab(tabs, view)); + menu.add(move); + menu.add(close); + menu.show(tabs, e.getX(), e.getY()); + } + + private void addClosableTab(JTabbedPane tabs, SequentView view) { + String title = titleFor(view); + tabs.addTab(title, view); + int idx = tabs.indexOfComponent(view); + tabs.setTabComponentAt(idx, tabComponent(new JLabel(title), () -> closeTab(tabs, view))); + } + + private String titleFor(SequentView view) { + Node node = view.pinnedNode(); + return node != null ? nodeLabel(node) : view.tabTitle(); + } + + /// A uniform tab component (used for both the main and the pinned tabs so their heights line + /// up): + /// a title label and, when `onClose` is given, a small ✕ close affordance. + private JComponent tabComponent(JLabel title, @Nullable Runnable onClose) { + JPanel tab = new JPanel(new FlowLayout(FlowLayout.LEFT, 4, 1)); + tab.setOpaque(false); + tab.add(title); + if (onClose != null) { + JLabel close = new JLabel("✕"); + close.setBorder(BorderFactory.createEmptyBorder(0, 4, 0, 0)); + close.setCursor(Cursor.getPredefinedCursor(Cursor.HAND_CURSOR)); + close.setToolTipText("Close"); + close.addMouseListener(new MouseAdapter() { + @Override + public void mouseClicked(MouseEvent e) { + onClose.run(); + } + }); + tab.add(close); + } + return tab; + } + + private void closeTab(JTabbedPane tabs, SequentView view) { + if (view == mainView) { + return; + } + tabs.remove(view); + views.remove(view); + if (tabs == rightTabs && rightTabs.getTabCount() == 0) { + collapseSplit(); + } + } + + private void moveToOtherSide(JTabbedPane from, SequentView view) { + JTabbedPane to; + if (from == leftTabs) { + ensureSplit(); + to = rightTabs; + } else { + to = leftTabs; + } + from.remove(view); + addClosableTab(to, view); + to.setSelectedComponent(view); + activeTabs = to; + if (from == rightTabs && rightTabs.getTabCount() == 0) { + collapseSplit(); + } + } + + private void ensureSplit() { + if (split != null) { + return; + } + JTabbedPane right = new JTabbedPane(); + wireGroup(right); + rightTabs = right; + remove(leftTabs); + JSplitPane sp = new JSplitPane(JSplitPane.HORIZONTAL_SPLIT, leftTabs, right); + sp.setResizeWeight(0.5); + sp.setOneTouchExpandable(true); + split = sp; + add(sp, BorderLayout.CENTER); + revalidate(); + repaint(); + SwingUtilities.invokeLater(() -> sp.setDividerLocation(0.5)); + } + + private void collapseSplit() { + if (split == null) { + return; + } + remove(split); + split = null; + rightTabs = null; + add(leftTabs, BorderLayout.CENTER); + activeTabs = leftTabs; + revalidate(); + repaint(); + } +} diff --git a/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/GoalsView.java b/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/GoalsView.java new file mode 100644 index 00000000000..38689650fa3 --- /dev/null +++ b/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/GoalsView.java @@ -0,0 +1,92 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package org.key_project.rusty.gui; + +import java.awt.BorderLayout; +import javax.swing.DefaultListModel; +import javax.swing.JList; +import javax.swing.JPanel; +import javax.swing.JScrollPane; +import javax.swing.ListSelectionModel; + +import org.key_project.rusty.proof.Goal; +import org.key_project.rusty.proof.Node; +import org.key_project.rusty.proof.Proof; +import org.key_project.rusty.proof.io.OutputStreamProofSaver; + +/// Lists the open goals of the current proof. Selecting a goal selects its node in the context (and +/// thus in the proof tree and sequent view). +public final class GoalsView extends JPanel implements ProofContext.Listener { + + private final ProofContext context; + private final DefaultListModel model = new DefaultListModel<>(); + private final JList list = new JList<>(model); + private boolean syncing; + + public GoalsView(ProofContext context) { + super(new BorderLayout()); + this.context = context; + list.setSelectionMode(ListSelectionModel.SINGLE_SELECTION); + list.setCellRenderer((jl, goal, idx, sel, focus) -> { + var label = new javax.swing.JLabel(describe(goal)); + label.setToolTipText(label.getText()); + label.setBorder(javax.swing.BorderFactory.createEmptyBorder(1, 4, 1, 4)); + label.setOpaque(true); + if (sel) { + label.setBackground(jl.getSelectionBackground()); + label.setForeground(jl.getSelectionForeground()); + } + return label; + }); + list.addListSelectionListener(e -> { + if (syncing || e.getValueIsAdjusting()) { + return; + } + Goal g = list.getSelectedValue(); + if (g != null) { + context.setSelectedNode(g.getNode()); + } + }); + add(new JScrollPane(list), BorderLayout.CENTER); + context.addListener(this); + } + + /// Sets the goals list font (family + size). + public void applyFont(java.awt.Font font) { + list.setFont(font); + } + + @Override + public void proofLoaded() { + refresh(); + } + + @Override + public void proofChanged() { + refresh(); + } + + private void refresh() { + model.clear(); + Proof proof = context.getProof(); + if (proof != null) { + for (Goal g : proof.openGoals()) { + model.addElement(g); + } + } + } + + /// A one-line label for a goal: the node number plus an abbreviated, whitespace-collapsed + /// rendering of its sequent, so goals can be told apart at a glance. + private static String describe(Goal goal) { + Node node = goal.getNode(); + String sequent = + OutputStreamProofSaver.printSequent(node.sequent(), node.proof().getServices()) + .replaceAll("\\s+", " ").trim(); + if (sequent.length() > 90) { + sequent = sequent.substring(0, 89) + "…"; + } + return node.getSerialNr() + ": " + sequent; + } +} diff --git a/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/MainWindow.java b/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/MainWindow.java new file mode 100644 index 00000000000..b7c8ef84b4f --- /dev/null +++ b/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/MainWindow.java @@ -0,0 +1,465 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package org.key_project.rusty.gui; + +import java.awt.BorderLayout; +import java.awt.Dimension; +import java.awt.FlowLayout; +import java.awt.Font; +import java.awt.Image; +import java.io.File; +import java.net.URL; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.List; +import java.util.prefs.Preferences; +import javax.swing.BorderFactory; +import javax.swing.Icon; +import javax.swing.ImageIcon; +import javax.swing.JButton; +import javax.swing.JComponent; +import javax.swing.JFileChooser; +import javax.swing.JFrame; +import javax.swing.JLabel; +import javax.swing.JMenu; +import javax.swing.JMenuBar; +import javax.swing.JMenuItem; +import javax.swing.JOptionPane; +import javax.swing.JPanel; +import javax.swing.JSlider; +import javax.swing.JSplitPane; +import javax.swing.JToolBar; +import javax.swing.SwingConstants; +import javax.swing.SwingUtilities; +import javax.swing.border.Border; +import javax.swing.filechooser.FileNameExtensionFilter; + +import org.key_project.rusty.control.KeYEnvironment; +import org.key_project.rusty.proof.Node; +import org.key_project.rusty.proof.Proof; +import org.key_project.rusty.proof.io.ProofSaver; + +import org.jspecify.annotations.Nullable; + +/// The single-window MVP over one [ProofContext]: a menu/toolbar (load/save/run), a status bar with +/// a zoom slider, and an IDE-like docked layout. The editor (sequent tabs) is the centre; the proof +/// tree and the open goals — the two navigation lists — are stacked in the left column; the live +/// strategy settings are the right tool window; the node info is the full-width bottom strip. The +/// tool windows are resizable/collapsible via the one-touch split dividers. No multi-proof task +/// management, no KeY-Java specific tooling. +public final class MainWindow extends JFrame { + + private static final int MAX_RECENT = 12; + private static final String RECENT_KEY = "recentFiles"; + private static final int BASE_FONT_SIZE = 13; // font size at 100% zoom + + private final ProofContext context = new ProofContext(); + private final Preferences prefs = Preferences.userNodeForPackage(MainWindow.class); + private final JMenu recentMenu = new JMenu("Recent files"); + private final JLabel statusLabel = new JLabel("No proof loaded"); + private final StrategyView strategyView = new StrategyView(context); + private final ProofTreePanel treePanel = new ProofTreePanel(context); + private final GoalsView goalsView = new GoalsView(context); + private final NodeInfoView infoView = new NodeInfoView(context); + private final EditorArea editor = new EditorArea(context, this::runAutoMode); + private int zoomPercent = 100; + + public MainWindow() { + super("KeYther"); + setDefaultCloseOperation(EXIT_ON_CLOSE); + setJMenuBar(buildMenuBar()); + + treePanel.setHoverListener(infoView::preview); + treePanel.setOpenNodeListener(editor::openNode); + treePanel.setPruneListener(this::prune); + + Icon logo = icon("key-color-icon-square.png", 0); // unscaled, for the window icon + if (logo instanceof ImageIcon img) { + setIconImage(img.getImage()); + } + + // IDE-like docked layout. The editor (sequent tabs) is the centre, with its own header. + // The left column stacks the two *navigation lists* — the proof tree and the open goals — + // because both want vertical room (a proof can have many goals). The node info is short but + // wide content (a taclet line is wide), so it gets the full-width bottom strip. The + // strategy + // settings are an always-visible right tool window. All dividers are one-touch collapsible. + JSplitPane leftColumn = new JSplitPane(JSplitPane.VERTICAL_SPLIT, + toolWindow("Proof tree", treePanel), toolWindow("Open goals", goalsView)); + leftColumn.setResizeWeight(0.6); + leftColumn.setDividerLocation(260); // give the goals list real height by default + leftColumn.setOneTouchExpandable(true); + + // Editor (grows) on the left, strategy tool window pinned to the right. + JSplitPane centreRight = new JSplitPane(JSplitPane.HORIZONTAL_SPLIT, editor, + toolWindow("Strategy", strategyView)); + centreRight.setResizeWeight(1.0); + centreRight.setOneTouchExpandable(true); + + JSplitPane editorSplit = + new JSplitPane(JSplitPane.HORIZONTAL_SPLIT, leftColumn, centreRight); + editorSplit.setDividerLocation(300); + editorSplit.setOneTouchExpandable(true); + + JSplitPane mainSplit = new JSplitPane(JSplitPane.VERTICAL_SPLIT, editorSplit, + toolWindow("Node info", infoView)); + mainSplit.setResizeWeight(1.0); + mainSplit.setOneTouchExpandable(true); + + add(buildToolBar(), BorderLayout.NORTH); + add(mainSplit, BorderLayout.CENTER); + add(buildStatusBar(), BorderLayout.SOUTH); + applyAllFonts(); + + // Sensible initial divider positions once the frame has a size (fractions need a realised + // component). The strategy pane sits ~230px from the right; node info is a short bottom + // band. + SwingUtilities.invokeLater(() -> { + centreRight.setDividerLocation(centreRight.getWidth() - 230); + mainSplit.setDividerLocation(mainSplit.getHeight() - 150); + }); + + // Keep the status bar in sync with the proof state. + context.addListener(new ProofContext.Listener() { + @Override + public void proofLoaded() { + updateStatus(); + } + + @Override + public void proofChanged() { + updateStatus(); + } + }); + + rebuildRecentMenu(); + setSize(1100, 700); + setLocationRelativeTo(null); + } + + /// Reflects the live proof state (node count, remaining goals, closed) in the status bar. + private void updateStatus() { + Proof proof = context.getProof(); + if (proof == null) { + statusLabel.setText("No proof loaded"); + return; + } + int nodes = proof.countNodes(); + int open = proof.openGoals().size(); + String state = proof.closed() ? "proof closed ✓" + : open + (open == 1 ? " open goal" : " open goals"); + statusLabel.setText(nodes + (nodes == 1 ? " node" : " nodes") + " · " + state); + } + + private JMenuBar buildMenuBar() { + JMenuBar bar = new JMenuBar(); + + JMenu file = new JMenu("File"); + file.add(menuItem("Open .key / .proof ...", this::openProof)); + file.add(menuItem("Reopen most recent", this::openMostRecent)); + file.add(recentMenu); + file.add(menuItem("Save proof ...", this::saveProof)); + file.addSeparator(); + file.add(menuItem("Preferences ...", this::openPreferences)); + file.add(menuItem("Exit", this::dispose)); + + JMenu proof = new JMenu("Proof"); + proof.add(menuItem("Run auto mode", this::runAutoMode)); + proof.add(menuItem("Prune proof at selected node", this::pruneAtSelected)); + + bar.add(file); + bar.add(proof); + return bar; + } + + private JToolBar buildToolBar() { + JToolBar bar = new JToolBar(); + bar.setFloatable(false); + // A thin band between the menu bar and the content, so the toolbar reads as its own strip. + bar.setBorder(BorderFactory.createCompoundBorder( + BorderFactory.createMatteBorder(1, 0, 1, 0, Theme.hairline()), + BorderFactory.createEmptyBorder(3, 6, 3, 6))); + bar.add(toolButton("Open", "Load a .key problem or .proof", icon("open.png", 18), + this::openProof)); + bar.add(toolButton("Reopen", "Reopen the most recently opened file", + icon("openMostRecent.png", 18), this::openMostRecent)); + bar.add(toolButton("Save", "Save the current proof", icon("saveFile.png", 18), + this::saveProof)); + bar.addSeparator(); + bar.add(toolButton("Run prover", "Run auto mode on the current proof", + icon("autoModeStart.png", 18), this::runAutoMode)); + bar.add(toolButton("Prune", "Prune the proof at the selected node", + icon("pruneProof.png", 18), this::pruneAtSelected)); + return bar; + } + + /// Loads a bundled KeY icon by name, scaled to `size` px (or unscaled when `size <= 0`); + /// returns + /// `null` when the resource is missing. + private @Nullable Icon icon(String name, int size) { + URL url = MainWindow.class.getResource("/org/key_project/rusty/gui/icons/" + name); + if (url == null) { + return null; + } + ImageIcon raw = new ImageIcon(url); + if (size <= 0) { + return raw; + } + return new ImageIcon(raw.getImage().getScaledInstance(size, size, Image.SCALE_SMOOTH)); + } + + /// Wraps a section in an IDE-like tool window: a thin title bar above the content. + private JComponent toolWindow(String title, JComponent content) { + JPanel panel = new JPanel(new BorderLayout()); + + JLabel titleBar = new JLabel(title.toUpperCase()); + titleBar.setHorizontalAlignment(SwingConstants.LEFT); + titleBar.setFont(titleBar.getFont().deriveFont(Font.BOLD, 11f)); + titleBar.setForeground(Theme.mutedText()); + titleBar.setOpaque(true); + titleBar.setBackground(Theme.surface()); + Border line = BorderFactory.createMatteBorder(0, 0, 1, 0, Theme.hairline()); + Border pad = BorderFactory.createEmptyBorder(3, 8, 3, 8); + titleBar.setBorder(BorderFactory.createCompoundBorder(line, pad)); + + panel.add(titleBar, BorderLayout.NORTH); + panel.add(content, BorderLayout.CENTER); + return panel; + } + + private JComponent buildStatusBar() { + JPanel bar = new JPanel(new BorderLayout()); + // A hairline above the status bar separates it from the panes. + bar.setBorder(BorderFactory.createCompoundBorder( + BorderFactory.createMatteBorder(1, 0, 0, 0, Theme.hairline()), + BorderFactory.createEmptyBorder(3, 8, 3, 8))); + + JPanel zoom = new JPanel(new FlowLayout(FlowLayout.RIGHT, 6, 0)); + JSlider slider = new JSlider(50, 200, zoomPercent); + slider.setPreferredSize(new Dimension(150, slider.getPreferredSize().height)); + slider.setToolTipText("Zoom (percentage of the configured font size)"); + JLabel value = new JLabel(zoomPercent + "%"); + slider.addChangeListener(e -> { + zoomPercent = slider.getValue(); + value.setText(zoomPercent + "%"); + applyAllFonts(); + }); + zoom.add(new JLabel("Zoom")); + zoom.add(slider); + zoom.add(value); + + bar.add(statusLabel, BorderLayout.WEST); + bar.add(zoom, BorderLayout.EAST); + return bar; + } + + /// Applies the configured fonts (global, with optional per-pane overrides, scaled by the zoom + /// percentage) to every pane. + private void applyAllFonts() { + treePanel.applyFont(fontFor("tree")); + editor.applyFont(fontFor("sequent")); + infoView.applyFont(fontFor("info")); + goalsView.applyFont(fontFor("goals")); + } + + /// The effective font for a pane: its per-pane override family/size if set, otherwise the + /// global + /// family/size, scaled by the current zoom percentage. + private Font fontFor(String pane) { + String globalFamily = prefs.get("font.family", Font.MONOSPACED); + int globalSize = prefs.getInt("font.size", BASE_FONT_SIZE); + String family = prefs.get("font." + pane + ".family", globalFamily); + int base = prefs.getInt("font." + pane + ".size", globalSize); + int size = Math.max(6, Math.round(base * zoomPercent / 100f)); + return new Font(family, Font.PLAIN, size); + } + + private void openPreferences() { + new PreferencesDialog(this, prefs, this::applyAllFonts).setVisible(true); + } + + private JMenuItem menuItem(String label, Runnable action) { + JMenuItem item = new JMenuItem(label); + item.addActionListener(e -> action.run()); + return item; + } + + private JButton toolButton(String label, String tip, @Nullable Icon icon, Runnable action) { + JButton button = new JButton(label); + if (icon != null) { + button.setIcon(icon); + } + button.setToolTipText(tip); + button.setFocusable(false); + button.addActionListener(e -> action.run()); + return button; + } + + // ── Recent files ──────────────────────────────────────────────────────── + + private List recentFiles() { + String stored = prefs.get(RECENT_KEY, ""); + return stored.isEmpty() ? new ArrayList<>() + : new ArrayList<>(Arrays.asList(stored.split("\n"))); + } + + private void addRecentFile(File file) { + String path = file.getAbsolutePath(); + List recent = recentFiles(); + recent.remove(path); + recent.add(0, path); + while (recent.size() > MAX_RECENT) { + recent.remove(recent.size() - 1); + } + prefs.put(RECENT_KEY, String.join("\n", recent)); + rebuildRecentMenu(); + } + + private void rebuildRecentMenu() { + recentMenu.removeAll(); + List recent = recentFiles(); + if (recent.isEmpty()) { + JMenuItem none = new JMenuItem("(none)"); + none.setEnabled(false); + recentMenu.add(none); + return; + } + for (String path : recent) { + File f = new File(path); + JMenuItem item = new JMenuItem(f.getName()); + item.setToolTipText(path); + item.addActionListener(e -> openProof(f)); + recentMenu.add(item); + } + recentMenu.addSeparator(); + recentMenu.add(menuItem("Clear recent files", () -> { + prefs.remove(RECENT_KEY); + rebuildRecentMenu(); + })); + } + + private @Nullable File lastDirectory() { + List recent = recentFiles(); + return recent.isEmpty() ? null : new File(recent.get(0)).getParentFile(); + } + + // ── Actions ───────────────────────────────────────────────────────────── + + private void openProof() { + JFileChooser chooser = new JFileChooser(lastDirectory()); + chooser.setFileFilter( + new FileNameExtensionFilter("KeY problem or proof (*.key, *.proof)", "key", "proof")); + if (chooser.showOpenDialog(this) == JFileChooser.APPROVE_OPTION) { + openProof(chooser.getSelectedFile()); + } + } + + private void openProof(File file) { + try { + KeYEnvironment env = KeYEnvironment.load(file); + Proof proof = env.getLoadedProof(); + if (proof == null) { + showError("No proof was loaded from " + file); + return; + } + context.setProof(env, proof); + addRecentFile(file); + } catch (Exception ex) { + showError("Could not load " + file + ":\n" + ex.getMessage()); + } + } + + private void saveProof() { + Proof proof = context.getProof(); + if (proof == null) { + showError("No proof is open."); + return; + } + JFileChooser chooser = new JFileChooser(lastDirectory()); + chooser.setFileFilter(new FileNameExtensionFilter("KeY proof (*.proof)", "proof")); + if (chooser.showSaveDialog(this) != JFileChooser.APPROVE_OPTION) { + return; + } + File file = chooser.getSelectedFile(); + if (!file.getName().endsWith(".proof")) { + file = new File(file.getParentFile(), file.getName() + ".proof"); + } + try { + ProofSaver.saveToFile(file, proof); + addRecentFile(file); + } catch (Exception ex) { + showError("Could not save proof:\n" + ex.getMessage()); + } + } + + /// Re-opens the file at the top of the recent-files list. + private void openMostRecent() { + List recent = recentFiles(); + if (recent.isEmpty()) { + showError("No recently opened files."); + return; + } + openProof(new File(recent.get(0))); + } + + /// Prunes the proof at the currently selected node (the node becomes an open goal again). + private void pruneAtSelected() { + Node node = context.getSelectedNode(); + if (node == null) { + showError("No node is selected."); + return; + } + if (node.childrenCount() == 0) { + showError("Nothing to prune: the selected node is a leaf."); + return; + } + prune(node); + } + + /// Prunes the proof at `node`, dropping its subtree, then refreshes the views. + private void prune(Node node) { + Proof proof = context.getProof(); + if (proof == null) { + return; + } + try { + proof.pruneProof(node); + context.fireProofChanged(); + context.setSelectedNode(node); + } catch (Exception ex) { + showError("Could not prune the proof:\n" + ex.getMessage()); + } + } + + private void runAutoMode() { + Proof proof = context.getProof(); + KeYEnvironment env = context.getEnvironment(); + if (proof == null || env == null) { + showError("No proof is open."); + return; + } + // Lock the strategy controls so a live edit cannot mutate the settings mid-run, then run + // the (blocking) strategy off the EDT and refresh the views. + strategyView.setRunning(true); + new Thread(() -> { + try { + env.getProofControl().startAndWaitForAutoMode(proof); + } catch (Exception ex) { + SwingUtilities.invokeLater(() -> { + strategyView.setRunning(false); + showError("Auto mode failed:\n" + ex.getMessage()); + }); + return; + } + SwingUtilities.invokeLater(() -> { + strategyView.setRunning(false); + context.fireProofChanged(); + }); + }, "solidity-auto-mode").start(); + } + + private void showError(String message) { + JOptionPane.showMessageDialog(this, message, "Error", JOptionPane.ERROR_MESSAGE); + } +} diff --git a/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/NodeInfoView.java b/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/NodeInfoView.java new file mode 100644 index 00000000000..916f36a57b0 --- /dev/null +++ b/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/NodeInfoView.java @@ -0,0 +1,168 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package org.key_project.rusty.gui; + +import java.awt.BorderLayout; +import java.awt.Color; +import java.awt.Cursor; +import java.awt.Font; +import javax.swing.BorderFactory; +import javax.swing.JButton; +import javax.swing.JPanel; +import javax.swing.JScrollPane; +import javax.swing.JTextArea; +import javax.swing.SwingConstants; + +import org.key_project.prover.rules.RuleApp; +import org.key_project.rusty.proof.Node; +import org.key_project.rusty.rule.TacletApp; + +import org.jspecify.annotations.Nullable; + +/// A read-only view describing the rule applied at a proof node. It *pins* to the selected node and +/// *previews* whichever node the cursor hovers in the proof tree, reverting to the pinned node when +/// the cursor leaves. When the rule is a taclet, the full taclet definition is available under a +/// collapsible toggle that shows only the taclet name when collapsed and the whole taclet when +/// expanded. +public final class NodeInfoView extends JPanel implements ProofContext.Listener { + + private final ProofContext context; + private final JTextArea info = new JTextArea(); + private final JButton toggle = new JButton(); + private final JTextArea tacletText = new JTextArea(); + private final JScrollPane tacletScroll; + + private boolean expanded; + private @Nullable String tacletName; + private @Nullable Node shown; + private Font contentFont = new Font(Font.MONOSPACED, Font.PLAIN, 12); + private final Color normalForeground; + + public NodeInfoView(ProofContext context) { + super(new BorderLayout()); + this.context = context; + + info.setEditable(false); + info.setFocusable(false); + info.setFont(new Font(Font.MONOSPACED, Font.PLAIN, 12)); + info.setMargin(new java.awt.Insets(6, 8, 2, 8)); + normalForeground = info.getForeground(); + + toggle.setHorizontalAlignment(SwingConstants.LEFT); + toggle.setBorderPainted(false); + toggle.setContentAreaFilled(false); + toggle.setFocusable(false); + toggle.setCursor(Cursor.getPredefinedCursor(Cursor.HAND_CURSOR)); + toggle.setVisible(false); + toggle.addActionListener(e -> { + expanded = !expanded; + updateTacletSection(); + }); + + tacletText.setEditable(false); + tacletText.setFocusable(false); + tacletText.setFont(new Font(Font.MONOSPACED, Font.PLAIN, 12)); + tacletText.setMargin(new java.awt.Insets(2, 14, 4, 6)); + tacletScroll = new JScrollPane(tacletText); + tacletScroll.setBorder(BorderFactory.createEmptyBorder()); + tacletScroll.setVisible(false); + + JPanel top = new JPanel(new BorderLayout()); + top.add(info, BorderLayout.CENTER); + top.add(toggle, BorderLayout.SOUTH); + add(top, BorderLayout.NORTH); + add(tacletScroll, BorderLayout.CENTER); + context.addListener(this); + } + + /// Pins the view to the selected node. + @Override + public void selectedNodeChanged() { + render(context.getSelectedNode()); + } + + @Override + public void proofLoaded() { + render(context.getSelectedNode()); + } + + @Override + public void proofChanged() { + render(context.getSelectedNode()); + } + + /// Previews `node` (e.g. while hovering the proof tree); reverts to the pinned, selected node + /// once the cursor leaves (`node == null`). + public void preview(@Nullable Node node) { + render(node != null ? node : context.getSelectedNode()); + } + + private void render(@Nullable Node node) { + shown = node; + if (node == null) { + info.setForeground(Theme.mutedText()); + info.setFont(new Font(Font.SANS_SERIF, Font.ITALIC, contentFont.getSize())); + info.setText( + "No node selected.\nHover or select a proof node to see its applied rule."); + } else { + info.setForeground(normalForeground); + info.setFont(contentFont); + info.setText(describe(node)); + } + info.setCaretPosition(0); + + RuleApp app = node == null ? null : node.getAppliedRuleApp(); + if (app instanceof TacletApp tacletApp) { + tacletName = tacletApp.taclet().name().toString(); + tacletText.setText(tacletApp.taclet().toString()); + tacletText.setCaretPosition(0); + } else { + tacletName = null; + tacletText.setText(""); + } + updateTacletSection(); + } + + /// Sets the font (family + size) of both the info and the taclet text. + public void applyFont(Font font) { + contentFont = font; + tacletText.setFont(font); + render(shown); + } + + private void updateTacletSection() { + boolean hasTaclet = tacletName != null; + toggle.setVisible(hasTaclet); + if (hasTaclet) { + toggle.setText((expanded ? "▼ " : "▶ ") + "Applied taclet: " + tacletName); + } + tacletScroll.setVisible(hasTaclet && expanded); + revalidate(); + repaint(); + } + + private static String describe(@Nullable Node node) { + if (node == null) { + return ""; + } + RuleApp app = node.getAppliedRuleApp(); + if (app == null) { + return "Node " + node.getSerialNr() + "\n(no rule applied — open or closed leaf)"; + } + StringBuilder sb = new StringBuilder(); + sb.append("Node ").append(node.getSerialNr()).append('\n'); + sb.append("Rule: ").append(app.rule().displayName()); + String internal = app.rule().name().toString(); + if (!internal.equals(app.rule().displayName())) { + sb.append(" (").append(internal).append(')'); + } + sb.append('\n'); + sb.append("Kind: ").append(app instanceof TacletApp ? "taclet" : "built-in rule"); + int children = node.childrenCount(); + if (children > 1) { + sb.append('\n').append("Splits into ").append(children).append(" branches"); + } + return sb.toString(); + } +} diff --git a/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/PreferencesDialog.java b/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/PreferencesDialog.java new file mode 100644 index 00000000000..692d0e6b8de --- /dev/null +++ b/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/PreferencesDialog.java @@ -0,0 +1,192 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package org.key_project.rusty.gui; + +import java.awt.BorderLayout; +import java.awt.Font; +import java.awt.Frame; +import java.awt.GraphicsEnvironment; +import java.awt.GridBagConstraints; +import java.awt.GridBagLayout; +import java.awt.Insets; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.List; +import java.util.prefs.Preferences; +import javax.swing.BorderFactory; +import javax.swing.Box; +import javax.swing.BoxLayout; +import javax.swing.JButton; +import javax.swing.JCheckBox; +import javax.swing.JComboBox; +import javax.swing.JDialog; +import javax.swing.JLabel; +import javax.swing.JPanel; +import javax.swing.JScrollPane; +import javax.swing.JSeparator; +import javax.swing.JSpinner; +import javax.swing.SpinnerNumberModel; + +/// A modal dialog to configure the fonts of the GUI: a global font family + size applied to every +/// pane, and an optional per-pane override (proof tree, sequent, node info, open goals). Settings +/// are stored in [Preferences] under `font.*`; `onApply` re-applies them to the live panes. +final class PreferencesDialog extends JDialog { + + /// The panes whose font can be overridden: a preferences key and a display label. + private static final String[][] PANES = { + { "tree", "Proof tree" }, + { "sequent", "Sequent" }, + { "info", "Node info" }, + { "goals", "Open goals" }, + }; + + private final Preferences prefs; + private final Runnable onApply; + + private final JComboBox globalFamily; + private final JSpinner globalSize; + private final List override = new ArrayList<>(); + private final List> paneFamily = new ArrayList<>(); + private final List paneSize = new ArrayList<>(); + + PreferencesDialog(Frame owner, Preferences prefs, Runnable onApply) { + super(owner, "Preferences", true); + this.prefs = prefs; + this.onApply = onApply; + + String[] families = fontFamilies(); + String globalFamilyValue = prefs.get("font.family", Font.MONOSPACED); + int globalSizeValue = prefs.getInt("font.size", 13); + + JPanel form = new JPanel(new GridBagLayout()); + form.setBorder(BorderFactory.createEmptyBorder(12, 12, 12, 12)); + GridBagConstraints g = new GridBagConstraints(); + g.insets = new Insets(3, 4, 3, 4); + g.anchor = GridBagConstraints.WEST; + int row = 0; + + row = header(form, g, row, "Global font (applies to every pane)"); + globalFamily = new JComboBox<>(families); + globalFamily.setSelectedItem(globalFamilyValue); + globalSize = new JSpinner(new SpinnerNumberModel(globalSizeValue, 6, 48, 1)); + row = fontRow(form, g, row, new JLabel("Font"), globalFamily, globalSize); + + row = separator(form, g, row); + row = header(form, g, row, "Per-pane overrides"); + + for (String[] pane : PANES) { + String key = pane[0]; + boolean has = prefs.get("font." + key + ".family", null) != null; + JCheckBox check = new JCheckBox(pane[1]); + check.setSelected(has); + JComboBox family = new JComboBox<>(families); + family.setSelectedItem(prefs.get("font." + key + ".family", globalFamilyValue)); + JSpinner size = new JSpinner(new SpinnerNumberModel( + prefs.getInt("font." + key + ".size", globalSizeValue), 6, 48, 1)); + override.add(check); + paneFamily.add(family); + paneSize.add(size); + int idx = override.size() - 1; + check.addActionListener(e -> updateEnabled(idx)); + row = fontRow(form, g, row, check, family, size); + updateEnabled(idx); + } + + JButton ok = new JButton("OK"); + ok.addActionListener(e -> { + apply(); + dispose(); + }); + JButton cancel = new JButton("Cancel"); + cancel.addActionListener(e -> dispose()); + JPanel buttons = new JPanel(); + buttons.setLayout(new BoxLayout(buttons, BoxLayout.LINE_AXIS)); + buttons.setBorder(BorderFactory.createEmptyBorder(0, 12, 12, 12)); + buttons.add(Box.createHorizontalGlue()); + buttons.add(cancel); + buttons.add(Box.createHorizontalStrut(6)); + buttons.add(ok); + + add(new JScrollPane(form), BorderLayout.CENTER); + add(buttons, BorderLayout.SOUTH); + getRootPane().setDefaultButton(ok); + pack(); + setLocationRelativeTo(owner); + } + + private int header(JPanel form, GridBagConstraints g, int row, String text) { + JLabel label = new JLabel(text); + label.setFont(label.getFont().deriveFont(Font.BOLD)); + g.gridx = 0; + g.gridy = row; + g.gridwidth = 3; + form.add(label, g); + g.gridwidth = 1; + return row + 1; + } + + private int separator(JPanel form, GridBagConstraints g, int row) { + g.gridx = 0; + g.gridy = row; + g.gridwidth = 3; + g.fill = GridBagConstraints.HORIZONTAL; + form.add(new JSeparator(), g); + g.fill = GridBagConstraints.NONE; + g.gridwidth = 1; + return row + 1; + } + + private int fontRow(JPanel form, GridBagConstraints g, int row, JLabel label, + JComboBox family, JSpinner size) { + g.gridy = row; + g.gridx = 0; + form.add(label, g); + g.gridx = 1; + form.add(family, g); + g.gridx = 2; + form.add(size, g); + return row + 1; + } + + private int fontRow(JPanel form, GridBagConstraints g, int row, JCheckBox check, + JComboBox family, JSpinner size) { + g.gridy = row; + g.gridx = 0; + form.add(check, g); + g.gridx = 1; + form.add(family, g); + g.gridx = 2; + form.add(size, g); + return row + 1; + } + + private void updateEnabled(int idx) { + boolean on = override.get(idx).isSelected(); + paneFamily.get(idx).setEnabled(on); + paneSize.get(idx).setEnabled(on); + } + + private void apply() { + prefs.put("font.family", (String) globalFamily.getSelectedItem()); + prefs.putInt("font.size", (Integer) globalSize.getValue()); + for (int i = 0; i < PANES.length; i++) { + String key = PANES[i][0]; + if (override.get(i).isSelected()) { + prefs.put("font." + key + ".family", (String) paneFamily.get(i).getSelectedItem()); + prefs.putInt("font." + key + ".size", (Integer) paneSize.get(i).getValue()); + } else { + prefs.remove("font." + key + ".family"); + prefs.remove("font." + key + ".size"); + } + } + onApply.run(); + } + + private static String[] fontFamilies() { + List all = new ArrayList<>(List.of(Font.MONOSPACED, Font.SANS_SERIF, Font.SERIF)); + all.addAll(Arrays.asList(GraphicsEnvironment.getLocalGraphicsEnvironment() + .getAvailableFontFamilyNames())); + return all.toArray(new String[0]); + } +} diff --git a/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/ProofContext.java b/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/ProofContext.java new file mode 100644 index 00000000000..7d2710d1509 --- /dev/null +++ b/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/ProofContext.java @@ -0,0 +1,76 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package org.key_project.rusty.gui; + +import java.util.ArrayList; +import java.util.List; + +import org.key_project.rusty.control.KeYEnvironment; +import org.key_project.rusty.proof.Node; +import org.key_project.rusty.proof.Proof; + +import org.jspecify.annotations.Nullable; + +/// The single-proof "mediator" of the minimal GUI. +/// +/// Unlike KeY-Java's mediator this holds at most one open proof and only the few pieces of state +/// the MVP views need: the loaded environment/proof and the currently selected proof node. Views +/// register as [Listener]s and are notified when the proof or the selection changes. +public final class ProofContext { + + /// Notified about changes to the open proof or the selected node. + public interface Listener { + /// A new proof was loaded (or the previous one was closed). + default void proofLoaded() {} + + /// The proof tree changed (a rule was applied, auto mode ran, ...). + default void proofChanged() {} + + /// The selected proof node changed. + default void selectedNodeChanged() {} + } + + private final List listeners = new ArrayList<>(); + + private @Nullable KeYEnvironment environment; + private @Nullable Proof proof; + private @Nullable Node selectedNode; + + public void addListener(Listener l) { + listeners.add(l); + } + + public @Nullable Proof getProof() { + return proof; + } + + public @Nullable KeYEnvironment getEnvironment() { + return environment; + } + + public @Nullable Node getSelectedNode() { + return selectedNode; + } + + /// Replaces the open proof, selects its root and notifies all listeners. + public void setProof(KeYEnvironment environment, Proof proof) { + this.environment = environment; + this.proof = proof; + this.selectedNode = proof.root(); + listeners.forEach(Listener::proofLoaded); + listeners.forEach(Listener::selectedNodeChanged); + } + + public void setSelectedNode(@Nullable Node node) { + if (node != selectedNode) { + this.selectedNode = node; + listeners.forEach(Listener::selectedNodeChanged); + } + } + + /// Signals that the proof tree was modified (e.g. after a rule application or auto mode). + public void fireProofChanged() { + listeners.forEach(Listener::proofChanged); + } +} diff --git a/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/ProofTreePanel.java b/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/ProofTreePanel.java new file mode 100644 index 00000000000..5d3030cbf2f --- /dev/null +++ b/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/ProofTreePanel.java @@ -0,0 +1,451 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package org.key_project.rusty.gui; + +import java.awt.BorderLayout; +import java.awt.Component; +import java.awt.Dimension; +import java.awt.FlowLayout; +import java.awt.Toolkit; +import java.awt.event.MouseAdapter; +import java.awt.event.MouseEvent; +import java.awt.event.MouseMotionAdapter; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.function.BiConsumer; +import java.util.function.Consumer; +import javax.swing.BorderFactory; +import javax.swing.BoxLayout; +import javax.swing.JButton; +import javax.swing.JCheckBox; +import javax.swing.JComponent; +import javax.swing.JMenuItem; +import javax.swing.JPanel; +import javax.swing.JPopupMenu; +import javax.swing.JScrollPane; +import javax.swing.JTextField; +import javax.swing.JTree; +import javax.swing.tree.DefaultMutableTreeNode; +import javax.swing.tree.DefaultTreeModel; +import javax.swing.tree.TreePath; +import javax.swing.tree.TreeSelectionModel; + +import org.key_project.rusty.proof.Goal; +import org.key_project.rusty.proof.Node; +import org.key_project.rusty.proof.Proof; + +/// A linearized proof-tree view (see [#buildBranch]) with the KeY-Java hide filters: hide +/// intermediate steps, show only interactive steps, hide closed subtrees and hide subtrees with no +/// automatic goals. Selecting a tree node updates the [ProofContext]; the view re-syncs when the +/// context changes. +public final class ProofTreePanel extends JPanel implements ProofContext.Listener { + + private final ProofContext context; + private final JTree tree = new JTree(new DefaultMutableTreeNode("(no proof)")); + private final Map nodeToTreeNode = new HashMap<>(); + private boolean syncing; + private @org.jspecify.annotations.Nullable Consumer<@org.jspecify.annotations.Nullable Node> hoverListener; + private @org.jspecify.annotations.Nullable BiConsumer openNodeListener; + private @org.jspecify.annotations.Nullable Consumer pruneListener; + + // Hide filters (mirroring de.uka.ilkd.key.gui.prooftree.ProofTreeViewFilter). + private boolean hideIntermediate; + private boolean onlyInteractive; + private boolean hideClosed; + private boolean hideNonAutomaticGoals; + + public ProofTreePanel(ProofContext context) { + super(new BorderLayout()); + this.context = context; + tree.getSelectionModel().setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION); + tree.setRootVisible(true); + tree.addTreeSelectionListener(e -> { + if (syncing) { + return; + } + if (tree.getLastSelectedPathComponent() instanceof DefaultMutableTreeNode dmtn) { + Object userObject = dmtn.getUserObject(); + if (userObject instanceof NodeRef ref) { + context.setSelectedNode(ref.node()); + } else if (userObject instanceof BranchRef branch) { + context.setSelectedNode(branch.node()); + } + } + }); + tree.addMouseMotionListener(new MouseMotionAdapter() { + @Override + public void mouseMoved(MouseEvent e) { + if (hoverListener != null) { + hoverListener.accept(nodeAt(e.getX(), e.getY())); + } + } + }); + tree.addMouseListener(new MouseAdapter() { + @Override + public void mousePressed(MouseEvent e) { + maybeShowOpenMenu(e); + } + + @Override + public void mouseReleased(MouseEvent e) { + maybeShowOpenMenu(e); + } + }); + add(buildToolbar(), BorderLayout.NORTH); + add(new JScrollPane(tree), BorderLayout.CENTER); + // Let the split divider shrink this pane to whatever the tree needs, not to the width the + // toolbar's controls would otherwise demand. + setMinimumSize(new Dimension(120, 0)); + context.addListener(this); + } + + /// Registers a listener notified about the node under the cursor as the user hovers the tree + /// (used to feed the node-info view); `null` when no node is under the cursor. + public void setHoverListener(Consumer<@org.jspecify.annotations.Nullable Node> listener) { + this.hoverListener = listener; + } + + /// Registers the action invoked from the node's right-click menu to open it in the editor. The + /// boolean is `true` when the node should open to the side (a new editor split) rather than as + /// a + /// tab in the current group. + public void setOpenNodeListener(BiConsumer listener) { + this.openNodeListener = listener; + } + + /// Registers the action invoked from an inner node's right-click menu to prune the proof there. + public void setPruneListener(Consumer listener) { + this.pruneListener = listener; + } + + private void maybeShowOpenMenu(MouseEvent e) { + if (!e.isPopupTrigger() || openNodeListener == null) { + return; + } + Node node = nodeAt(e.getX(), e.getY()); + if (node == null) { + return; + } + context.setSelectedNode(node); + JPopupMenu menu = new JPopupMenu(); + JMenuItem open = new JMenuItem("Open node " + node.getSerialNr() + " in a tab"); + open.addActionListener(ev -> openNodeListener.accept(node, false)); + JMenuItem openSide = new JMenuItem("Open node " + node.getSerialNr() + " to the side"); + openSide.addActionListener(ev -> openNodeListener.accept(node, true)); + menu.add(open); + menu.add(openSide); + // Pruning only makes sense at an inner node (it drops the subtree below it). + if (pruneListener != null && node.childrenCount() > 0) { + menu.addSeparator(); + JMenuItem prune = new JMenuItem("Prune proof at node " + node.getSerialNr()); + prune.addActionListener(ev -> pruneListener.accept(node)); + menu.add(prune); + } + menu.show(tree, e.getX(), e.getY()); + } + + private @org.jspecify.annotations.Nullable Node nodeAt(int x, int y) { + TreePath path = tree.getPathForLocation(x, y); + if (path != null + && path.getLastPathComponent() instanceof DefaultMutableTreeNode dmtn) { + Object userObject = dmtn.getUserObject(); + if (userObject instanceof NodeRef ref) { + return ref.node(); + } + if (userObject instanceof BranchRef branch) { + return branch.node(); + } + } + return null; + } + + /// A compact toolbar grounded by a hairline: an icon row (magnifier + "Filter ▾"), with the + /// search field and the filter checkboxes each in their own full-width row below, shown only + /// when their button is toggled. The filters are plain checkboxes (you can flip several at + /// once) + /// rather than a popup menu that closes after each click. + private JPanel buildToolbar() { + JPanel top = new JPanel(new BorderLayout(0, 4)); + top.setBorder(BorderFactory.createCompoundBorder( + BorderFactory.createMatteBorder(0, 0, 1, 0, Theme.hairline()), + BorderFactory.createEmptyBorder(3, 6, 3, 6))); + + JComponent searchRow = buildSearchRow(); + JComponent filterRow = buildFilterRow(); + + JButton searchToggle = toolbarButton("🔍", "Search the proof tree"); + searchToggle.addActionListener(e -> toggleRow(top, searchRow)); + JButton filterToggle = toolbarButton("Filter ▾", "Hide filters"); + filterToggle.addActionListener(e -> toggleRow(top, filterRow)); + + JPanel iconRow = new JPanel(new FlowLayout(FlowLayout.LEFT, 4, 0)); + iconRow.setOpaque(false); + iconRow.add(searchToggle); + iconRow.add(filterToggle); + + JPanel expandable = new JPanel(); + expandable.setOpaque(false); + expandable.setLayout(new BoxLayout(expandable, BoxLayout.PAGE_AXIS)); + expandable.add(searchRow); + expandable.add(filterRow); + + top.add(iconRow, BorderLayout.NORTH); + top.add(expandable, BorderLayout.CENTER); + return top; + } + + private void toggleRow(JComponent toolbar, JComponent row) { + boolean show = !row.isVisible(); + row.setVisible(show); + toolbar.revalidate(); + toolbar.repaint(); + if (show) { + row.requestFocusInWindow(); + } + } + + private JComponent buildSearchRow() { + JTextField field = new JTextField(); + field.setToolTipText("Find a node by label"); + JButton prev = new JButton("▲"); + JButton next = new JButton("▼"); + prev.setToolTipText("Previous match"); + next.setToolTipText("Next match"); + for (JButton b : new JButton[] { prev, next }) { + b.setFocusable(false); + b.setMargin(new java.awt.Insets(1, 6, 1, 6)); + } + field.addActionListener(e -> search(field.getText(), true)); // Enter = next match + next.addActionListener(e -> search(field.getText(), true)); + prev.addActionListener(e -> search(field.getText(), false)); + + JPanel matchButtons = new JPanel(new FlowLayout(FlowLayout.LEFT, 2, 0)); + matchButtons.setOpaque(false); + matchButtons.add(prev); + matchButtons.add(next); + + JPanel row = new JPanel(new BorderLayout(4, 0)); + row.setOpaque(false); + row.add(field, BorderLayout.CENTER); // full width of the panel + row.add(matchButtons, BorderLayout.EAST); + row.setAlignmentX(Component.LEFT_ALIGNMENT); + row.setMaximumSize(new Dimension(Integer.MAX_VALUE, row.getPreferredSize().height)); + row.setVisible(false); + return row; + } + + /// A stacked list of filter checkboxes (mirrors + /// de.uka.ilkd.key.gui.prooftree.ProofTreeViewFilter) + /// that fits a narrow pane and lets several be toggled without re-opening. + private JComponent buildFilterRow() { + JPanel row = new JPanel(); + row.setOpaque(false); + row.setLayout(new BoxLayout(row, BoxLayout.PAGE_AXIS)); + row.add(filterCheck("Hide intermediate", v -> hideIntermediate = v)); + row.add(filterCheck("Only interactive", v -> onlyInteractive = v)); + row.add(filterCheck("Hide closed", v -> hideClosed = v)); + row.add(filterCheck("Hide automatic goals", v -> hideNonAutomaticGoals = v)); + row.setAlignmentX(Component.LEFT_ALIGNMENT); + row.setMaximumSize(new Dimension(Integer.MAX_VALUE, row.getPreferredSize().height)); + row.setVisible(false); + return row; + } + + private JCheckBox filterCheck(String label, Consumer setter) { + JCheckBox box = new JCheckBox(label); + box.setOpaque(false); + box.setAlignmentX(Component.LEFT_ALIGNMENT); + box.addActionListener(e -> { + setter.accept(box.isSelected()); + rebuild(); + }); + return box; + } + + private JButton toolbarButton(String label, String tooltip) { + JButton button = new JButton(label); + button.setToolTipText(tooltip); + button.setFocusable(false); + button.setMargin(new java.awt.Insets(2, 6, 2, 6)); + return button; + } + + /// Selects the next/previous tree node (in display order, wrapping around) whose label contains + /// `query` (case-insensitive). Returns whether a match was found. + boolean search(String query, boolean forward) { + String q = query.trim().toLowerCase(); + int rows = tree.getRowCount(); + if (q.isEmpty() || rows == 0) { + return false; + } + int start = Math.max(tree.getLeadSelectionRow(), 0); + for (int k = 1; k <= rows; k++) { + int row = forward ? (start + k) % rows : ((start - k) % rows + rows) % rows; + TreePath path = tree.getPathForRow(row); + if (path != null + && path.getLastPathComponent().toString().toLowerCase().contains(q)) { + tree.setSelectionRow(row); + tree.scrollRowToVisible(row); + return true; + } + } + Toolkit.getDefaultToolkit().beep(); + return false; + } + + /// Package-private access to the underlying tree, for tests. + JTree getTree() { + return tree; + } + + /// Sets the tree's font (family + size). + public void applyFont(java.awt.Font font) { + tree.setFont(font); + tree.setRowHeight(0); // recompute the row height for the new font + } + + /// Package-private filter control, for tests. + void setFilters(boolean intermediate, boolean interactive, boolean closed, boolean autoGoals) { + this.hideIntermediate = intermediate; + this.onlyInteractive = interactive; + this.hideClosed = closed; + this.hideNonAutomaticGoals = autoGoals; + rebuild(); + } + + @Override + public void proofLoaded() { + rebuild(); + } + + @Override + public void proofChanged() { + rebuild(); + } + + @Override + public void selectedNodeChanged() { + Node node = context.getSelectedNode(); + DefaultMutableTreeNode tn = node == null ? null : nodeToTreeNode.get(node); + if (tn == null) { + return; + } + syncing = true; + try { + TreePath path = new TreePath(tn.getPath()); + tree.setSelectionPath(path); + tree.scrollPathToVisible(path); + } finally { + syncing = false; + } + } + + private void rebuild() { + nodeToTreeNode.clear(); + Proof proof = context.getProof(); + DefaultMutableTreeNode root = proof == null ? new DefaultMutableTreeNode("(no proof)") + : buildBranch(proof.root(), "Proof Tree"); + tree.setModel(new DefaultTreeModel(root)); + for (int i = 0; i < tree.getRowCount(); i++) { + tree.expandRow(i); + } + selectedNodeChanged(); + } + + /// Builds one branch of the linearized tree: the maximal linear chain of proof nodes starting + /// at `start` is added as flat leaves, and each child of the chain's final (splitting) node + /// starts a new sub-branch. Nodes hidden by the local filters are dropped from the chain, and + /// sub-branches hidden by the global filters are skipped entirely. + private DefaultMutableTreeNode buildBranch(Node start, String label) { + DefaultMutableTreeNode branch = new DefaultMutableTreeNode(new BranchRef(start, label)); + + List chain = new ArrayList<>(); + Node n = start; + while (true) { + chain.add(n); + if (n.childrenCount() == 1) { + n = n.child(0); + } else { + break; + } + } + Node endpoint = n; + for (Node step : chain) { + if (showChainNode(step, endpoint)) { + DefaultMutableTreeNode leaf = new DefaultMutableTreeNode(new NodeRef(step)); + leaf.setAllowsChildren(false); + nodeToTreeNode.putIfAbsent(step, leaf); + branch.add(leaf); + } else { + // keep the selection resolvable: a hidden step maps to its enclosing branch + nodeToTreeNode.putIfAbsent(step, branch); + } + } + + for (int i = 0; i < endpoint.childrenCount(); i++) { + Node child = endpoint.child(i); + if (hiddenByGlobalFilters(child)) { + continue; + } + String childLabel = child.getNodeInfo().getBranchLabel(); + branch.add(buildBranch(child, childLabel != null ? childLabel : "Case " + (i + 1))); + } + return branch; + } + + /// Whether a node of a linear chain is shown (the chain endpoint is always shown). + private boolean showChainNode(Node step, Node endpoint) { + if (step == endpoint) { + return true; + } + if (onlyInteractive) { + return step.getNodeInfo().getInteractiveRuleApplication(); + } + return !hideIntermediate; + } + + /// Whether the subtree rooted at `node` is hidden by an active global filter. + private boolean hiddenByGlobalFilters(Node node) { + if (hideClosed && node.isClosed()) { + return true; + } + return hideNonAutomaticGoals && !hasAutomaticGoal(node); + } + + private static boolean hasAutomaticGoal(Node node) { + Proof proof = node.proof(); + var goals = proof.getSubtreeGoals(node); + if (goals.isEmpty()) { + return true; // a closed subtree is still shown (matches KeY) + } + for (Goal goal : goals) { + if (goal.isAutomatic()) { + return true; + } + } + return false; + } + + /// Wraps a single proof [Node] (a leaf of the tree); the label is its (single-line) name. + private record NodeRef(Node node) { + @Override + public String toString() { + String name = node.name().replace('\n', ' ').trim(); + return node.getSerialNr() + ": " + name; + } + } + + /// Wraps a proof branch (its first node and a label); shown as an inner tree node. A closed + /// branch is marked. + private record BranchRef(Node node, String label) { + @Override + public String toString() { + String shown = node.getNodeInfo().getBranchLabel(); + String base = shown != null ? shown : label; + return node.isClosed() ? base + " ✓" : base; + } + } +} diff --git a/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/RustyMain.java b/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/RustyMain.java new file mode 100644 index 00000000000..35945d29c65 --- /dev/null +++ b/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/RustyMain.java @@ -0,0 +1,34 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package org.key_project.rusty.gui; + +import javax.swing.SwingUtilities; +import javax.swing.UIManager; + +import com.formdev.flatlaf.FlatLightLaf; + +/// Entry point of KeYther, the minimal Rusty prover GUI. +public final class RustyMain { + + private RustyMain() {} + + public static void main(String[] args) { + SwingUtilities.invokeLater(() -> { + // A modern, flat cross-platform look (away from the native Aqua/Metal styling). + try { + UIManager.put("Component.focusWidth", 1); + UIManager.put("TabbedPane.tabType", "card"); + UIManager.put("ScrollBar.showButtons", false); + FlatLightLaf.setup(); + } catch (Exception ex) { + try { + UIManager.setLookAndFeel(UIManager.getSystemLookAndFeelClassName()); + } catch (Exception ignored) { + // fall back to the default look and feel + } + } + new MainWindow().setVisible(true); + }); + } +} diff --git a/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/SequentView.java b/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/SequentView.java new file mode 100644 index 00000000000..b9db705d020 --- /dev/null +++ b/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/SequentView.java @@ -0,0 +1,443 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package org.key_project.rusty.gui; + +import java.awt.BorderLayout; +import java.awt.Color; +import java.awt.Font; +import java.awt.Toolkit; +import java.awt.datatransfer.StringSelection; +import java.awt.event.MouseAdapter; +import java.awt.event.MouseEvent; +import java.util.ArrayList; +import java.util.Comparator; +import java.util.List; +import javax.swing.BorderFactory; +import javax.swing.JComponent; +import javax.swing.JLabel; +import javax.swing.JMenu; +import javax.swing.JMenuItem; +import javax.swing.JOptionPane; +import javax.swing.JPanel; +import javax.swing.JPopupMenu; +import javax.swing.JScrollPane; +import javax.swing.JTextArea; +import javax.swing.SwingUtilities; +import javax.swing.text.BadLocationException; +import javax.swing.text.DefaultHighlighter; +import javax.swing.text.Highlighter; + +import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.rusty.Services; +import org.key_project.rusty.pp.IdentitySequentPrintFilter; +import org.key_project.rusty.pp.InitialPositionTable; +import org.key_project.rusty.pp.LogicPrinter; +import org.key_project.rusty.pp.NotationInfo; +import org.key_project.rusty.pp.PosInSequent; +import org.key_project.rusty.pp.PosTableLayouter; +import org.key_project.rusty.pp.Range; +import org.key_project.rusty.proof.Goal; +import org.key_project.rusty.proof.Node; +import org.key_project.rusty.proof.Proof; +import org.key_project.rusty.rule.FindTaclet; +import org.key_project.rusty.rule.NoPosTacletApp; +import org.key_project.rusty.rule.TacletApp; + +import org.jspecify.annotations.Nullable; + +/// Shows the sequent of the selected node (inner or leaf). A small header carries the node/rule +/// info; the sequent itself is rendered with the position-table printer so a left-click maps to the +/// term under the cursor and offers the applicable taclets of an open goal in a popup. Taclets with +/// open schema variables are completed via the [TacletCompletionDialog] before being applied. +public final class SequentView extends JPanel implements ProofContext.Listener { + + private final ProofContext context; + private final JLabel header = new JLabel(" "); + private final JTextArea text = new JTextArea(); + private final IdentitySequentPrintFilter filter = new IdentitySequentPrintFilter(); + + private final Highlighter.HighlightPainter painter = + new DefaultHighlighter.DefaultHighlightPainter(Theme.selection()); + private @Nullable Object highlightTag; + + private @Nullable InitialPositionTable positionTable; + private @Nullable Node node; + private @Nullable Runnable runProverAction; + + /// When pinned to a node this view shows that node; otherwise it follows the selection. + private @Nullable Node pinnedNode; + private boolean follow = true; + private Font contentFont = new Font(Font.MONOSPACED, Font.PLAIN, 13); + private final Color normalForeground; + + public SequentView(ProofContext context) { + super(new BorderLayout()); + this.context = context; + + // Cut from the same cloth as the tool-window title bars (same surface + hairline) so the + // editor reads as part of the family, but carries node/rule data rather than a label. + header.setOpaque(true); + header.setBackground(Theme.surface()); + header.setBorder(BorderFactory.createCompoundBorder( + BorderFactory.createMatteBorder(0, 0, 1, 0, Theme.hairline()), + BorderFactory.createEmptyBorder(4, 8, 4, 8))); + + text.setEditable(false); + // No text caret: the hover highlight already shows the focused term, and a blinking caret + // next to it is just noise. Making the area non-focusable suppresses the caret while mouse + // highlighting and the popup keep working. + text.setFocusable(false); + text.setFont(contentFont); + text.setMargin(new java.awt.Insets(6, 8, 6, 8)); + normalForeground = text.getForeground(); + MouseAdapter mouse = new MouseAdapter() { + @Override + public void mouseClicked(MouseEvent e) { + if (SwingUtilities.isLeftMouseButton(e)) { + showTacletPopup(e); + } + } + + @Override + public void mousePressed(MouseEvent e) { + if (e.isPopupTrigger()) { + showContextMenu(e); + } + } + + @Override + public void mouseReleased(MouseEvent e) { + if (e.isPopupTrigger()) { + showContextMenu(e); + } + } + + @Override + public void mouseMoved(MouseEvent e) { + highlightAt(text.viewToModel2D(e.getPoint())); + } + + @Override + public void mouseExited(MouseEvent e) { + clearHighlight(); + } + }; + text.addMouseListener(mouse); + text.addMouseMotionListener(mouse); + + add(header, BorderLayout.NORTH); + add(new JScrollPane(text), BorderLayout.CENTER); + context.addListener(this); + render(); // show the empty-state hint until a proof is loaded + } + + /// Highlights the term/formula whose printed range contains `offset` (the lowest such subterm), + /// or clears the highlight when `offset` does not point inside a term. + private void highlightAt(int offset) { + if (positionTable == null) { + clearHighlight(); + return; + } + PosInSequent pis = positionTable.getPosInSequent(offset, filter); + if (pis == null || pis.isSequent() || pis.getBounds() == null) { + clearHighlight(); + return; + } + var bounds = pis.getBounds(); + try { + clearHighlight(); + highlightTag = + text.getHighlighter().addHighlight(bounds.start(), bounds.end(), painter); + } catch (BadLocationException ignored) { + // range no longer valid (e.g. just re-rendered); ignore + } + } + + private void clearHighlight() { + if (highlightTag != null) { + text.getHighlighter().removeHighlight(highlightTag); + highlightTag = null; + } + } + + @Override + public void selectedNodeChanged() { + render(); + } + + @Override + public void proofLoaded() { + render(); + } + + @Override + public void proofChanged() { + render(); + } + + /// Pins this view to a specific node (it stops following the selection). + public void pinTo(Node node) { + this.pinnedNode = node; + this.follow = false; + render(); + } + + /// A short title for this view's editor tab: the pinned node, or the live selection. + public String tabTitle() { + return pinnedNode != null ? "Node " + pinnedNode.getSerialNr() : "Selection"; + } + + /// The node this view is pinned to, or `null` when it follows the selection. + public @Nullable Node pinnedNode() { + return pinnedNode; + } + + private void render() { + highlightTag = null; // setText below drops all highlights + node = follow ? context.getSelectedNode() : pinnedNode; + if (node == null) { + header.setText(" "); + // A quiet, non-monospace hint — clearly chrome, not a sequent to be read. + text.setForeground(Theme.mutedText()); + text.setFont( + new Font(Font.SANS_SERIF, Font.ITALIC, Math.max(contentFont.getSize(), 13))); + text.setText("\n Open a .key problem or .proof to begin.\n\n" + + " Use File ▸ Open, or the Open button in the toolbar."); + text.setCaretPosition(0); + positionTable = null; + return; + } + // Real content: prominent, in the configured font and normal colour. + text.setForeground(normalForeground); + text.setFont(contentFont); + boolean goal = goalFor(node) != null; + StringBuilder head = new StringBuilder("Node ").append(node.getSerialNr()) + .append(" • ").append(goal ? "open goal" : "inner node"); + if (node.getAppliedRuleApp() != null) { + head.append(" • rule: ").append(node.getAppliedRuleApp().rule().name()); + } + header.setText(head.toString()); + + Services services = node.proof().getServices(); + PosTableLayouter layouter = PosTableLayouter.positionTable(80); + LogicPrinter printer = new LogicPrinter(new NotationInfo(), services, layouter); + printer.printSequent(node.sequent()); + text.setText(printer.result()); + positionTable = layouter.getInitialPositionTable(); + filter.setSequent(node.sequent()); + text.setCaretPosition(0); + } + + /// Left-click popup: the taclets applicable to the formula/term under the cursor. + private void showTacletPopup(MouseEvent e) { + if (positionTable == null || node == null) { + return; + } + Goal goal = goalFor(node); + JPopupMenu menu = new JPopupMenu(); + if (goal == null) { + JMenuItem item = new JMenuItem("(not an open goal)"); + item.setEnabled(false); + menu.add(item); + menu.show(text, e.getX(), e.getY()); + return; + } + + int offset = text.viewToModel2D(e.getPoint()); + highlightAt(offset); // show what the popup targets + PosInSequent pis = positionTable.getPosInSequent(offset, filter); + PosInOccurrence occ = pis == null ? null : pis.getPosInOccurrence(); + + // Rules that apply to the clicked formula/term go first, most-specific match (deepest find + // pattern) on top; the sequent-wide (no-find) rules are tucked away in a submenu so they do + // not bury the term-specific ones. + List termApps = applicableTaclets(goal, occ); + termApps.sort(BY_SPECIFICITY); + List sequentApps = noFindTaclets(goal); + sequentApps.sort(BY_SPECIFICITY); + if (termApps.isEmpty() && sequentApps.isEmpty()) { + JMenuItem item = new JMenuItem("(no applicable rules here)"); + item.setEnabled(false); + menu.add(item); + } else if (termApps.isEmpty()) { + // Whole-sequent selection: no term-specific rules to bury, so show the sequent rules + // directly (chunked into submenus only when there are too many). + addTacletItems(menu, sequentApps, goal, null); + } else { + addTacletItems(menu, termApps, goal, occ); + if (!sequentApps.isEmpty()) { + // A term was clicked: tuck the sequent-wide rules away so they do not bury the + // term-specific ones. + menu.addSeparator(); + JMenu sequentMenu = new JMenu("Sequent rules"); + addTacletItems(sequentMenu, sequentApps, goal, null); + menu.add(sequentMenu); + } + } + menu.show(text, e.getX(), e.getY()); + } + + /// Orders taclet applications by most specific match first (deepest find pattern), breaking + /// ties + /// alphabetically by display name. + private static final Comparator BY_SPECIFICITY = + Comparator.comparingInt(SequentView::specificity).reversed() + .thenComparing(app -> app.rule().displayName()); + + /// A specificity score for ordering: the depth of the taclet's find pattern (no-find taclets, + /// which match the whole sequent, score 0 — the least specific). + private static int specificity(TacletApp app) { + return app.taclet() instanceof FindTaclet find ? find.find().depth() : 0; + } + + /// Adds the apps to `parent`, never showing more than six taclets in one menu: when there are + /// more, the five most specific stay and the rest nest under a "More rules…" submenu + /// (recursively + /// chunked the same way). + private void addTacletItems(JComponent parent, List apps, Goal goal, + @Nullable PosInOccurrence occ) { + if (apps.size() <= 6) { + for (TacletApp app : apps) { + parent.add(tacletItem(app, goal, occ)); + } + return; + } + for (int i = 0; i < 5; i++) { + parent.add(tacletItem(apps.get(i), goal, occ)); + } + JMenu more = new JMenu("More rules…"); + addTacletItems(more, apps.subList(5, apps.size()), goal, occ); + parent.add(more); + } + + private JMenuItem tacletItem(TacletApp app, Goal goal, @Nullable PosInOccurrence occ) { + JMenuItem item = new JMenuItem(app.rule().displayName()); + item.addActionListener(ev -> applyTaclet(app, goal, occ)); + return item; + } + + /// Right-click context menu: general actions (run the prover, copy the term under the cursor). + private void showContextMenu(MouseEvent e) { + if (node == null) { + return; + } + int offset = text.viewToModel2D(e.getPoint()); + highlightAt(offset); + JPopupMenu menu = new JPopupMenu(); + + JMenuItem run = new JMenuItem("Run prover"); + run.setEnabled(runProverAction != null && context.getProof() != null); + run.addActionListener(ev -> { + if (runProverAction != null) { + runProverAction.run(); + } + }); + menu.add(run); + + JMenuItem copy = new JMenuItem("Copy term"); + copy.addActionListener(ev -> copyTerm(offset)); + menu.add(copy); + + menu.show(text, e.getX(), e.getY()); + } + + /// Copies the printed text of the term/formula under `offset` (or the whole sequent if the + /// offset is not inside a term) to the system clipboard. + private void copyTerm(int offset) { + String content = text.getText(); + if (positionTable != null) { + PosInSequent pis = positionTable.getPosInSequent(offset, filter); + if (pis != null && pis.getBounds() != null) { + Range b = pis.getBounds(); + content = content.substring(b.start(), b.end()); + } + } + Toolkit.getDefaultToolkit().getSystemClipboard() + .setContents(new StringSelection(content), null); + } + + /// Sets the action invoked by the context menu's "Run prover" entry (wired by the main window). + public void setRunProverAction(@Nullable Runnable runProverAction) { + this.runProverAction = runProverAction; + } + + /// Sets the font (family + size) of the sequent text. + public void applyFont(Font font) { + this.contentFont = font; + render(); // re-applies the right font/colour for content vs. the empty-state hint + } + + /// The open goal sitting on `node`, or `null` if `node` is not an open goal. + private @Nullable Goal goalFor(Node node) { + Proof proof = context.getProof(); + if (proof == null) { + return null; + } + for (Goal g : proof.openGoals()) { + if (g.getNode() == node) { + return g; + } + } + return null; + } + + /// The find-taclet applications at `occ` (the rules that apply to the formula/term under the + /// cursor). Applications with open schema variables are included; they are completed via the + /// taclet-completion dialog when chosen. + List applicableTaclets(Goal goal, @Nullable PosInOccurrence occ) { + List result = new ArrayList<>(); + if (occ != null) { + Services services = goal.getOverlayServices(); + for (TacletApp app : goal.ruleAppIndex().getTacletAppAt(occ, services)) { + result.add(app); + } + } + return result; + } + + /// The no-find (sequent-wide) taclet applications, e.g. cut (which is completed via the + /// dialog). + List noFindTaclets(Goal goal) { + List result = new ArrayList<>(); + for (NoPosTacletApp app : goal.ruleAppIndex().getNoFindTaclet(goal.getOverlayServices())) { + result.add(app); + } + return result; + } + + /// Applies a taclet to the goal, refreshing the views. If the application still has open schema + /// variables, the taclet-completion dialog is shown first; cancelling it aborts the + /// application. + void applyTaclet(TacletApp app, Goal goal, @Nullable PosInOccurrence occ) { + try { + TacletApp toApply = occ != null ? app.setPosInOccurrence(occ, goal.getOverlayServices()) + : app; + if (!toApply.complete()) { + TacletApp completed = TacletCompletionDialog.completeApp(this, toApply, goal); + if (completed == null) { + return; // cancelled or invalid + } + toApply = completed; + } + goal.apply(toApply); + context.fireProofChanged(); + context.setSelectedNode(goal.getNode()); + } catch (Exception ex) { + JOptionPane.showMessageDialog(this, + "Could not apply " + app.rule().displayName() + ":\n" + + ex.getMessage(), + "Rule application failed", JOptionPane.ERROR_MESSAGE); + } + } + + /// Package-private accessors for tests. + String renderedText() { + return text.getText(); + } + + @Nullable + PosInSequent posAt(int offset) { + return positionTable == null ? null : positionTable.getPosInSequent(offset, filter); + } +} diff --git a/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/StrategyView.java b/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/StrategyView.java new file mode 100644 index 00000000000..8a152752474 --- /dev/null +++ b/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/StrategyView.java @@ -0,0 +1,250 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package org.key_project.rusty.gui; + +import java.awt.BorderLayout; +import java.awt.Component; +import java.awt.Dimension; +import java.awt.Rectangle; +import java.util.ArrayList; +import java.util.List; +import javax.swing.BorderFactory; +import javax.swing.Box; +import javax.swing.BoxLayout; +import javax.swing.JComboBox; +import javax.swing.JComponent; +import javax.swing.JLabel; +import javax.swing.JPanel; +import javax.swing.JScrollPane; +import javax.swing.JSpinner; +import javax.swing.Scrollable; +import javax.swing.SpinnerNumberModel; + +import org.key_project.rusty.proof.Proof; +import org.key_project.rusty.settings.StrategySettings; +import org.key_project.rusty.strategy.StrategyProperties; + +import org.jspecify.annotations.Nullable; + +import static org.key_project.rusty.strategy.StrategyProperties.FUNCTION_CONTRACT; +import static org.key_project.rusty.strategy.StrategyProperties.FUNCTION_EXPAND; +import static org.key_project.rusty.strategy.StrategyProperties.FUNCTION_NONE; +import static org.key_project.rusty.strategy.StrategyProperties.FUNCTION_OPTIONS_KEY; +import static org.key_project.rusty.strategy.StrategyProperties.NON_LIN_ARITH_COMPLETION; +import static org.key_project.rusty.strategy.StrategyProperties.NON_LIN_ARITH_DEF_OPS; +import static org.key_project.rusty.strategy.StrategyProperties.NON_LIN_ARITH_NONE; +import static org.key_project.rusty.strategy.StrategyProperties.NON_LIN_ARITH_OPTIONS_KEY; +import static org.key_project.rusty.strategy.StrategyProperties.SPLITTING_DELAYED; +import static org.key_project.rusty.strategy.StrategyProperties.SPLITTING_NORMAL; +import static org.key_project.rusty.strategy.StrategyProperties.SPLITTING_OFF; +import static org.key_project.rusty.strategy.StrategyProperties.SPLITTING_OPTIONS_KEY; +import static org.key_project.rusty.strategy.StrategyProperties.STOPMODE_DEFAULT; +import static org.key_project.rusty.strategy.StrategyProperties.STOPMODE_NONCLOSE; +import static org.key_project.rusty.strategy.StrategyProperties.STOPMODE_OPTIONS_KEY; + +/// An always-visible tool window for the automatic proof search of the current proof: it shows the +/// live strategy settings (max rule applications, timeout, and the main option groups) and writes +/// every edit straight back to the proof's settings, so there is no open/apply round-trip. It +/// repopulates whenever a proof is loaded and disables itself when none is open. +public final class StrategyView extends JPanel implements ProofContext.Listener { + + /// A single multiple-choice strategy option (a property key and its labelled values). + private record Choice(String label, String key, String[] values, String[] valueLabels) { + } + + private static final Choice[] CHOICES = { + new Choice("Stop at", STOPMODE_OPTIONS_KEY, + new String[] { STOPMODE_DEFAULT, STOPMODE_NONCLOSE }, + new String[] { "Default", "Unclosable goal" }), + new Choice("Splitting", SPLITTING_OPTIONS_KEY, + new String[] { SPLITTING_NORMAL, SPLITTING_DELAYED, SPLITTING_OFF }, + new String[] { "Normal", "Delayed", "Off" }), + new Choice("Functions", FUNCTION_OPTIONS_KEY, + new String[] { FUNCTION_EXPAND, FUNCTION_CONTRACT, FUNCTION_NONE }, + new String[] { "Expand", "Contract", "None" }), + new Choice("Arithmetic", NON_LIN_ARITH_OPTIONS_KEY, + new String[] { NON_LIN_ARITH_NONE, NON_LIN_ARITH_DEF_OPS, NON_LIN_ARITH_COMPLETION }, + new String[] { "Basic", "DefOps", "Model search" }), + }; + + private final ProofContext context; + private final JSpinner maxSteps = + new JSpinner(new SpinnerNumberModel(0, 0, 1_000_000, 100)); + private final JSpinner timeout = + new JSpinner(new SpinnerNumberModel(-1.0, -1.0, Long.MAX_VALUE, 1000)); + private final List> combos = new ArrayList<>(); + private final List controls = new ArrayList<>(); + + /// Guards the change listeners while the controls are repopulated from the settings. + private boolean loading; + + /// While an auto-mode run is in progress the controls are locked, so a live edit can never + /// mutate the settings the prover thread is reading. + private boolean running; + + public StrategyView(ProofContext context) { + super(new BorderLayout()); + this.context = context; + + // Stack the label above its control so each row only needs the width of one control: the + // pane stays usable when narrow instead of forcing a horizontal scrollbar. The form tracks + // the viewport width (see ScrollableForm) so the controls shrink to fit and are never + // clipped on the right. + JPanel form = new ScrollableForm(); + form.setLayout(new BoxLayout(form, BoxLayout.PAGE_AXIS)); + form.setBorder(BorderFactory.createEmptyBorder(8, 8, 8, 8)); + + maxSteps.addChangeListener(e -> applyMaxSteps()); + addGroup(form, "Max. rule apps", maxSteps); + controls.add(maxSteps); + + timeout.addChangeListener(e -> applyTimeout()); + timeout.setToolTipText("Timeout in ms; -1 disables it"); + addGroup(form, "Timeout (ms)", timeout); + controls.add(timeout); + + for (Choice c : CHOICES) { + JComboBox combo = new JComboBox<>(c.valueLabels()); + int index = combos.size(); + combo.addActionListener(e -> applyChoice(index)); + combos.add(combo); + controls.add(combo); + addGroup(form, c.label(), combo); + } + + form.add(Box.createVerticalGlue()); // keep the groups pinned to the top + + // No horizontal scrollbar: groups always fit the pane width. + add(new JScrollPane(form, JScrollPane.VERTICAL_SCROLLBAR_AS_NEEDED, + JScrollPane.HORIZONTAL_SCROLLBAR_NEVER), BorderLayout.CENTER); + + // Let the divider drag this pane narrow; it does not demand a wide minimum. + setMinimumSize(new Dimension(150, 0)); + + context.addListener(this); + load(); + } + + @Override + public void proofLoaded() { + load(); + } + + /// Locks the controls while an auto-mode run is in progress and restores them afterwards. + public void setRunning(boolean running) { + this.running = running; + updateEnabled(); + } + + private void addGroup(JPanel form, String label, JComponent field) { + JPanel group = new JPanel(new BorderLayout(0, 2)); + group.setAlignmentX(Component.LEFT_ALIGNMENT); + group.add(new JLabel(label), BorderLayout.NORTH); + group.add(field, BorderLayout.CENTER); + // Let the group grow horizontally but never stretch vertically. + group.setMaximumSize(new Dimension(Integer.MAX_VALUE, group.getPreferredSize().height)); + form.add(group); + form.add(Box.createVerticalStrut(10)); + } + + private @Nullable StrategySettings settings() { + Proof proof = context.getProof(); + return proof == null ? null : proof.getSettings().getStrategySettings(); + } + + /// Repopulates the controls from the current proof's settings (or disables them if none). + private void load() { + StrategySettings settings = settings(); + if (settings != null) { + loading = true; + try { + maxSteps.setValue(Math.max(settings.getMaxSteps(), 0)); + timeout.setValue((double) settings.getTimeout()); + StrategyProperties props = settings.getActiveStrategyProperties(); + for (int i = 0; i < CHOICES.length; i++) { + combos.get(i).setSelectedIndex( + indexOf(CHOICES[i], props.getProperty(CHOICES[i].key()))); + } + } finally { + loading = false; + } + } + updateEnabled(); + } + + private void applyMaxSteps() { + StrategySettings settings = liveSettings(); + if (settings != null) { + settings.setMaxSteps((Integer) maxSteps.getValue()); + } + } + + private void applyTimeout() { + StrategySettings settings = liveSettings(); + if (settings != null) { + settings.setTimeout(((Number) timeout.getValue()).longValue()); + } + } + + private void applyChoice(int i) { + StrategySettings settings = liveSettings(); + if (settings == null) { + return; + } + StrategyProperties props = settings.getActiveStrategyProperties(); + props.setProperty(CHOICES[i].key(), CHOICES[i].values()[combos.get(i).getSelectedIndex()]); + settings.setActiveStrategyProperties(props); + } + + /// The settings to write to from a user edit, or `null` while repopulating or with no proof. + private @Nullable StrategySettings liveSettings() { + return loading ? null : settings(); + } + + /// Controls are usable only when a proof is open and no run is in progress. + private void updateEnabled() { + boolean enabled = !running && settings() != null; + for (JComponent control : controls) { + control.setEnabled(enabled); + } + } + + private static int indexOf(Choice c, String value) { + for (int i = 0; i < c.values().length; i++) { + if (c.values()[i].equals(value)) { + return i; + } + } + return 0; + } + + /// A form panel that is as wide as the scroll viewport (never wider), so its controls shrink to + /// fit the pane and are never clipped on the right; it still scrolls vertically when too tall. + private static final class ScrollableForm extends JPanel implements Scrollable { + @Override + public Dimension getPreferredScrollableViewportSize() { + return getPreferredSize(); + } + + @Override + public int getScrollableUnitIncrement(Rectangle visible, int orientation, int direction) { + return 16; + } + + @Override + public int getScrollableBlockIncrement(Rectangle visible, int orientation, int direction) { + return Math.max(visible.height - 16, 16); + } + + @Override + public boolean getScrollableTracksViewportWidth() { + return true; + } + + @Override + public boolean getScrollableTracksViewportHeight() { + return false; + } + } +} diff --git a/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/TacletCompletionDialog.java b/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/TacletCompletionDialog.java new file mode 100644 index 00000000000..455c377a32c --- /dev/null +++ b/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/TacletCompletionDialog.java @@ -0,0 +1,382 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package org.key_project.rusty.gui; + +import java.awt.BorderLayout; +import java.awt.Color; +import java.awt.Component; +import java.awt.Dimension; +import java.awt.Font; +import java.awt.GridBagConstraints; +import java.awt.GridBagLayout; +import java.awt.Insets; +import java.awt.Window; +import java.util.ArrayList; +import java.util.List; +import javax.swing.BorderFactory; +import javax.swing.Box; +import javax.swing.BoxLayout; +import javax.swing.JButton; +import javax.swing.JComponent; +import javax.swing.JDialog; +import javax.swing.JLabel; +import javax.swing.JOptionPane; +import javax.swing.JPanel; +import javax.swing.JScrollPane; +import javax.swing.JSeparator; +import javax.swing.JTextArea; +import javax.swing.JTextField; +import javax.swing.SwingUtilities; +import javax.swing.Timer; +import javax.swing.event.DocumentEvent; +import javax.swing.event.DocumentListener; + +import org.key_project.logic.op.sv.SchemaVariable; +import org.key_project.prover.sequent.FormulaChangeInfo; +import org.key_project.prover.sequent.SequentChangeInfo; +import org.key_project.prover.sequent.SequentFormula; +import org.key_project.rusty.Services; +import org.key_project.rusty.logic.op.sv.ModalOperatorSV; +import org.key_project.rusty.logic.op.sv.ProgramSV; +import org.key_project.rusty.logic.op.sv.VariableSV; +import org.key_project.rusty.proof.Goal; +import org.key_project.rusty.proof.io.IntermediateProofReplayer; +import org.key_project.rusty.proof.io.OutputStreamProofSaver; +import org.key_project.rusty.rule.TacletApp; +import org.key_project.rusty.rule.TacletExecutor; +import org.key_project.util.collection.ImmutableList; + +import org.jspecify.annotations.Nullable; + +/// A modal dialog to complete the open schema-variable instantiations of a taclet application +/// before +/// it is applied. On the left it shows the rule's definition and a typed input field per +/// uninstantiated schema variable; on the right it shows a *live result preview* of the sequents +/// the +/// application would produce (with added/removed/modified formulas diffed). The preview is computed +/// side-effect-free via [TacletExecutor#getResultSequentChanges] (never `Goal.apply`), so it never +/// touches the proof. On apply the completed application is returned (or `null` when cancelled). +final class TacletCompletionDialog extends JDialog { + + private static final Color ADDED = new Color(0x1D, 0x9E, 0x75); + private static final Color REMOVED = new Color(0xC0, 0x39, 0x2B); + + private final TacletApp app; + private final Goal goal; + private final List svs = new ArrayList<>(); + private final List fields = new ArrayList<>(); + private final JLabel status = new JLabel(" "); + private final JButton apply = new JButton("Apply"); + private final JPanel previewBody = new JPanel(); + private final Timer debounce = new Timer(150, e -> validateInputs()); + private @Nullable TacletApp result; + + private TacletCompletionDialog(@Nullable Window owner, TacletApp app, Goal goal) { + super(owner, "Complete taclet: " + app.taclet().name(), ModalityType.APPLICATION_MODAL); + this.app = app; + this.goal = goal; + debounce.setRepeats(false); + + JPanel left = new JPanel(new BorderLayout(0, 10)); + left.setBorder(BorderFactory.createEmptyBorder(12, 12, 12, 6)); + left.add(buildRuleSection(), BorderLayout.NORTH); + left.add(buildInstantiateSection(), BorderLayout.CENTER); + + apply.addActionListener(e -> onApply()); + JButton cancel = new JButton("Cancel"); + cancel.addActionListener(e -> dispose()); + status.setForeground(Theme.mutedText()); + JPanel south = new JPanel(new BorderLayout()); + south.setBorder(BorderFactory.createEmptyBorder(8, 12, 12, 12)); + south.add(status, BorderLayout.WEST); + JPanel buttons = new JPanel(); + buttons.setLayout(new BoxLayout(buttons, BoxLayout.LINE_AXIS)); + buttons.add(cancel); + buttons.add(Box.createHorizontalStrut(6)); + buttons.add(apply); + south.add(buttons, BorderLayout.EAST); + + javax.swing.JSplitPane split = new javax.swing.JSplitPane( + javax.swing.JSplitPane.HORIZONTAL_SPLIT, left, buildPreviewSection()); + split.setResizeWeight(0.55); + + add(split, BorderLayout.CENTER); + add(south, BorderLayout.SOUTH); + getRootPane().setDefaultButton(apply); + validateInputs(); + setSize(880, 560); + setLocationRelativeTo(owner); + SwingUtilities.invokeLater(() -> split.setDividerLocation(0.55)); + } + + /// Opens the dialog for `app` (which still has uninstantiated schema variables) and returns the + /// completed application, or `null` if the user cancelled or the input was invalid. + static @Nullable TacletApp completeApp(Component parent, TacletApp app, Goal goal) { + Window owner = SwingUtilities.getWindowAncestor(parent); + TacletCompletionDialog dialog = new TacletCompletionDialog(owner, app, goal); + dialog.setVisible(true); + return dialog.result; + } + + // ── left column ─────────────────────────────────────────────────────────── + + private JPanel buildRuleSection() { + JPanel section = new JPanel(new BorderLayout(0, 4)); + section.add(sectionLabel("Rule: " + app.taclet().name()), BorderLayout.NORTH); + JTextArea body = new JTextArea(app.taclet().toString()); + body.setEditable(false); + body.setFocusable(false); + body.setFont(new Font(Font.MONOSPACED, Font.PLAIN, 12)); + body.setMargin(new Insets(4, 6, 4, 6)); + JScrollPane scroll = new JScrollPane(body); + scroll.setPreferredSize(new Dimension(420, 150)); + section.add(scroll, BorderLayout.CENTER); + return section; + } + + private JPanel buildInstantiateSection() { + JPanel section = new JPanel(new BorderLayout(0, 4)); + section.add(sectionLabel("Instantiate schema variables"), BorderLayout.NORTH); + + JPanel form = new JPanel(new GridBagLayout()); + GridBagConstraints g = new GridBagConstraints(); + g.insets = new Insets(3, 4, 3, 4); + g.anchor = GridBagConstraints.WEST; + int row = 0; + DocumentListener live = new DocumentListener() { + @Override + public void insertUpdate(DocumentEvent e) { + onEdit(); + } + + @Override + public void removeUpdate(DocumentEvent e) { + onEdit(); + } + + @Override + public void changedUpdate(DocumentEvent e) { + onEdit(); + } + }; + for (SchemaVariable sv : app.uninstantiatedVars()) { + svs.add(sv); + JTextField field = new JTextField(20); + field.getDocument().addDocumentListener(live); + fields.add(field); + g.gridy = row; + g.gridx = 0; + form.add(new JLabel(sv.name() + " (" + kind(sv) + ")"), g); + g.gridx = 1; + g.fill = GridBagConstraints.HORIZONTAL; + g.weightx = 1; + form.add(field, g); + g.fill = GridBagConstraints.NONE; + g.weightx = 0; + row++; + } + JPanel top = new JPanel(new BorderLayout()); + top.add(form, BorderLayout.NORTH); + section.add(new JScrollPane(top), BorderLayout.CENTER); + return section; + } + + // ── right column (preview) ──────────────────────────────────────────────── + + private JPanel buildPreviewSection() { + JPanel section = new JPanel(new BorderLayout(0, 4)); + section.setBorder(BorderFactory.createEmptyBorder(12, 6, 12, 12)); + section.add(sectionLabel("Result preview"), BorderLayout.NORTH); + previewBody.setLayout(new BoxLayout(previewBody, BoxLayout.Y_AXIS)); + JPanel top = new JPanel(new BorderLayout()); + top.add(previewBody, BorderLayout.NORTH); + section.add(new JScrollPane(top), BorderLayout.CENTER); + return section; + } + + /// Single source of truth for the dialog state: parses the current inputs and sets the status + /// line, the Apply button and the preview together. Apply is enabled only when every field + /// parses and the application is complete. + private void validateInputs() { + previewBody.removeAll(); + if (hasEmptyField()) { + setState(Theme.mutedText(), "Enter an instantiation for every schema variable.", false); + previewMessage("Complete the instantiations to preview the result."); + } else { + try { + TacletApp built = parseApp(); + if (!built.complete()) { + setState(Theme.mutedText(), "Some schema variables are still open.", false); + previewMessage("Complete the instantiations to preview the result."); + } else { + setState(Theme.mutedText(), "Ready to apply.", true); + TacletExecutor exec = (TacletExecutor) built.taclet().getExecutor(); + ImmutableList changes = + exec.getResultSequentChanges(goal, built); + if (changes.isEmpty()) { + previewMessage("No preview available for this rule."); + } else { + renderGoals(changes); + } + } + } catch (Exception ex) { + setState(REMOVED, "The instantiation cannot be parsed.", false); + previewMessage("Fix the instantiation to preview the result."); + } + } + previewBody.revalidate(); + previewBody.repaint(); + } + + private boolean hasEmptyField() { + for (JTextField field : fields) { + if (field.getText().trim().isEmpty()) { + return true; + } + } + return false; + } + + private void setState(Color colour, String text, boolean ready) { + status.setForeground(colour); + status.setText(text); + apply.setEnabled(ready); + } + + private void renderGoals(ImmutableList changes) { + Services services = goal.proof().getServices(); + int n = changes.size(); + int i = 1; + for (SequentChangeInfo sci : changes) { + if (i > 1) { + previewBody.add(new JSeparator()); + } + if (n > 1) { + JLabel head = new JLabel("Goal " + i + " of " + n); + head.setForeground(Theme.mutedText()); + head.setBorder(BorderFactory.createEmptyBorder(6, 0, 2, 0)); + previewBody.add(head); + } + renderSide(sci, true, services); + renderSide(sci, false, services); + i++; + } + } + + private void renderSide(SequentChangeInfo sci, boolean antec, Services services) { + ImmutableList removed = sci.removedFormulas(antec); + ImmutableList added = sci.addedFormulas(antec); + ImmutableList modified = sci.modifiedFormulas(antec); + if (removed.isEmpty() && added.isEmpty() && modified.isEmpty()) { + return; + } + JLabel head = new JLabel(antec ? "antecedent" : "succedent"); + head.setForeground(Theme.mutedText()); + head.setBorder(BorderFactory.createEmptyBorder(4, 0, 1, 0)); + previewBody.add(head); + for (SequentFormula f : removed) { + previewBody.add(changeRow("−", REMOVED, f.formula(), services)); + } + for (FormulaChangeInfo m : modified) { + previewBody.add(changeRow("−", REMOVED, m.getOriginalFormula().formula(), services)); + previewBody.add(changeRow("+", ADDED, m.newFormula().formula(), services)); + } + for (SequentFormula f : added) { + previewBody.add(changeRow("+", ADDED, f.formula(), services)); + } + } + + private JComponent changeRow(String marker, Color color, + org.key_project.logic.Term formula, Services services) { + JPanel p = new JPanel(new BorderLayout(6, 0)); + p.setOpaque(false); + JLabel m = new JLabel(marker); + m.setForeground(color); + m.setFont(m.getFont().deriveFont(Font.BOLD)); + m.setBorder(BorderFactory.createEmptyBorder(0, 8, 0, 0)); + p.add(m, BorderLayout.WEST); + String printed = OutputStreamProofSaver.printTerm(formula, services).replace('\n', ' '); + JLabel term = new JLabel(printed); + term.setFont(new Font(Font.MONOSPACED, Font.PLAIN, 12)); + term.setToolTipText(printed); + p.add(term, BorderLayout.CENTER); + return p; + } + + private void previewMessage(String text) { + JLabel l = new JLabel(text); + l.setForeground(Theme.mutedText()); + previewBody.add(l); + } + + // ── shared ──────────────────────────────────────────────────────────────── + + private JLabel sectionLabel(String text) { + JLabel label = new JLabel(text); + label.setFont(label.getFont().deriveFont(Font.BOLD)); + return label; + } + + private static String kind(SchemaVariable sv) { + if (sv.isFormula()) { + return "formula"; + } + if (sv.isVariable()) { + return "variable"; + } + if (sv.isSkolemTerm()) { + return "skolem term"; + } + if (sv instanceof ProgramSV) { + return "program"; + } + if (sv instanceof ModalOperatorSV) { + return "modality"; + } + return "term"; + } + + private void onEdit() { + // Disable Apply until the (debounced) validation confirms the new input parses. + apply.setEnabled(false); + debounce.restart(); + } + + /// Builds the (possibly completed) application from the current field inputs, reusing the + /// proof-replayer's parsing. Throws when an input is missing or cannot be parsed. + private TacletApp parseApp() throws Exception { + Services services = goal.proof().getServices(); + TacletApp current = app; + for (int i = 0; i < svs.size(); i++) { + if (svs.get(i) instanceof VariableSV vsv) { + current = IntermediateProofReplayer.parseSV1(current, vsv, + fields.get(i).getText().trim(), services); + } + } + for (int i = 0; i < svs.size(); i++) { + if (!(svs.get(i) instanceof VariableSV)) { + current = IntermediateProofReplayer.parseSV2(current, svs.get(i), + fields.get(i).getText().trim(), goal); + } + } + return current; + } + + private void onApply() { + try { + TacletApp completed = parseApp(); + if (!completed.complete()) { + status.setForeground(REMOVED); + status.setText("The taclet is still not completely instantiated."); + return; + } + result = completed; + dispose(); + } catch (Exception ex) { + JOptionPane.showMessageDialog(this, + "Could not complete the taclet:\n" + ex.getMessage(), "Invalid instantiation", + JOptionPane.ERROR_MESSAGE); + } + } +} diff --git a/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/Theme.java b/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/Theme.java new file mode 100644 index 00000000000..0f0ce00bbac --- /dev/null +++ b/keyext.rusty.gui/src/main/java/org/key_project/rusty/gui/Theme.java @@ -0,0 +1,59 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package org.key_project.rusty.gui; + +import java.awt.Color; +import javax.swing.UIManager; + +/// Look-and-feel-derived colours for the GUI chrome, so the docked layout adapts to the active +/// theme (light or dark) instead of hardcoding a light palette. Each accessor falls back to a light +/// default when the look and feel does not define the key. +final class Theme { + + private Theme() {} + + /// Surface of the tool-window title bars and the sequent header: a shade nudged away from the + /// plain panel background, so a header reads as a distinct band rather than melding into the + /// flat panels and the split-divider arrows next to it. + static Color surface() { + return shade(color("Panel.background", new Color(0xEC, 0xEC, 0xEC))); + } + + /// The hairline separating a title bar / header from its content. + static Color hairline() { + return color("Separator.foreground", color("controlShadow", new Color(0xCC, 0xCC, 0xCC))); + } + + /// Muted text for title-bar labels. + static Color mutedText() { + return color("Label.disabledForeground", new Color(0x55, 0x55, 0x55)); + } + + /// Selection-style highlight for the hovered/targeted sequent term. + static Color selection() { + return color("textHighlight", new Color(0xBB, 0xD6, 0xFB)); + } + + /// Accent colour, used to mark the live (selection-following) editor tab. + static Color accent() { + return color("Component.accentColor", new Color(0x24, 0x75, 0xBF)); + } + + private static Color color(String key, Color fallback) { + Color c = UIManager.getColor(key); + return c != null ? c : fallback; + } + + /// Nudges a colour toward higher contrast with itself: darker in a light theme, lighter in a + /// dark one, so a header band stands slightly apart from the surrounding panels. + private static Color shade(Color c) { + boolean dark = c.getRed() + c.getGreen() + c.getBlue() < 384; + double f = dark ? 1.16 : 0.92; + return new Color(clamp(c.getRed() * f), clamp(c.getGreen() * f), clamp(c.getBlue() * f)); + } + + private static int clamp(double v) { + return Math.max(0, Math.min(255, (int) Math.round(v))); + } +} diff --git a/keyext.rusty.gui/src/main/resources/org/key_project/rusty/gui/icons/autoModeStart.png b/keyext.rusty.gui/src/main/resources/org/key_project/rusty/gui/icons/autoModeStart.png new file mode 100644 index 00000000000..34bca9d799e Binary files /dev/null and b/keyext.rusty.gui/src/main/resources/org/key_project/rusty/gui/icons/autoModeStart.png differ diff --git a/keyext.rusty.gui/src/main/resources/org/key_project/rusty/gui/icons/key-color-icon-square.png b/keyext.rusty.gui/src/main/resources/org/key_project/rusty/gui/icons/key-color-icon-square.png new file mode 100644 index 00000000000..d412f9b94be Binary files /dev/null and b/keyext.rusty.gui/src/main/resources/org/key_project/rusty/gui/icons/key-color-icon-square.png differ diff --git a/keyext.rusty.gui/src/main/resources/org/key_project/rusty/gui/icons/open.png b/keyext.rusty.gui/src/main/resources/org/key_project/rusty/gui/icons/open.png new file mode 100644 index 00000000000..aa697e0212d Binary files /dev/null and b/keyext.rusty.gui/src/main/resources/org/key_project/rusty/gui/icons/open.png differ diff --git a/keyext.rusty.gui/src/main/resources/org/key_project/rusty/gui/icons/openMostRecent.png b/keyext.rusty.gui/src/main/resources/org/key_project/rusty/gui/icons/openMostRecent.png new file mode 100644 index 00000000000..22d5e193956 Binary files /dev/null and b/keyext.rusty.gui/src/main/resources/org/key_project/rusty/gui/icons/openMostRecent.png differ diff --git a/keyext.rusty.gui/src/main/resources/org/key_project/rusty/gui/icons/pruneProof.png b/keyext.rusty.gui/src/main/resources/org/key_project/rusty/gui/icons/pruneProof.png new file mode 100644 index 00000000000..d6837ad0702 Binary files /dev/null and b/keyext.rusty.gui/src/main/resources/org/key_project/rusty/gui/icons/pruneProof.png differ diff --git a/keyext.rusty.gui/src/main/resources/org/key_project/rusty/gui/icons/saveFile.png b/keyext.rusty.gui/src/main/resources/org/key_project/rusty/gui/icons/saveFile.png new file mode 100644 index 00000000000..cd5a7377242 Binary files /dev/null and b/keyext.rusty.gui/src/main/resources/org/key_project/rusty/gui/icons/saveFile.png differ diff --git a/keyext.rusty.gui/src/test/java/org/key_project/rusty/gui/GuiSmokeTest.java b/keyext.rusty.gui/src/test/java/org/key_project/rusty/gui/GuiSmokeTest.java new file mode 100644 index 00000000000..2760a147e5c --- /dev/null +++ b/keyext.rusty.gui/src/test/java/org/key_project/rusty/gui/GuiSmokeTest.java @@ -0,0 +1,81 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package org.key_project.rusty.gui; + +import java.io.File; +import java.nio.file.Files; +import java.nio.file.Path; + +import org.key_project.rusty.control.KeYEnvironment; +import org.key_project.rusty.proof.Node; +import org.key_project.rusty.proof.Proof; +import org.key_project.rusty.proof.io.OutputStreamProofSaver; + +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.assertFalse; +import static org.junit.jupiter.api.Assertions.assertNotNull; +import static org.junit.jupiter.api.Assertions.assertTrue; + +/// Headless smoke test: load an example, wire it through the [ProofContext] and the views, run auto +/// mode and check the model/views update without error. Top-level windows are not created (they +/// need +/// a display), but the panels are exercised. +public class GuiSmokeTest { + + static { + System.setProperty("java.awt.headless", "true"); + } + + private static File example() { + Path p = Path.of("keyext.rusty/src/test/resources/testcase/examples/if.key"); + Path q = Files.exists(p) ? p + : Path.of("../keyext.rusty/src/test/resources/testcase/examples/if.key"); + return q.toFile(); + } + + @Test + void loadsWiresAndRefreshesViews() throws Exception { + File file = example(); + assertTrue(file.exists(), "example must exist: " + file.getAbsolutePath()); + + KeYEnvironment env = KeYEnvironment.load(file); + Proof proof = env.getLoadedProof(); + assertNotNull(proof); + + ProofContext context = new ProofContext(); + // Construct the views (registers them as listeners); panels are headless-safe. + ProofTreePanel tree = new ProofTreePanel(context); + GoalsView goals = new GoalsView(context); + SequentView sequent = new SequentView(context); + NodeInfoView info = new NodeInfoView(context); + EditorArea editor = new EditorArea(context, () -> { + }); + StrategyView strategy = new StrategyView(context); + assertNotNull(tree); + assertNotNull(goals); + assertNotNull(sequent); + assertNotNull(info); + assertNotNull(editor); + assertNotNull(strategy); + + context.setProof(env, proof); + assertTrue(context.getSelectedNode() == proof.root(), "root should be selected on load"); + assertFalse(proof.openGoals().isEmpty(), "freshly loaded proof should have an open goal"); + + // The selected node renders to a non-empty sequent. + Node root = proof.root(); + String rendered = + OutputStreamProofSaver.printSequent(root.sequent(), root.proof().getServices()); + assertTrue(rendered.contains("=") || rendered.contains("\\<"), + "root sequent should render: " + rendered); + + // Run auto mode and refresh; it should apply at least one rule (the proof grows). + env.getProofControl().startAndWaitForAutoMode(proof); + context.fireProofChanged(); + assertTrue(proof.countNodes() > 1, "auto mode should apply rules"); + + env.dispose(); + } +} diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/proof/io/OutputStreamProofSaver.java b/keyext.rusty/src/main/java/org/key_project/rusty/proof/io/OutputStreamProofSaver.java index fd3638b78c7..4434a7225ba 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/proof/io/OutputStreamProofSaver.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/proof/io/OutputStreamProofSaver.java @@ -392,7 +392,7 @@ public Collection getInterestingInstantiations(SVInstantiations inst) { return s; } - private static String printSequent(Sequent val, + public static String printSequent(Sequent val, Services services) { final LogicPrinter printer = createLogicPrinter(services, services == null); printer.printSequent(val); diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/TacletExecutor.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/TacletExecutor.java index 2f90b937e2e..4cec4774c88 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/TacletExecutor.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/TacletExecutor.java @@ -227,4 +227,13 @@ protected void applyAddProgVars(ImmutableSet getResultSequentChanges(Goal goal, + org.key_project.prover.rules.RuleApp ruleApp) { + return ImmutableSLList.nil(); + } } diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/executor/rustydl/FindTacletExecutor.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/executor/rustydl/FindTacletExecutor.java index 2627a7a89a0..2c04ca28be6 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/executor/rustydl/FindTacletExecutor.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/executor/rustydl/FindTacletExecutor.java @@ -84,6 +84,36 @@ public ImmutableList apply(Goal goal, org.key_project.prover.rules.RuleApp return newGoals; } + @Override + public org.key_project.util.collection.ImmutableList getResultSequentChanges( + Goal goal, org.key_project.prover.rules.RuleApp ruleApp) { + final var services = goal.getOverlayServices(); + final var tacletApp = (TacletApp) ruleApp; + final MatchConditions mc = tacletApp.matchConditions(); + final var newSequentsForGoals = checkAssumesGoals(goal, + tacletApp.assumesFormulaInstantiations(), mc, taclet.goalTemplates().size()); + org.key_project.util.collection.ImmutableList result = + org.key_project.util.collection.ImmutableSLList.nil(); + final var it = newSequentsForGoals.iterator(); + for (var nextGT : taclet.goalTemplates()) { + final var gt = (TacletGoalTemplate) nextGT; + final SequentChangeInfo currentSequent = it.next(); + // Mirrors apply(...) but never splits the goal or sets its sequent; skips the + // goal-mutating add-rule / add-progvar steps: only builds the would-be sequents. + applyReplacewith(gt, currentSequent, tacletApp.posInOccurrence(), mc, goal, tacletApp, + services); + final PosInOccurrence posWhereToAdd = + updatePositionInformation(tacletApp, gt, currentSequent); + applyAdd(gt.sequent(), currentSequent, posWhereToAdd, tacletApp.posInOccurrence(), mc, + goal, tacletApp, services); + result = result.append(currentSequent); + } + while (it.hasNext()) { + result = result.append(it.next()); + } + return result; + } + /// applies the `add`-expressions of taclet goal descriptions /// /// @param add the [Sequent] with the uninstantiated [SequentFormula]'s to be added diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/executor/rustydl/NoFindTacletExecutor.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/executor/rustydl/NoFindTacletExecutor.java index 1f8037b5833..f7bb14a3ffa 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/executor/rustydl/NoFindTacletExecutor.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/executor/rustydl/NoFindTacletExecutor.java @@ -63,6 +63,29 @@ public ImmutableList apply(Goal goal, org.key_project.prover.rules.RuleApp return newGoals; } + @Override + public org.key_project.util.collection.ImmutableList getResultSequentChanges( + Goal goal, org.key_project.prover.rules.RuleApp ruleApp) { + final var services = goal.getOverlayServices(); + final var tacletApp = (TacletApp) ruleApp; + final MatchConditions mc = tacletApp.matchConditions(); + final var newSequentsForGoals = checkAssumesGoals(goal, + tacletApp.assumesFormulaInstantiations(), mc, taclet.goalTemplates().size()); + org.key_project.util.collection.ImmutableList result = + org.key_project.util.collection.ImmutableSLList.nil(); + final var it = newSequentsForGoals.iterator(); + for (var nextGT : taclet.goalTemplates()) { + final TacletGoalTemplate gt = (TacletGoalTemplate) nextGT; + final SequentChangeInfo currentSequent = it.next(); + applyAdd(gt.sequent(), currentSequent, services, mc, goal, tacletApp); + result = result.append(currentSequent); + } + while (it.hasNext()) { + result = result.append(it.next()); + } + return result; + } + /// adds the sequent of the add part of the Taclet to the goal sequent /// /// @param add the Sequent to be added diff --git a/settings.gradle b/settings.gradle index 420f02e86da..f6832857fb3 100644 --- a/settings.gradle +++ b/settings.gradle @@ -22,6 +22,7 @@ include 'keyext.slicing' include 'keyext.caching' include 'keyext.isabelletranslation' include 'keyext.rusty' +include 'keyext.rusty.gui' // ENABLE NULLNESS here or on the CLI // This flag is activated to enable the checker framework.