From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- library/summary.mli | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'library/summary.mli') diff --git a/library/summary.mli b/library/summary.mli index c24a0b4b..1b57613c 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 *) @@ -71,3 +82,7 @@ val unfreeze_summary : frozen_bits -> unit val surgery_summary : frozen -> frozen_bits -> frozen val project_summary : frozen -> ?complement:bool -> string list -> frozen_bits val pointer_equal : frozen_bits -> frozen_bits -> bool + +(** {6 Debug} *) + +val dump : unit -> (int * string) list -- cgit v1.2.3