From 64cb952f3fcf41c25a66a92bd124bba82e6db3f6 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Wed, 14 Mar 2018 10:23:51 +0100
Subject: Notation: no more chains of prim_token_interpreter

 This cleanup prepares for forthcoming synchronization of prim_token_interpreter
 wrt to Summary. These chains of prim_token_interpreter were anyway never used,
 only one interpreter was declared per numeral scope.

 After sync wrt Summary, we'll anyway be able to backtrack to a previous
 interpreter.
---
 interp/notation.ml | 18 +++++++-----------
 1 file changed, 7 insertions(+), 11 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 625d072b9f..36d4b0aa15 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -319,12 +319,7 @@ let prim_token_interpreter_tab =
   (Hashtbl.create 7 : (scope_name, internal_prim_token_interpreter) Hashtbl.t)
 
 let add_prim_token_interpreter sc interp =
-  try
-    let cont = Hashtbl.find prim_token_interpreter_tab sc in
-    Hashtbl.replace prim_token_interpreter_tab sc (interp cont)
-  with Not_found ->
-    let cont = (fun ?loc _p -> raise Not_found) in
-    Hashtbl.add prim_token_interpreter_tab sc (interp cont)
+  Hashtbl.replace prim_token_interpreter_tab sc interp
 
 let declare_prim_token_interpreter sc interp (patl,uninterp,b) =
   declare_scope sc;
@@ -351,8 +346,8 @@ type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign
 
 let declare_rawnumeral_interpreter sc dir interp (patl,uninterp,inpat) =
   declare_prim_token_interpreter sc
-    (fun cont ?loc -> function Numeral (n,s) -> delay dir interp ?loc (n,s)
-                            | p -> cont ?loc p)
+    (fun ?loc -> function Numeral (n,s) -> delay dir interp ?loc (n,s)
+                            | _ -> raise Not_found)
     (patl, (fun r -> match uninterp r with
                      | None -> None
                      | Some (n,s) -> Some (Numeral (n,s))), inpat)
@@ -360,13 +355,14 @@ let declare_rawnumeral_interpreter sc dir interp (patl,uninterp,inpat) =
 let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) =
   let interp' ?loc (n,s) = interp ?loc (ofNumeral n s) in
   declare_prim_token_interpreter sc
-    (fun cont ?loc -> function Numeral (n,s) -> delay dir interp' ?loc (n,s)
-                            | p -> cont ?loc p)
+    (fun ?loc -> function Numeral (n,s) -> delay dir interp' ?loc (n,s)
+                            | _ -> raise Not_found)
     (patl, (fun r -> Option.map mkNumeral (uninterp r)), inpat)
 
 let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
   declare_prim_token_interpreter sc
-    (fun cont ?loc -> function String s -> delay dir interp ?loc s | p -> cont ?loc p)
+    (fun ?loc -> function String s -> delay dir interp ?loc s
+                        | _ -> raise Not_found)
     (patl, (fun r -> mkString (uninterp r)), inpat)
 
 let check_required_module ?loc sc (sp,d) =
-- 
cgit v1.2.3


From fa8e58f00b6774ac8669a7282d7863f8a605abd2 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Wed, 14 Mar 2018 11:17:50 +0100
Subject: Notation: avoid one intermediate (unit -> ...)

---
 interp/notation.ml | 47 ++++++++++++++++++++++++++---------------------
 1 file changed, 26 insertions(+), 21 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 36d4b0aa15..4b25146c50 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -304,6 +304,8 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
 
 type required_module = full_path * string list
 
+type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign
+
 type 'a prim_token_interpreter =
     ?loc:Loc.t -> 'a -> glob_constr
 
@@ -313,17 +315,19 @@ type 'a prim_token_uninterpreter =
     glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status
 
 type internal_prim_token_interpreter =
-    ?loc:Loc.t -> prim_token -> required_module * (unit -> glob_constr)
+  | ForNumeral of rawnum prim_token_interpreter
+  | ForString of string prim_token_interpreter
 
 let prim_token_interpreter_tab =
-  (Hashtbl.create 7 : (scope_name, internal_prim_token_interpreter) Hashtbl.t)
+  (Hashtbl.create 7 :
+     (scope_name, required_module * internal_prim_token_interpreter) Hashtbl.t)
 
-let add_prim_token_interpreter sc interp =
-  Hashtbl.replace prim_token_interpreter_tab sc interp
+let add_prim_token_interpreter sc (dir,interp) =
+  Hashtbl.replace prim_token_interpreter_tab sc (dir,interp)
 
-let declare_prim_token_interpreter sc interp (patl,uninterp,b) =
+let declare_prim_token_interpreter sc (dir,interp) (patl,uninterp,b) =
   declare_scope sc;
-  add_prim_token_interpreter sc interp;
+  add_prim_token_interpreter sc (dir,interp);
   List.iter (fun pat ->
       prim_token_key_table := KeyMap.add
         (glob_prim_constr_key pat) (sc,uninterp,b) !prim_token_key_table)
@@ -340,29 +344,21 @@ let mkString = function
 | None -> None
 | Some s -> if Unicode.is_utf8 s then Some (String s) else None
 
-let delay dir int ?loc x = (dir, (fun () -> int ?loc x))
-
-type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign
-
 let declare_rawnumeral_interpreter sc dir interp (patl,uninterp,inpat) =
   declare_prim_token_interpreter sc
-    (fun ?loc -> function Numeral (n,s) -> delay dir interp ?loc (n,s)
-                            | _ -> raise Not_found)
+    (dir, ForNumeral interp)
     (patl, (fun r -> match uninterp r with
                      | None -> None
                      | Some (n,s) -> Some (Numeral (n,s))), inpat)
 
 let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) =
-  let interp' ?loc (n,s) = interp ?loc (ofNumeral n s) in
   declare_prim_token_interpreter sc
-    (fun ?loc -> function Numeral (n,s) -> delay dir interp' ?loc (n,s)
-                            | _ -> raise Not_found)
+    (dir, ForNumeral (fun ?loc (n,s) -> interp ?loc (ofNumeral n s)))
     (patl, (fun r -> Option.map mkNumeral (uninterp r)), inpat)
 
 let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
   declare_prim_token_interpreter sc
-    (fun ?loc -> function String s -> delay dir interp ?loc s
-                        | _ -> raise Not_found)
+    (dir, ForString interp)
     (patl, (fun r -> mkString (uninterp r)), inpat)
 
 let check_required_module ?loc sc (sp,d) =
@@ -472,9 +468,14 @@ let find_prim_token check_allowed ?loc p sc =
     pat, df
   with Not_found ->
   (* Try for a primitive numerical notation *)
-  let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc ?loc p in
+  let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc in
   check_required_module ?loc sc spdir;
-  let pat = interp () in
+  let pat =
+    match p, interp with
+    | Numeral (n,s), ForNumeral interp -> interp ?loc (n,s)
+    | String s, ForString interp -> interp ?loc s
+    | _ -> raise Not_found
+  in
   check_allowed pat;
   pat, ((dirpath (fst spdir),DirPath.empty),"")
 
@@ -680,8 +681,12 @@ let uninterp_prim_token_cases_pattern c =
 
 let availability_of_prim_token n printer_scope local_scopes =
   let f scope =
-    try ignore ((Hashtbl.find prim_token_interpreter_tab scope) n); true
-    with Not_found -> false in
+    match n, Hashtbl.find prim_token_interpreter_tab scope with
+    | exception Not_found -> false
+    | Numeral _, (_,ForNumeral _) -> true
+    | String _, (_,ForString _) -> true
+    | _ -> false
+  in
   let scopes = make_current_scopes local_scopes in
   Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes)
 
-- 
cgit v1.2.3


From 3099be05553dab10b41d864f4981860eb105f145 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Wed, 4 Apr 2018 16:06:50 +0200
Subject: Notation: remove support for prim tokens denoting inductive types in
 "return"

 This is prim token notations for inductive *types*, not values.
 So we're speaking of a scope where 0 is the type nat, 1 is the type bool, etc.

 To my knowledge, this feature hasn't ever been used, and is very unlikely
 to be used ever, so let's clean the code a bit by removing it.
---
 interp/notation.ml | 14 --------------
 1 file changed, 14 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 4b25146c50..ebb734cb08 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -654,20 +654,6 @@ let uninterp_prim_token c =
       | Some n -> (sc,n)
   with Not_found -> raise Notation_ops.No_match
 
-let uninterp_prim_token_ind_pattern ind args =
-  let ref = IndRef ind in
-  try
-    let k = RefKey (canonical_gr ref) in
-    let (sc,numpr,b) = KeyMap.find k !prim_token_key_table in
-    if not b then raise Notation_ops.No_match;
-    let args' = List.map
-      (fun x -> snd (glob_constr_of_closed_cases_pattern x)) args in
-    let ref = DAst.make @@ GRef (ref,None) in
-    match numpr (AnyGlobConstr (DAst.make @@ GApp (ref,args'))) with
-      | None -> raise Notation_ops.No_match
-      | Some n -> (sc,n)
-  with Not_found -> raise Notation_ops.No_match
-
 let uninterp_prim_token_cases_pattern c =
   try
     let k = cases_pattern_key c in
-- 
cgit v1.2.3


From b3c75936a4912ca794cdcecfeb92044552336c63 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Wed, 4 Apr 2018 10:43:38 +0200
Subject: prim notations backtrackable, their declarations now in two parts
 (API change)

 The first part (e.g. register_bignumeral_interpretation) deals only with
 the interp/uninterp closures. It should typically be done as a side
 effect during a syntax plugin loading. No prim notation are active yet
 after this phase.

 The second part (enable_prim_token_interpretation) activates the prim
 notation. It is now correctly talking to Summary and to the LibStack.
 To avoid "phantom" objects in libstack after a mere Require, this
 second part should be done inside a Mltop.declare_cache_obj

 The link between the two parts is a prim_token_uid (a string), which
 should be unique for each primitive notation. When this primitive
 notation is specific to a scope, the scope_name could be used as uid.

 Btw, the list of "patterns" for detecting when an uninterpreter should
 be considered is now restricted to a list of global_reference
 (inductive constructors, or injection functions such as IZR).
 The earlier API was accepting a glob_constr list, but was actually
 only working well for global_reference.

 A minimal compatibility is provided (declare_numeral_interpreter),
 but is discouraged, since it is known to store uncessary objects
 in the libstack.
---
 interp/notation.ml | 272 ++++++++++++++++++++++++++++++++++++-----------------
 1 file changed, 188 insertions(+), 84 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index ebb734cb08..f60ddcf909 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -266,16 +266,14 @@ let keymap_find key map =
 (* Scopes table : interpretation -> scope_name *)
 let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t)
 
-let prim_token_key_table = ref (KeyMap.empty : (string * (any_glob_constr -> prim_token option) * bool) KeyMap.t)
-
 let glob_prim_constr_key c = match DAst.get c with
-  | GRef (ref, _) -> RefKey (canonical_gr ref)
+  | GRef (ref, _) -> Some (canonical_gr ref)
   | GApp (c, _) ->
     begin match DAst.get c with
-    | GRef (ref, _) -> RefKey (canonical_gr ref)
-    | _ -> Oth
+    | GRef (ref, _) -> Some (canonical_gr ref)
+    | _ -> None
     end
-  | _ -> Oth
+  | _ -> None
 
 let glob_constr_keys c = match DAst.get c with
   | GApp (c, _) ->
@@ -303,63 +301,167 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
 (* Interpreting numbers (not in summary because functional objects)   *)
 
 type required_module = full_path * string list
-
 type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign
 
-type 'a prim_token_interpreter =
-    ?loc:Loc.t -> 'a -> glob_constr
+type prim_token_uid = string
+
+type 'a prim_token_interpreter = ?loc:Loc.t -> 'a -> glob_constr
+type 'a prim_token_uninterpreter = any_glob_constr -> 'a option
+
+type 'a prim_token_interpretation =
+  'a prim_token_interpreter * 'a prim_token_uninterpreter
+
+module InnerPrimToken = struct
 
-type cases_pattern_status = bool (* true = use prim token in patterns *)
+  type interpreter =
+    | RawNumInterp of (?loc:Loc.t -> rawnum -> glob_constr)
+    | BigNumInterp of (?loc:Loc.t -> Bigint.bigint -> glob_constr)
+    | StringInterp of (?loc:Loc.t -> string -> glob_constr)
 
-type 'a prim_token_uninterpreter =
-    glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status
+  let interp_eq f f' = match f,f' with
+    | RawNumInterp f, RawNumInterp f' -> f == f'
+    | BigNumInterp f, BigNumInterp f' -> f == f'
+    | StringInterp f, StringInterp f' -> f == f'
+    | _ -> false
+
+  let ofNumeral n s =
+    if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n)
+
+  let do_interp ?loc interp primtok =
+    match primtok, interp with
+    | Numeral (n,s), RawNumInterp interp -> interp ?loc (n,s)
+    | Numeral (n,s), BigNumInterp interp -> interp ?loc (ofNumeral n s)
+    | String s, StringInterp interp -> interp ?loc s
+    | _ -> raise Not_found
+
+  type uninterpreter =
+    | RawNumUninterp of (any_glob_constr -> rawnum option)
+    | BigNumUninterp of (any_glob_constr -> Bigint.bigint option)
+    | StringUninterp of (any_glob_constr -> string option)
+
+  let uninterp_eq f f' = match f,f' with
+    | RawNumUninterp f, RawNumUninterp f' -> f == f'
+    | BigNumUninterp f, BigNumUninterp f' -> f == f'
+    | StringUninterp f, StringUninterp f' -> f == f'
+    | _ -> false
 
-type internal_prim_token_interpreter =
-  | ForNumeral of rawnum prim_token_interpreter
-  | ForString of string prim_token_interpreter
+  let mkNumeral n =
+    if Bigint.is_pos_or_zero n then Numeral (Bigint.to_string n, true)
+    else Numeral (Bigint.to_string (Bigint.neg n), false)
 
-let prim_token_interpreter_tab =
-  (Hashtbl.create 7 :
-     (scope_name, required_module * internal_prim_token_interpreter) Hashtbl.t)
+  let mkString = function
+    | None -> None
+    | Some s -> if Unicode.is_utf8 s then Some (String s) else None
 
-let add_prim_token_interpreter sc (dir,interp) =
-  Hashtbl.replace prim_token_interpreter_tab sc (dir,interp)
+  let do_uninterp uninterp g = match uninterp with
+    | RawNumUninterp u -> Option.map (fun (n,s) -> Numeral (n,s)) (u g)
+    | BigNumUninterp u -> Option.map mkNumeral (u g)
+    | StringUninterp u -> mkString (u g)
 
-let declare_prim_token_interpreter sc (dir,interp) (patl,uninterp,b) =
+end
+
+(* The following two tables of (un)interpreters will *not* be synchronized.
+   But their indexes will be checked to be unique *)
+let prim_token_interpreters =
+  (Hashtbl.create 7 : (prim_token_uid, InnerPrimToken.interpreter) Hashtbl.t)
+
+let prim_token_uninterpreters =
+  (Hashtbl.create 7 : (prim_token_uid, InnerPrimToken.uninterpreter) Hashtbl.t)
+
+(* Table from scope_name to backtrack-able informations about interpreters
+   (in particular interpreter unique id). *)
+let prim_token_interp_infos =
+  ref (String.Map.empty : (required_module * prim_token_uid) String.Map.t)
+
+(* Table from global_reference to backtrack-able informations about
+   prim_token uninterpretation (in particular uninterpreter unique id). *)
+let prim_token_uninterp_infos =
+  ref (Refmap.empty : (scope_name * prim_token_uid * bool) Refmap.t)
+
+let hashtbl_check_and_set uid f h eq =
+  match Hashtbl.find h uid with
+   | exception Not_found -> Hashtbl.add h uid f
+   | g when eq f g -> ()
+   | _ ->
+      user_err ~hdr:"prim_token_interpreter"
+       (str "Unique identifier " ++ str uid ++
+        str " already used to register a numeral or string (un)interpreter.")
+
+let register_gen_interpretation uid (interp, uninterp) =
+  hashtbl_check_and_set
+    uid interp prim_token_interpreters InnerPrimToken.interp_eq;
+  hashtbl_check_and_set
+    uid uninterp prim_token_uninterpreters InnerPrimToken.uninterp_eq
+
+let register_rawnumeral_interpretation uid (interp, uninterp) =
+  register_gen_interpretation uid
+    (InnerPrimToken.RawNumInterp interp, InnerPrimToken.RawNumUninterp uninterp)
+
+let register_bignumeral_interpretation uid (interp, uninterp) =
+  register_gen_interpretation uid
+    (InnerPrimToken.BigNumInterp interp, InnerPrimToken.BigNumUninterp uninterp)
+
+let register_string_interpretation uid (interp, uninterp) =
+  register_gen_interpretation uid
+    (InnerPrimToken.StringInterp interp, InnerPrimToken.StringUninterp uninterp)
+
+type prim_token_infos = {
+  pt_scope : scope_name; (** Concerned scope *)
+  pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *)
+  pt_required : required_module; (** Module that should be loaded first *)
+  pt_refs : global_reference list; (** Entry points during uninterpretation *)
+  pt_in_match : bool (** Is this prim token legal in match patterns ? *)
+}
+
+let cache_prim_token_interpretation (_,infos) =
+  let sc = infos.pt_scope in
+  let uid = infos.pt_uid in
   declare_scope sc;
-  add_prim_token_interpreter sc (dir,interp);
-  List.iter (fun pat ->
-      prim_token_key_table := KeyMap.add
-        (glob_prim_constr_key pat) (sc,uninterp,b) !prim_token_key_table)
-    patl
-
-let mkNumeral n =
-  if Bigint.is_pos_or_zero n then Numeral (Bigint.to_string n, true)
-  else Numeral (Bigint.to_string (Bigint.neg n), false)
-
-let ofNumeral n s =
-  if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n)
-
-let mkString = function
-| None -> None
-| Some s -> if Unicode.is_utf8 s then Some (String s) else None
-
-let declare_rawnumeral_interpreter sc dir interp (patl,uninterp,inpat) =
-  declare_prim_token_interpreter sc
-    (dir, ForNumeral interp)
-    (patl, (fun r -> match uninterp r with
-                     | None -> None
-                     | Some (n,s) -> Some (Numeral (n,s))), inpat)
-
-let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) =
-  declare_prim_token_interpreter sc
-    (dir, ForNumeral (fun ?loc (n,s) -> interp ?loc (ofNumeral n s)))
-    (patl, (fun r -> Option.map mkNumeral (uninterp r)), inpat)
-
-let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
-  declare_prim_token_interpreter sc
-    (dir, ForString interp)
-    (patl, (fun r -> mkString (uninterp r)), inpat)
+  prim_token_interp_infos :=
+    String.Map.add sc (infos.pt_required,infos.pt_uid) !prim_token_interp_infos;
+  List.iter (fun r -> prim_token_uninterp_infos :=
+                        Refmap.add r (sc,uid,infos.pt_in_match)
+                          !prim_token_uninterp_infos)
+            infos.pt_refs
+
+let subst_prim_token_interpretation (subs,infos) =
+  { infos with
+    pt_refs = List.map (subst_global_reference subs) infos.pt_refs }
+
+let inPrimTokenInterp : prim_token_infos -> obj =
+  declare_object {(default_object "PRIM-TOKEN-INTERP") with
+     cache_function = cache_prim_token_interpretation;
+     load_function  = (fun _ -> cache_prim_token_interpretation);
+     subst_function = subst_prim_token_interpretation;
+     classify_function = (fun o -> Substitute o)}
+
+let enable_prim_token_interpretation infos =
+  Lib.add_anonymous_leaf (inPrimTokenInterp infos)
+
+(** Compatibility.
+    Avoid the next two functions, they will now store unnecessary
+    objects in the library segment. Instead, combine
+    [register_*_interpretation] and [enable_prim_token_interpretation]
+    (the latter inside a [Mltop.declare_cache_obj]).
+*)
+
+let declare_numeral_interpreter sc dir interp (patl,uninterp,b) =
+  register_bignumeral_interpretation sc (interp,uninterp);
+  enable_prim_token_interpretation
+    { pt_scope = sc;
+      pt_uid = sc;
+      pt_required = dir;
+      pt_refs = List.map_filter glob_prim_constr_key patl;
+      pt_in_match = b }
+let declare_string_interpreter sc dir interp (patl,uninterp,b) =
+  register_string_interpretation sc (interp,uninterp);
+  enable_prim_token_interpretation
+    { pt_scope = sc;
+      pt_uid = sc;
+      pt_required = dir;
+      pt_refs = List.map_filter glob_prim_constr_key patl;
+      pt_in_match = b }
+
 
 let check_required_module ?loc sc (sp,d) =
   try let _ = Nametab.global_of_path sp in ()
@@ -468,14 +570,10 @@ let find_prim_token check_allowed ?loc p sc =
     pat, df
   with Not_found ->
   (* Try for a primitive numerical notation *)
-  let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc in
+  let (spdir,uid) = String.Map.find sc !prim_token_interp_infos in
   check_required_module ?loc sc spdir;
-  let pat =
-    match p, interp with
-    | Numeral (n,s), ForNumeral interp -> interp ?loc (n,s)
-    | String s, ForString interp -> interp ?loc s
-    | _ -> raise Not_found
-  in
+  let interp = Hashtbl.find prim_token_interpreters uid in
+  let pat = InnerPrimToken.do_interp ?loc interp p in
   check_allowed pat;
   pat, ((dirpath (fst spdir),DirPath.empty),"")
 
@@ -646,32 +744,33 @@ let entry_has_ident = function
      try String.Map.find s !entry_has_ident_map <= n with Not_found -> false
 
 let uninterp_prim_token c =
-  try
-    let (sc,numpr,_) =
-      KeyMap.find (glob_prim_constr_key c) !prim_token_key_table in
-    match numpr (AnyGlobConstr c) with
-      | None -> raise Notation_ops.No_match
-      | Some n -> (sc,n)
-  with Not_found -> raise Notation_ops.No_match
+  match glob_prim_constr_key c with
+  | None -> raise Notation_ops.No_match
+  | Some r ->
+     try
+       let (sc,uid,_) = Refmap.find r !prim_token_uninterp_infos in
+       let uninterp = Hashtbl.find prim_token_uninterpreters uid in
+       match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with
+       | None -> raise Notation_ops.No_match
+       | Some n -> (sc,n)
+     with Not_found -> raise Notation_ops.No_match
 
 let uninterp_prim_token_cases_pattern c =
-  try
-    let k = cases_pattern_key c in
-    let (sc,numpr,b) = KeyMap.find k !prim_token_key_table in
-    if not b then raise Notation_ops.No_match;
-    let na,c = glob_constr_of_closed_cases_pattern c in
-    match numpr (AnyGlobConstr c) with
-      | None -> raise Notation_ops.No_match
-      | Some n -> (na,sc,n)
-  with Not_found -> raise Notation_ops.No_match
+  match glob_constr_of_closed_cases_pattern c with
+  | exception Not_found -> raise Notation_ops.No_match
+  | na,c -> let (sc,n) = uninterp_prim_token c in (na,sc,n)
 
 let availability_of_prim_token n printer_scope local_scopes =
   let f scope =
-    match n, Hashtbl.find prim_token_interpreter_tab scope with
-    | exception Not_found -> false
-    | Numeral _, (_,ForNumeral _) -> true
-    | String _, (_,ForString _) -> true
-    | _ -> false
+    try
+      let uid = snd (String.Map.find scope !prim_token_interp_infos) in
+      let interp = Hashtbl.find prim_token_interpreters uid in
+      let open InnerPrimToken in
+      match n, interp with
+      | Numeral _, (RawNumInterp _ | BigNumInterp _) -> true
+      | String _, StringInterp _ -> true
+      | _ -> 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)
@@ -1193,16 +1292,19 @@ let pr_visibility prglob = function
 let freeze _ =
  (!scope_map, !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,coe,globs,ids) =
+let unfreeze (scm,scs,asc,dlm,fkm,clsc,ptii,ptui,coe,globs,ids) =
   scope_map := scm;
   scope_stack := scs;
   delimiters_map := dlm;
   arguments_scope := asc;
   notations_key_table := fkm;
   scope_class_map := clsc;
+  prim_token_interp_infos := ptii;
+  prim_token_uninterp_infos := ptui;
   entry_coercion_map := coe;
   entry_has_global_map := globs;
   entry_has_ident_map := ids
@@ -1211,7 +1313,9 @@ let init () =
   init_scope_map ();
   delimiters_map := String.Map.empty;
   notations_key_table := KeyMap.empty;
-  scope_class_map := initial_scope_class_map
+  scope_class_map := initial_scope_class_map;
+  prim_token_interp_infos := String.Map.empty;
+  prim_token_uninterp_infos := Refmap.empty
 
 let _ =
   Summary.declare_summary "symbols"
-- 
cgit v1.2.3


From fa0f378c91286d9127777a06b1dc557f695c22ae Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sat, 14 Jul 2018 06:25:22 -0400
Subject: Fix numeral notation for a rebase on top of master

Some of this code is cargo-culted or kludged to work.

As I understand it, the situation is as follows:
There are two sorts of use-cases that need to be supported:
1. A plugin registers an OCaml function as a numeral interpreter.  In
   this case, the function registration must be synchronized with the
   document state, but the functions should not be marshelled / stored
   in the .vo.
2. A vernacular registers a Gallina function as a numeral interpreter.
   In this case, the registration must be synchronized, and the function
   should be marshelled / stored in the .vo.

In case (1), we can compare functions by pointer equality, and we should
be able to rely on globally unique keys, even across backtracking.

In case (2), we cannot compare functions by pointer equality (because
they must be regenerated on unmarshelling when `Require`ing a .vo file),
and we also cannot rely on any sort of unique key being both unique and
persistent across files.

The solution we use here is that we ask clients to provide "unique"
keys, and that clients tell us whether or not to overwrite existing
registered functions, i.e., to tell us whether or not we should expect
interpreter functions to be globally unique under pointer equality.  For
plugins, a simple string suffices, as long as the string does not clash
between different plugins.  In the case of vernacular-registered
functions, use marshell a description of all of the data used to
generate the function, and use that string as a unique key which is
expected to persist across files.  Because we cannot rely on
function-pointer uniqueness here, we tell the
interpretation-registration to allow overwriting.

----

Some of this code is response to comments on the PR

----

Some code is to fix an issue that bignums revealed:

Both Int31 and bignums registered numeral notations in int31_scope.  We
now prepend a globally unique identifier when registering numeral
notations from OCaml plugins.  This is permissible because we don't
store the uid information for such notations in .vo files (assuming I'm
understanding the code correctly).
---
 interp/notation.ml | 37 ++++++++++++++++++++++---------------
 1 file changed, 22 insertions(+), 15 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index f60ddcf909..56d6acbdae 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -378,38 +378,39 @@ let prim_token_interp_infos =
 let prim_token_uninterp_infos =
   ref (Refmap.empty : (scope_name * prim_token_uid * bool) Refmap.t)
 
-let hashtbl_check_and_set uid f h eq =
+let hashtbl_check_and_set allow_overwrite uid f h eq =
   match Hashtbl.find h uid with
    | exception Not_found -> Hashtbl.add h uid f
+   | _ when allow_overwrite -> Hashtbl.add h uid f
    | g when eq f g -> ()
    | _ ->
       user_err ~hdr:"prim_token_interpreter"
        (str "Unique identifier " ++ str uid ++
         str " already used to register a numeral or string (un)interpreter.")
 
-let register_gen_interpretation uid (interp, uninterp) =
+let register_gen_interpretation allow_overwrite uid (interp, uninterp) =
   hashtbl_check_and_set
-    uid interp prim_token_interpreters InnerPrimToken.interp_eq;
+    allow_overwrite uid interp prim_token_interpreters InnerPrimToken.interp_eq;
   hashtbl_check_and_set
-    uid uninterp prim_token_uninterpreters InnerPrimToken.uninterp_eq
+    allow_overwrite uid uninterp prim_token_uninterpreters InnerPrimToken.uninterp_eq
 
-let register_rawnumeral_interpretation uid (interp, uninterp) =
-  register_gen_interpretation uid
+let register_rawnumeral_interpretation ?(allow_overwrite=false) uid (interp, uninterp) =
+  register_gen_interpretation allow_overwrite uid
     (InnerPrimToken.RawNumInterp interp, InnerPrimToken.RawNumUninterp uninterp)
 
-let register_bignumeral_interpretation uid (interp, uninterp) =
-  register_gen_interpretation uid
+let register_bignumeral_interpretation ?(allow_overwrite=false) uid (interp, uninterp) =
+  register_gen_interpretation allow_overwrite uid
     (InnerPrimToken.BigNumInterp interp, InnerPrimToken.BigNumUninterp uninterp)
 
-let register_string_interpretation uid (interp, uninterp) =
-  register_gen_interpretation uid
+let register_string_interpretation ?(allow_overwrite=false) uid (interp, uninterp) =
+  register_gen_interpretation allow_overwrite uid
     (InnerPrimToken.StringInterp interp, InnerPrimToken.StringUninterp uninterp)
 
 type prim_token_infos = {
   pt_scope : scope_name; (** Concerned scope *)
   pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *)
   pt_required : required_module; (** Module that should be loaded first *)
-  pt_refs : global_reference list; (** Entry points during uninterpretation *)
+  pt_refs : GlobRef.t list; (** Entry points during uninterpretation *)
   pt_in_match : bool (** Is this prim token legal in match patterns ? *)
 }
 
@@ -445,19 +446,25 @@ let enable_prim_token_interpretation infos =
     (the latter inside a [Mltop.declare_cache_obj]).
 *)
 
+let fresh_string_of =
+  let count = ref 0 in
+  fun root -> count := !count+1; (string_of_int !count)^"_"^root
+
 let declare_numeral_interpreter sc dir interp (patl,uninterp,b) =
-  register_bignumeral_interpretation sc (interp,uninterp);
+  let uid = fresh_string_of sc in
+  register_bignumeral_interpretation uid (interp,uninterp);
   enable_prim_token_interpretation
     { pt_scope = sc;
-      pt_uid = sc;
+      pt_uid = uid;
       pt_required = dir;
       pt_refs = List.map_filter glob_prim_constr_key patl;
       pt_in_match = b }
 let declare_string_interpreter sc dir interp (patl,uninterp,b) =
-  register_string_interpretation sc (interp,uninterp);
+  let uid = fresh_string_of sc in
+  register_string_interpretation uid (interp,uninterp);
   enable_prim_token_interpretation
     { pt_scope = sc;
-      pt_uid = sc;
+      pt_uid = uid;
       pt_required = dir;
       pt_refs = List.map_filter glob_prim_constr_key patl;
       pt_in_match = b }
-- 
cgit v1.2.3


From 6dcbbeb95682bbf470e58e25e0a357a84c3283b6 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 23 Aug 2018 11:03:29 -0400
Subject: Make Numeral Notation follow Import, not Require

Because that's the sane thing to do.

This will inevitably cause issues for projects which do not `Import
Coq.Strings.Ascii` before trying to use ascii notations.

We also move the syntax plugin for `int31` notations from `Cyclic31` to
`Int31`, so that users (like CompCert) who merely `Require Import
Coq.Numbers.Cyclic.Int31.Int31` get the `int31` numeral syntax.  Since
`Cyclic31` `Export`s `Int31`, this should not cause any additional
incompatibilities.
---
 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 56d6acbdae..d6bd62e121 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -431,8 +431,8 @@ let subst_prim_token_interpretation (subs,infos) =
 
 let inPrimTokenInterp : prim_token_infos -> obj =
   declare_object {(default_object "PRIM-TOKEN-INTERP") with
+     open_function  = (fun i o -> if Int.equal i 1 then cache_prim_token_interpretation o);
      cache_function = cache_prim_token_interpretation;
-     load_function  = (fun _ -> cache_prim_token_interpretation);
      subst_function = subst_prim_token_interpretation;
      classify_function = (fun o -> Substitute o)}
 
-- 
cgit v1.2.3


From e9d44aefa9d6058c72845788745468aa010708b5 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 23 Aug 2018 15:10:58 -0400
Subject: Make Numeral Notation obey Local/Global

Thanks to Emilio and Pierre-Marie Pédrot for pointers.
---
 interp/notation.ml | 16 +++++++++++-----
 1 file changed, 11 insertions(+), 5 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index d6bd62e121..551f1bfa83 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -407,6 +407,7 @@ let register_string_interpretation ?(allow_overwrite=false) uid (interp, uninter
     (InnerPrimToken.StringInterp interp, InnerPrimToken.StringUninterp uninterp)
 
 type prim_token_infos = {
+  pt_local : bool; (** Is this interpretation local? *)
   pt_scope : scope_name; (** Concerned scope *)
   pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *)
   pt_required : required_module; (** Module that should be loaded first *)
@@ -429,12 +430,15 @@ let subst_prim_token_interpretation (subs,infos) =
   { infos with
     pt_refs = List.map (subst_global_reference subs) infos.pt_refs }
 
+let classify_prim_token_interpretation infos =
+    if infos.pt_local then Dispose else Substitute infos
+
 let inPrimTokenInterp : prim_token_infos -> obj =
   declare_object {(default_object "PRIM-TOKEN-INTERP") with
      open_function  = (fun i o -> if Int.equal i 1 then cache_prim_token_interpretation o);
      cache_function = cache_prim_token_interpretation;
      subst_function = subst_prim_token_interpretation;
-     classify_function = (fun o -> Substitute o)}
+     classify_function = classify_prim_token_interpretation}
 
 let enable_prim_token_interpretation infos =
   Lib.add_anonymous_leaf (inPrimTokenInterp infos)
@@ -450,20 +454,22 @@ let fresh_string_of =
   let count = ref 0 in
   fun root -> count := !count+1; (string_of_int !count)^"_"^root
 
-let declare_numeral_interpreter sc dir interp (patl,uninterp,b) =
+let declare_numeral_interpreter ?(local=false) sc dir interp (patl,uninterp,b) =
   let uid = fresh_string_of sc in
   register_bignumeral_interpretation uid (interp,uninterp);
   enable_prim_token_interpretation
-    { pt_scope = sc;
+    { pt_local = local;
+      pt_scope = sc;
       pt_uid = uid;
       pt_required = dir;
       pt_refs = List.map_filter glob_prim_constr_key patl;
       pt_in_match = b }
-let declare_string_interpreter sc dir interp (patl,uninterp,b) =
+let declare_string_interpreter ?(local=false) sc dir interp (patl,uninterp,b) =
   let uid = fresh_string_of sc in
   register_string_interpretation uid (interp,uninterp);
   enable_prim_token_interpretation
-    { pt_scope = sc;
+    { pt_local = local;
+      pt_scope = sc;
       pt_uid = uid;
       pt_required = dir;
       pt_refs = List.map_filter glob_prim_constr_key patl;
-- 
cgit v1.2.3


From 17cb475550a0f4efe9f3f4c58fdbd9039f5fdd68 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 31 Aug 2018 17:01:43 -0400
Subject: Give a proper error message on num-not in functor

Numeral Notations are not well-supported inside functors.  We now give a
proper error message rather than an anomaly when this occurs.
---
 interp/notation.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 551f1bfa83..55ead946cb 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -479,8 +479,11 @@ let declare_string_interpreter ?(local=false) sc dir interp (patl,uninterp,b) =
 let check_required_module ?loc sc (sp,d) =
   try let _ = Nametab.global_of_path sp in ()
   with Not_found ->
-    user_err ?loc ~hdr:"prim_token_interpreter"
-    (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".")
+    match d with
+    | [] -> user_err ?loc ~hdr:"prim_token_interpreter"
+       (str "Cannot interpret in " ++ str sc ++ str " because " ++ pr_path sp ++ str " could not be found in the current environment.")
+    | _ -> user_err ?loc ~hdr:"prim_token_interpreter"
+       (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".")
 
 (* Look if some notation or numeral printer in [scope] can be used in
    the scope stack [scopes], and if yes, using delimiters or not *)
-- 
cgit v1.2.3