From 65505b835d6a77b8702d11d09e8cf6b84c529c65 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Aug 2017 13:42:01 +0200 Subject: Adding support for re-folding notation referring to isolated "forall '(x,y), t". Was apparently forgotten in a67bd7f9. --- test-suite/output/Notations3.v | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'test-suite/output/Notations3.v') diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index a8d6c97fbd..773241f90e 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -253,3 +253,8 @@ 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. -- cgit v1.2.3 From 7c10b4020e061fb14e01cb3abc92bb5265aa65b9 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 13 Aug 2017 18:17:32 +0200 Subject: Fixing/improving notations with recursive patterns. - The "terminator" of a recursive notation is now interpreted in the environment in which it occurs rather than the environment at the beginning of the recursive patterns. Note that due to a tolerance in checking unbound variables of notations, a variable unbound in the environment was still working ok as long as no user-given variable was shadowing a private variable of the notation - see the "exists_mixed" example in test-suite. Conversely, in a notation such as: Notation "!! x .. y # A #" := ((forall x, True), .. ((forall y, True), A) ..) (at level 200, x binder). Check !! a b # a=b #. The unbound "a" was detected only at pretyping and not as expected at internalizing time, due to "a=b" interpreted in context containing a and b. - Similarly, each binder is now interpreted in the environment in which it occurs rather than as if the sequence of binders was dependent from the left to the right (such a dependency was ok for "forall" or "exists" but not in general). For instance, in: Notation "!! x .. y # A #" := ((forall x, True), .. ((forall y, True), A) ..) (at level 200, x binder). Check !! (a:nat) (b:a=a) # True #. The illegal dependency of the type of b in a was detected only at pretyping time. - If a let-in occurs in the sequence of binders of a notation with a recursive pattern, it is now inserted in between the occurrences of the iterator rather than glued with the forall/fun of the iterator. For instance, in: 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), x=y. We now get exists '(x, y), True /\ (let u := 0 in True /\ x = y) while we had before the let-in breaking the repeated pattern: exists '(x, y), (let u := 0 in True /\ x = y) This is more compositional, and, in particular, the printer algorithm now recognizes the pattern which is otherwise broken. --- test-suite/output/Notations3.v | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) (limited to 'test-suite/output/Notations3.v') diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 773241f90e..3e07fbce91 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -258,3 +258,23 @@ End B. (* 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. -- cgit v1.2.3 From d4c2ed95fcfd64cdcc10e51e40be739d9f1c4a74 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 13 Aug 2017 20:05:03 +0200 Subject: Allows recursive patterns for binders to be associative on the left. This makes treatment of recursive binders closer to the one of recursive terms. It is unclear whether there are interesting notations liable to use this, but this shall make easier mixing recursive binders and recursive terms as in next commits. Example of (artificial) notation that this commit supports: Notation "! x .. y # A #" := (.. (A,(forall x, True)) ..,(forall y, True)) (at level 200, x binder). --- test-suite/output/Notations3.v | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'test-suite/output/Notations3.v') diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 3e07fbce91..a7fed35611 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -278,3 +278,7 @@ 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 #. -- cgit v1.2.3 From a18e87f6a929ce296f8c277b310e286151e06293 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 14 Aug 2017 01:27:04 +0200 Subject: Allowing variables used in recursive notation to occur several times in pattern. This allows for instance to support recursive notations of the form: 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). --- test-suite/output/Notations3.v | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) (limited to 'test-suite/output/Notations3.v') diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index a7fed35611..c7e32f733a 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -282,3 +282,28 @@ 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. -- cgit v1.2.3 From 96d6ef7036e19bf1def1512abae5ef8c6ace06b0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 14 Aug 2017 13:29:39 +0200 Subject: Supporting recursive notations reversing the left-to-right order. Seizing this opportunity to generalize the possibility for different associativity into simply reversing the order or not. Also dropping some dead code. Example of recursive notation now working: Notation "[ a , .. , b |- A ]" := (cons b .. (cons a nil) .., A). --- test-suite/output/Notations3.v | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) (limited to 'test-suite/output/Notations3.v') diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index c7e32f733a..fd5846e71c 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -307,3 +307,22 @@ 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. + +(* 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. -- cgit v1.2.3 From 34cf92821e03a2c6ce64c78c66a00624d0fe9c99 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 15 Aug 2017 14:55:44 +0200 Subject: In printing notations with "match", reasoning up to the order of clauses. --- test-suite/output/Notations3.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'test-suite/output/Notations3.v') diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index fd5846e71c..d81cc702af 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -326,3 +326,10 @@ 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. -- cgit v1.2.3 From 398358618bb3eabfe822b79c669703c1c33b67e6 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 15 Aug 2017 18:32:02 +0200 Subject: Adding patterns in the category of binders for notations. For instance, the following is now possible: Check {(x,y)|x+y=0}. Some questions remains. Maybe, by consistency, the notation should be "{'(x,y)|x+y=0}"... --- test-suite/output/Notations3.v | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'test-suite/output/Notations3.v') diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index d81cc702af..201198b3eb 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -333,3 +333,7 @@ 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}. -- cgit v1.2.3 From edd0d22429354a5f2c703a8c7bd1f775e2f97d9e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Aug 2017 09:15:40 +0200 Subject: Adding support for parsing subterms of a notation as "pattern". This allows in particular to define notations with 'pat style binders. E.g.: A non-trivial change in this commit is storing binders and patterns separately from terms. This is not strictly necessary but has some advantages. However, it is relatively common to have binders also used as terms, or binders parsed as terms. Thus, it is already relatively common to embed binders into terms (see e.g. notation for ETA in output test Notations3.v) or to coerce terms to idents (see e.g. the notation for {x|P} where x is parsed as a constr). So, it is as simple to always store idents (and eventually patterns) as terms. --- test-suite/output/Notations3.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'test-suite/output/Notations3.v') diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 201198b3eb..46e0c1b1b5 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -337,3 +337,10 @@ Check fun x => if x is n.+1 then n else 1. (* Examples with binding patterns *) Check {(x,y)|x+y=0}. + +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. -- cgit v1.2.3 From 3a6b1d2c04ceeb568accbc9ddfc3fc0f14faf25b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 17 Aug 2017 12:35:56 +0200 Subject: Respecting the ident/pattern distinction in notation modifiers. --- test-suite/output/Notations3.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'test-suite/output/Notations3.v') diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 46e0c1b1b5..ee6f0a09e0 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -338,9 +338,16 @@ Check fun x => if x is n.+1 then n else 1. 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 *) + +Check ex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y). -- cgit v1.2.3 From bc73f267ad2da0f1e24e66cb481725be018a8ce6 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 21 Aug 2017 23:25:21 +0200 Subject: A (significant) simplification in printing notations with recursive binders. For historical reasons (this was one of the first examples of notations with binders), there was a special treatment for notations whose right-hand side had the form "forall x, P" or "fun x => P". Not only this is not necessary, but this prevents notations binding to expressions such as "forall x, x>0 -> P" to be used in printing. We let the general case absorb this particular case. We add the integration of "let x:=c in ..." in the middle of a notation with recursive binders as part of the binder list, reprinting it "(x:=c)" (this was formerly the case only for the above particular case). Note that integrating "let" in sequence of binders is stil not the case for the regular "forall"/"fun". Should we? --- test-suite/output/Notations3.v | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'test-suite/output/Notations3.v') diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index ee6f0a09e0..d768b9ba49 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -308,6 +308,11 @@ Notation "'exists_non_null' x .. y , 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) ..). -- cgit v1.2.3 From 50970e4043d73d9a4fbd17ffe765745f6d726317 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 21 Aug 2017 23:01:04 +0200 Subject: Using an "as" clause when needed for printing irrefutable patterns. Example which is now reprinted as parsed: fun '((x,y) as z) => (y,x)=z --- test-suite/output/Notations3.v | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) (limited to 'test-suite/output/Notations3.v') diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index d768b9ba49..9ec459ed69 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -356,3 +356,23 @@ End D. pattern where only an ident could be reparsed *) Check ex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y). + +(* 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 *) -- cgit v1.2.3 From e4d93d1cef27d3a8c1e36139fc1e118730406f67 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 17 Aug 2017 20:12:55 +0200 Subject: Adding general support for irrefutable disjunctive patterns. This now works not only for parsing of fun/forall (as in 8.6), but also for arbitraty notations with binders and for printing. --- test-suite/output/Notations3.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'test-suite/output/Notations3.v') diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 9ec459ed69..9f6302f6f2 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -376,3 +376,10 @@ 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. -- cgit v1.2.3 From 5806b0476a1ac9b903503641cc3e2997d3e8d960 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 24 Aug 2017 15:18:23 +0200 Subject: When printing a notation with "match", more flexibility in matching equations. We reason up to order, and accept to match a final catch-all clauses with any other clause. This allows for instance to parse and print a notation of the form "if t is S n then p else q". --- test-suite/output/Notations3.v | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'test-suite/output/Notations3.v') diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 9f6302f6f2..b4ad4a7b3c 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -383,3 +383,11 @@ 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. -- cgit v1.2.3 From dcfd5c2c2cefcd8ae6a5b2e90fcbd98da4f1b120 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 25 Nov 2017 20:50:03 +0100 Subject: Notations: Adding modifiers to tell which kind of binder a constr can parse. Concretely, we provide "constr as ident", "constr as strict pattern" and "constr as pattern". This tells to parse a binder as a constr, restricting to only ident or to only a strict pattern, or to a pattern which can also be an ident. The "strict pattern" modifier allows to restrict the use of patterns in printing rules. This allows e.g. to select the appropriate rule for printing between {x|P} and {'pat|P}. --- test-suite/output/Notations3.v | 2 -- 1 file changed, 2 deletions(-) (limited to 'test-suite/output/Notations3.v') diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index b4ad4a7b3c..9ea218481e 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -341,8 +341,6 @@ 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, -- cgit v1.2.3 From 0c4eea2553d5b3b70d0b5baaf92781a544de83bd Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 23 Nov 2017 13:30:36 +0100 Subject: Change default for notations with variables bound to both terms and binders. For compatibility, the default is to parse as ident and not as pattern. --- test-suite/output/Notations3.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'test-suite/output/Notations3.v') diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 9ea218481e..df3d86793f 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -389,3 +389,15 @@ Notation "'if' c 'is' p 'then' u 'else' v" := (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 E. + (* 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 E. -- cgit v1.2.3 From 9fe03a830ae7b10e1c5fb2b9d41213257bd617f0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 3 Nov 2017 11:48:36 +0100 Subject: Adding notations of the form "{'pat|P}", "exists2 'pat, P & Q", etc. --- test-suite/output/Notations3.v | 27 ++++++++++++++++++++++++--- 1 file changed, 24 insertions(+), 3 deletions(-) (limited to 'test-suite/output/Notations3.v') diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index df3d86793f..f41ddac4d4 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -341,6 +341,10 @@ Check fun x => if x is n.+1 then n else 1. (* Examples with binding patterns *) +Import SpecifPatternNotations. + +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, @@ -353,7 +357,15 @@ End D. (* Ensuring for reparsability that printer of notations does not use a pattern where only an ident could be reparsed *) -Check ex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y). +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 *) @@ -391,7 +403,7 @@ 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 E. +Module F. (* First without an indirection *) Notation "[ n | t ]" := (n, (fun n : nat => t)). Check fun S : nat => [ S | S+S ]. @@ -400,4 +412,13 @@ Check fun N : nat => (N, (fun n => n+0)). (* another test in passing *) Notation "[[ n | p | t ]]" := (n, (fun p : nat => t)). Notation "[[ n | t ]]" := [[ n | n | t ]]. Check fun S : nat => [[ S | S+S ]]. -End E. +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). -- cgit v1.2.3 From 0af54860172efe1aa5da419b81e4cb34348320ee Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 23 Nov 2017 13:42:41 +0100 Subject: Trying a hack to support {'pat|P} without breaking compatibility. Concretely, we bypass the following limitation: The notation "{ ' pat | P }" broke the parsing of expressions of the form "{ forall x, P } + { Q }". Indeed the latter works thanks to a tolerance of Camlp5 in parsing "forall x, P" at level 200 while the rule asks to actually parse the interior of "{ ... }" at level 99 (the reason for 99 is to be below the rule for "M : T" which is at level 100, so that "{ x : A | P }" does not see "x : A" as a cast). Adding an extra "'"; pat = pattern in parallel to c = constr LEVEL "99" broke the tolerance for constr at level 200. We fix this by adding an ad hoc rule for "{ binder_constr }" in the native grammar (g_constr.ml4). Actually, this is inconsistent with having a rule for "{ constr at level 99 }" in Notations.v. We should have both rules in Notations.v or both rules hard-wired in the native grammar. But I still don't know what is the best decision to take, so leaving as it at the current time. Advantages of hard-wiring both rules in g_constr.ml4: a bit simpler in metasyntax.ml (no need to ensure that the rule exist). Disadvantages: if one wants a different initial state without the business needing the "{ }" for sumbool, sumor, sig, sigT, one still have the rules there. Advantages of having them in Notations.v: more modular, we can change the initial state. Disadvantages: one would need a new kind of modifier, something like "x at level 99 || binder_constr", with all the difficulty to find a nice, intuitive, name for "binder_constr", and the difficulty of understanding if there is a generality to this "||" disjunction operator, and whether it should be documented or not. --- test-suite/output/Notations3.v | 2 -- 1 file changed, 2 deletions(-) (limited to 'test-suite/output/Notations3.v') diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index f41ddac4d4..c98bfff413 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -341,8 +341,6 @@ Check fun x => if x is n.+1 then n else 1. (* Examples with binding patterns *) -Import SpecifPatternNotations. - Check {'(x,y)|x+y=0}. Module D. -- cgit v1.2.3