Highlight graph changes per rewrite step in proof view #190

test/test_highlight.py

@@ -0,0 +1,143 @@
+from __future__ import annotations
+
+import copy
+import sys
+import types
+
+import pytest
+from PySide6 import QtCore
+from pytestqt.qtbot import QtBot
+from pyzx.utils import EdgeType, VertexType
+
+
+# Ensure compatibility with pyzx versions used by ZXLive. We only patch things
+# that are missing, and leave real implementations untouched when they exist.
+import pyzx
+
+try:  # pragma: no cover - defensive shims for newer pyzx
+    import pyzx.tikz as _pyzx_tikz  # type: ignore[import]
+    if not hasattr(_pyzx_tikz, "synonyms_dummy"):
+        _pyzx_tikz.synonyms_dummy = ()  # type: ignore[attr-defined]
+
+    import pyzx.settings as _pyzx_settings  # type: ignore[import]
+    tc = getattr(_pyzx_settings, "tikz_classes", None)
+    if not isinstance(tc, dict) or "dummy" not in tc:
+        tc = dict(tc or {})
+        tc.setdefault("dummy", "")
+        _pyzx_settings.tikz_classes = tc  # type: ignore[attr-defined]
+except Exception:
+    pass
+
+
+# Newer versions of pyzx no longer expose the historical `pyzx.rewrite` module,
+# but ZXLive still imports `RewriteSimpGraph` from there. Try to import the real
+# module first; if that fails, provide a minimal compatibility shim.
+try:  # pragma: no cover - prefer real module if available
+    import pyzx.rewrite as _pyzx_rewrite  # type: ignore[import]
+except Exception:  # pragma: no cover - fallback shim
+    if "pyzx.rewrite" not in sys.modules:
+        rewrite_module = types.ModuleType("pyzx.rewrite")
+
+        class RewriteSimpGraph:  # type: ignore[override]
+            def __init__(self, *args: object, **kwargs: object) -> None:
+                pass
+
+            def __class_getitem__(cls, item: object) -> type:  # type: ignore[override]
+                return cls
+
+        rewrite_module.RewriteSimpGraph = RewriteSimpGraph  # type: ignore[attr-defined]
+        rewrite_module.Rewrite = object  # type: ignore[attr-defined]
+        sys.modules["pyzx.rewrite"] = rewrite_module
+
+
+from zxlive.commands import AddRewriteStep
+from zxlive.common import GraphT, new_graph
+from zxlive.edit_panel import GraphEditPanel
+from zxlive.mainwindow import MainWindow
+from zxlive.proof_panel import ProofPanel
+from zxlive.settings import display_setting
+
+
+def make_two_spider_graph() -> tuple[GraphT, GraphT]:
+    """Create initial graph (2 Z spiders, phase 0 and 0.5, connected) and fused graph."""
+    g = new_graph()
+
+    v0 = g.add_vertex(VertexType.Z, 0, 0.0)
+    v1 = g.add_vertex(VertexType.Z, 0, 1.0)
+
+    # We rely on these being 0 and 1 for clarity in assertions below.
+    assert v0 == 0
+    assert v1 == 1
+
+    g.set_phase(v1, 0.5)
+    g.add_edge((v0, v1), EdgeType.SIMPLE)
+
+    g_fused = copy.deepcopy(g)
+    pyzx.rewrite_rules.fuse(g_fused, v0, v1)
+
+    return g, g_fused
+
+
+@pytest.fixture
+def app(qtbot: QtBot) -> MainWindow:
+    mw = MainWindow()
+    qtbot.addWidget(mw)
+    return mw
+
+
+def test_rewrite_highlight_set_and_cleared_on_step_change(app: MainWindow, qtbot: QtBot) -> None:
+    initial_graph, fused_graph = make_two_spider_graph()
+
+    # Open a new tab with our simple two-spider graph.
+    app.new_graph(initial_graph, name="Highlight Test")
+    assert app.active_panel is not None
+    assert isinstance(app.active_panel, GraphEditPanel)
+    edit_panel: GraphEditPanel = app.active_panel
+
+    # Start a derivation from this graph to enter proof mode.
+    qtbot.mouseClick(edit_panel.start_derivation, QtCore.Qt.MouseButton.LeftButton)
+    assert app.active_panel is not None
+    assert isinstance(app.active_panel, ProofPanel)
+    proof_panel: ProofPanel = app.active_panel
+
+    # Ensure rewrite highlighting is on so the test is independent of user settings.
+    display_setting.highlight_rewrites = True
+
+    # Add a Fuse spiders rewrite with match pair so step 0 highlights the fused vertices/edge.
+    cmd = AddRewriteStep(
+        proof_panel.graph_view, fused_graph, proof_panel.step_view, "Fuse spiders",
+        highlight_match_pairs=[(0, 1)],
+    )
+    proof_panel.undo_stack.push(cmd)
+
+    scene = proof_panel.graph_scene
+
+    # "Next change" semantics: on START (index 0) we show the graph at step 0
+    # and highlight what will change in the transition 0 -> 1 (the fuse).
+    proof_panel.step_view.move_to_step(0)
+    # Both spiders that will be fused, and the edge between them, should be highlighted.
+    assert scene.is_vertex_highlighted(0)
+    assert scene.is_vertex_highlighted(1)
+    edges_01 = list(scene.g.edges(0, 1))
+    assert len(edges_01) >= 1
+    e = edges_01[0]
+    s, t = scene.g.edge_st(e)
+    edge_01 = (s, t, scene.g.edge_type(e))
+    assert scene.is_edge_highlighted(edge_01)
+
+    # On the last step (index 1) there is no "next" transition, so no highlight.
+    proof_panel.step_view.move_to_step(1)
+    assert not any(scene.is_vertex_highlighted(v) for v in scene.g.vertices())
+
+    # Back to START: again highlight the next change (0 -> 1).
+    proof_panel.step_view.move_to_step(0)
+    assert scene.is_vertex_highlighted(0)
+    assert scene.is_vertex_highlighted(1)
+
+    # Now simulate the user using Undo to remove the rewrite step entirely.
+    # When the proof returns to the START state via the undo stack, there
+    # should again be no rewrite highlighting at all.
+    proof_panel.undo_stack.undo()
+    assert proof_panel.step_view.currentIndex().row() == 0
+    assert not any(scene.is_vertex_highlighted(v) for v in scene.g.vertices())
+

zxlive/animations.py

@@ -303,23 +303,38 @@ def make_animation(self: RewriteAction, panel: ProofPanel, g: GraphT, matches: l
         for v in rem_verts:
             anim_before.addAnimation(remove_id(panel.graph_scene.vertex_map[v]))
     elif self.name == rules_basic['copy']['text']:
+        # COPY is MATCH_SINGLE: matches is a list of vertices. We animate the
+        # neighbor each spider is being copied through.
         anim_before = QParallelAnimationGroup()
         for v in matches:
             w = list(panel.graph.neighbors(v))[0]
-            anim_before.addAnimation(fuse(panel.graph_scene.vertex_map[v],
-                                          panel.graph_scene.vertex_map[w]))
+            anim_before.addAnimation(
+                fuse(panel.graph_scene.vertex_map[v],
+                     panel.graph_scene.vertex_map[w])
+            )
         anim_after = QParallelAnimationGroup()
         for v in matches:
             w = list(panel.graph.neighbors(v))[0]
-            anim_after.addAnimation(strong_comp(panel.graph, g, w, panel.graph_scene))
+            anim_after.addAnimation(
+                strong_comp(panel.graph, g, w, panel.graph_scene)
+            )
     elif self.name == rules_basic['pauli']['text']:
+        # PAULI is MATCH_DOUBLE: matches is a list of (v1, v2) pairs.
         anim_before = QParallelAnimationGroup()
         for m in matches:
-            anim_before.addAnimation(fuse(panel.graph_scene.vertex_map[m[0]],
-                                          panel.graph_scene.vertex_map[m[1]]))
+            if isinstance(m, tuple) and len(m) == 2:
+                v1, v2 = m
+                anim_before.addAnimation(
+                    fuse(panel.graph_scene.vertex_map[v1],
+                         panel.graph_scene.vertex_map[v2])
+                )
         anim_after = QParallelAnimationGroup()
         for m in matches:
-            anim_after.addAnimation(strong_comp(panel.graph, g, m[1], panel.graph_scene))
+            if isinstance(m, tuple) and len(m) == 2:
+                _, v2 = m
+                anim_after.addAnimation(
+                    strong_comp(panel.graph, g, v2, panel.graph_scene)
+                )
     elif self.name == rules_basic['bialgebra']['text']:
         anim_before = QParallelAnimationGroup()
         for v1, v2 in matches:

zxlive/app.py

@@ -147,8 +147,8 @@ def main() -> None:
     zxl = ZXLive()
     if sys.platform == "darwin":  # 'darwin' is macOS
         if dark_mode_setting == "dark":
-            zxl.styleHints().setColorScheme(Qt.ColorScheme.Dark)
+            zxl.styleHints().setColorScheme(Qt.ColorScheme.Dark)  # type: ignore[attr-defined]
         elif dark_mode_setting == "light":
-            zxl.styleHints().setColorScheme(Qt.ColorScheme.Light)
+            zxl.styleHints().setColorScheme(Qt.ColorScheme.Light)  # type: ignore[attr-defined]
         # For "system", don't set the color scheme to let Qt auto-detect
     zxl.exec_()

zxlive/commands.py

@@ -6,10 +6,7 @@
 from fractions import Fraction
 from typing import Callable, Iterable, Optional, Set, Union
 
-from PySide6.QtCore import QModelIndex
 from PySide6.QtGui import QUndoCommand
-from PySide6.QtWidgets import QListView
-from pyzx.graph.diff import GraphDiff
 from pyzx.symbolic import Poly
 from pyzx.utils import EdgeType, VertexType, get_w_partner, vertex_is_w, get_w_io, get_z_box_label, set_z_box_label
 
@@ -441,9 +438,11 @@ class AddRewriteStep(UpdateGraph):
     The rewrite is inserted after the currently selected step. In particular, it
     replaces all rewrites that were previously after the current selection.
     """
-    step_view: QListView
+    step_view: ProofStepView
     name: str
-    diff: Optional[GraphDiff] = None
+    highlight_match_pairs: Optional[list[tuple[int, int]]] = None
+    highlight_verts: Optional[list[int]] = None
+    highlight_edge_pairs: Optional[list[tuple[int, int]]] = None
 
     _old_selected: Optional[int] = field(default=None, init=False)
     _old_steps: list[tuple[Rewrite, GraphT]] = field(default_factory=list, init=False)
@@ -461,33 +460,38 @@ def redo(self) -> None:
         for _ in range(self.proof_model.rowCount() - self._old_selected - 1):
             self._old_steps.append(self.proof_model.pop_rewrite())
 
-        self.proof_model.add_rewrite(Rewrite(self.name, self.name, self.new_g))
+        hp_list = list(self.highlight_match_pairs) if self.highlight_match_pairs else None
+        hv_list = list(self.highlight_verts) if self.highlight_verts else None
+        he_list = list(self.highlight_edge_pairs) if self.highlight_edge_pairs else None
+        self.proof_model.add_rewrite(
+            Rewrite(self.name, self.name, self.new_g, None, hp_list, hv_list, he_list)
+        )
 
-        # Select the added step
-        idx = self.step_view.model().index(self.proof_model.rowCount() - 1, 0, QModelIndex())
-        self.step_view.selectionModel().blockSignals(True)
-        self.step_view.setCurrentIndex(idx)
-        self.step_view.selectionModel().blockSignals(False)
+        # Move to the added step so that the graph view and rewrite-step
+        # highlighting are updated consistently.
+        new_index = self.proof_model.rowCount()
         super().redo()
+        self.step_view.move_to_step(new_index - 1)
 
     def undo(self) -> None:
         # Undo the rewrite
         self.step_view.selectionModel().blockSignals(True)
         self.proof_model.pop_rewrite()
         self.step_view.selectionModel().blockSignals(False)
 
-        # Add back steps that were previously removed
+        # Add back steps that were previously removed.
         for rewrite, graph in reversed(self._old_steps):
             self.proof_model.add_rewrite(rewrite)
 
-        # Select the previously selected step
-        assert self._old_selected is not None
-        idx = self.step_view.model().index(self._old_selected, 0, QModelIndex())
-        self.step_view.selectionModel().blockSignals(True)
-        self.step_view.setCurrentIndex(idx)
-        self.step_view.selectionModel().blockSignals(False)
+        # First restore the underlying graph to its previous state.
         super().undo()
 
+        # Then move the proof view back to the previously selected step so that
+        # the graph view and rewrite-step highlighting are updated consistently
+        # (including clearing highlights at START).
+        assert self._old_selected is not None
+        self.step_view.move_to_step(self._old_selected)
+
 
 @dataclass
 class GroupRewriteSteps(BaseCommand):

zxlive/custom_rule.py

@@ -33,6 +33,7 @@ def __init__(self, lhs_graph: GraphT, rhs_graph: GraphT, name: str, description:
         self.name = name
         self.description = description
         self.last_rewrite_center = None
+        self.last_rewrite_verts: Optional[list[VT]] = None
         self.is_rewrite_unfusable = is_rewrite_unfusable(lhs_graph)
         if self.is_rewrite_unfusable:
             self.lhs_graph_without_boundaries_nx = nx.MultiGraph(self.lhs_graph_nx.subgraph(
@@ -96,6 +97,13 @@ def applier(self, graph: BaseGraph[VT, ET], vertices: list[VT]) -> bool:
             etab[(v1, v2)][data['type'] - 1] += 1
 
         graph.add_edge_table(etab)
+        # Prefer non-boundary RHS vertices so highlight is limited to the gadget region;
+        # fall back to all mapped vertices if there are no non-boundary (e.g. degenerate rule).
+        non_boundary = [
+            vertex_map[v] for v in self.rhs_graph_nx.nodes()
+            if self.rhs_graph_nx.nodes()[v].get('type') != VertexType.BOUNDARY
+        ]
+        self.last_rewrite_verts = non_boundary if non_boundary else list(vertex_map.values())
         graph.remove_vertices(vertices_to_remove)
         return True
 

zxlive/eitem.py

@@ -106,6 +106,12 @@ def refresh(self) -> None:
         if self.g.edge_type(self.e) == EdgeType.HADAMARD:
             pen.setDashPattern([4.0, 2.0])
         pen.setColor(self.color)
+
+        if self.graph_scene.is_edge_highlighted(self.e):
+            # Emphasize highlighted edges with a thicker, accent-colored pen.
+            pen.setWidthF(self.thickness + 2.0)
+            pen.setColor(display_setting.effective_colors["rewrite_highlight_edge"])
+
         self.setPen(QPen(pen))
 
         if not self.is_dragging:

zxlive/graphscene.py

@@ -62,6 +62,8 @@ def __init__(self) -> None:
         self.vertex_map: dict[VT, VItem] = {}
         self.edge_map: dict[ET, dict[int, EItem]] = {}
         self.g: GraphT
+        self._highlighted_verts: set[VT] = set()
+        self._highlighted_edges: set[ET] = set()
 
     def update_background_brush(self) -> None:
         if display_setting.dark_mode:
@@ -97,6 +99,44 @@ def select_vertices(self, vs: Iterable[VT]) -> None:
                 vs.remove(it.v)
         self.selection_changed_custom.emit()
 
+    def set_rewrite_highlight(self, verts: Iterable[VT], edges: Iterable[ET]) -> None:
+        """Set the vertices and edges that should be highlighted as part of a rewrite step."""
+        new_verts = set(verts)
+        new_edges = set(edges)
+
+        # Capture old highlight sets so we can refresh anything whose
+        # highlight status may have changed.
+        old_verts = self._highlighted_verts
+        old_edges = self._highlighted_edges
+
+        # Update internal highlight state *before* refreshing items so that
+        # VItem.refresh / EItem.refresh see the new highlight flags.
+        self._highlighted_verts = new_verts
+        self._highlighted_edges = new_edges
+
+        # Refresh vertices whose highlight status changed
+        for v in old_verts.union(new_verts):
+            if v in self.vertex_map:
+                self.vertex_map[v].refresh()
+
+        # Refresh edges whose highlight status changed
+        for e in old_edges.union(new_edges):
+            if e in self.edge_map:
+                for e_item in self.edge_map[e].values():
+                    e_item.refresh()
+
+        self.update()
+
+    def clear_rewrite_highlight(self) -> None:
+        """Clear all rewrite-step highlighting."""
+        self.set_rewrite_highlight(set(), set())
+
+    def is_vertex_highlighted(self, v: VT) -> bool:
+        return v in self._highlighted_verts
+
+    def is_edge_highlighted(self, e: ET) -> bool:
+        return e in self._highlighted_edges
+
     def set_graph(self, g: GraphT) -> None:
         """Set the PyZX graph for the scene.
         If the scene already contains a graph, it will be replaced."""