Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)

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.