Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
53 changes: 52 additions & 1 deletion coqpyt/coq/context.py
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
45 changes: 9 additions & 36 deletions coqpyt/coq/proof_file.py
Original file line number Diff line number Diff line change
Expand Up @@ -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):
Expand Down Expand Up @@ -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)
Expand All @@ -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):
Expand All @@ -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)
Expand Down Expand Up @@ -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
)

Expand Down
6 changes: 3 additions & 3 deletions coqpyt/tests/proof_file/expected/valid_file.yml
Original file line number Diff line number Diff line change
Expand Up @@ -185,7 +185,7 @@ proofs:
end:
line: 25
character: 16
- text: "\n Defined."
- text: "\n Abort."
goals:
position:
line: 26
Expand All @@ -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."
Expand Down Expand Up @@ -275,7 +275,7 @@ proofs:
context:
- text: "Ltac reduce_eq := simpl; reflexivity."
type: TACTIC
- text: "\n Qed."
- text: "\n Defined."
goals:
position:
line: 38
Expand Down
4 changes: 2 additions & 2 deletions coqpyt/tests/resources/test_valid.v
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ Section Random.
rewrite -> (plus_O_n (S n * m)).
Compute True /\ True.
reflexivity.
Defined.
Abort.
End Random.

Module Extra.
Expand All @@ -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.
Expand Down
Loading