Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Refactor ProofFile tests #25

Merged
merged 9 commits into from
Nov 21, 2023
Merged

Refactor ProofFile tests #25

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
8ac8d21
Refactor test_get_proofs
Nfsaavedra Nov 16, 2023
d09cee4
Refactor test_get_proofs_valid_change
Nfsaavedra Nov 16, 2023
2baea51
black
Nfsaavedra Nov 16, 2023
07f2051
refactor some more tests
Nfsaavedra Nov 17, 2023
c2e8c2f
WIP: refactor proof file tests structure
Nfsaavedra Nov 20, 2023
a09a72e
Refactor tests to classes
Nfsaavedra Nov 21, 2023
6b2b644
Split proof_file tests
Nfsaavedra Nov 21, 2023
b086842
black
Nfsaavedra Nov 21, 2023
1f753f8
add yaml to requirements
Nfsaavedra Nov 21, 2023
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
7 changes: 4 additions & 3 deletions coqpyt/coq/base_file.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -425,9 +425,10 @@ def current_goals(self) -> Optional[GoalAnswer]:
Returns:
Optional[GoalAnswer]: Goals in the current position if there are goals.
"""
end_pos = (
Position(0, 0) if self.steps_taken == 0 else self.prev_step.ast.range.end
)
if self.steps_taken == len(self.steps):
end_pos = self.prev_step.ast.range.end
else:
end_pos = self.curr_step.ast.range.start

if end_pos != self.__last_end_pos:
self.__current_goals = self._goals(end_pos)
Expand Down
179 changes: 179 additions & 0 deletions coqpyt/tests/proof_file/expected/imports.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,179 @@
proofs:
# 1st proof
- text: "Theorem plus_O_n : forall n:nat, 0 + n = n."
steps:
- text: "\nProof."
goals:
goals:
goals:
- hyps: []
ty: "∀ n : nat, 0 + n = n"
position:
line: 6
character: 0
- text: "\n intros n."
goals:
goals:
goals:
- hyps: []
ty: "∀ n : nat, 0 + n = n"
position:
line: 7
character: 2
- text: "\n Print plus."
goals:
goals:
goals:
- hyps:
- names:
- n
ty: nat
ty: "0 + n = n"
position:
line: 8
character: 2
context:
- text: "Notation plus := Nat.add (only parsing)."
type: NOTATION
- text: "\n Print Nat.add."
goals:
goals:
goals:
- hyps:
- names:
- n
ty: nat
ty: "0 + n = n"
position:
line: 9
character: 2
context:
- text: 'Fixpoint add n m := match n with | 0 => m | S p => S (p + m) end where "n + m" := (add n m) : nat_scope.'
type: FIXPOINT
- text: "\n reduce_eq."
goals:
goals:
goals:
- hyps:
- names:
- n
ty: nat
ty: "0 + n = n"
position:
line: 10
character: 2
context:
- text: "Ltac reduce_eq := simpl; reflexivity."
type: TACTIC
- text: "\nQed."
goals:
position:
line: 11
character: 0
context:
- text: "Inductive nat : Set := | O : nat | S : nat -> nat."
type: INDUCTIVE
- text: 'Notation "x = y" := (eq x y) : type_scope.'
type: NOTATION
- text: 'Fixpoint add n m := match n with | 0 => m | S p => S (p + m) end where "n + m" := (add n m) : nat_scope.'
type: NOTATION
# 2nd proof
- text: "Definition mult_0_plus : ∀ n m : nat, 0 + (S n * m) = S n * m."
steps:
- text: "\nProof."
goals:
goals:
goals:
- hyps: []
ty: "∀ n m : nat, 0 + S n * m = S n * m"
position:
line: 15
character: 0
- text: "\n intros n m."
goals:
goals:
goals:
- hyps: []
ty: "∀ n m : nat, 0 + S n * m = S n * m"
position:
line: 16
character: 2
- text: "\n rewrite -> (plus_O_n (S n * m))."
goals:
goals:
goals:
- hyps:
- names:
- n
- m
ty: nat
ty: "0 + S n * m = S n * m"
position:
line: 17
character: 2
context:
- text: "Local Theorem plus_O_n : forall n:nat, 0 + n = n."
type: THEOREM
- text: 'Fixpoint mul n m := match n with | 0 => 0 | S p => m + p * m end where "n * m" := (mul n m) : nat_scope.'
type: NOTATION
- text: "Inductive nat : Set := | O : nat | S : nat -> nat."
type: INDUCTIVE
- text: "\n Locate test_import2.plus_O_n."
goals:
goals:
goals:
- hyps:
- names:
- n
- m
ty: nat
ty: "S n * m = S n * m"
position:
line: 18
character: 2
# FIXME in the future we should get a Local Theorem from the other file here
- text: "\n Locate Peano.plus_O_n."
goals:
goals:
goals:
- hyps:
- names:
- n
- m
ty: nat
ty: "S n * m = S n * m"
position:
line: 19
character: 2
context:
- text: "Lemma plus_O_n : forall n:nat, 0 + n = n."
type: LEMMA
- text: "\n reflexivity."
goals:
goals:
goals:
- hyps:
- names:
- n
- m
ty: nat
ty: "S n * m = S n * m"
position:
line: 20
character: 2
- text: "\nDefined."
goals:
position:
line: 21
character: 0
context:
- text: "Notation \"∀ x .. y , P\" := (forall x, .. (forall y, P) ..) (at level 200, x binder, y binder, right associativity, format \"'[ ' '[ ' ∀ x .. y ']' , '/' P ']'\") : type_scope."
type: NOTATION
- text: 'Notation "x = y" := (eq x y) : type_scope.'
type: NOTATION
- text: 'Fixpoint add n m := match n with | 0 => m | S p => S (p + m) end where "n + m" := (add n m) : nat_scope.'
type: NOTATION
- text: 'Fixpoint mul n m := match n with | 0 => 0 | S p => m + p * m end where "n * m" := (mul n m) : nat_scope.'
type: NOTATION
- text: "Inductive nat : Set := | O : nat | S : nat -> nat."
type: INDUCTIVE
41 changes: 41 additions & 0 deletions coqpyt/tests/proof_file/expected/list_notation.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
proofs:
- text: "Goal [1] ++ [2] = [1; 2]."
steps:
- text: "\nProof."
goals:
goals:
goals:
- hyps: []
ty: "[1] ++ [2] = [1; 2]"
position:
line: 4
character: 0
- text: " reflexivity."
goals:
goals:
goals:
- hyps: []
ty: "[1] ++ [2] = [1; 2]"
position:
line: 4
character: 7
context:
# FIXME issue #24
- text: "Class Reflexive (R : A -> A -> Prop) := reflexivity : forall x : A, R x x."
type: CLASS
- text: " Qed."
goals:
position:
line: 4
character: 20
context:
- text: 'Notation "x = y" := (eq x y) : type_scope.'
type: NOTATION
- text: 'Infix "++" := app (right associativity, at level 60) : list_scope.'
type: NOTATION
- text: 'Notation "[ x ]" := (cons x nil) : list_scope.'
type: NOTATION
module: ["ListNotations"]
- text: "Notation \"[ x ; y ; .. ; z ]\" := (cons x (cons y .. (cons z nil) ..)) (format \"[ '[' x ; '/' y ; '/' .. ; '/' z ']' ]\") : list_scope."
type: NOTATION
module: ["ListNotations"]
Loading