From a9f32885991263cf17093c6959732a339d473b45 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 21 Nov 2013 18:49:33 +0100 Subject: Using hashes in Summary, like the previous commit did with Dyn. --- library/summary.ml | 103 ++++++++++++++++++++++++++++------------------------- 1 file changed, 55 insertions(+), 48 deletions(-) (limited to 'library') 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 -- cgit v1.2.3