Merge PR #11264: Type safe summary & libobject implementation

Reviewed-by: ejgallego

3 files changed, 88 insertions, 116 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
 
diff --git a/library/summary.ml b/library/summary.ml
index d3ae42694a..2afccda847 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -19,57 +19,47 @@ type 'a summary_declaration = {
   unfreeze_function : 'a -> unit;
   init_function : unit -> unit }
 
-let sum_mod = ref None
-let sum_map = ref String.Map.empty
+module DynMap = Dyn.Map(struct type 'a t = 'a summary_declaration end)
+
+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 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
+  sum_mod := Some 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;
+  ml_module : ml_modules 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;
+  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 decl -> decl.freeze_function ~marshallable) !sum_mod;
   }
 
@@ -87,23 +77,23 @@ 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 decl -> Option.iter (fun state -> decl.unfreeze_function state) 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 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 +102,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 +127,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
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. *)