aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/summary.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-09-05 16:23:09 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-09-05 16:37:00 +0200
commit6f393734e54146c4d26325aea006368380d97280 (patch)
treedb447c39ec86206fe8da06692b279f22a6c1b1cc /library/summary.ml
parent3cf399dd17759cc0258295045742f1b50e376d5a (diff)
Summary: simpler API for process-local storage
Diffstat (limited to 'library/summary.ml')
-rw-r--r--library/summary.ml25
1 files changed, 25 insertions, 0 deletions
diff --git a/library/summary.ml b/library/summary.ml
index 4fef06438..6efa07f38 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -186,4 +186,29 @@ let ref ?(freeze=fun _ r -> r) ~name x =
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