Using hashes in Summary, like the previous commit did with Dyn.

1 files changed, 55 insertions, 48 deletions

diff --git a/library/summary.ml b/library/summary.ml
index dcc6cce90..d546b3ede 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -16,11 +16,12 @@ type 'a summary_declaration = {
   unfreeze_function : 'a -> unit;
   init_function : unit -> unit }
 
-let summaries =
-  (Hashtbl.create 17 : (string, Dyn.t summary_declaration) Hashtbl.t)
+let summaries = ref Int.Map.empty
 
-let internal_declare_summary sumname sdecl =
-  let (infun,outfun) = Dyn.create sumname in
+let mangle id = id ^ "-SUMMARY"
+
+let internal_declare_summary hash sumname sdecl =
+  let (infun, outfun) = Dyn.create (mangle sumname) in
   let dyn_freeze b = infun (sdecl.freeze_function b)
   and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum)
   and dyn_init = sdecl.init_function in
@@ -29,56 +30,60 @@ let internal_declare_summary sumname sdecl =
     unfreeze_function = dyn_unfreeze;
     init_function = dyn_init }
   in
-  Hashtbl.add summaries sumname ddecl
-
-let mangle id = id ^ "-SUMMARY"
+  summaries := Int.Map.add hash (sumname, ddecl) !summaries
 
-let all_declared_summaries = ref CString.Set.empty
+let all_declared_summaries = ref Int.Set.empty
 
 let declare_summary sumname decl =
-  if CString.Set.mem sumname !all_declared_summaries then
+  let hash = String.hash sumname in
+  let () = if Int.Map.mem hash !summaries then
+    let (name, _) = Int.Map.find hash !summaries in
     anomaly ~label:"Summary.declare_summary"
-      (str "Cannot declare a summary twice: " ++ str sumname);
-  all_declared_summaries := CString.Set.add sumname !all_declared_summaries;
-  internal_declare_summary (mangle sumname) decl;
-
-type frozen = Dyn.t String.Map.t
-
-let freeze_summaries ~marshallable =
-  let m = ref String.Map.empty in
-  Hashtbl.iter
-    (fun id decl -> 
-       (* to debug missing Lazy.force 
-       if marshallable <> `No then begin
-         prerr_endline ("begin marshalling " ^ id);
-         ignore(Marshal.to_string (decl.freeze_function marshallable) []);
-         prerr_endline ("end marshalling " ^ id);
-       end;
-        /debug *)
-       m := String.Map.add id (decl.freeze_function marshallable) !m)
-    summaries;
+      (str "Colliding summary names: " ++ str sumname ++ str " vs. " ++ str name)
+  in
+  all_declared_summaries := Int.Set.add hash !all_declared_summaries;
+  internal_declare_summary hash sumname decl
+
+type frozen = Dyn.t Int.Map.t
+
+let freeze_summaries ~marshallable : frozen =
+  let m = ref Int.Map.empty in
+  let iter id (_, decl) =
+    (* to debug missing Lazy.force
+    if marshallable <> `No then begin
+      prerr_endline ("begin marshalling " ^ id);
+      ignore(Marshal.to_string (decl.freeze_function marshallable) []);
+      prerr_endline ("end marshalling " ^ id);
+    end;
+    /debug *)
+    m := Int.Map.add id (decl.freeze_function marshallable) !m
+  in
+  let () = Int.Map.iter iter !summaries in
   !m
 
 let ml_modules = "ML-MODULES"
-let ml_modules_summary = mangle ml_modules
+let ml_modules_summary = String.hash ml_modules
 
 let unfreeze_summaries fs =
   (* The unfreezing of [ml_modules_summary] has to be anticipated since it
    * may modify the content of [summaries] ny loading new ML modules *)
-  (try
-    (Hashtbl.find summaries ml_modules_summary).unfreeze_function 
-      (String.Map.find ml_modules_summary fs)
-  with Not_found -> anomaly (str"Undeclared summary "++str ml_modules_summary));
-  Hashtbl.iter
-    (fun id decl ->
-       if String.equal id ml_modules_summary then () (* already unfreezed *)
+  let () =
+    try
+      let (_, decl) = Int.Map.find ml_modules_summary !summaries in
+      let state = Int.Map.find ml_modules_summary fs in
+      decl.unfreeze_function state
+    with Not_found -> anomaly (str"Undeclared summary "++str ml_modules)
+  in
+  Int.Map.iter
+    (fun id (_, decl) ->
+       if Int.equal id ml_modules_summary then () (* already unfreezed *)
        else
-         try decl.unfreeze_function (String.Map.find id fs)
+         try decl.unfreeze_function (Int.Map.find id fs)
          with Not_found -> decl.init_function())
-    summaries
+    !summaries
 
 let init_summaries () =
-  Hashtbl.iter (fun _ decl -> decl.init_function()) summaries
+  Int.Map.iter (fun _ (_, decl) -> decl.init_function ()) !summaries
 
 (** For global tables registered statically before the end of coqtop
     launch, the following empty [init_function] could be used. *)
@@ -87,30 +92,32 @@ let nop () = ()
 
 (** Selective freeze *)
 
-type frozen_bits = (string * Dyn.t) list
+type frozen_bits = (int * Dyn.t) list
 
 let freeze_summary ~marshallable ?(complement=false) ids =
   let ids =
-    if not complement then ids
+    if not complement then List.map String.hash ids
     else
-      CString.Set.elements
-        (CString.Set.diff !all_declared_summaries
-          (List.fold_right CString.Set.add ids CString.Set.empty))
+      let fold accu id =
+        let id = String.hash id in
+        Int.Set.remove id accu
+      in
+      let ids = List.fold_left fold !all_declared_summaries ids in
+      Int.Set.elements ids
   in
     List.map (fun id ->
-      let id = mangle id in
-      let summary = Hashtbl.find summaries id in
+      let (_, summary) = Int.Map.find id !summaries in
       id, summary.freeze_function marshallable)
     ids
 
 let unfreeze_summary datas =
   List.iter
     (fun (id, data) ->
-      let summary = Hashtbl.find summaries id in
+      let (name, summary) = Int.Map.find id !summaries in
       try summary.unfreeze_function data
       with e ->
         let e = Errors.push e in
-        prerr_endline ("Exception unfreezing " ^ id);
+        prerr_endline ("Exception unfreezing " ^ name);
         raise e)
   datas