From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 library/summary.mli | 53 ++++++++++++++++++++++++++++++++++++++++-------------
 1 file changed, 40 insertions(+), 13 deletions(-)

(limited to 'library/summary.mli')

diff --git a/library/summary.mli b/library/summary.mli
index 1b57613c..ed6c26b1 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (** This module registers the declaration of global tables, which will be kept
@@ -14,6 +16,8 @@ type marshallable =
   | `No        (* Full data will be store in memory, e.g. for Undo            *)
   | `Shallow ] (* Only part of the data will be marshalled to a slave process *)
 
+(** Types of global Coq states. The ['a] type should be pure and marshallable by
+    the standard OCaml marshalling function. *)
 type 'a summary_declaration = {
   (** freeze_function [true] is for marshalling to disk. 
    *  e.g. lazy must be forced *)
@@ -34,6 +38,12 @@ type 'a summary_declaration = {
 
 val declare_summary : string -> 'a summary_declaration -> unit
 
+(** We provide safe projection from the summary to the types stored in
+   it.*)
+module Dyn : Dyn.S
+
+val declare_summary_tag : string -> 'a summary_declaration -> 'a Dyn.tag
+
 (** All-in-one reference declaration + summary registration.
     It behaves just as OCaml's standard [ref] function, except
     that a [declare_summary] is done, with [name] as string.
@@ -41,6 +51,7 @@ val declare_summary : string -> 'a summary_declaration -> unit
     The [freeze_function] can be overridden *)
 
 val ref : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref
+val ref_tag : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref * 'a Dyn.tag
 
 (* 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. *)
@@ -53,10 +64,11 @@ module Local : sig
 
 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 *)
-val ml_modules : string
+(** Special summary for 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 properly.
+   *)
+val declare_ml_modules_summary : 'a summary_declaration -> unit
 
 (** For global tables registered statically before the end of coqtop
     launch, the following empty [init_function] could be used. *)
@@ -70,19 +82,34 @@ type frozen
 
 val empty_frozen : frozen
 val freeze_summaries : marshallable:marshallable -> frozen
-val unfreeze_summaries : frozen -> unit
+val unfreeze_summaries : ?partial:bool -> frozen -> unit
 val init_summaries : unit -> unit
 
-(** The type [frozen_bits] is a snapshot of some of the registered tables *)
+(** Typed projection of the summary. Experimental API, use with CARE *)
+
+val modify_summary : frozen -> 'a Dyn.tag -> 'a -> frozen
+val project_from_summary : frozen -> 'a Dyn.tag -> 'a
+val remove_from_summary : frozen -> 'a Dyn.tag -> frozen
+
+(** The type [frozen_bits] is a snapshot of some of the registered
+    tables. It is DEPRECATED in favor of the typed projection
+    version. *)
+
 type frozen_bits
+[@@ocaml.deprecated "Please use the typed version of summary projection"]
 
-val freeze_summary :
-  marshallable:marshallable -> ?complement:bool -> string list -> frozen_bits
+[@@@ocaml.warning "-3"]
+val freeze_summary : marshallable:marshallable -> ?complement:bool -> string list -> frozen_bits
+[@@ocaml.deprecated "Please use the typed version of summary projection"]
 val unfreeze_summary : frozen_bits -> unit
+[@@ocaml.deprecated "Please use the typed version of summary projection"]
 val surgery_summary : frozen -> frozen_bits -> frozen
+[@@ocaml.deprecated "Please use the typed version of summary projection"]
 val project_summary : frozen -> ?complement:bool -> string list -> frozen_bits
+[@@ocaml.deprecated "Please use the typed version of summary projection"]
 val pointer_equal : frozen_bits -> frozen_bits -> bool
+[@@ocaml.deprecated "Please use the typed version of summary projection"]
+[@@@ocaml.warning "+3"]
 
 (** {6 Debug} *)
-
 val dump : unit -> (int * string) list
-- 
cgit v1.2.3