aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-07 17:46:53 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-07 17:46:53 +0200
commit79e7a0de25bcb2f10a7f3d1960a8f16eefdbb5a6 (patch)
tree92ce430c64b7bea374b926d81acc5433d39fdcbb /library
parentf79f2b32da8e5e443428d4f642216ddfb404857c (diff)
parenta18fb93587ccbe32a2edfad38d2e9095f6c8e901 (diff)
Merge branch 'v8.6'
Diffstat (limited to 'library')
-rw-r--r--library/goptions.ml4
-rw-r--r--library/summary.ml25
-rw-r--r--library/summary.mli11
3 files changed, 38 insertions, 2 deletions
diff --git a/library/goptions.ml b/library/goptions.ml
index 0459417fb..1cf25987b 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -365,8 +365,8 @@ let set_string_option_value = set_string_option_value_gen None
let msg_option_value (name,v) =
match v with
- | BoolValue true -> str "true"
- | BoolValue false -> str "false"
+ | BoolValue true -> str "on"
+ | BoolValue false -> str "off"
| IntValue (Some n) -> int n
| IntValue None -> str "undefined"
| StringValue s -> str s
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
diff --git a/library/summary.mli b/library/summary.mli
index 27889cab2..1b57613cb 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -42,6 +42,17 @@ val declare_summary : string -> 'a summary_declaration -> unit
val ref : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref
+(* As [ref] but the value is local to a process, i.e. not sent to, say, proof
+ * workers. It is useful to implement a local cache for example. *)
+module Local : sig
+
+ type 'a local_ref
+ val ref : ?freeze:('a -> 'a) -> name:string -> 'a -> 'a local_ref
+ val (:=) : 'a local_ref -> 'a -> unit
+ val (!) : 'a local_ref -> 'a
+
+end
+
(** Special name for the summary of ML modules. This summary entry is
special because its unfreeze may load ML code and hence add summary
entries. Thus is has to be recognizable, and handled appropriately *)