Printing priority to most recent notation in case of non-open scopes with delim.

This modifies the strategy in previous commits so that priorities are
as before in case of non-open scopes with delimiters.

Additionally, we document the rare situation of overlapping
applicative notations (maybe this is too rare and ad hoc to be worth
being documented though).

4 files changed, 71 insertions, 27 deletions

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 66fa3af052..ce79e2915e 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1337,10 +1337,22 @@ Coq will use the following rules for printing priorities:
 - In case no abbreviation, nor lonely notation, nor notation in an
   explicitly open scope, nor notation in a temporarily open scope of
   arguments, has been found, notations in those closed scopes which
-  have a delimiter are considered. A notation is chosen and the
-  corresponding delimiter is inserted, making the corresponding scope
-  the most recent explicitly open scope for all subterms of the
-  current term.
+  have a delimiter are considered, giving priority to the most
+  recently defined (or imported) ones. The corresponding delimiter is
+  inserted, making the corresponding scope the most recent explicitly
+  open scope for all subterms of the current term.
+
+- As a refinement of the previous rule, in the case of applied global
+  references, notations in a non-opened scope with delimiter
+  specifically defined for this applied global reference take priority
+  over notations in a non-opened scope with delimiter for generic
+  applications. For instance, in the presence of ``Notation "f ( x
+  )" := (f x) (at level 10, format "f ( x )") : app_scope`` and
+  ``Notation "x '.+1'" := (S x) (at level 10, format "x '.+1'") :
+  mynat_scope.`` and both of ``app_scope`` and ``mynat_scope`` being
+  bound to a delimiter *and* both not opened, the latter, more
+  specific notation will always take precedence over the first, more
+  generic one.
 
 - A scope can be closed by using :cmd:`Close Scope` and its delimiter
   removed by using :cmd:`Undelimit Scope`. To remove automatic
diff --git a/interp/notation.ml b/interp/notation.ml
index 3f973b5230..ea6d0f8871 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -173,6 +173,7 @@ type interp_rule =
   | NotationRule of scope_name option * notation
   | SynDefRule of KerName.t
 
+type scoped_notation_rule_core = scope_name * notation * interpretation * int option
 type notation_rule_core = interp_rule * interpretation * int option
 type notation_rule = notation_rule_core * delimiters option * bool
 
@@ -312,18 +313,26 @@ let key_compare k1 k2 = match k1, k2 with
 module KeyOrd = struct type t = key let compare = key_compare end
 module KeyMap = Map.Make(KeyOrd)
 
-let keymap_add key sc interp map =
-  let oldkeymap = try ScopeMap.find sc map with Not_found -> KeyMap.empty in
+let keymap_add key sc interp (scope_map,global_map) =
+  (* Adding to scope keymap for printing based on open scopes *)
+  let oldkeymap = try ScopeMap.find sc scope_map with Not_found -> KeyMap.empty in
   let oldscmap = try KeyMap.find key oldkeymap with Not_found -> [] in
   let newscmap = KeyMap.add key (interp :: oldscmap) oldkeymap in
-  ScopeMap.add sc newscmap map
+  let scope_map = ScopeMap.add sc newscmap scope_map in
+  (* Adding to global keymap of scoped notations in case the scope is not open *)
+  let global_map = match interp with
+  | NotationRule (Some sc,ntn), interp, c ->
+      let oldglobalkeymap = try KeyMap.find key global_map with Not_found -> [] in
+      KeyMap.add key ((sc,ntn,interp,c) :: oldglobalkeymap) global_map
+  | (NotationRule (None,_) | SynDefRule _), _, _ -> global_map in
+  (scope_map, global_map)
 
 let keymap_extract keys sc map =
-  let keymap, map =
-    try ScopeMap.find (Some sc) map, ScopeMap.remove (Some sc) map
-    with Not_found -> KeyMap.empty, map in
+  let keymap =
+    try ScopeMap.find (Some sc) map
+    with Not_found -> KeyMap.empty in
   let add_scope rule = (rule,(String.Map.find sc !scope_map).delimiters,false) in
-  List.map_append (fun key -> try List.map add_scope (KeyMap.find key keymap) with Not_found -> []) keys, map
+  List.map_append (fun key -> try List.map add_scope (KeyMap.find key keymap) with Not_found -> []) keys
 
 let find_with_delimiters = function
   | None -> None
@@ -332,17 +341,22 @@ let find_with_delimiters = function
         | Some key -> Some (Some key)
         | None -> None
 
-let keymap_extract_remainder keys map =
-  ScopeMap.fold (fun sc keymap acc ->
-      match find_with_delimiters sc with
-      | None -> acc
-      | Some delim ->
-         let add_scope rule = (rule,delim,true) in
-         let l = List.map_append (fun key -> try List.map add_scope (KeyMap.find key keymap) with Not_found -> []) keys in
-      l @ acc) map []
+let rec keymap_extract_remainder scope_seen = function
+  | [] -> []
+  | (sc,ntn,interp,c) :: l ->
+      if String.Set.mem sc scope_seen then keymap_extract_remainder scope_seen l
+      else
+        match find_with_delimiters (Some sc) with
+        | None -> keymap_extract_remainder scope_seen l
+        | Some delim ->
+           let rule = (NotationRule (Some sc, ntn), interp, c) in
+           (rule,delim,true) :: keymap_extract_remainder scope_seen l
 
 (* Scopes table : interpretation -> scope_name *)
-let notations_key_table = ref (ScopeMap.empty : notation_rule_core list KeyMap.t ScopeMap.t)
+let notations_key_table =
+  ref ((ScopeMap.empty, KeyMap.empty) :
+       notation_rule_core list KeyMap.t ScopeMap.t *
+       scoped_notation_rule_core list KeyMap.t)
 
 let glob_prim_constr_key c = match DAst.get c with
   | GRef (ref, _) -> Some (canonical_gr ref)
@@ -1051,13 +1065,15 @@ let interp_notation ?loc ntn local_scopes =
 
 let extract_notations scopes keys =
   if keys == [] then [] (* shortcut *) else
-  let rec aux scopes map =
+  let scope_map, global_map = !notations_key_table in
+  let rec aux scopes seen =
   match scopes with
-  | UninterpScope sc :: scopes ->
-      let l, map = keymap_extract keys sc map in l @ aux scopes map
-  | UninterpSingle rule :: scopes -> (rule,None,false) :: aux scopes map
-  | [] -> keymap_extract_remainder keys map
-  in aux scopes !notations_key_table
+  | UninterpScope sc :: scopes -> keymap_extract keys sc scope_map @ aux scopes (String.Set.add sc seen)
+  | UninterpSingle rule :: scopes -> (rule,None,false) :: aux scopes seen
+  | [] ->
+      let find key = try KeyMap.find key global_map with Not_found -> [] in
+      keymap_extract_remainder seen (List.flatten (List.map find keys))
+  in aux scopes String.Set.empty
 
 let uninterp_notations scopes c =
   let scopes = make_current_uninterp_scopes scopes in
@@ -1773,7 +1789,7 @@ let init () =
   init_scope_map ();
   uninterp_scope_stack := [];
   delimiters_map := String.Map.empty;
-  notations_key_table := ScopeMap.empty;
+  notations_key_table := (ScopeMap.empty,KeyMap.empty);
   scope_class_map := initial_scope_class_map;
   prim_token_interp_infos := String.Map.empty;
   prim_token_uninterp_infos := GlobRef.Map.empty
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 2ff21f6a57..40d875e8ab 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -31,3 +31,5 @@ fun x : nat => ### x
      : nat -> nat
 fun x : nat => ## x
      : nat -> nat
+fun x : nat => (x.-1)%pred
+     : nat -> nat
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 4720cb0561..4196c7e6b4 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -122,3 +122,17 @@ 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.