summaryrefslogtreecommitdiff
path: root/library/summary.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/summary.ml')
-rw-r--r--library/summary.ml50
1 files changed, 43 insertions, 7 deletions
diff --git a/library/summary.ml b/library/summary.ml
index 46c52acc..6efa07f3 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -7,9 +7,11 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
+module Dyn = Dyn.Make(struct end)
+
type marshallable = [ `Yes | `No | `Shallow ]
type 'a summary_declaration = {
freeze_function : marshallable -> 'a;
@@ -21,7 +23,7 @@ let summaries = ref Int.Map.empty
let mangle id = id ^ "-SUMMARY"
let internal_declare_summary hash sumname sdecl =
- let (infun, outfun) = Dyn.create (mangle sumname) in
+ let (infun, outfun) = Dyn.Easy.make_dyn (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
@@ -103,10 +105,10 @@ let unfreeze_summaries fs =
in
let fold id decl state =
try fold id decl state
- with e when Errors.noncritical e ->
- let e = Errors.push e in
+ with e when CErrors.noncritical e ->
+ let e = CErrors.push e in
Printf.eprintf "Error unfrezing summay %s\n%s\n%!"
- (name_of_summary id) (Pp.string_of_ppcmds (Errors.iprint e));
+ (name_of_summary id) (Pp.string_of_ppcmds (CErrors.iprint e));
iraise e
in
(** We rely on the order of the frozen list, and the order of folding *)
@@ -147,7 +149,7 @@ let unfreeze_summary datas =
let (name, summary) = Int.Map.find id !summaries in
try summary.unfreeze_function data
with e ->
- let e = Errors.push e in
+ let e = CErrors.push e in
prerr_endline ("Exception unfreezing " ^ name);
iraise e)
datas
@@ -164,8 +166,15 @@ let project_summary { summaries; ml_module } ?(complement=false) ids =
List.filter (fun (id, _) -> List.mem id ids) summaries
let pointer_equal l1 l2 =
+ let ptr_equal d1 d2 =
+ let Dyn.Dyn (t1, x1) = d1 in
+ let Dyn.Dyn (t2, x2) = d2 in
+ match Dyn.eq t1 t2 with
+ | None -> false
+ | Some Refl -> x1 == x2
+ in
CList.for_all2eq
- (fun (id1,v1) (id2,v2) -> id1 = id2 && Dyn.pointer_equal v1 v2) l1 l2
+ (fun (id1,v1) (id2,v2) -> id1 = id2 && ptr_equal v1 v2) l1 l2
(** All-in-one reference declaration + registration *)
@@ -176,3 +185,30 @@ let ref ?(freeze=fun _ r -> r) ~name x =
unfreeze_function = ((:=) r);
init_function = (fun () -> r := x) };
r
+
+module Local = struct
+
+type 'a local_ref = ('a CEphemeron.key * string) ref
+
+let (:=) r v = r := (CEphemeron.create v, snd !r)
+
+let (!) r =
+ let key, name = !r in
+ try CEphemeron.get key
+ with CEphemeron.InvalidKey ->
+ let _, { init_function } =
+ Int.Map.find (String.hash (mangle name)) !summaries 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 _ -> freeze !r);
+ unfreeze_function = ((:=) r);
+ init_function = (fun () -> r := init) };
+ r
+
+end
+
+let dump = Dyn.dump