diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-09-05 16:23:09 +0200 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-09-05 16:37:00 +0200 |
commit | 6f393734e54146c4d26325aea006368380d97280 (patch) | |
tree | db447c39ec86206fe8da06692b279f22a6c1b1cc /library/summary.ml | |
parent | 3cf399dd17759cc0258295045742f1b50e376d5a (diff) |
Summary: simpler API for process-local storage
Diffstat (limited to 'library/summary.ml')
-rw-r--r-- | library/summary.ml | 25 |
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 |