[summary] Allow typed projections from global state + rework of internals.

In the transition towards a less global state handling we have the
necessity of mix imperative setting [notably for the modules/section
code] and functional handling of state [notably in the STM].

In that scenario, it is very convenient to have typed access to the
Coq's `summary`. Thus, I reify the API to support typed access to the
`summary`, and implement such access in a couple of convenient places.

We also update some internal datatypes to simplify the `frozen` data
type. We also remove the use of hashes as it doesn't really make
things faster, and most operations are now over `Maps` anyways.

I believe this goes in line with recent work by @ppedrot.

We also deprecate the non-typed accessors, which were only supposed to
be used in the STM, which is now ported to the finer primitives.

1 files changed, 31 insertions, 8 deletions

diff --git a/library/summary.mli b/library/summary.mli
index d093d95f2..9fc6df6ad 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -36,6 +36,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.
@@ -43,6 +49,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. *)
@@ -55,10 +62,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. *)
@@ -75,16 +83,31 @@ val freeze_summaries : marshallable:marshallable -> frozen
 val unfreeze_summaries : 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