From 35ebaaa4b5f8303faede4973d7d808302e22829e Mon Sep 17 00:00:00 2001 From: Pedro Carrott <43729507+pcarrott@users.noreply.github.com> Date: Fri, 18 Oct 2024 17:05:31 +0100 Subject: [PATCH] (incomplete) handling of aborted proofs (#56) --- coqpyt/coq/context.py | 53 ++++++++++++++++++- coqpyt/coq/proof_file.py | 45 ++++------------ .../tests/proof_file/expected/valid_file.yml | 6 +-- coqpyt/tests/resources/test_valid.v | 4 +- 4 files changed, 66 insertions(+), 42 deletions(-) diff --git a/coqpyt/coq/context.py b/coqpyt/coq/context.py index e2b457d..26f0d86 100644 --- 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 index 0597f4f..899d904 100644 --- 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 .] - 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 index 4e1b4aa..5d8c695 100644 --- 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 index 0a00dc0..85d32bf 100644 --- 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.