Remove graph diffs

Previously we stored the proof as both a series of graphs and as an
initial graph together with a series of diffs. Now we have removed the
diffs to avoid possible synchronisation issues.

Additionally, the diffs did not record repositioned vertices, which made
adding an OCM step difficult (Issue: #150)

zxlive/commands.py

@@ -385,8 +385,7 @@ def redo(self) -> None:
         for _ in range(self.proof_model.rowCount() - self._old_selected - 1):
             self._old_steps.append(self.proof_model.pop_rewrite())
 
-        diff = self.diff or GraphDiff(self.g, self.new_g)
-        self.proof_model.add_rewrite(Rewrite(self.name, self.name, diff), self.new_g)
+        self.proof_model.add_rewrite(Rewrite(self.name, self.name, self.new_g))
 
         # Select the added step
         idx = self.step_view.model().index(self.proof_model.rowCount() - 1, 0, QModelIndex())
@@ -403,7 +402,7 @@ def undo(self) -> None:
 
         # Add back steps that were previously removed
         for rewrite, graph in reversed(self._old_steps):
-            self.proof_model.add_rewrite(rewrite, graph)
+            self.proof_model.add_rewrite(rewrite)
 
         # Select the previously selected step
         assert self._old_selected is not None
@@ -456,10 +455,10 @@ def redo(self) -> None:
         super().redo()
         model = self.step_view.model()
         assert isinstance(model, ProofModel)
-        model.graphs[self.step_view.currentIndex().row()] = self.g
+        model.set_graph(self.step_view.currentIndex().row(), self.g)
 
     def undo(self) -> None:
         super().undo()
         model = self.step_view.model()
         assert isinstance(model, ProofModel)
-        model.graphs[self.step_view.currentIndex().row()] = self.g
+        model.set_graph(self.step_view.currentIndex().row(), self.g)

zxlive/mainwindow.py

@@ -282,7 +282,7 @@ def _open_file_from_output(self, out: ImportGraphOutput | ImportProofOutput | Im
             if isinstance(out, ImportGraphOutput):
                 self.new_graph(out.g, name)
             elif isinstance(out, ImportProofOutput):
-                graph = out.p.graphs[-1]
+                graph = out.p.graphs()[-1]
                 self.new_deriv(graph, name)
                 assert isinstance(self.active_panel, ProofPanel)
                 proof_panel: ProofPanel = self.active_panel
@@ -542,8 +542,8 @@ def proof_as_lemma(self) -> None:
         name, description = get_lemma_name_and_description(self)
         if name is None or description is None:
             return
-        lhs_graph = self.active_panel.proof_model.graphs[0]
-        rhs_graph = self.active_panel.proof_model.graphs[-1]
+        lhs_graph = self.active_panel.proof_model.graphs()[0]
+        rhs_graph = self.active_panel.proof_model.graphs()[-1]
         rule = CustomRule(lhs_graph, rhs_graph, name, description)
         save_rule_dialog(rule, self, name + ".zxr" if name else "")
 

zxlive/proof.py

@@ -14,14 +14,14 @@ class Rewrite(NamedTuple):
 
     display_name: str # Name of proof displayed to user
     rule: str  # Name of the rule that was applied to get to this step
-    diff: GraphDiff  # Diff from the last step to this step
+    graph: GraphT  # Diff from the last step to this step
 
     def to_json(self) -> str:
         """Serializes the rewrite to JSON."""
         return json.dumps({
             "display_name": self.display_name,
             "rule": self.rule,
-            "diff": self.diff.to_json()
+            "graph": self.graph.to_json()
         })
 
     @staticmethod
@@ -32,7 +32,7 @@ def from_json(json_str: str) -> "Rewrite":
         return Rewrite(
             display_name=d.get("display_name", d["rule"]), # Old proofs may not have display names
             rule=d["rule"],
-            diff=GraphDiff.from_json(d["diff"])
+            graph=GraphT.from_json(d["graph"]),
         )
 
 class ProofModel(QAbstractListModel):
@@ -42,29 +42,29 @@ class ProofModel(QAbstractListModel):
     rewrite that was used to go from one graph to next.
     """
 
-    graphs: list[GraphT]  # n graphs
-    steps: list[Rewrite]  # n-1 rewrite steps
+    initial_graph: GraphT
+    steps: list[Rewrite]
 
     def __init__(self, start_graph: GraphT):
         super().__init__()
-        self.graphs = [start_graph]
+        self.initial_graph = start_graph
         self.steps = []
 
-    def set_data(self, graphs: list[GraphT], steps: list[Rewrite]) -> None:
-        """Sets the model data.
+    def set_graph(self, index: int, graph: GraphT):
+        if index == 0:
+            self.initial_graph = graph
+        else:
+            old_step = self.steps[index-1]
+            new_step = Rewrite(old_step.display_name, old_step.rule, graph)
+            self.steps[index-1] = new_step
 
-        Can be used to load the model from a saved state.
-        """
-        assert len(steps) == len(graphs) - 1
-        self.beginResetModel()
-        self.graphs = graphs
-        self.steps = steps
-        self.endResetModel()
+    def graphs(self) -> [GraphT]:
+        return [self.initial_graph] + [step.graph for step in self.steps]
 
     def data(self, index: Union[QModelIndex, QPersistentModelIndex], role: int=Qt.ItemDataRole.DisplayRole) -> Any:
         """Overrides `QAbstractItemModel.data` to populate a view with rewrite steps"""
 
-        if index.row() >= len(self.graphs) or index.column() >= 1:
+        if index.row() >= len(self.steps)+1 or index.column() >= 1:
             return None
 
         if role == Qt.ItemDataRole.DisplayRole:
@@ -93,14 +93,13 @@ def rowCount(self, index: Union[QModelIndex, QPersistentModelIndex] = QModelInde
         # user has to specify the index of the parent. In a list, we always expect the
         # parent to be `None` or the empty `QModelIndex()`
         if not index or not index.isValid():
-            return len(self.graphs)
+            return len(self.steps)+1
         else:
             return 0
 
-    def add_rewrite(self, rewrite: Rewrite, new_graph: GraphT) -> None:
+    def add_rewrite(self, rewrite: Rewrite) -> None:
         """Adds a rewrite step to the model."""
-        self.beginInsertRows(QModelIndex(), len(self.graphs), len(self.graphs))
-        self.graphs.append(new_graph)
+        self.beginInsertRows(QModelIndex(), len(self.steps), len(self.steps))
         self.steps.append(rewrite)
         self.endInsertRows()
 
@@ -109,35 +108,37 @@ def pop_rewrite(self) -> tuple[Rewrite, GraphT]:
 
         Returns the rewrite and the graph that previously resulted from this rewrite.
         """
-        self.beginRemoveRows(QModelIndex(), len(self.graphs) - 1, len(self.graphs) - 1)
+        self.beginRemoveRows(QModelIndex(), len(self.steps), len(self.steps))
         rewrite = self.steps.pop()
-        graph = self.graphs.pop()
         self.endRemoveRows()
-        return rewrite, graph
+        return rewrite, rewrite.graph
 
     def get_graph(self, index: int) -> GraphT:
         """Returns the grap at a given position in the proof."""
-        copy = self.graphs[index].copy()
-        # Mypy issue: https://github.com/python/mypy/issues/11673
-        assert isinstance(copy, GraphT)  # type: ignore
-        return copy
+        if index == 0:
+            return self.initial_graph.copy()
+        else:
+            copy = self.steps[index-1].graph.copy()
+            # Mypy issue: https://github.com/python/mypy/issues/11673
+            assert isinstance(copy, GraphT)  # type: ignore
+            return copy
 
     def rename_step(self, index: int, name: str):
         """Change the display name"""
-        old_step = self.steps[index]
+        old_step = self.steps[index-1]
 
         # Must create a new Rewrite object instead of modifying current object
         # since Rewrite inherits NamedTuple and is hence immutable
-        self.steps[index] = Rewrite(name, old_step.rule, old_step.diff)
+        self.steps[index-1] = Rewrite(name, old_step.rule, old_step.diff)
 
         # Rerender the proof step otherwise it will display the old name until
         # the cursor moves
-        modelIndex = self.createIndex(index, 0)
+        modelIndex = self.createIndex(index-1, 0)
         self.dataChanged.emit(modelIndex, modelIndex, [])
 
     def to_json(self) -> str:
         """Serializes the model to JSON."""
-        initial_graph = self.graphs[0].to_json()
+        initial_graph = self.initial_graph.to_json()
         proof_steps = [step.to_json() for step in self.steps]
 
         return json.dumps({
@@ -155,8 +156,5 @@ def from_json(json_str: str) -> "ProofModel":
         model = ProofModel(initial_graph)
         for step in d["proof_steps"]:
             rewrite = Rewrite.from_json(step)
-            rewritten_graph = rewrite.diff.apply_diff(model.graphs[-1])
-            # Mypy issue: https://github.com/python/mypy/issues/11673
-            assert isinstance(rewritten_graph, GraphT)  # type: ignore
-            model.add_rewrite(rewrite, rewritten_graph)
+            model.add_rewrite(rewrite)
         return model

zxlive/tikz.py

@@ -15,7 +15,7 @@ def proof_to_tikz(proof: ProofModel) -> str:
     yoffset = -10
     idoffset = 0
     total_verts, total_edges = [], []
-    for i, g in enumerate(proof.graphs):
+    for i, g in enumerate(proof.graphs()):
         # Compute graph dimensions
         width = max(g.row(v) for v in g.vertices()) - min(g.row(v) for v in g.vertices())
         height = max(g.qubit(v) for v in g.vertices()) - min(g.qubit(v) for v in g.vertices())