Merge PR #8187: Notation printing based on scopes (take 2, including bug fixes)

8 files changed, 197 insertions, 25 deletions

diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
index 6d65db9e22..5a548cfae4 100644
--- a/test-suite/output/Inductive.out
+++ b/test-suite/output/Inductive.out
@@ -1,6 +1,6 @@
 The command has indeed failed with message:
 Last occurrence of "list'" must have "A" as 1st argument in
- "A -> list' A -> list' (A * A)%type".
+ "A -> list' A -> list' (A * A)".
 Monomorphic Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=
     Foo : foo A x
 
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 94b86fc222..bec4fc1579 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -72,7 +72,7 @@ Nil
      : forall A : Type, list A
 NIL : list nat
      : list nat
-(false && I 3)%bool /\ I 6
+(false && I 3)%bool /\ (I 6)%bool
      : Prop
 [|1, 2, 3; 4, 5, 6|]
      : Z * Z * Z * (Z * Z * Z)
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index adab324cf0..2ffc3b14e2 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -30,7 +30,7 @@ Check (decomp (true,true) as t, u in (t,u)).
 
 Section A.
 
-Notation "! A" := (forall _:nat, A) (at level 60).
+Notation "! A" := (forall _:nat, A) (at level 60) : type_scope.
 
 Check ! (0=0).
 Check forall n, n=0.
@@ -195,9 +195,9 @@ Open Scope nat_scope.
 
 Coercion is_true := fun b => b=true.
 Coercion of_nat n := match n with 0 => true | _ => false end.
-Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10).
+Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10) : bool_scope.
 
-Check (false && I 3)%bool /\ I 6.
+Check (false && I 3)%bool /\ (I 6)%bool.
 
 (**********************************************************************)
 (* Check notations with several recursive patterns                    *)
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index bcb2468792..923caedace 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -71,6 +71,7 @@ Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2.
 (* Note: does not work for pattern *)
 Module A.
 Notation "f ( x )" := (f x) (at level 10, format "f ( x )").
+Open Scope nat_scope.
 Check fun f x => f x + S x.
 
 Open Scope list_scope.
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 48379f713d..f53313def9 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -128,25 +128,27 @@ return (1, 2, 3, 4)
      : nat
 *(1.2)
      : nat
-! '{{x, y}}, x.y = 0
+! '{{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
+    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
+    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
+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
+(_ : Reflexive R) (y : nat), x + y = 0 -> forall z : A, R z z
      : Prop
 {{{{True, nat -> True}}, nat -> True}}
      : Prop * Prop * Prop
@@ -182,22 +184,22 @@ pair
             (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}
+{'{{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
+fun '({{x, y}} as z) => x + y = 0 /\ z = z
      : nat * nat -> Prop
-myexists ({{x, y}} as z), x.y = 0 /\ z = z
+myexists ({{x, y}} as z), x + y = 0 /\ z = z
      : Prop
-exists '({{x, y}} as z), x.y = 0 /\ z = z
+exists '({{x, y}} as z), x + y = 0 /\ z = z
      : Prop
-∀ '({{x, y}} as z), x.y = 0 /\ z = z
+∀ '({{x, y}} as z), x + y = 0 /\ z = z
      : Prop
-fun '({{{{x, y}}, true}} | {{{{x, y}}, false}}) => x.y
+fun '({{{{x, y}}, true}} | {{{{x, y}}, false}}) => x + y
      : nat * nat * bool -> nat
 myexists ({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y
      : Prop
@@ -209,17 +211,17 @@ 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]
+fun S : nat => [S | S + S]
      : nat -> nat * (nat -> nat)
-fun N : nat => [N | N.0]
+fun N : nat => [N | N + 0]
      : nat -> nat * (nat -> nat)
-fun S : nat => [[S | S.S]]
+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}
+{'{{x, y}} : nat * nat | x + y = 0}
      : Set
 exists2 '{{y, z}} : nat * nat, y > z & z > y
      : Prop
@@ -253,3 +255,17 @@ myfoo01 tt
      : nat
 myfoo01 tt
      : nat
+[{0; 0}]
+     : list (list nat)
+[{1; 2; 3};
+ {4; 5; 6};
+ {7; 8; 9}]
+     : list (list nat)
+Monomorphic amatch = mmatch 0 (with 0 => 1| 1 => 2 end)
+     : unit
+
+amatch is not universe polymorphic
+Monomorphic alist = [0; 1; 2]
+     : list nat
+
+alist is not universe polymorphic
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 180e8d337e..15211f1233 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -59,7 +59,7 @@ Check fun f => CURRYINVLEFT (x:nat) (y:bool), f.
 (* Notations with variables bound both as a term and as a binder      *)
 (* This is #4592 *)
 
-Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)).
+Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)) : type_scope.
 Check forall n:nat, {# n | 1 > n}.
 
 Parameter foo : forall {T}(x : T)(P : T -> Prop), Prop.
@@ -183,9 +183,13 @@ Check letpair x [1] = {0}; return (1,2,3,4).
 
 (* Test spacing in #5569 *)
 
+Section S1.
+Variable plus : nat -> nat -> nat.
+Infix "+" := plus.
 Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut)
   (at level 0, xR at level 39, format "{ {  xL  |  xR  //  xcut  } }").
 Check 1+1+1.
+End S1.
 
 (* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *)
 Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder).
@@ -193,10 +197,12 @@ Check !!! (x y:nat), True.
 
 (* Allow level for leftmost nonterminal when printing-only, BZ#5739 *)
 
-Notation "* x" := (id x) (only printing, at level 15, format "* x").
-Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y").
+Section S2.
+Notation "* x" := (id x) (only printing, at level 15, format "* x") : nat_scope.
+Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y") : nat_scope.
 Check (((id 1) + 2) + 3).
 Check (id (1 + 2)).
+End S2.
 
 (* Test contraction of "forall x, let 'pat := x in ..." into "forall 'pat, ..." *)
 (* for isolated "forall" (was not working already in 8.6) *)
@@ -410,3 +416,58 @@ Check myfoo0 1 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI]
 Check myfoo01 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI]  *)
 
 End Issue8126.
+
+(* Test printing of notations guided by scope *)
+
+Module A.
+
+Declare Scope line_scope.
+Delimit Scope line_scope with line.
+Declare Scope matx_scope.
+Notation "{ }" := nil (format "{ }") : line_scope.
+Notation "{ x }" := (cons x nil) : line_scope.
+Notation "{ x ; y ; .. ; z }" :=  (cons x (cons y .. (cons z nil) ..)) : line_scope.
+Notation "[ ]" := nil (format "[ ]") : matx_scope.
+Notation "[ l ]" := (cons l%line nil) : matx_scope.
+Notation "[ l ; l' ; .. ; l'' ]" :=  (cons l%line (cons l'%line .. (cons l''%line nil) ..))
+  (format "[ '[v' l ; '/' l' ; '/' .. ; '/' l'' ']' ]") : matx_scope.
+
+Open Scope matx_scope.
+Check [[0;0]].
+Check [[1;2;3];[4;5;6];[7;8;9]].
+
+End A.
+
+(* Example by Beta Ziliani *)
+
+Require Import Lists.List.
+
+Module B.
+
+Import ListNotations.
+
+Declare Scope pattern_scope.
+Delimit Scope pattern_scope with pattern.
+
+Declare Scope patterns_scope.
+Delimit Scope patterns_scope with patterns.
+
+Notation "a => b" := (a, b) (at level 201) : pattern_scope.
+Notation "'with' p1 | .. | pn 'end'" :=
+  ((cons p1%pattern (.. (cons pn%pattern nil) ..)))
+    (at level 91, p1 at level 210, pn at level 210) : patterns_scope.
+
+Definition mymatch (n:nat) (l : list (nat * nat)) := tt.
+Arguments mymatch _ _%patterns.
+Notation "'mmatch' n ls" := (mymatch n ls) (at level 0).
+
+Close Scope patterns_scope.
+Close Scope pattern_scope.
+
+Definition amatch := mmatch 0 with 0 => 1 | 1 => 2 end.
+Print amatch. (* Good: amatch = mmatch 0 (with 0 => 1| 1 => 2 end) *)
+
+Definition alist := [0;1;2].
+Print alist.
+
+End B.
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index d25ad5dca8..d58e4bf2d6 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -21,3 +21,27 @@ Let "x" e1 e2
      : expr
 Let "x" e1 e2
      : expr
+fun x : nat => (# x)%nat
+     : nat -> nat
+fun x : nat => ## x
+     : nat -> nat
+fun x : nat => # x
+     : nat -> nat
+fun x : nat => ### x
+     : nat -> nat
+fun x : nat => ## x
+     : nat -> nat
+fun x : nat => (x.-1)%pred
+     : nat -> nat
+∀ a : nat, a = 0
+     : Prop
+((∀ a : nat, a = 0) -> True)%type
+     : Prop
+#
+     : Prop
+# -> True
+     : Prop
+((∀ a : nat, a = 0) -> True)%type
+     : Prop
+##
+     : Prop
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 7800e91ee5..61206b6dd0 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -5,8 +5,8 @@ Module A.
 Declare Custom Entry myconstr.
 
 Notation "[ x ]" := x (x custom myconstr at level 6).
-Notation "x + y" := (Nat.add x y) (in custom myconstr at level 5).
-Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4).
+Notation "x + y" := (Nat.add x y) (in custom myconstr at level 5) : nat_scope.
+Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4) : nat_scope.
 Notation "< x >" := x (in custom myconstr at level 3, x constr at level 10).
 Check [ < 0 > + < 1 > * < 2 >].
 
@@ -94,3 +94,73 @@ Coercion App : expr >-> Funclass.
 Check (Let "x" e1 e2).
 
 End D.
+
+(* Check fix of #8551: a delimiter should be inserted because the
+   lonely notation hides the scope nat_scope, even though the latter
+   is open *)
+
+Module E.
+
+Notation "# x" := (S x) (at level 20) : nat_scope.
+Notation "# x" := (Some x).
+Check fun x => (# x)%nat.
+
+End E.
+
+(* Other tests of precedence *)
+
+Module F.
+
+Notation "# x" := (S x) (at level 20) : nat_scope.
+Notation "## x" := (S x) (at level 20).
+Check fun x => S x.
+Open Scope nat_scope.
+Check fun x => S x.
+Notation "### x" := (S x) (at level 20) : nat_scope.
+Check fun x => S x.
+Close Scope nat_scope.
+Check fun x => S x.
+
+End F.
+
+(* Lower priority of generic application rules *)
+
+Module G.
+
+Declare Scope predecessor_scope.
+Delimit Scope predecessor_scope with pred.
+Declare Scope app_scope.
+Delimit Scope app_scope with app.
+Notation "x .-1" := (Nat.pred x) (at level 10, format "x .-1") : predecessor_scope.
+Notation "f ( x )" := (f x) (at level 10, format "f ( x )") : app_scope.
+Check fun x => pred x.
+
+End G.
+
+(* Checking arbitration between in the presence of a notation in type scope *)
+
+Module H.
+
+Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+  (at level 200, x binder, y binder, right associativity,
+  format "'[  ' '[  ' ∀  x  ..  y ']' ,  '/' P ']'") : type_scope.
+Check forall a, a = 0.
+
+Close Scope type_scope.
+Check ((forall a, a = 0) -> True)%type.
+Open Scope type_scope.
+
+Notation "#" := (forall a, a = 0).
+Check #.
+Check # -> True.
+
+Close Scope type_scope.
+Check (# -> True)%type.
+Open Scope type_scope.
+
+Declare Scope my_scope.
+Notation "##" := (forall a, a = 0) : my_scope.
+Open Scope my_scope.
+Check ##.
+
+End H.