From f00ad3178990c84c5169e4e86bb9a65dbfd539ff Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 9 Dec 2019 17:44:33 +0100
Subject: Type-safe implementation of summary state.

For historical reasons we were wrapping the data stored in the summary objects
with dynamic type casts. There is no reason to do so since we have a proper
Dyn API. Furthermore, this had a small runtime cost when we knew that it was
never going to fail.
---
 library/summary.ml | 103 ++++++++++++++++++++++++++---------------------------
 1 file changed, 51 insertions(+), 52 deletions(-)

diff --git a/library/summary.ml b/library/summary.ml
index d3ae42694a..3ebd977d12 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -19,58 +19,49 @@ type 'a summary_declaration = {
   unfreeze_function : 'a -> unit;
   init_function : unit -> unit }
 
+module DynMap = Dyn.Map(struct type 'a t = 'a summary_declaration end)
+
 let sum_mod = ref None
-let sum_map = ref String.Map.empty
+let sum_map = ref DynMap.empty
 
 let mangle id = id ^ "-SUMMARY"
-let unmangle id = String.(sub id 0 (length id - 8))
 
 let ml_modules = "ML-MODULES"
 
-let internal_declare_summary fadd sumname sdecl =
-  let infun, outfun, tag = Dyn.Easy.make_dyn_tag (mangle sumname) in
-  let dyn_freeze ~marshallable = infun (sdecl.freeze_function ~marshallable)
-  and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum)
-  and dyn_init = sdecl.init_function in
-  let ddecl = {
-    freeze_function = dyn_freeze;
-    unfreeze_function = dyn_unfreeze;
-    init_function = dyn_init }
-  in
-  fadd sumname ddecl;
-  tag
-
 let declare_ml_modules_summary decl =
-  let ml_add _ ddecl = sum_mod := Some ddecl in
-  internal_declare_summary ml_add ml_modules decl
+  let tag = Dyn.create ml_modules in
+  sum_mod := Some (DynMap.Any (tag, decl))
 
-let declare_ml_modules_summary decl =
-  ignore(declare_ml_modules_summary decl)
+let check_name sumname = match Dyn.name sumname with
+| None -> ()
+| Some (Dyn.Any tag) ->
+  anomaly ~label:"Summary.declare_summary"
+    (str "Colliding summary names: " ++ str sumname ++ str " vs. " ++ str (Dyn.repr tag) ++ str ".")
 
 let declare_summary_tag sumname decl =
-  let fadd name ddecl = sum_map := String.Map.add name ddecl !sum_map in
-  let () = if String.Map.mem sumname !sum_map then
-      anomaly ~label:"Summary.declare_summary"
-        (str "Colliding summary names: " ++ str sumname ++ str " vs. " ++ str sumname ++ str ".")
-  in
-  internal_declare_summary fadd sumname decl
+  let () = check_name (mangle sumname) in
+  let tag = Dyn.create (mangle sumname) in
+  let () = sum_map := DynMap.add tag decl !sum_map in
+  tag
 
 let declare_summary sumname decl =
   ignore(declare_summary_tag sumname decl)
 
+module Frozen = Dyn.Map(struct type 'a t = 'a end)
+
 type frozen = {
-  summaries : Dyn.t String.Map.t;
+  summaries : Frozen.t;
   (** Ordered list w.r.t. the first component. *)
   ml_module : Dyn.t option;
   (** Special handling of the ml_module summary. *)
 }
 
-let empty_frozen = { summaries = String.Map.empty; ml_module = None }
+let empty_frozen = { summaries = Frozen.empty; ml_module = None }
 
 let freeze_summaries ~marshallable : frozen =
-  let smap decl = decl.freeze_function ~marshallable in
-  { summaries = String.Map.map smap !sum_map;
-    ml_module = Option.map (fun decl -> decl.freeze_function ~marshallable) !sum_mod;
+  let fold (DynMap.Any (tag, decl)) accu = Frozen.add tag (decl.freeze_function ~marshallable) accu in
+  { summaries = DynMap.fold fold !sum_map Frozen.empty;
+    ml_module = Option.map (fun (DynMap.Any (tag, decl)) -> Dyn.Dyn (tag, decl.freeze_function ~marshallable)) !sum_mod;
   }
 
 let warn_summary_out_of_scope =
@@ -88,22 +79,27 @@ let unfreeze_summaries ?(partial=false) { summaries; ml_module } =
    * may modify the content of [summaries] by loading new ML modules *)
   begin match !sum_mod with
   | None -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".")
-  | Some decl -> Option.iter (fun state -> decl.unfreeze_function state) ml_module
+  | Some (DynMap.Any (tag, decl)) ->
+    let iter (Dyn.Dyn (tag', v)) = match Dyn.eq tag tag' with
+    | None -> anomaly (str "Type mismatch in ML module summary")
+    | Some Refl -> decl.unfreeze_function v
+    in
+    Option.iter iter ml_module
   end;
   (* We must be independent on the order of the map! *)
-  let ufz name decl =
-    try decl.unfreeze_function String.Map.(find name summaries)
+  let ufz (DynMap.Any (name, decl)) =
+    try decl.unfreeze_function Frozen.(find name summaries)
     with Not_found ->
       if not partial then begin
-        warn_summary_out_of_scope name;
+        warn_summary_out_of_scope (Dyn.repr name);
         decl.init_function ()
       end;
   in
   (* String.Map.iter unfreeze_single !sum_map *)
-  String.Map.iter ufz !sum_map
+  DynMap.iter ufz !sum_map
 
 let init_summaries () =
-  String.Map.iter (fun _ decl -> decl.init_function ()) !sum_map
+  DynMap.iter (fun (DynMap.Any (_, decl)) -> decl.init_function ()) !sum_map
 
 (** For global tables registered statically before the end of coqtop
     launch, the following empty [init_function] could be used. *)
@@ -112,18 +108,15 @@ let nop () = ()
 
 (** Summary projection *)
 let project_from_summary { summaries } tag =
-  let id = unmangle (Dyn.repr tag) in
-  let state = String.Map.find id summaries in
-  Option.get (Dyn.Easy.prj state tag)
+  Frozen.find tag summaries
 
 let modify_summary st tag v =
-  let id = unmangle (Dyn.repr tag) in
-  let summaries = String.Map.set id (Dyn.Easy.inj v tag) st.summaries in
+  let () = assert (Frozen.mem tag st.summaries) in
+  let summaries = Frozen.add tag v st.summaries in
   {st with summaries}
 
 let remove_from_summary st tag =
-  let id = unmangle (Dyn.repr tag) in
-  let summaries = String.Map.remove id st.summaries in
+  let summaries = Frozen.remove tag st.summaries in
   {st with summaries}
 
 (** All-in-one reference declaration + registration *)
@@ -140,26 +133,32 @@ let ref ?freeze ~name x = fst @@ ref_tag ?freeze ~name x
 
 module Local = struct
 
-type 'a local_ref = ('a CEphemeron.key * string) ref
+type 'a local_ref = ('a CEphemeron.key * 'a Dyn.tag) ref
 
-let (:=) r v = r := (CEphemeron.create v, snd !r)
+let set r v = r := (CEphemeron.create v, snd !r)
 
-let (!) r =
+let get r =
   let key, name = !r in
   try CEphemeron.get key
   with CEphemeron.InvalidKey ->
-    let { init_function } = String.Map.find name !sum_map in
+    let { init_function } = DynMap.find name !sum_map in
     init_function ();
     CEphemeron.get (fst !r)
 
 let ref ?(freeze=fun x -> x) ~name init =
-  let r = pervasives_ref (CEphemeron.create init, name) in
-  declare_summary name
-    { freeze_function = (fun ~marshallable -> freeze !r);
-      unfreeze_function = ((:=) r);
-      init_function = (fun () -> r := init) };
+  let () = check_name (mangle name) in
+  let tag : 'a Dyn.tag = Dyn.create (mangle name) in
+  let r = pervasives_ref (CEphemeron.create init, tag) in
+  let () = sum_map := DynMap.add tag
+    { freeze_function = (fun ~marshallable -> freeze (get r));
+      unfreeze_function = (set r);
+      init_function = (fun () -> set r init) } !sum_map
+  in
   r
 
+let (!) = get
+let (:=) = set
+
 end
 
 let dump = Dyn.dump
-- 
cgit v1.2.3


From 675579e23be006e2d545f1f458baf7a0f6b5883a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 9 Dec 2019 18:50:47 +0100
Subject: Simplify the implementation of Summary by specifying the type of
 ML-MODULES.

No need to deploy an existential type machinery when we already know this type
in advance.
---
 library/summary.ml  | 22 ++++++++--------------
 library/summary.mli |  2 +-
 2 files changed, 9 insertions(+), 15 deletions(-)

diff --git a/library/summary.ml b/library/summary.ml
index 3ebd977d12..2afccda847 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -21,16 +21,15 @@ type 'a summary_declaration = {
 
 module DynMap = Dyn.Map(struct type 'a t = 'a summary_declaration end)
 
-let sum_mod = ref None
+type ml_modules = (string * string option) list
+
+let sum_mod : ml_modules summary_declaration option ref = ref None
 let sum_map = ref DynMap.empty
 
 let mangle id = id ^ "-SUMMARY"
 
-let ml_modules = "ML-MODULES"
-
 let declare_ml_modules_summary decl =
-  let tag = Dyn.create ml_modules in
-  sum_mod := Some (DynMap.Any (tag, decl))
+  sum_mod := Some decl
 
 let check_name sumname = match Dyn.name sumname with
 | None -> ()
@@ -52,7 +51,7 @@ module Frozen = Dyn.Map(struct type 'a t = 'a end)
 type frozen = {
   summaries : Frozen.t;
   (** Ordered list w.r.t. the first component. *)
-  ml_module : Dyn.t option;
+  ml_module : ml_modules option;
   (** Special handling of the ml_module summary. *)
 }
 
@@ -61,7 +60,7 @@ let empty_frozen = { summaries = Frozen.empty; ml_module = None }
 let freeze_summaries ~marshallable : frozen =
   let fold (DynMap.Any (tag, decl)) accu = Frozen.add tag (decl.freeze_function ~marshallable) accu in
   { summaries = DynMap.fold fold !sum_map Frozen.empty;
-    ml_module = Option.map (fun (DynMap.Any (tag, decl)) -> Dyn.Dyn (tag, decl.freeze_function ~marshallable)) !sum_mod;
+    ml_module = Option.map (fun decl -> decl.freeze_function ~marshallable) !sum_mod;
   }
 
 let warn_summary_out_of_scope =
@@ -78,13 +77,8 @@ let unfreeze_summaries ?(partial=false) { summaries; ml_module } =
   (* The unfreezing of [ml_modules_summary] has to be anticipated since it
    * may modify the content of [summaries] by loading new ML modules *)
   begin match !sum_mod with
-  | None -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".")
-  | Some (DynMap.Any (tag, decl)) ->
-    let iter (Dyn.Dyn (tag', v)) = match Dyn.eq tag tag' with
-    | None -> anomaly (str "Type mismatch in ML module summary")
-    | Some Refl -> decl.unfreeze_function v
-    in
-    Option.iter iter ml_module
+  | None -> anomaly (str "Undeclared ML-MODULES summary.")
+  | Some decl -> Option.iter decl.unfreeze_function ml_module
   end;
   (* We must be independent on the order of the map! *)
   let ufz (DynMap.Any (name, decl)) =
diff --git a/library/summary.mli b/library/summary.mli
index 3a122edf3d..f4550b38f9 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -63,7 +63,7 @@ end
     because its unfreeze may load ML code and hence add summary
     entries.  Thus is has to be recognizable, and handled properly.
    *)
-val declare_ml_modules_summary : 'a summary_declaration -> unit
+val declare_ml_modules_summary : (string * string option) list summary_declaration -> unit
 
 (** For global tables registered statically before the end of coqtop
     launch, the following empty [init_function] could be used. *)
-- 
cgit v1.2.3


From 7943acfd346466b512eca88fd32c738cdfe44299 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 9 Dec 2019 21:48:12 +0100
Subject: Type-safe implementation of libobjects.

Same justification as the change in implementation of Summary.
---
 library/libobject.ml | 97 ++++++++++++++++++++--------------------------------
 1 file changed, 38 insertions(+), 59 deletions(-)

diff --git a/library/libobject.ml b/library/libobject.ml
index a632a426fd..c9ea6bcff8 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -82,79 +82,58 @@ and objects = (Names.Id.t * t) list
 
 and substitutive_objects = MBId.t list * algebraic_objects
 
-type dynamic_object_declaration = {
-  dyn_cache_function : object_name * obj -> unit;
-  dyn_load_function : int -> object_name * obj -> unit;
-  dyn_open_function : int -> object_name * obj -> unit;
-  dyn_subst_function : Mod_subst.substitution * obj -> obj;
-  dyn_classify_function : obj -> obj substitutivity;
-  dyn_discharge_function : object_name * obj -> obj option;
-  dyn_rebuild_function : obj -> obj }
-
 let object_tag (Dyn.Dyn (t, _)) = Dyn.repr t
 
-let cache_tab =
-  (Hashtbl.create 223 : (string,dynamic_object_declaration) Hashtbl.t)
+module DynMap = Dyn.Map (struct type 'a t = 'a object_declaration end)
+
+let cache_tab = ref DynMap.empty
 
 let declare_object_full odecl =
   let na = odecl.object_name in
-  let (infun, outfun) = Dyn.Easy.make_dyn na in
-  let cacher (oname,lobj) = odecl.cache_function (oname,outfun lobj)
-  and loader i (oname,lobj) = odecl.load_function i (oname,outfun lobj)
-  and opener i (oname,lobj) = odecl.open_function i (oname,outfun lobj)
-  and substituter (sub,lobj) = infun (odecl.subst_function (sub,outfun lobj))
-  and classifier lobj = match odecl.classify_function (outfun lobj) with
-  | Dispose -> Dispose
-  | Substitute atomic_obj -> Substitute (infun atomic_obj)
-  | Keep atomic_obj -> Keep (infun atomic_obj)
-  | Anticipate (atomic_obj) -> Anticipate (infun atomic_obj)
-  and discharge (oname,lobj) =
-    Option.map infun (odecl.discharge_function (oname,outfun lobj))
-  and rebuild lobj = infun (odecl.rebuild_function (outfun lobj))
+  let tag = Dyn.create na in
+  let () = cache_tab := DynMap.add tag odecl !cache_tab in
+  let infun v = Dyn.Dyn (tag, v) in
+  let outfun v = match Dyn.Easy.prj v tag with
+  | None -> assert false
+  | Some v -> v
   in
-  Hashtbl.add cache_tab na { dyn_cache_function = cacher;
-                             dyn_load_function = loader;
-                             dyn_open_function = opener;
-                             dyn_subst_function = substituter;
-                             dyn_classify_function = classifier;
-                             dyn_discharge_function = discharge;
-                             dyn_rebuild_function = rebuild };
   (infun,outfun)
 
 let declare_object odecl = fst (declare_object_full odecl)
-let declare_object_full odecl = declare_object_full odecl
 
-(* this function describes how the cache, load, open, and export functions
-   are triggered. *)
-
-let apply_dyn_fun f lobj =
-  let tag = object_tag lobj in
-  let dodecl =
-    try Hashtbl.find cache_tab tag
-    with Not_found -> assert false
-  in
-  f dodecl
+let cache_object (sp, Dyn.Dyn (tag, v)) =
+  let decl = DynMap.find tag !cache_tab in
+  decl.cache_function (sp, v)
 
-let cache_object ((_,lobj) as node) =
-  apply_dyn_fun (fun d -> d.dyn_cache_function node) lobj
+let load_object i (sp, Dyn.Dyn (tag, v)) =
+  let decl = DynMap.find tag !cache_tab in
+  decl.load_function i (sp, v)
 
-let load_object i ((_,lobj) as node) =
-  apply_dyn_fun (fun d -> d.dyn_load_function i node) lobj
+let open_object i (sp, Dyn.Dyn (tag, v)) =
+  let decl = DynMap.find tag !cache_tab in
+  decl.open_function i (sp, v)
 
-let open_object i ((_,lobj) as node) =
-  apply_dyn_fun (fun d -> d.dyn_open_function i node) lobj
+let subst_object (subs, Dyn.Dyn (tag, v)) =
+  let decl = DynMap.find tag !cache_tab in
+  Dyn.Dyn (tag, decl.subst_function (subs, v))
 
-let subst_object ((_,lobj) as node) =
-  apply_dyn_fun (fun d -> d.dyn_subst_function node) lobj
-
-let classify_object lobj =
-  apply_dyn_fun (fun d -> d.dyn_classify_function lobj) lobj
-
-let discharge_object ((_,lobj) as node) =
-  apply_dyn_fun (fun d -> d.dyn_discharge_function node) lobj
-
-let rebuild_object lobj =
-  apply_dyn_fun (fun d -> d.dyn_rebuild_function lobj) lobj
+let classify_object (Dyn.Dyn (tag, v)) =
+  let decl = DynMap.find tag !cache_tab in
+  match decl.classify_function v with
+  | Dispose -> Dispose
+  | Substitute v -> Substitute (Dyn.Dyn (tag, v))
+  | Keep v -> Keep (Dyn.Dyn (tag, v))
+  | Anticipate v -> Anticipate (Dyn.Dyn (tag, v))
+
+let discharge_object (sp, Dyn.Dyn (tag, v)) =
+  let decl = DynMap.find tag !cache_tab in
+  match decl.discharge_function (sp, v) with
+  | None -> None
+  | Some v -> Some (Dyn.Dyn (tag, v))
+
+let rebuild_object (Dyn.Dyn (tag, v)) =
+  let decl = DynMap.find tag !cache_tab in
+  Dyn.Dyn (tag, decl.rebuild_function v)
 
 let dump = Dyn.dump
 
-- 
cgit v1.2.3