Refactor Proof State

README.md

@@ -20,7 +20,7 @@ python -m pip install -e .
 ```python
 import os
 from coqlspclient.coq_file import CoqFile
-from coqlspclient.proof_state import ProofState
+from coqlspclient.proof_file import ProofFile
 from coqlspclient.coq_structs import TermType
 
 # Open Coq file
@@ -55,33 +55,32 @@ with CoqFile(os.path.join(os.getcwd(), "examples/example.v")) as coq_file:
     # Get all terms defined until now
     print("Number of terms:", len(coq_file.context.terms))
 
-with CoqFile(os.path.join(os.getcwd(), "examples/example.v")) as coq_file:
-    with ProofState(coq_file) as proof_state:
-        # Number of proofs in the file
-        print("Number of proofs:", len(proof_state.proofs))
-        print("Proof:", proof_state.proofs[0].text)
-
-        # Print steps of proof
-        for step in proof_state.proofs[0].steps:
-            print(step.text, end="")
-        print()
-
-        # Get the context used in the third step
-        print(proof_state.proofs[0].steps[2].context)
-        # Print the goals in the third step
-        print(proof_state.proofs[0].steps[2].goals)
-
-        # Print number of terms in context
-        print("Number of terms:", len(proof_state.context.terms))
-        # Filter for Notations only
-        print("Number of notations:",
-            len(
-                list(filter(
-                    lambda term: term.type == TermType.NOTATION,
-                    proof_state.context.terms.values(),
-                ))
-            )
+with ProofFile(os.path.join(os.getcwd(), "examples/example.v")) as proof_file:
+    # Number of proofs in the file
+    print("Number of proofs:", len(proof_file.proofs))
+    print("Proof:", proof_file.proofs[0].text)
+
+    # Print steps of proof
+    for step in proof_file.proofs[0].steps:
+        print(step.text, end="")
+    print()
+
+    # Get the context used in the third step
+    print(proof_file.proofs[0].steps[2].context)
+    # Print the goals in the third step
+    print(proof_file.proofs[0].steps[2].goals)
+
+    # Print number of terms in context
+    print("Number of terms:", len(proof_file.context.terms))
+    # Filter for Notations only
+    print("Number of notations:",
+        len(
+            list(filter(
+                lambda term: term.type == TermType.NOTATION,
+                proof_file.context.terms.values(),
+            ))
         )
+    )
 ```
 
 ### Run tests

coqlspclient/coq_changes.py

@@ -0,0 +1,16 @@
+from dataclasses import dataclass
+
+
+class CoqChange:
+    pass
+
+
+@dataclass
+class CoqAddStep(CoqChange):
+    step_text: str
+    previous_step_index: int
+
+
+@dataclass
+class CoqDeleteStep(CoqChange):
+    step_index: int

coqlspclient/coq_exceptions.py

@@ -0,0 +1,26 @@
+class InvalidChangeException(Exception):
+    pass
+
+
+class InvalidStepException(InvalidChangeException):
+    def __init__(self, step: str):
+        self.step: str = step
+
+    def __str__(self):
+        return "The step {} is not valid.".format(self.step)
+
+
+class InvalidDeleteException(InvalidChangeException):
+    def __init__(self, step_to_delete: str):
+        self.step_to_delete: str = step_to_delete
+
+    def __str__(self):
+        return "Deleting the step {} is not valid.".format(self.delete)
+
+
+class InvalidFileException(Exception):
+    def __init__(self, file: str):
+        self.file: str = file
+
+    def __str__(self):
+        return "The file {} is not valid.".format(self.file)