(incomplete) handling of aborted proofs (#56)

sr-lab · Oct 18, 2024 · 35ebaaa · 35ebaaa
1 parent 17a16bc
commit 35ebaaa
Show file tree

Hide file tree

Showing 4 changed files with 66 additions and 42 deletions.
diff --git a/coqpyt/coq/context.py b/coqpyt/coq/context.py
@@ -489,10 +489,61 @@ def term_type(self, step: Step) -> TermType:
             step (Step): The step to be processed.
 
         Returns:
-            List: The term type of the step.
+            TermType: The term type of the step.
         """
         return self.__term_type(self.expr(step))
 
+    def is_proof_term(self, step: Step) -> bool:
+        """
+        Args:
+            step (Step): The step to be processed.
+
+        Returns:
+            bool: Whether the step introduces a new proof term.
+        """
+        term_type = self.term_type(step)
+        # Assume that terms of the following types do not introduce new proofs
+        # FIXME: Should probably check if goals were changed
+        return term_type not in [
+            TermType.TACTIC,
+            TermType.NOTATION,
+            TermType.INDUCTIVE,
+            TermType.COINDUCTIVE,
+            TermType.RECORD,
+            TermType.CLASS,
+            TermType.SCHEME,
+            TermType.VARIANT,
+            TermType.OTHER,
+        ]
+
+    def is_end_proof(self, step: Step) -> bool:
+        """
+        Args:
+            step (Step): The step to be processed.
+
+        Returns:
+            bool: Whether the step closes an open proof term.
+        """
+        # FIXME: Refer to issue #55: https://github.com/sr-lab/coqpyt/issues/55
+        expr = self.expr(step)[0]
+        return expr in ["VernacEndProof", "VernacExactProof", "VernacAbort"]
+
+    def is_segment_delimiter(self, step: Step) -> bool:
+        """
+        Args:
+            step (Step): The step to be processed.
+
+        Returns:
+            bool: Whether the step delimits a segment (module or section).
+        """
+        expr = self.expr(step)[0]
+        return expr in [
+            "VernacEndSegment",
+            "VernacDefineModule",
+            "VernacDeclareModuleType",
+            "VernacBeginSection",
+        ]
+
     def update(self, context: Union["FileContext", Dict[str, Term]] = {}):
         """Updates the context with new terms.
 

diff --git a/coqpyt/coq/proof_file.py b/coqpyt/coq/proof_file.py
@@ -533,48 +533,21 @@ def __handle_proof_term(
                 index, ProofTerm(proof_term, statement_context, [], program)
             )
 
-    def __is_proof_term(self, step: Step):
-        term_type = self.context.term_type(step)
-        # Assume that terms of the following types do not introduce new proofs
-        # FIXME: Should probably check if goals were changed
-        return term_type not in [
-            TermType.TACTIC,
-            TermType.NOTATION,
-            TermType.INDUCTIVE,
-            TermType.COINDUCTIVE,
-            TermType.RECORD,
-            TermType.CLASS,
-            TermType.SCHEME,
-            TermType.VARIANT,
-            TermType.OTHER,
-        ]
-
-    def __is_end_proof(self, step: Step):
-        return self.context.expr(step)[0] in ["VernacEndProof", "VernacExactProof"]
-
     def __check_proof_step(self, step: Step, undo: bool = False):
         # Avoids Tactics, Notations, Inductive...
         if self.context.term_type(step) == TermType.OTHER:
             self.__handle_proof_step(step, undo=undo)
-        elif self.__is_proof_term(step):
+        elif self.context.is_proof_term(step):
             self.__handle_proof_term(step, undo=undo)
 
-    def __is_segment_delimiter(self, step: Step):
-        return self.context.expr(step)[0] in [
-            "VernacEndSegment",
-            "VernacDefineModule",
-            "VernacDeclareModuleType",
-            "VernacBeginSection",
-        ]
-
     def __step(self, step: Step, undo: bool):
         file_change = self.__aux_file.truncate if undo else self.__aux_file.append
         file_change(step.text)
         # Ignore segment delimiters because it affects Program handling
-        if self.__is_segment_delimiter(step):
+        if self.context.is_segment_delimiter(step):
             return
         # Found [Qed]/[Defined]/[Admitted] or [Proof <exact>.]
-        if self.__is_end_proof(step):
+        if self.context.is_end_proof(step):
             self.__handle_end_proof(step, undo=undo)
         # New obligations were introduced
         elif self.__has_obligations(step):
@@ -685,12 +658,12 @@ def __local_exec(self, n_steps=1):
     def __add_step(self, index: int):
         step = self.steps[index]
         # Ignore segment delimiters because it affects Program handling
-        if self.__is_segment_delimiter(step):
+        if self.context.is_segment_delimiter(step):
             pass
 
         optional = self.__find_step(self.steps[index - 1].ast.range)
         # Handles case where Qed is added
-        if self.__is_end_proof(step):
+        if self.context.is_end_proof(step):
             # This is not outside of the ifs for performance reasons
             goals = self.__goals(step.ast.range.end)
             index = self.__find_proof_index(step)
@@ -700,7 +673,7 @@ def __add_step(self, index: int):
         elif self.__has_obligations(step):
             self.__handle_obligations(step)
         # Allows to add open proofs
-        elif self.__is_proof_term(step):
+        elif self.context.is_proof_term(step):
             # This is not outside of the ifs for performance reasons
             goals = self.__goals(step.ast.range.end)
             if self.__in_proof(goals):
@@ -722,12 +695,12 @@ def __add_step(self, index: int):
 
     def __delete_step(self, step: Step):
         # Ignore segment delimiters because it affects Program handling
-        if self.__is_segment_delimiter(step):
+        if self.context.is_segment_delimiter(step):
             return
 
         optional = self.__find_step(step.ast.range)
         # Handles case where Qed is deleted
-        if self.__is_end_proof(step):
+        if self.context.is_end_proof(step):
             index = self.__find_proof_index(step) - 1
             open_index = self.__find_open_proof_index(step)
             self.__handle_end_proof(step, index=index, open_index=open_index, undo=True)
@@ -816,7 +789,7 @@ def __is_proven(self, proof: ProofTerm) -> bool:
         if len(proof.steps) == 0:
             return False
         return (
-            self.__is_end_proof(proof.steps[-1].step)
+            self.context.is_end_proof(proof.steps[-1].step)
             and "Admitted" not in proof.steps[-1].step.short_text
         )
 

diff --git a/coqpyt/tests/proof_file/expected/valid_file.yml b/coqpyt/tests/proof_file/expected/valid_file.yml
@@ -185,7 +185,7 @@ proofs:
           end:
             line: 25
             character: 16
-      - text: "\n  Defined."
+      - text: "\n  Abort."
         goals:
           position:
             line: 26
@@ -196,7 +196,7 @@ proofs:
             character: 2
           end:
             line: 26
-            character: 10
+            character: 8
     context:
       - "8.19.x":
           text: "Notation \"∀ x .. y , P\" := (forall x, .. (forall y, P) ..) (at level 10, x binder, y binder, P at level 200, format \"'[ ' '[ ' ∀ x .. y ']' , '/' P ']'\") : type_scope."
@@ -275,7 +275,7 @@ proofs:
         context:
           - text: "Ltac reduce_eq := simpl; reflexivity."
             type: TACTIC
-      - text: "\n    Qed."
+      - text: "\n    Defined."
         goals:
           position:
             line: 38

diff --git a/coqpyt/tests/resources/test_valid.v b/coqpyt/tests/resources/test_valid.v
@@ -24,7 +24,7 @@ Section Random.
     rewrite -> (plus_O_n (S n * m)).
     Compute True /\ True.
     reflexivity.
-  Defined.
+  Abort.
 End Random.
 
 Module Extra.
@@ -36,7 +36,7 @@ Module Extra.
       Compute mk_example n n.
       Compute Out.In.plus_O_n.
       reduce_eq.
-    Qed.
+    Defined.
   End Fst.
 
   Module Snd.