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.

1 files changed, 43 insertions, 18 deletions

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.")