From 93a65415ff582d2ceb5bb9d994edaa6068da8280 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 25 Nov 2017 12:14:59 +0100
Subject: Pre-isolating a notation test to avoid interferences.

---
 interp/notation.ml | 41 ++++++++++++++++++++++++++++++++---------
 1 file changed, 32 insertions(+), 9 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index db8ee5bc18..49403c6e34 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -982,15 +982,38 @@ let interp_notation ?loc ntn local_scopes =
     user_err ?loc 
     (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".")
 
-let uninterp_notations c =
-  List.map_append (fun key -> keymap_find key !notations_key_table)
-    (glob_constr_keys c)
-
-let uninterp_cases_pattern_notations c =
-  keymap_find (cases_pattern_key c) !notations_key_table
-
-let uninterp_ind_pattern_notations ind =
-  keymap_find (RefKey (canonical_gr (IndRef ind))) !notations_key_table
+let sort_notations scopes l =
+  let extract_scope l = function
+    | Scope sc -> List.partitioni (fun _i x ->
+                      match x with
+                      | NotationRule (Some sc',_),_,_ -> String.equal sc sc'
+                      | _ -> false) l
+    | SingleNotation ntn -> List.partitioni (fun _i x ->
+                      match x with
+                      | NotationRule (None,ntn'),_,_ -> notation_eq ntn ntn'
+                      | _ -> false) l in
+  let rec aux l scopes =
+    if l == [] then [] (* shortcut *) else
+    match scopes with
+    | sc :: scopes -> let ntn_in_sc,l = extract_scope l sc in ntn_in_sc @ aux l scopes
+    | [] -> l in
+  aux l scopes
+
+let uninterp_notations scopes c =
+  let scopes = make_current_scopes scopes in
+  let keys = glob_constr_keys c in
+  let maps = List.map_append (fun key -> keymap_find key !notations_key_table) keys in
+  sort_notations scopes maps
+
+let uninterp_cases_pattern_notations scopes c =
+  let scopes = make_current_scopes scopes in
+  let maps = keymap_find (cases_pattern_key c) !notations_key_table in
+  sort_notations scopes maps
+
+let uninterp_ind_pattern_notations scopes ind =
+  let scopes = make_current_scopes scopes in
+  let maps = keymap_find (RefKey (canonical_gr (IndRef ind))) !notations_key_table in
+  sort_notations scopes maps
 
 let availability_of_notation (ntn_scope,ntn) scopes =
   let f scope =
-- 
cgit v1.2.3


From 06fc6caa49b67526cf3521d1b5885aae6710358b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 8 Mar 2018 18:22:50 +0100
Subject: Addressing issues with PR#873: performance and use of abbreviation
 for printing.

We do a couple of changes:

- Splitting notation keys into more categories to make table smaller.
  This should (a priori) make printing faster (see #6416).

- Abbreviations are treated for printing like single notations: they
  are pushed to the scope stack, so that in a situation such as

  Open Scope foo_scope.
  Notation foo := term.
  Open Scope bar_scope.

  one looks for notations first in scope bar_scope, then try to use
  foo, they try for notations in scope foo_scope.

- We seize the opportunity of this commit to simplify
  availability_of_notation which is now integrated to
  uninterp_notation and which does not have to be called explicitly
  anymore.
---
 interp/notation.ml | 205 ++++++++++++++++++++++++++++++++++-------------------
 1 file changed, 133 insertions(+), 72 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 49403c6e34..d5b43860c1 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -156,6 +156,8 @@ let scope_eq s1 s2 = match s1, s2 with
 | Scope _, SingleNotation _
 | SingleNotation _, Scope _ -> false
 
+(* Scopes for interpretation *)
+
 let scope_stack = ref []
 
 let current_scopes () = !scope_stack
@@ -165,14 +167,56 @@ let scope_is_open_in_scopes sc l =
 
 let scope_is_open sc = scope_is_open_in_scopes sc (!scope_stack)
 
+(* Uninterpretation tables *)
+
+type interp_rule =
+  | NotationRule of scope_name option * notation
+  | SynDefRule of KerName.t
+
+type notation_rule_core = interp_rule * interpretation * int option
+type notation_rule = notation_rule_core * delimiters option
+
+(* Scopes for uninterpretation: includes abbreviations (i.e. syntactic definitions) and  *)
+
+type uninterp_scope_elem =
+  | UninterpScope of scope_name
+  | UninterpSingle of notation_rule_core
+
+let uninterp_scope_eq_weak s1 s2 = match s1, s2 with
+| UninterpScope s1, UninterpScope s2 -> String.equal s1 s2
+| UninterpSingle s1, UninterpSingle s2 -> false
+| (UninterpSingle _ | UninterpScope _), _ -> false
+
+module ScopeOrd =
+  struct
+    type t = scope_name option
+    let compare = Pervasives.compare
+  end
+
+module ScopeMap = CMap.Make(ScopeOrd)
+
+let uninterp_scope_stack = ref []
+
+let push_uninterp_scope sc scopes = UninterpScope sc :: scopes
+
+let push_uninterp_scopes = List.fold_right push_uninterp_scope
+
+let make_current_uninterp_scopes (tmp_scope,scopes) =
+  Option.fold_right push_uninterp_scope tmp_scope
+    (push_uninterp_scopes scopes !uninterp_scope_stack)
+
 (* TODO: push nat_scope, z_scope, ... in scopes summary *)
 
 (* Exportation of scopes *)
 let open_scope i (_,(local,op,sc)) =
-  if Int.equal i 1 then
+  if Int.equal i 1 then begin
     scope_stack :=
-      if op then sc :: !scope_stack
-      else List.except scope_eq sc !scope_stack
+      if op then Scope sc :: !scope_stack
+      else List.except scope_eq (Scope sc) !scope_stack;
+    uninterp_scope_stack :=
+      if op then UninterpScope sc :: !uninterp_scope_stack
+      else List.except uninterp_scope_eq_weak (UninterpScope sc) !uninterp_scope_stack
+    end
 
 let cache_scope o =
   open_scope 1 o
@@ -187,7 +231,7 @@ let discharge_scope (_,(local,_,_ as o)) =
 let classify_scope (local,_,_ as o) =
   if local then Dispose else Substitute o
 
-let inScope : bool * bool * scope_elem -> obj =
+let inScope : bool * bool * scope_name -> obj =
   declare_object {(default_object "SCOPE") with
       cache_function = cache_scope;
       open_function = open_scope;
@@ -196,7 +240,7 @@ let inScope : bool * bool * scope_elem -> obj =
       classify_function = classify_scope }
 
 let open_close_scope (local,opening,sc) =
-  Lib.add_anonymous_leaf (inScope (local,opening,Scope (normalize_scope sc)))
+  Lib.add_anonymous_leaf (inScope (local,opening,normalize_scope sc))
 
 let empty_scope_stack = []
 
@@ -250,40 +294,55 @@ let find_delimiters_scope ?loc key =
     user_err ?loc ~hdr:"find_delimiters"
       (str "Unknown scope delimiting key " ++ str key ++ str ".")
 
-(* Uninterpretation tables *)
-
-type interp_rule =
-  | NotationRule of scope_name option * notation
-  | SynDefRule of KerName.t
-
 (* We define keys for glob_constr and aconstr to split the syntax entries
    according to the key of the pattern (adapted from Chet Murthy by HH) *)
 
 type key =
   | RefKey of GlobRef.t
+  | LambdaKey
+  | ProdKey
   | Oth
 
 let key_compare k1 k2 = match k1, k2 with
 | RefKey gr1, RefKey gr2 -> GlobRef.Ordered.compare gr1 gr2
-| RefKey _, Oth -> -1
-| Oth, RefKey _ -> 1
-| Oth, Oth -> 0
+| RefKey _, _ -> -1
+| _, RefKey _ -> 1
+| k1, k2 -> Pervasives.compare k1 k2
 
 module KeyOrd = struct type t = key let compare = key_compare end
 module KeyMap = Map.Make(KeyOrd)
 
-type notation_rule = interp_rule * interpretation * int option
+let keymap_add key sc interp map =
+  let oldkeymap = try ScopeMap.find sc 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 keymap_add key interp map =
-  let old = try KeyMap.find key map with Not_found -> [] in
-  KeyMap.add key (interp :: old) map
+let keymap_extract keys sc map =
+  let keymap, map =
+    try ScopeMap.find sc map, ScopeMap.remove sc map
+    with Not_found -> KeyMap.empty, map in
+  let add_scope rule = (rule,None) in
+  List.map_append (fun key -> try List.map add_scope (KeyMap.find key keymap) with Not_found -> []) keys, map
 
-let keymap_find key map =
-  try KeyMap.find key map
-  with Not_found -> []
+let find_with_delimiters = function
+  | None -> None
+  | Some scope ->
+      match (String.Map.find scope !scope_map).delimiters with
+        | 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) 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 []
 
 (* Scopes table : interpretation -> scope_name *)
-let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t)
+let notations_key_table = ref (ScopeMap.empty : notation_rule_core list KeyMap.t ScopeMap.t)
 
 let glob_prim_constr_key c = match DAst.get c with
   | GRef (ref, _) -> Some (canonical_gr ref)
@@ -295,12 +354,14 @@ let glob_prim_constr_key c = match DAst.get c with
   | _ -> None
 
 let glob_constr_keys c = match DAst.get c with
+  | GRef (ref,_) -> [RefKey (canonical_gr ref)]
   | GApp (c, _) ->
     begin match DAst.get c with
     | GRef (ref, _) -> [RefKey (canonical_gr ref); Oth]
     | _ -> [Oth]
     end
-  | GRef (ref,_) -> [RefKey (canonical_gr ref)]
+  | GLambda _ -> [LambdaKey]
+  | GProd _ -> [ProdKey]
   | _ -> [Oth]
 
 let cases_pattern_key c = match DAst.get c with
@@ -314,6 +375,8 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
       RefKey (canonical_gr ref), Some (List.length args)
   | NRef ref -> RefKey(canonical_gr ref), None
   | NApp (_,args) -> Oth, Some (List.length args)
+  | NLambda _ | NBinderList (_,_,NLambda _,_,_) | NList (_,_,NLambda _,_,_) -> LambdaKey, None
+  | NProd _ | NBinderList (_,_,NProd _,_,_) | NList (_,_,NProd _,_,_) -> ProdKey, None
   | _ -> Oth, None
 
 (**********************************************************************)
@@ -839,19 +902,12 @@ let check_required_module ?loc sc (sp,d) =
 (* Look if some notation or numeral printer in [scope] can be used in
    the scope stack [scopes], and if yes, using delimiters or not *)
 
-let find_with_delimiters = function
-  | None -> None
-  | Some scope ->
-      match (String.Map.find scope !scope_map).delimiters with
-	| Some key -> Some (Some scope, Some key)
-	| None -> None
-
 let rec find_without_delimiters find (ntn_scope,ntn) = function
-  | Scope scope :: scopes ->
+  | UninterpScope 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' ->
-	Some (None,None)
+        Some None
       | _ ->
 	(* If the most recently open scope has a notation/numeral printer
     	   but not the expected one then we need delimiters *)
@@ -860,13 +916,14 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
 	else
 	  find_without_delimiters find (ntn_scope,ntn) scopes
       end
-  | SingleNotation ntn' :: scopes ->
+  | UninterpSingle (NotationRule (_,ntn'),_,_) :: scopes ->
       begin match ntn_scope, ntn with
       | None, Some ntn when notation_eq ntn ntn' ->
-	Some (None, None)
+        Some None
       | _ ->
 	find_without_delimiters find (ntn_scope,ntn) scopes
       end
+  | UninterpSingle (SynDefRule _,_,_) :: scopes -> find_without_delimiters find (ntn_scope,ntn) scopes
   | [] ->
       (* Can we switch to [scope]? Yes if it has defined delimiters *)
       find_with_delimiters ntn_scope
@@ -902,9 +959,19 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint =
   | Some _ -> ()
   end
 
+let scope_of_rule = function
+  | NotationRule (None,_) | SynDefRule _ -> None
+  | NotationRule (Some sc as sco,_) -> sco
+
+let uninterp_scope_to_add pat n = function
+  | NotationRule (None,_) | SynDefRule _ as rule -> Some (UninterpSingle (rule,pat,n))
+  | NotationRule (Some sc,_) -> None
+
 let declare_uninterpretation rule (metas,c as pat) =
   let (key,n) = notation_constr_key c in
-  notations_key_table := keymap_add key (rule,pat,n) !notations_key_table
+  let sc = scope_of_rule rule in
+  notations_key_table := keymap_add key sc (rule,pat,n) !notations_key_table;
+  uninterp_scope_stack := Option.List.cons (uninterp_scope_to_add pat n rule) !uninterp_scope_stack
 
 let rec find_interpretation ntn find = function
   | [] -> raise Not_found
@@ -982,43 +1049,27 @@ let interp_notation ?loc ntn local_scopes =
     user_err ?loc 
     (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".")
 
-let sort_notations scopes l =
-  let extract_scope l = function
-    | Scope sc -> List.partitioni (fun _i x ->
-                      match x with
-                      | NotationRule (Some sc',_),_,_ -> String.equal sc sc'
-                      | _ -> false) l
-    | SingleNotation ntn -> List.partitioni (fun _i x ->
-                      match x with
-                      | NotationRule (None,ntn'),_,_ -> notation_eq ntn ntn'
-                      | _ -> false) l in
-  let rec aux l scopes =
-    if l == [] then [] (* shortcut *) else
-    match scopes with
-    | sc :: scopes -> let ntn_in_sc,l = extract_scope l sc in ntn_in_sc @ aux l scopes
-    | [] -> l in
-  aux l scopes
+let extract_notations scopes keys =
+  if keys == [] then [] (* shortcut *) else
+  let rec aux scopes map =
+  match scopes with
+  | UninterpScope sc :: scopes ->
+      let l, map = keymap_extract keys (Some sc) map in l @ aux scopes map
+  | UninterpSingle rule :: scopes -> (rule,None) :: aux scopes map
+  | [] -> keymap_extract_remainder keys map
+  in aux scopes !notations_key_table
 
 let uninterp_notations scopes c =
-  let scopes = make_current_scopes scopes in
-  let keys = glob_constr_keys c in
-  let maps = List.map_append (fun key -> keymap_find key !notations_key_table) keys in
-  sort_notations scopes maps
+  let scopes = make_current_uninterp_scopes scopes in
+  extract_notations scopes (glob_constr_keys c)
 
 let uninterp_cases_pattern_notations scopes c =
-  let scopes = make_current_scopes scopes in
-  let maps = keymap_find (cases_pattern_key c) !notations_key_table in
-  sort_notations scopes maps
+  let scopes = make_current_uninterp_scopes scopes in
+  extract_notations scopes [cases_pattern_key c]
 
 let uninterp_ind_pattern_notations scopes ind =
-  let scopes = make_current_scopes scopes in
-  let maps = keymap_find (RefKey (canonical_gr (IndRef ind))) !notations_key_table in
-  sort_notations scopes maps
-
-let availability_of_notation (ntn_scope,ntn) scopes =
-  let f scope =
-    NotationMap.mem ntn (String.Map.find scope !scope_map).notations in
-  find_without_delimiters f (ntn_scope,Some ntn) (make_current_scopes scopes)
+  let scopes = make_current_uninterp_scopes scopes in
+  extract_notations scopes [RefKey (canonical_gr (IndRef ind))]
 
 (* We support coercions from a custom entry at some level to an entry
    at some level (possibly the same), and from and to the constr entry. E.g.:
@@ -1172,8 +1223,8 @@ let availability_of_prim_token n printer_scope local_scopes =
         | _ -> false
     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)
+  let scopes = make_current_uninterp_scopes local_scopes in
+  find_without_delimiters f (Some printer_scope,None) scopes
 
 (* Miscellaneous *)
 
@@ -1209,6 +1260,14 @@ let exists_notation_in_scope scopt ntn onlyprint r =
     interpretation_eq n.not_interp r
   with Not_found -> false
 
+let exists_notation_interpretation_in_scope scopt ntn =
+  let scope = match scopt with Some s -> s | None -> default_scope in
+  try
+    let sc = String.Map.find scope !scope_map in
+    let _ = NotationMap.find ntn sc.notations in
+    true
+  with Not_found -> false
+
 let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false
 
 (**********************************************************************)
@@ -1690,17 +1749,18 @@ let pr_visibility prglob = function
 (* Synchronisation with reset *)
 
 let freeze _ =
- (!scope_map, !scope_stack, !arguments_scope,
+ (!scope_map, !scope_stack, !uninterp_scope_stack, !arguments_scope,
   !delimiters_map, !notations_key_table, !scope_class_map,
   !prim_token_interp_infos, !prim_token_uninterp_infos,
   !entry_coercion_map, !entry_has_global_map,
   !entry_has_ident_map)
 
-let unfreeze (scm,scs,asc,dlm,fkm,clsc,ptii,ptui,coe,globs,ids) =
+let unfreeze (scm,scs,uscs,asc,dlm,fkm,clsc,ptii,ptui,coe,globs,ids) =
   scope_map := scm;
   scope_stack := scs;
-  delimiters_map := dlm;
+  uninterp_scope_stack := uscs;
   arguments_scope := asc;
+  delimiters_map := dlm;
   notations_key_table := fkm;
   scope_class_map := clsc;
   prim_token_interp_infos := ptii;
@@ -1711,8 +1771,9 @@ let unfreeze (scm,scs,asc,dlm,fkm,clsc,ptii,ptui,coe,globs,ids) =
 
 let init () =
   init_scope_map ();
+  uninterp_scope_stack := [];
   delimiters_map := String.Map.empty;
-  notations_key_table := KeyMap.empty;
+  notations_key_table := ScopeMap.empty;
   scope_class_map := initial_scope_class_map;
   prim_token_interp_infos := String.Map.empty;
   prim_token_uninterp_infos := GlobRef.Map.empty
-- 
cgit v1.2.3


From 9bc339f529fc2ee2389a717914514829a73686bc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 24 Sep 2018 23:14:29 +0200
Subject: Fixing #8551 (missing delimiters when notation exists both lonely and
 in scope).

---
 interp/notation.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index d5b43860c1..3f973b5230 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -174,7 +174,7 @@ type interp_rule =
   | SynDefRule of KerName.t
 
 type notation_rule_core = interp_rule * interpretation * int option
-type notation_rule = notation_rule_core * delimiters option
+type notation_rule = notation_rule_core * delimiters option * bool
 
 (* Scopes for uninterpretation: includes abbreviations (i.e. syntactic definitions) and  *)
 
@@ -320,9 +320,9 @@ let keymap_add key sc interp map =
 
 let keymap_extract keys sc map =
   let keymap, map =
-    try ScopeMap.find sc map, ScopeMap.remove sc map
+    try ScopeMap.find (Some sc) map, ScopeMap.remove (Some sc) map
     with Not_found -> KeyMap.empty, map in
-  let add_scope rule = (rule,None) 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
 
 let find_with_delimiters = function
@@ -337,7 +337,7 @@ let keymap_extract_remainder keys map =
       match find_with_delimiters sc with
       | None -> acc
       | Some delim ->
-         let add_scope rule = (rule,delim) in
+         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 []
 
@@ -1054,8 +1054,8 @@ let extract_notations scopes keys =
   let rec aux scopes map =
   match scopes with
   | UninterpScope sc :: scopes ->
-      let l, map = keymap_extract keys (Some sc) map in l @ aux scopes map
-  | UninterpSingle rule :: scopes -> (rule,None) :: aux scopes map
+      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
 
-- 
cgit v1.2.3


From 8f7c82b8a67a3c94073e55289996f02285c04914 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 15 Oct 2018 15:50:28 +0200
Subject: 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).
---
 interp/notation.ml | 62 ++++++++++++++++++++++++++++++++++--------------------
 1 file changed, 39 insertions(+), 23 deletions(-)

(limited to 'interp/notation.ml')

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
-- 
cgit v1.2.3


From 4b02fbd92ec47f1477db71425d2627898019cd5d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 15 Oct 2018 19:46:41 +0200
Subject: Fixing missing newline in display of Locate for notations.

---
 interp/notation.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index ea6d0f8871..2a095d7466 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1702,7 +1702,7 @@ let locate_notation prglob ntn scope =
     str "Notation" ++ fnl () ++
     prlist_with_sep fnl (fun (ntn,l) ->
       let scope = find_default ntn scopes in
-      prlist
+      prlist_with_sep fnl
 	(fun (sc,r,(_,df)) ->
 	  hov 0 (
 	    pr_notation_info prglob df r ++
-- 
cgit v1.2.3


From 11d293e692adc801545f714d3851fa7a4fef8266 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 31 Oct 2018 20:29:47 +0100
Subject: Notation.ml: Moving code about binding scopes to coercion classes
 earlier.

We shall need it for changing the semantics of type_scope.
---
 interp/notation.ml | 78 ++++++++++++++++++++++++++----------------------------
 1 file changed, 38 insertions(+), 40 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 2a095d7466..33113312e8 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -21,6 +21,7 @@ open Notation_term
 open Glob_term
 open Glob_ops
 open Context.Named.Declaration
+open Classops
 
 (*i*)
 
@@ -205,6 +206,43 @@ let push_uninterp_scopes = List.fold_right push_uninterp_scope
 let make_current_uninterp_scopes (tmp_scope,scopes) =
   Option.fold_right push_uninterp_scope tmp_scope
     (push_uninterp_scopes scopes !uninterp_scope_stack)
+(**********************************************************************)
+(* Mapping classes to scopes *)
+
+type scope_class = cl_typ
+
+let scope_class_compare : scope_class -> scope_class -> int =
+  cl_typ_ord
+
+let compute_scope_class sigma t =
+  let (cl,_,_) = find_class_type sigma t in
+  cl
+
+module ScopeClassOrd =
+struct
+  type t = scope_class
+  let compare = scope_class_compare
+end
+
+module ScopeClassMap = Map.Make(ScopeClassOrd)
+
+let initial_scope_class_map : scope_name ScopeClassMap.t =
+  ScopeClassMap.empty
+
+let scope_class_map = ref initial_scope_class_map
+
+let declare_scope_class sc cl =
+  scope_class_map := ScopeClassMap.add cl sc !scope_class_map
+
+let find_scope_class cl =
+  ScopeClassMap.find cl !scope_class_map
+
+let find_scope_class_opt = function
+  | None -> None
+  | Some cl -> try Some (find_scope_class cl) with Not_found -> None
+
+let current_type_scope_name () =
+   find_scope_class_opt (Some CL_SORT)
 
 (* TODO: push nat_scope, z_scope, ... in scopes summary *)
 
@@ -1286,43 +1324,6 @@ let exists_notation_interpretation_in_scope scopt ntn =
 
 let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false
 
-(**********************************************************************)
-(* Mapping classes to scopes *)
-
-open Classops
-
-type scope_class = cl_typ
-
-let scope_class_compare : scope_class -> scope_class -> int =
-  cl_typ_ord
-
-let compute_scope_class sigma t =
-  let (cl,_,_) = find_class_type sigma t in
-  cl
-
-module ScopeClassOrd =
-struct
-  type t = scope_class
-  let compare = scope_class_compare
-end
-
-module ScopeClassMap = Map.Make(ScopeClassOrd)
-
-let initial_scope_class_map : scope_name ScopeClassMap.t =
-  ScopeClassMap.empty
-
-let scope_class_map = ref initial_scope_class_map
-
-let declare_scope_class sc cl =
-  scope_class_map := ScopeClassMap.add cl sc !scope_class_map
-
-let find_scope_class cl =
-  ScopeClassMap.find cl !scope_class_map
-
-let find_scope_class_opt = function
-  | None -> None
-  | Some cl -> try Some (find_scope_class cl) with Not_found -> None
-
 (**********************************************************************)
 (* Special scopes associated to arguments of a global reference *)
 
@@ -1343,9 +1344,6 @@ let compute_arguments_scope sigma t = fst (compute_arguments_scope_full sigma t)
 let compute_type_scope sigma t =
   find_scope_class_opt (try Some (compute_scope_class sigma t) with Not_found -> None)
 
-let current_type_scope_name () =
-   find_scope_class_opt (Some CL_SORT)
-
 let scope_class_of_class (x : cl_typ) : scope_class =
   x
 
-- 
cgit v1.2.3


From 0336e86ea5ef63a587aae695adeeb4607346c337 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 31 Oct 2018 20:32:11 +0100
Subject: Giving to type_scope a softer role in printing.

Namely, it does not explicitly open a scope, but we remember that we
don't need the %type delimiter when in type position.
---
 interp/notation.ml | 73 ++++++++++++++++++++++++++++++++++--------------------
 1 file changed, 46 insertions(+), 27 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 33113312e8..0af75b5bfa 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -203,9 +203,6 @@ let push_uninterp_scope sc scopes = UninterpScope sc :: scopes
 
 let push_uninterp_scopes = List.fold_right push_uninterp_scope
 
-let make_current_uninterp_scopes (tmp_scope,scopes) =
-  Option.fold_right push_uninterp_scope tmp_scope
-    (push_uninterp_scopes scopes !uninterp_scope_stack)
 (**********************************************************************)
 (* Mapping classes to scopes *)
 
@@ -287,9 +284,20 @@ let push_scope sc scopes = Scope sc :: scopes
 
 let push_scopes = List.fold_right push_scope
 
+let make_type_scope_soft tmp_scope =
+  if Option.equal String.equal tmp_scope (current_type_scope_name ()) then
+    true, None
+  else
+    false, tmp_scope
+
 let make_current_scopes (tmp_scope,scopes) =
   Option.fold_right push_scope tmp_scope (push_scopes scopes !scope_stack)
 
+let make_current_uninterp_scopes (tmp_scope,scopes) =
+  let istyp,tmp_scope = make_type_scope_soft tmp_scope in
+  istyp,Option.fold_right push_uninterp_scope tmp_scope
+    (push_uninterp_scopes scopes !uninterp_scope_stack)
+
 (**********************************************************************)
 (* Delimiters *)
 
@@ -365,30 +373,42 @@ let keymap_add key sc interp (scope_map,global_map) =
   | (NotationRule (None,_) | SynDefRule _), _, _ -> global_map in
   (scope_map, global_map)
 
-let keymap_extract keys sc map =
+let keymap_extract istype keys sc map =
   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
+  let delim =
+    if istype && Option.equal String.equal (Some sc) (current_type_scope_name ()) then
+      (* A type is re-interpreted with type_scope on top, so never need a delimiter *)
+      None
+    else
+      (* Pass the delimiter so that it can be used if ever the notation is masked *)
+      (String.Map.find sc !scope_map).delimiters in
+  let add_scope rule = (rule,delim,false) in
   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
+let find_with_delimiters istype = function
+  | None ->
+      None
+  | Some _ as scope when istype && Option.equal String.equal scope (current_type_scope_name ()) ->
+      (* This is in case type_scope (which by default is open in the
+         initial state) has been explicitly closed *)
+      Some None
   | Some scope ->
       match (String.Map.find scope !scope_map).delimiters with
         | Some key -> Some (Some key)
         | None -> None
 
-let rec keymap_extract_remainder scope_seen = function
+let rec keymap_extract_remainder istype scope_seen = function
   | [] -> []
   | (sc,ntn,interp,c) :: l ->
-      if String.Set.mem sc scope_seen then keymap_extract_remainder scope_seen l
+      if String.Set.mem sc scope_seen then keymap_extract_remainder istype scope_seen l
       else
-        match find_with_delimiters (Some sc) with
-        | None -> keymap_extract_remainder scope_seen l
+        match find_with_delimiters istype (Some sc) with
+        | None -> keymap_extract_remainder istype scope_seen l
         | Some delim ->
            let rule = (NotationRule (Some sc, ntn), interp, c) in
-           (rule,delim,true) :: keymap_extract_remainder scope_seen l
+           (rule,delim,true) :: keymap_extract_remainder istype scope_seen l
 
 (* Scopes table : interpretation -> scope_name *)
 let notations_key_table =
@@ -954,7 +974,7 @@ let check_required_module ?loc sc (sp,d) =
 (* Look if some notation or numeral printer in [scope] can be used in
    the scope stack [scopes], and if yes, using delimiters or not *)
 
-let rec find_without_delimiters find (ntn_scope,ntn) = function
+let rec find_without_delimiters find (istype,ntn_scope,ntn as ntndata) = function
   | UninterpScope scope :: scopes ->
       (* Is the expected ntn/numpr attached to the most recently open scope? *)
       begin match ntn_scope with
@@ -964,21 +984,21 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
 	(* If the most recently open scope has a notation/numeral printer
     	   but not the expected one then we need delimiters *)
 	if find scope then
-	  find_with_delimiters ntn_scope
+          find_with_delimiters istype ntn_scope
 	else
-	  find_without_delimiters find (ntn_scope,ntn) scopes
+          find_without_delimiters find ntndata scopes
       end
   | UninterpSingle (NotationRule (_,ntn'),_,_) :: scopes ->
       begin match ntn_scope, ntn with
       | None, Some ntn when notation_eq ntn ntn' ->
         Some None
       | _ ->
-	find_without_delimiters find (ntn_scope,ntn) scopes
+        find_without_delimiters find ntndata  scopes
       end
-  | UninterpSingle (SynDefRule _,_,_) :: scopes -> find_without_delimiters find (ntn_scope,ntn) scopes
+  | UninterpSingle (SynDefRule _,_,_) :: scopes -> find_without_delimiters find ntndata  scopes
   | [] ->
       (* Can we switch to [scope]? Yes if it has defined delimiters *)
-      find_with_delimiters ntn_scope
+      find_with_delimiters istype ntn_scope
 
 (* The mapping between notations and their interpretation *)
 
@@ -1101,16 +1121,16 @@ let interp_notation ?loc ntn local_scopes =
     user_err ?loc 
     (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".")
 
-let extract_notations scopes keys =
+let extract_notations (istype,scopes) keys =
   if keys == [] then [] (* shortcut *) else
   let scope_map, global_map = !notations_key_table in
   let rec aux scopes seen =
   match scopes with
-  | UninterpScope sc :: scopes -> keymap_extract keys sc scope_map @ aux scopes (String.Set.add sc seen)
+  | UninterpScope sc :: scopes -> keymap_extract istype 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))
+      keymap_extract_remainder istype seen (List.flatten (List.map find keys))
   in aux scopes String.Set.empty
 
 let uninterp_notations scopes c =
@@ -1277,13 +1297,11 @@ let availability_of_prim_token n printer_scope local_scopes =
         | _ -> false
     with Not_found -> false
   in
-  let scopes = make_current_uninterp_scopes local_scopes in
-  find_without_delimiters f (Some printer_scope,None) scopes
+  let istype,scopes = make_current_uninterp_scopes local_scopes in
+  find_without_delimiters f (istype,Some printer_scope,None) scopes
 
 (* Miscellaneous *)
 
-let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2
-
 let notation_binder_source_eq s1 s2 = match s1, s2 with
 | NtnParsedAsIdent,  NtnParsedAsIdent -> true
 | NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2
@@ -1297,9 +1315,10 @@ let ntpe_eq t1 t2 = match t1, t2 with
 | NtnTypeBinderList, NtnTypeBinderList -> true
 | (NtnTypeConstr | NtnTypeBinder _ | NtnTypeConstrList | NtnTypeBinderList), _ -> false
 
-let var_attributes_eq (_, ((entry1, sc1), tp1)) (_, ((entry2, sc2), tp2)) =
+let var_attributes_eq (_, ((entry1, (tmpsc1, scl1)), tp1)) (_, ((entry2, (tmpsc2, scl2)), tp2)) =
   notation_entry_level_eq entry1 entry2 &&
-  pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 &&
+  Option.equal String.equal tmpsc1 tmpsc2 &&
+  List.equal String.equal scl1 scl2 &&
   ntpe_eq tp1 tp2
 
 let interpretation_eq (vars1, t1) (vars2, t2) =
-- 
cgit v1.2.3