Addressing #6082 and #7766 (overriding format of notation).

We do two changes:
- We distinguish between a notion of format generically attached to
  notations and a new notion of format attached to interpreted
  notations. "Reserved Notation" attaches a format
  generically. "Notation" attaches the format specifically to the given
  interpretation, and additionally, attaches it generically if it is the
  first time the notation is defined.
- We warn before overriding an explicitly reserved generic format, or
  a specific format.

5 files changed, 73 insertions, 39 deletions

diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index dcc3a87b11..d6c6c365cb 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -199,11 +199,11 @@ GRAMMAR EXTEND Gram
              collapse -(3) into the numeral -3. *)
           (match c.CAst.v with
             | CPrim (Numeral (SPlus,n)) ->
-                CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"( _ )"),([c],[],[],[]))
+                CAst.make ~loc @@ CNotation(None,(InConstrEntrySomeLevel,"( _ )"),([c],[],[],[]))
             | _ -> c) }
       | "{|"; c = record_declaration; bar_cbrace -> { c }
       | "{"; c = binder_constr ; "}" ->
-        { CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) }
+        { CAst.make ~loc @@ CNotation(None,(InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) }
       | "`{"; c = operconstr LEVEL "200"; "}" ->
         { CAst.make ~loc @@ CGeneralization (MaxImplicit, None, c) }
       | "`("; c = operconstr LEVEL "200"; ")" ->
@@ -380,7 +380,7 @@ GRAMMAR EXTEND Gram
              collapse -(3) into the numeral -3. *)
           match p.CAst.v with
           | CPatPrim (Numeral (SPlus,n)) ->
-              CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[])
+              CAst.make ~loc @@ CPatNotation(None,(InConstrEntrySomeLevel,"( _ )"),([p],[]),[])
           | _ -> p }
       | "("; p = pattern LEVEL "200"; "|" ; pl = LIST1 pattern LEVEL "200" SEP "|"; ")" ->
         { CAst.make ~loc @@ CPatOr (p::pl) }
diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
index 5c220abeda..915799e997 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -14,21 +14,23 @@ open Util
 open Notation
 open Notation_gram
 
-(* Uninterpreted notation levels *)
+(* Register the level of notation for parsing and printing
+   (we also register a precomputed parsing rule) *)
 
 let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty
 
-let declare_notation_level ?(onlyprint=false) ntn level =
+let declare_notation_level ntn ~onlyprint parsing_rule level =
   try
-    let (level,onlyprint) = NotationMap.find ntn !notation_level_map in
-    if not onlyprint then anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.")
+    let _ = NotationMap.find ntn !notation_level_map in
+    anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.")
   with Not_found ->
-  notation_level_map := NotationMap.add ntn (level,onlyprint) !notation_level_map
+  notation_level_map := NotationMap.add ntn (onlyprint,parsing_rule,level) !notation_level_map
 
-let level_of_notation ?(onlyprint=false) ntn =
-  let (level,onlyprint') = NotationMap.find ntn !notation_level_map in
-  if onlyprint' && not onlyprint then raise Not_found;
-  level
+let level_of_notation ntn =
+  NotationMap.find ntn !notation_level_map
+
+let get_defined_notations () =
+  NotationSet.elements @@ NotationMap.domain !notation_level_map
 
 (**********************************************************************)
 (* Equality *)
diff --git a/parsing/notgram_ops.mli b/parsing/notgram_ops.mli
index c31f4505e7..d5711569f0 100644
--- a/parsing/notgram_ops.mli
+++ b/parsing/notgram_ops.mli
@@ -16,5 +16,9 @@ val level_eq : level -> level -> bool
 
 (** {6 Declare and test the level of a (possibly uninterpreted) notation } *)
 
-val declare_notation_level : ?onlyprint:bool -> notation -> level -> unit
-val level_of_notation : ?onlyprint:bool -> notation -> level (** raise [Not_found] if no level or not respecting onlyprint *)
+val declare_notation_level : notation -> onlyprint:bool -> notation_grammar -> level -> unit
+val level_of_notation : notation -> bool (* = onlyprint *) * notation_grammar * level
+  (** raise [Not_found] if not declared *)
+
+(** Returns notations with defined parsing/printing rules *)
+val get_defined_notations : unit -> notation list
diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml
index 7368f4109e..92f44faec8 100644
--- a/parsing/ppextend.ml
+++ b/parsing/ppextend.ml
@@ -47,31 +47,56 @@ type unparsing =
 
 type unparsing_rule = unparsing list * precedence
 type extra_unparsing_rules = (string * string) list
+
+let rec unparsing_eq unp1 unp2 = match (unp1,unp2) with
+  | UnpMetaVar (n1,p1), UnpMetaVar (n2,p2) -> n1 = n2 && p1 = p2
+  | UnpBinderMetaVar (n1,p1), UnpBinderMetaVar (n2,p2) -> n1 = n2 && p1 = p2
+  | UnpListMetaVar (n1,p1,l1), UnpListMetaVar (n2,p2,l2) -> n1 = n2 && p1 = p2 && List.for_all2eq unparsing_eq l1 l2
+  | UnpBinderListMetaVar (n1,b1,l1), UnpBinderListMetaVar (n2,b2,l2) -> n1 = n2 && b1 = b2 && List.for_all2eq unparsing_eq l1 l2
+  | UnpTerminal s1, UnpTerminal s2 -> String.equal s1 s2
+  | UnpBox (b1,l1), UnpBox (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq (List.map snd l1) (List.map snd l2)
+  | UnpCut p1, UnpCut p2 -> p1 = p2
+  | (UnpMetaVar _ | UnpBinderMetaVar _ | UnpListMetaVar _ |
+     UnpBinderListMetaVar _ | UnpTerminal _ | UnpBox _ | UnpCut _), _ -> false
+
 (* Concrete syntax for symbolic-extension table *)
-let notation_rules =
-  Summary.ref ~name:"notation-rules" (NotationMap.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) NotationMap.t)
+let generic_notation_printing_rules =
+  Summary.ref ~name:"generic-notation-printing-rules" (NotationMap.empty : (unparsing_rule * bool * extra_unparsing_rules) NotationMap.t)
+
+let specific_notation_printing_rules =
+  Summary.ref ~name:"specific-notation-printing-rules" (SpecificNotationMap.empty : (unparsing_rule * extra_unparsing_rules) SpecificNotationMap.t)
+
+let declare_generic_notation_printing_rules ntn ~reserved ~extra unpl =
+  generic_notation_printing_rules := NotationMap.add ntn (unpl,reserved,extra) !generic_notation_printing_rules
+let declare_specific_notation_printing_rules specific_ntn ~extra unpl =
+  specific_notation_printing_rules := SpecificNotationMap.add specific_ntn (unpl,extra) !specific_notation_printing_rules
+
+let has_generic_notation_printing_rule ntn =
+  NotationMap.mem ntn !generic_notation_printing_rules
+
+let find_generic_notation_printing_rule ntn =
+  NotationMap.find ntn !generic_notation_printing_rules
 
-let declare_notation_rule ntn ~extra unpl gram =
-  notation_rules := NotationMap.add ntn (unpl,extra,gram) !notation_rules
+let find_specific_notation_printing_rule specific_ntn =
+  SpecificNotationMap.find specific_ntn !specific_notation_printing_rules
 
-let find_notation_printing_rule ntn =
-  try pi1 (NotationMap.find ntn !notation_rules)
-  with Not_found -> anomaly (str "No printing rule found for " ++ pr_notation ntn ++ str ".")
-let find_notation_extra_printing_rules ntn =
-  try pi2 (NotationMap.find ntn !notation_rules)
-  with Not_found -> []
-let find_notation_parsing_rules ntn =
-  try pi3 (NotationMap.find ntn !notation_rules)
-  with Not_found -> anomaly (str "No parsing rule found for " ++ pr_notation ntn ++ str ".")
+let find_notation_printing_rule which ntn =
+  try match which with
+  | None -> raise Not_found (* Normally not the case *)
+  | Some which -> fst (find_specific_notation_printing_rule (which,ntn))
+  with Not_found -> pi1 (find_generic_notation_printing_rule ntn)
 
-let get_defined_notations () =
-  NotationSet.elements @@ NotationMap.domain !notation_rules
+let find_notation_extra_printing_rules which ntn =
+  try match which with
+  | None -> raise Not_found
+  | Some which -> snd (find_specific_notation_printing_rule (which,ntn))
+  with Not_found -> pi3 (find_generic_notation_printing_rule ntn)
 
 let add_notation_extra_printing_rule ntn k v =
   try
-    notation_rules :=
-      let p, pp, gr = NotationMap.find ntn !notation_rules in
-      NotationMap.add ntn (p, (k,v) :: pp, gr) !notation_rules
+    generic_notation_printing_rules :=
+      let p, b, pp = NotationMap.find ntn !generic_notation_printing_rules in
+      NotationMap.add ntn (p, b, (k,v) :: pp) !generic_notation_printing_rules
   with Not_found ->
     user_err ~hdr:"add_notation_extra_printing_rule"
       (str "No such Notation.")
diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli
index be5af75e72..7996e7696d 100644
--- a/parsing/ppextend.mli
+++ b/parsing/ppextend.mli
@@ -41,11 +41,14 @@ type unparsing =
 
 type unparsing_rule = unparsing list * precedence
 type extra_unparsing_rules = (string * string) list
-val declare_notation_rule : notation -> extra:extra_unparsing_rules -> unparsing_rule -> notation_grammar -> unit
-val find_notation_printing_rule : notation -> unparsing_rule
-val find_notation_extra_printing_rules : notation -> extra_unparsing_rules
-val find_notation_parsing_rules : notation -> notation_grammar
-val add_notation_extra_printing_rule : notation -> string -> string -> unit
 
-(** Returns notations with defined parsing/printing rules *)
-val get_defined_notations : unit -> notation list
+val unparsing_eq : unparsing -> unparsing -> bool
+
+val declare_generic_notation_printing_rules : notation -> reserved:bool -> extra:extra_unparsing_rules -> unparsing_rule -> unit
+val declare_specific_notation_printing_rules : specific_notation -> extra:extra_unparsing_rules -> unparsing_rule -> unit
+val has_generic_notation_printing_rule : notation -> bool
+val find_generic_notation_printing_rule : notation -> unparsing_rule * bool * extra_unparsing_rules
+val find_specific_notation_printing_rule : specific_notation -> unparsing_rule * extra_unparsing_rules
+val find_notation_printing_rule : notation_with_optional_scope option -> notation -> unparsing_rule
+val find_notation_extra_printing_rules : notation_with_optional_scope option -> notation -> extra_unparsing_rules
+val add_notation_extra_printing_rule : notation -> string -> string -> unit