Selecting which notation to print based on current stack of scope.

See discussion on coq-club starting on 23 August 2016.

8 files changed, 105 insertions, 26 deletions

diff --git a/CHANGES.md b/CHANGES.md
index 1f88b77b51..7a4af0d7a8 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -148,6 +148,11 @@ Notations
   that will do it automatically, using the output of coqc. The script
   contains documentation on its usage in a comment at the top.
 
+- When several notations are available for the same expression,
+  priority is given to latest notations defined in the scopes being
+  opened, in order, rather than to the latest notations defined
+  independently of whether they are in an opened scope or not.
+
 Tactics
 
 - Added toplevel goal selector `!` which expects a single focused goal.
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 94b86fc222..e3816d65fd 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -64,7 +64,7 @@ The command has indeed failed with message:
 Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
 Both ends of the recursive pattern are the same.
-SUM (nat * nat) nat
+(nat * nat + nat)%type
      : Set
 FST (0; 1)
      : Z
@@ -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.out b/test-suite/output/Notations2.out
index 41d1593758..672a742f24 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -51,7 +51,7 @@ end
 match n with
 | nil => 2
 | 0 :: _ => 2
-| list1 => 0
+| 1 :: nil => 0
 | 1 :: _ :: _ => 2
 | plus2 _ :: _ => 2
 end
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 421ec987ff..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.
@@ -197,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) *)
@@ -414,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.v b/test-suite/output/Notations4.v
index 7800e91ee5..191a073051 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 >].