From 6f393734e54146c4d26325aea006368380d97280 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 5 Sep 2016 16:23:09 +0200 Subject: Summary: simpler API for process-local storage --- library/summary.mli | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'library/summary.mli') 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 *) -- cgit v1.2.3