From 0106348975b86102f3d5743b6659895383a042cc Mon Sep 17 00:00:00 2001 From: Pedro Carrott <43729507+pcarrott@users.noreply.github.com> Date: Thu, 7 Dec 2023 23:30:46 +0000 Subject: [PATCH] Minor fixes to change_steps (#29) Handle exceptions in ProofFile.change_steps Deepcopy steps in CoqFile changes --- coqpyt/coq/base_file.py | 56 +++++++++++++++++++++++++--------------- coqpyt/coq/proof_file.py | 19 +++++++------- 2 files changed, 44 insertions(+), 31 deletions(-) diff --git a/coqpyt/coq/base_file.py b/coqpyt/coq/base_file.py index f8587e2..8f853d4 100644 --- a/coqpyt/coq/base_file.py +++ b/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 diff --git a/coqpyt/coq/proof_file.py b/coqpyt/coq/proof_file.py index a4ad54a..d1c079d 100644 --- a/coqpyt/coq/proof_file.py +++ b/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()