Minor fixes to change_steps (#29)

Handle exceptions in ProofFile.change_steps
Deepcopy steps in CoqFile changes

coqpyt/coq/base_file.py

@@ -2,6 +2,7 @@
 import shutil
 import uuid
 import tempfile
+from copy import deepcopy
 from typing import Optional, List
 
 from coqpyt.lsp.structs import (
@@ -212,17 +213,16 @@ def _make_change(self, change_function, *args):
         if not self.is_valid:
             raise InvalidFileException(self.path)
 
-        previous_steps = self.steps
+        self.__set_backup_steps()
         old_steps_taken = self.steps_taken
         old_diagnostics = self.coq_lsp_client.lsp_endpoint.diagnostics
-        lines = self.__read().split("\n")
-        old_text = "\n".join(lines)
+        old_text = self.__read()
 
         try:
             change_function(*args)
         except InvalidChangeException as e:
             # Rollback changes
-            self.steps = previous_steps
+            self.steps = self.__backup_steps
             self.steps_taken = old_steps_taken
             self.coq_lsp_client.lsp_endpoint.diagnostics = old_diagnostics
             self.is_valid = True
@@ -323,29 +323,41 @@ def __add_update_ast(self, previous_step_index: int, step_text: str) -> Step:
 
         return added_step
 
-    def __copy_steps(self, previous_steps: List[Step]):
-        for i, step in enumerate(previous_steps):
-            step.text, step.ast = self.steps[i].text, self.steps[i].ast
-            step.diagnostics = self.steps[i].diagnostics
-            step.short_text = self.steps[i].short_text
-        self.steps = previous_steps
+    def __copy_steps(self):
+        for i, step in enumerate(self.steps):
+            index = self.__index_tracker[i]
+            if index is None:  # Newly added steps
+                continue
+
+            backup = self.__backup_steps[index]
+            backup.text, backup.ast = step.text, step.ast
+            backup.diagnostics = step.diagnostics
+            backup.short_text = step.short_text
+            self.steps[i] = backup
+
+    def __set_backup_steps(self):
+        self.__backup_steps = self.steps[:]
+        self.__index_tracker: List[Optional[int]] = []
+        for i, step in enumerate(self.__backup_steps):
+            self.steps[i] = deepcopy(step)
+            self.__index_tracker.append(i)
 
     def _delete_step(self, step_index: int) -> None:
-        deleted_text = self.steps[step_index].text
+        deleted_step = self.steps[step_index]
+        deleted_text = deleted_step.text
         self.__delete_step_text(step_index)
 
         # Modify the previous steps instead of creating new ones
         # This is important to preserve their references
         # For instance, in the ProofFile
-        previous_steps = self.steps
         self.__update_steps()
 
         if not self.is_valid:
             raise InvalidDeleteException(deleted_text)
 
         # We will remove the step from the previous steps
-        deleted_step = previous_steps.pop(step_index)
-        self.__copy_steps(previous_steps)
+        self.__index_tracker.pop(step_index)
+        self.__copy_steps()
 
         if self.steps_taken > step_index:
             self.steps_taken -= 1
@@ -361,18 +373,18 @@ def _add_step(self, previous_step_index: int, step_text: str) -> None:
         # Modify the previous steps instead of creating new ones
         # This is important to preserve their references
         # For instance, in the ProofFile
-        previous_steps = self.steps
+        previous_steps_size = len(self.steps)
         step_index = previous_step_index + 1
         self.__update_steps()
 
         # NOTE: We check if exactly 1 step was added, because the text might contain
         # two steps or something that might lead to similar unwanted behaviour.
-        if len(self.steps) != len(previous_steps) + 1 or not self.is_valid:
+        if len(self.steps) != previous_steps_size + 1 or not self.is_valid:
             raise InvalidAddException(step_text)
 
-        # We will add the new step to the previous_steps
-        previous_steps.insert(step_index, self.steps[step_index])
-        self.__copy_steps(previous_steps)
+        # We will add the new step to the previous steps
+        self.__index_tracker.insert(step_index, None)
+        self.__copy_steps()
 
         if self.steps_taken > step_index:
             self.steps_taken += 1
@@ -401,7 +413,7 @@ def _get_steps_taken_offset(self, changes: List[CoqChange]):
     def __change_steps(self, changes: List[CoqChange]):
         previous_steps_takens = self.steps_taken
         offset_steps, offset_steps_taken = 0, self._get_steps_taken_offset(changes)
-        previous_steps, previous_steps_size = self.steps, len(self.steps)
+        previous_steps_size = len(self.steps)
         CoqFile.exec(self, -self.steps_taken)
 
         for change in changes:
@@ -411,11 +423,13 @@ def __change_steps(self, changes: List[CoqChange]):
                     change.previous_step_index, change.step_text
                 )
                 self.steps.insert(change.previous_step_index + 1, step)
+                self.__index_tracker.insert(change.previous_step_index + 1, None)
                 offset_steps += 1
             elif isinstance(change, CoqDeleteStep):
                 self.__delete_step_text(change.step_index)
                 self.__delete_update_ast(change.step_index)
                 self.steps.pop(change.step_index)
+                self.__index_tracker.pop(change.step_index)
                 offset_steps -= 1
             else:
                 raise NotImplementedError(f"Unknown change: {change}")
@@ -426,7 +440,7 @@ def __change_steps(self, changes: List[CoqChange]):
         if len(self.steps) != previous_steps_size + offset_steps or not self.is_valid:
             raise InvalidChangeException()
 
-        self.__copy_steps(previous_steps)
+        self.__copy_steps()
         CoqFile.exec(self, previous_steps_takens + offset_steps_taken)
 
     @property

coqpyt/coq/proof_file.py

@@ -787,9 +787,7 @@ def add_step(self, previous_step_index: int, step_text: str):
             n_steps = self.steps_taken - previous_step_index - 2
             self.__local_exec(-n_steps)  # Backtrack until added step
             self.steps_taken -= 1  # Ignore added step while backtracking
-            self.__local_exec(
-                1, program=False
-            )  # Execute added step, updating last_term
+            self.__local_exec(1, program=False)  # Execute added step
             self.__add_step(previous_step_index + 1)
             self.__local_exec(n_steps)  # Execute until starting point
 
@@ -815,18 +813,19 @@ def change_steps(self, changes: List[CoqChange]):
             else:
                 self.__local_exec(-1)
 
-        n_steps = 0 if len(adds) == 0 else self.steps_taken - max(0, adds[0])
+        n_steps = 0 if len(adds) == 0 else max(0, self.steps_taken - adds[0])
         self.__local_exec(-n_steps)  # Step back until first Add
-        super().change_steps(changes)  # Apply (faster) changes in CoqFile
+        try:
+            super().change_steps(changes)  # Apply (faster) changes in CoqFile
+        except InvalidChangeException as e:
+            self.__local_exec(n_steps)  # Reset pointer
+            raise e
 
         # Add ProofSteps to ProofFile after Steps are added to CoqFile
-        steps_taken = self.steps_taken
         for add in adds:
-            n_steps = add + 1 - steps_taken
-            self.__local_exec(n_steps, program=False)
+            self.__local_exec(add + 1 - self.steps_taken, program=False)
             self.__add_step(add)
-            steps_taken += n_steps
-        self.__local_exec(new_steps_taken - steps_taken)
+        self.__local_exec(new_steps_taken - self.steps_taken)
 
     def close(self):
         super().close()