Imported Upstream version 8.6upstream/8.6

1 files changed, 15 insertions, 0 deletions

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