Merge PR coq#6275: [summary] Allow typed projections from global state.

engine/evarutil.ml

@@ -199,9 +199,10 @@ let whd_head_evar sigma c =
 let meta_counter_summary_name = "meta counter"
 
 (* Generator of metavariables *)
-let new_meta =
-  let meta_ctr = Summary.ref 0 ~name:meta_counter_summary_name in
-  fun () -> incr meta_ctr; !meta_ctr
+let meta_ctr, meta_counter_summary_tag =
+  Summary.ref_tag 0 ~name:meta_counter_summary_name
+
+let new_meta () = incr meta_ctr; !meta_ctr
 
 let mk_new_meta () = EConstr.mkMeta(new_meta())
 

engine/evarutil.mli

@@ -236,7 +236,7 @@ val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b ->
 val subterm_source : Evar.t -> Evar_kinds.t Loc.located ->
   Evar_kinds.t Loc.located
 
-val meta_counter_summary_name : string
+val meta_counter_summary_tag : int Summary.Dyn.tag
 
 (** Deprecated *)
 type type_constraint = types option

engine/evd.ml

@@ -466,9 +466,8 @@ let add d e i = add_with_name d e i
 let evar_counter_summary_name = "evar counter"
 
 (* Generator of existential names *)
-let new_untyped_evar =
-  let evar_ctr = Summary.ref 0 ~name:evar_counter_summary_name in
-  fun () -> incr evar_ctr; Evar.unsafe_of_int !evar_ctr
+let evar_ctr, evar_counter_summary_tag = Summary.ref_tag 0 ~name:evar_counter_summary_name
+let new_untyped_evar () = incr evar_ctr; Evar.unsafe_of_int !evar_ctr
 
 let new_evar evd ?name evi =
   let evk = new_untyped_evar () in

engine/evd.mli

@@ -613,7 +613,7 @@ type unsolvability_explanation = SeveralInstancesFound of int
 
 (* This stuff is internal and should not be used. Currently a hack in
    the STM relies on it. *)
-val evar_counter_summary_name : string
+val evar_counter_summary_tag : int Summary.Dyn.tag
 
 (** {5 Deprecated functions} *)
 val create_evar_defs : evar_map -> evar_map

lib/dyn.ml

@@ -55,6 +55,8 @@ sig
   include PreS
 
   module Easy : sig
+
+    val make_dyn_tag : string -> ('a -> t) * (t -> 'a) * 'a tag
     val make_dyn : string -> ('a -> t) * (t -> 'a)
     val inj : 'a -> 'a tag -> t
     val prj : t -> 'a tag -> 'a option
@@ -129,18 +131,22 @@ end
 include Self
 
 module Easy = struct
+
 (* now tags are opaque, we can do the trick *)
-let make_dyn (s : string) =
+let make_dyn_tag (s : string) =
  (fun (type a) (tag : a tag) ->
   let infun : (a -> t) = fun x -> Dyn (tag, x) in
   let outfun : (t -> a) = fun (Dyn (t, x)) ->
     match eq tag t with
     | None -> assert false
     | Some CSig.Refl -> x
   in
-  (infun, outfun))
+  infun, outfun, tag)
  (create s)
 
+let make_dyn (s : string) =
+  let inf, outf, _ = make_dyn_tag s in inf, outf
+
 let inj x tag = Dyn(tag,x)
 let prj : type a. t -> a tag -> a option =
     fun (Dyn(tag',x)) tag ->

lib/dyn.mli

@@ -53,6 +53,7 @@ val dump : unit -> (int * string) list
 module Easy : sig
 
   (* To create a dynamic type on the fly *)
+  val make_dyn_tag : string -> ('a -> t) * (t -> 'a) * 'a tag
   val make_dyn : string -> ('a -> t) * (t -> 'a)
 
   (* For types declared with the [create] function above *)

library/global.ml

@@ -20,6 +20,7 @@ module GlobalSafeEnv : sig
   val set_safe_env : Safe_typing.safe_environment -> unit
   val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit
   val is_joined_environment : unit -> bool
+  val global_env_summary_tag : Safe_typing.safe_environment Summary.Dyn.tag
 
 end = struct
 
@@ -30,9 +31,9 @@ let join_safe_environment ?except () =
 
 let is_joined_environment () =
   Safe_typing.is_joined_environment !global_env
-  
-let () =
-  Summary.declare_summary global_env_summary_name
+
+let global_env_summary_tag =
+  Summary.declare_summary_tag global_env_summary_name
     { Summary.freeze_function = (function
         | `Yes -> join_safe_environment (); !global_env
         | `No -> !global_env
@@ -51,6 +52,8 @@ let set_safe_env e = global_env := e
 
 end
 
+let global_env_summary_tag = GlobalSafeEnv.global_env_summary_tag
+
 let safe_env = GlobalSafeEnv.safe_env
 let join_safe_environment ?except () =
   GlobalSafeEnv.join_safe_environment ?except ()

library/global.mli

@@ -159,4 +159,4 @@ val current_dirpath : unit -> DirPath.t
 
 val with_global : (Environ.env -> DirPath.t -> 'a Univ.in_universe_context_set) -> 'a
 
-val global_env_summary_name : string
+val global_env_summary_tag : Safe_typing.safe_environment Summary.Dyn.tag