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, 25 insertions, 11 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 789d59eda9..744528ca0b 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -49,6 +49,11 @@ let notation_entry_level_eq s1 s2 = match (s1,s2) with
 | InCustomEntryLevel (s1,n1), InCustomEntryLevel (s2,n2) -> String.equal s1 s2 && n1 = n2
 | (InConstrEntrySomeLevel | InCustomEntryLevel _), _ -> false
 
+let notation_with_optional_scope_eq inscope1 inscope2 = match (inscope1,inscope2) with
+ | LastLonelyNotation, LastLonelyNotation -> true
+ | NotationInScope s1, NotationInScope s2 -> String.equal s1 s2
+ | (LastLonelyNotation | NotationInScope _), _ -> false
+
 let notation_eq (from1,ntn1) (from2,ntn2) =
   notation_entry_level_eq from1 from2 && String.equal ntn1 ntn2
 
@@ -63,6 +68,15 @@ module NotationOrd =
 module NotationSet = Set.Make(NotationOrd)
 module NotationMap = CMap.Make(NotationOrd)
 
+module SpecificNotationOrd =
+  struct
+    type t = specific_notation
+    let compare = pervasives_compare
+  end
+
+module SpecificNotationSet = Set.Make(SpecificNotationOrd)
+module SpecificNotationMap = CMap.Make(SpecificNotationOrd)
+
 (**********************************************************************)
 (* Scope of symbols *)
 
@@ -254,7 +268,7 @@ let find_delimiters_scope ?loc key =
 (* Uninterpretation tables *)
 
 type interp_rule =
-  | NotationRule of scope_name option * notation
+  | NotationRule of specific_notation
   | SynDefRule of KerName.t
 
 (* We define keys for glob_constr and aconstr to split the syntax entries
@@ -1064,8 +1078,8 @@ let check_required_module ?loc sc (sp,d) =
    the scope stack [scopes], and if yes, using delimiters or not *)
 
 let find_with_delimiters = function
-  | None -> None
-  | Some scope ->
+  | LastLonelyNotation -> None
+  | NotationInScope scope ->
       match (String.Map.find scope !scope_map).delimiters with
         | Some key -> Some (Some scope, Some key)
         | None -> None
@@ -1074,7 +1088,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
   | OpenScopeItem scope :: scopes ->
       (* Is the expected ntn/numpr attached to the most recently open scope? *)
       begin match ntn_scope with
-      | Some scope' when String.equal scope scope' ->
+      | NotationInScope scope' when String.equal scope scope' ->
         Some (None,None)
       | _ ->
         (* If the most recently open scope has a notation/numeral printer
@@ -1086,7 +1100,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
       end
   | LonelyNotationItem ntn' :: scopes ->
       begin match ntn_scope, ntn with
-      | None, Some ntn when notation_eq ntn ntn' ->
+      | LastLonelyNotation, Some ntn when notation_eq ntn ntn' ->
         Some (None, None)
       | _ ->
         find_without_delimiters find (ntn_scope,ntn) scopes
@@ -1244,7 +1258,7 @@ let availability_of_notation (ntn_scope,ntn) scopes =
    commonly from the lowest level of the source entry to the highest
    level of the target entry. *)
 
-type entry_coercion = notation list
+type entry_coercion = (notation_with_optional_scope * notation) list
 
 module EntryCoercionOrd =
  struct
@@ -1295,7 +1309,7 @@ let rec insert_coercion_path path = function
       else if shorter_path path path' then path::allpaths
       else path'::insert_coercion_path path paths
 
-let declare_entry_coercion (entry,_ as ntn) entry' =
+let declare_entry_coercion (scope,(entry,_) as specific_ntn) entry' =
   let entry, lev = decompose_custom_entry entry in
   let entry', lev' = decompose_custom_entry entry' in
   (* Transitive closure *)
@@ -1304,19 +1318,19 @@ let declare_entry_coercion (entry,_ as ntn) entry' =
         List.fold_right (fun ((lev'',lev'''),path) l ->
         if notation_entry_eq entry entry''' && level_ord lev lev''' &&
            not (notation_entry_eq entry' entry'')
-        then ((entry'',entry'),((lev'',lev'),path@[ntn]))::l else l) paths l)
+        then ((entry'',entry'),((lev'',lev'),path@[specific_ntn]))::l else l) paths l)
       !entry_coercion_map [] in
   let toaddright =
     EntryCoercionMap.fold (fun (entry'',entry''') paths l ->
         List.fold_right (fun ((lev'',lev'''),path) l ->
         if entry' = entry'' && level_ord lev' lev'' && entry <> entry'''
-        then ((entry,entry'''),((lev,lev'''),path@[ntn]))::l else l) paths l)
+        then ((entry,entry'''),((lev,lev'''),path@[specific_ntn]))::l else l) paths l)
       !entry_coercion_map [] in
   entry_coercion_map :=
     List.fold_right (fun (pair,path) ->
         let olds = try EntryCoercionMap.find pair !entry_coercion_map with Not_found -> [] in
         EntryCoercionMap.add pair (insert_coercion_path path olds))
-      (((entry,entry'),((lev,lev'),[ntn]))::toaddright@toaddleft)
+      (((entry,entry'),((lev,lev'),[specific_ntn]))::toaddright@toaddleft)
       !entry_coercion_map
 
 let entry_has_global_map = ref String.Map.empty
@@ -1417,7 +1431,7 @@ let availability_of_prim_token n printer_scope local_scopes =
     with Not_found -> false
   in
   let scopes = make_current_scopes local_scopes in
-  Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes)
+  Option.map snd (find_without_delimiters f (NotationInScope printer_scope,None) scopes)
 
 (* Miscellaneous *)