diff options
author | 2018-02-21 19:02:56 +0100 | |
---|---|---|
committer | 2018-02-21 19:02:56 +0100 | |
commit | 4b0fe4e09d547f0e6ee98da3fd6f7a134e51f3fd (patch) | |
tree | 9550d5b99c9023c9c0ad84d2d7b89e05f344348b /test-suite | |
parent | 2f13806f10b2781f84417014c8018097c8e8b2ad (diff) | |
parent | 2aff5c40ba9b40b4e0188b799dde6f31585e356b (diff) |
Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/bugs/closed/5532.v | 15 | ||||
-rw-r--r-- | test-suite/output/Notations.out | 2 | ||||
-rw-r--r-- | test-suite/output/Notations2.out | 7 | ||||
-rw-r--r-- | test-suite/output/Notations2.v | 5 | ||||
-rw-r--r-- | test-suite/output/Notations3.out | 97 | ||||
-rw-r--r-- | test-suite/output/Notations3.v | 167 | ||||
-rw-r--r-- | test-suite/output/PatternsInBinders.out | 8 | ||||
-rw-r--r-- | test-suite/output/PatternsInBinders.v | 5 | ||||
-rw-r--r-- | test-suite/success/Notations2.v | 29 |
9 files changed, 323 insertions, 12 deletions
diff --git a/test-suite/bugs/closed/5532.v b/test-suite/bugs/closed/5532.v new file mode 100644 index 000000000..ee5446e54 --- /dev/null +++ b/test-suite/bugs/closed/5532.v @@ -0,0 +1,15 @@ +(* A wish granted by the new support for patterns in notations *) + +Local Notation mkmatch0 e p + := match e with + | p => true + | _ => false + end. +Local Notation "'mkmatch' [[ e ]] [[ p ]]" + := match e with + | p => true + | _ => false + end + (at level 0, p pattern). +Check mkmatch0 _ ((0, 0)%core). +Check mkmatch [[ _ ]] [[ ((0, 0)%core) ]]. diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 2f0ee765d..891296b0a 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -41,7 +41,7 @@ fun x : nat => ifn x is succ n then n else 0 -4 : Z The command has indeed failed with message: -x should not be bound in a recursive pattern of the right-hand side. +Cannot find where the recursive pattern starts. The command has indeed failed with message: in the right-hand side, y and z should appear in term position as part of a recursive pattern. diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 121a369a9..6ffe56e11 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -17,10 +17,9 @@ fun (P : nat -> nat -> Prop) (x : nat) => exists y, P x y ∃ n p : nat, n + p = 0 : Prop let a := 0 in -∃ x y : nat, -let b := 1 in -let c := b in -let d := 2 in ∃ z : nat, let e := 3 in let f := 4 in x + y = z + d +∃ (x y : nat) (b := 1) (c := b) (d := 2) (z : nat), +let e := 3 in +let f := 4 in x + y = z + d : Prop ∀ n p : nat, n + p = 0 : Prop diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index 531398bb0..923caedac 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -36,8 +36,9 @@ Check fun P:nat->nat->Prop => fun x:nat => ex (P x). (* Test notations with binders *) -Notation "∃ x .. y , P":= (ex (fun x => .. (ex (fun y => P)) ..)) - (x binder, y binder, at level 200, right associativity). +Notation "∃ x .. y , P":= (ex (fun x => .. (ex (fun y => P)) ..)) + (x binder, y binder, at level 200, right associativity, + format "'[ ' ∃ x .. y ']' , P"). Check (∃ n p, n+p=0). diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 1b5725275..e6a6e0288 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -138,3 +138,100 @@ amatch = mmatch 0 (with 0 => 1| 1 => 2 end) : unit alist = [0; 1; 2] : list nat +! '{{x, y}}, x + y = 0 + : Prop +exists x : nat, + nat -> + exists y : nat, + nat -> + exists '{{u, t}}, forall z1 : nat, z1 = 0 /\ x + y = 0 /\ u + t = 0 + : Prop +exists x : nat, + nat -> + exists y : nat, + nat -> + exists '{{z, t}}, forall z2 : nat, z2 = 0 /\ x + y = 0 /\ z + t = 0 + : Prop +exists_true '{{x, y}} (u := 0) '{{z, t}}, x + y = 0 /\ z + t = 0 + : Prop +exists_true (A : Type) (R : A -> A -> Prop) (_ : Reflexive R), +(forall x : A, R x x) + : Prop +exists_true (x : nat) (A : Type) (R : A -> A -> Prop) +(_ : Reflexive R) (y : nat), x + y = 0 -> forall z : A, R z z + : Prop +{{{{True, nat -> True}}, nat -> True}} + : Prop * Prop * Prop +{{D 1, 2}} + : nat * nat * (nat * nat * (nat * nat)) +! a b : nat # True # + : Prop * (Prop * Prop) +!!!! a b : nat # True # + : Prop * Prop * (Prop * Prop * Prop) +@@ a b : nat # a = b # b = a # + : Prop * Prop +exists_non_null x y z t : nat , x = y /\ z = t + : Prop +forall_non_null x y z t : nat , x = y /\ z = t + : Prop +{{RL 1, 2}} + : nat * (nat * nat) +{{RR 1, 2}} + : nat * nat * nat +@pair nat (prod nat nat) (S (S O)) (@pair nat nat (S O) O) + : prod nat (prod nat nat) +@pair (prod nat nat) nat (@pair nat nat O (S (S O))) (S O) + : prod (prod nat nat) nat +{{RLRR 1, 2}} + : nat * (nat * nat) * (nat * nat * nat) * (nat * (nat * nat)) * + (nat * nat * nat) +pair + (pair + (pair (pair (S (S O)) (pair (S O) O)) (pair (pair O (S (S O))) (S O))) + (pair (S O) (pair (S (S O)) O))) (pair (pair O (S O)) (S (S O))) + : prod + (prod (prod (prod nat (prod nat nat)) (prod (prod nat nat) nat)) + (prod nat (prod nat nat))) (prod (prod nat nat) nat) +fun x : nat => if x is n .+ 1 then n else 1 + : nat -> nat +{'{{x, y}} : nat * nat | x + y = 0} + : Set +exists2' {{x, y}}, x = 0 & y = 0 + : Prop +myexists2 x : nat * nat, + let '{{y, z}} := x in y > z & let '{{y, z}} := x in z > y + : Prop +fun '({{x, y}} as z) => x + y = 0 /\ z = z + : nat * nat -> Prop +myexists ({{x, y}} as z), x + y = 0 /\ z = z + : Prop +exists '({{x, y}} as z), x + y = 0 /\ z = z + : Prop +∀ '({{x, y}} as z), x + y = 0 /\ z = z + : Prop +fun '({{{{x, y}}, true}} | {{{{x, y}}, false}}) => x + y + : nat * nat * bool -> nat +myexists ({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y + : Prop +exists '({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y + : Prop +∀ '({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y + : Prop +fun p : nat => if p is S n then n else 0 + : nat -> nat +fun p : comparison => if p is Lt then 1 else 0 + : comparison -> nat +fun S : nat => [S | S + S] + : nat -> nat * (nat -> nat) +fun N : nat => [N | N + 0] + : nat -> nat * (nat -> nat) +fun S : nat => [[S | S + S]] + : nat -> nat * (nat -> nat) +{I : nat | I = I} + : Set +{'I : True | I = I} + : Prop +{'{{x, y}} : nat * nat | x + y = 0} + : Set +exists2 '{{y, z}} : nat * nat, y > z & z > y + : Prop diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index a8d6c97fb..c98bfff41 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -253,3 +253,170 @@ Definition alist := [0;1;2]. Print alist. End B. + +(* Test contraction of "forall x, let 'pat := x in ..." into "forall 'pat, ..." *) +(* for isolated "forall" (was not working already in 8.6) *) +Notation "! x .. y , A" := (id (forall x, .. (id (forall y, A)) .. )) (at level 200, x binder). +Check ! '(x,y), x+y=0. + +(* Check that the terminator of a recursive pattern is interpreted in + the correct environment of bindings *) +Notation "'exists_mixed' x .. y , P" := (ex (fun x => forall z:nat, .. (ex (fun y => forall z:nat, z=0 /\ P)) ..)) (at level 200, x binder). +Check exists_mixed x y '(u,t), x+y=0/\u+t=0. +Check exists_mixed x y '(z,t), x+y=0/\z+t=0. + +(* Check that intermediary let-in are inserted inbetween instances of + the repeated pattern *) +Notation "'exists_true' x .. y , P" := (exists x, True /\ .. (exists y, True /\ P) ..) (at level 200, x binder). +Check exists_true '(x,y) (u:=0) '(z,t), x+y=0/\z+t=0. + +(* Check that generalized binders are correctly interpreted *) + +Module G. +Generalizable Variables A R. +Class Reflexive {A:Type} (R : A->A->Prop) := reflexivity : forall x : A, R x x. +Check exists_true `{Reflexive A R}, forall x, R x x. +Check exists_true x `{Reflexive A R} y, x+y=0 -> forall z, R z z. +End G. + +(* Allows recursive patterns for binders to be associative on the left *) +Notation "!! x .. y # A #" := (.. (A,(forall x, True)) ..,(forall y, True)) (at level 200, x binder). +Check !! a b : nat # True #. + +(* Examples where the recursive pattern refer several times to the recursive variable *) + +Notation "{{D x , .. , y }}" := ((x,x), .. ((y,y),(0,0)) ..). +Check {{D 1, 2 }}. + +Notation "! x .. y # A #" := + ((forall x, x=x), .. ((forall y, y=y), A) ..) + (at level 200, x binder). +Check ! a b : nat # True #. + +Notation "!!!! x .. y # A #" := + (((forall x, x=x),(forall x, x=0)), .. (((forall y, y=y),(forall y, y=0)), A) ..) + (at level 200, x binder). +Check !!!! a b : nat # True #. + +Notation "@@ x .. y # A # B #" := + ((forall x, .. (forall y, A) ..), (forall x, .. (forall y, B) ..)) + (at level 200, x binder). +Check @@ a b : nat # a=b # b=a #. + +Notation "'exists_non_null' x .. y , P" := + (ex (fun x => x <> 0 /\ .. (ex (fun y => y <> 0 /\ P)) ..)) + (at level 200, x binder). +Check exists_non_null x y z t , x=y/\z=t. + +Notation "'forall_non_null' x .. y , P" := + (forall x, x <> 0 -> .. (forall y, y <> 0 -> P) ..) + (at level 200, x binder). +Check forall_non_null x y z t , x=y/\z=t. + +(* Examples where the recursive pattern is in reverse order *) + +Notation "{{RL c , .. , d }}" := (pair d .. (pair c 0) ..). +Check {{RL 1 , 2}}. + +Notation "{{RR c , .. , d }}" := (pair .. (pair 0 d) .. c). +Check {{RR 1 , 2}}. + +Set Printing All. +Check {{RL 1 , 2}}. +Check {{RR 1 , 2}}. +Unset Printing All. + +Notation "{{RLRR c , .. , d }}" := (pair d .. (pair c 0) .., pair .. (pair 0 d) .. c, pair c .. (pair d 0) .., pair .. (pair 0 c) .. d). +Check {{RLRR 1 , 2}}. +Unset Printing Notations. +Check {{RLRR 1 , 2}}. +Set Printing Notations. + +(* Check insensitivity of "match" clauses to order *) + +Notation "'if' t 'is' n .+ 1 'then' p 'else' q" := + (match t with S n => p | 0 => q end) + (at level 200). +Check fun x => if x is n.+1 then n else 1. + +(* Examples with binding patterns *) + +Check {'(x,y)|x+y=0}. + +Module D. +Notation "'exists2'' x , p & q" := (ex2 (fun x => p) (fun x => q)) + (at level 200, x pattern, p at level 200, right associativity, + format "'[' 'exists2'' '/ ' x , '/ ' '[' p & '/' q ']' ']'") + : type_scope. + +Check exists2' (x,y), x=0 & y=0. +End D. + +(* Ensuring for reparsability that printer of notations does not use a + pattern where only an ident could be reparsed *) + +Module E. +Inductive myex2 {A:Type} (P Q:A -> Prop) : Prop := + myex_intro2 : forall x:A, P x -> Q x -> myex2 P Q. +Notation "'myexists2' x : A , p & q" := (myex2 (A:=A) (fun x => p) (fun x => q)) + (at level 200, x ident, A at level 200, p at level 200, right associativity, + format "'[' 'myexists2' '/ ' x : A , '/ ' '[' p & '/' q ']' ']'") + : type_scope. +Check myex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y). +End E. + +(* A canonical example of a notation with a non-recursive binder *) + +Parameter myex : forall {A}, (A -> Prop) -> Prop. +Notation "'myexists' x , p" := (myex (fun x => p)) + (at level 200, x pattern, p at level 200, right associativity). + +(* A canonical example of a notation with recursive binders *) + +Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity) : type_scope. + +(* Check that printing 'pat uses an "as" when the variable bound to + the pattern is dependent. We check it for the three kinds of + notations involving bindings of patterns *) + +Check fun '((x,y) as z) => x+y=0/\z=z. (* Primitive fun/forall *) +Check myexists ((x,y) as z), x+y=0/\z=z. (* Isolated binding pattern *) +Check exists '((x,y) as z), x+y=0/\z=z. (* Applicative recursive binder *) +Check ∀ '((x,y) as z), x+y=0/\z=z. (* Other example of recursive binder, now treated as the exists case *) + +(* Check parsability and printability of irrefutable disjunctive patterns *) + +Check fun '(((x,y),true)|((x,y),false)) => x+y. +Check myexists (((x,y),true)|((x,y),false)), x>y. +Check exists '(((x,y),true)|((x,y),false)), x>y. +Check ∀ '(((x,y),true)|((x,y),false)), x>y. + +(* Check Georges' printability of a "if is then else" notation *) + +Notation "'if' c 'is' p 'then' u 'else' v" := + (match c with p => u | _ => v end) + (at level 200, p pattern at level 100). +Check fun p => if p is S n then n else 0. +Check fun p => if p is Lt then 1 else 0. + +(* Check that mixed binders and terms defaults to ident and not pattern *) +Module F. + (* First without an indirection *) +Notation "[ n | t ]" := (n, (fun n : nat => t)). +Check fun S : nat => [ S | S+S ]. +Check fun N : nat => (N, (fun n => n+0)). (* another test in passing *) + (* Then with an indirection *) +Notation "[[ n | p | t ]]" := (n, (fun p : nat => t)). +Notation "[[ n | t ]]" := [[ n | n | t ]]. +Check fun S : nat => [[ S | S+S ]]. +End F. + +(* Check parsability/printability of {x|P} and variants *) + +Check {I:nat|I=I}. +Check {'I:True|I=I}. +Check {'(x,y)|x+y=0}. + +(* Check exists2 with a pattern *) +Check ex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y). diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out index 95be04c32..8a6d94c73 100644 --- a/test-suite/output/PatternsInBinders.out +++ b/test-suite/output/PatternsInBinders.out @@ -31,7 +31,7 @@ exists '(x, y) '(z, w), swap (x, y) = (z, w) : Prop both_z = fun pat : nat * nat => -let '(n, p) as pat0 := pat return (F pat0) in (Z n, Z p) : F (n, p) +let '(n, p) as x := pat return (F x) in (Z n, Z p) : F (n, p) : forall pat : nat * nat, F pat fun '(x, y) '(z, t) => swap (x, y) = (z, t) : A * B -> B * A -> Prop @@ -39,3 +39,9 @@ forall '(x, y) '(z, t), swap (x, y) = (z, t) : Prop fun (pat : nat) '(x, y) => x + y = pat : nat -> nat * nat -> Prop +f = fun x : nat => x + x + : nat -> nat + +Argument scope is [nat_scope] +fun x : nat => x + x + : nat -> nat diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v index 0bad472f4..d671053c0 100644 --- a/test-suite/output/PatternsInBinders.v +++ b/test-suite/output/PatternsInBinders.v @@ -67,3 +67,8 @@ End Suboptimal. (** Test risk of collision for internal name *) Check fun pat => fun '(x,y) => x+y = pat. + +(** Test name in degenerate case *) +Definition f 'x := x+x. +Print f. +Check fun 'x => x+x. diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index 2655b651a..7c2cf3ee5 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -92,16 +92,37 @@ Check ##### 0 _ 0%bool 0%bool : prod' bool bool. Check fun A (x :prod' bool A) => match x with ##### 0 _ y 0%bool => 2 | _ => 1 end. (* 10. Check computation of binding variable through other notations *) -(* i should be detected as binding variable and the scopes not being checked *) - +(* it should be detected as binding variable and the scopes not being checked *) Notation "'FUNNAT' i => t" := (fun i : nat => i = t) (at level 200). Notation "'Funnat' i => t" := (FUNNAT i => t + i%nat) (at level 200). (* 11. Notations with needed factorization of a recursive pattern *) (* See https://github.com/coq/coq/issues/6078#issuecomment-342287412 *) -Module A. +Module M11. Notation "[:: x1 ; .. ; xn & s ]" := (cons x1 .. (cons xn s) ..). Notation "[:: x1 ; .. ; xn ]" := (cons x1 .. (cons xn nil) ..). Check [:: 1 ; 2 ; 3 ]. Check [:: 1 ; 2 ; 3 & nil ]. (* was failing *) -End A. +End M11. + +(* 12. Preventively check that a variable which does not occur can be instantiated *) +(* by any term. In particular, it should not be restricted to a binder *) +Module M12. +Notation "N ++ x" := (S x) (only parsing). +Check 2 ++ 0. +End M12. + +(* 13. Check that internal data about associativity are not used in comparing levels *) +Module M13. +Notation "x ;; z" := (x + z) + (at level 100, z at level 200, only parsing, right associativity). +Notation "x ;; z" := (x * z) + (at level 100, z at level 200, only parsing) : foo_scope. +End M13. + +(* 14. Check that a notation with a "ident" binder does not include a pattern *) +Module M14. +Notation "'myexists' x , p" := (ex (fun x => p)) + (at level 200, x ident, p at level 200, right associativity) : type_scope. +Check myexists I, I = 0. (* Should not be seen as a constructor *) +End M14. |