[summary] Adapt STM to the new Summary API.

We need to a partial restore. I think that we could design a better
API, but further work on the toplevel state should improve it
progressively.

11 files changed, 57 insertions, 35 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 907f1b1ac..3445b744a 100644
--- a/engine/evarutil.ml
+++ b/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())
 
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 5fd4634d6..9d0b973a7 100644
--- a/engine/evarutil.mli
+++ b/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
diff --git a/engine/evd.ml b/engine/evd.ml
index 45d2a8b08..e33c851f6 100644
--- a/engine/evd.ml
+++ b/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
diff --git a/engine/evd.mli b/engine/evd.mli
index fb5a6cd16..a915dd7ad 100644
--- a/engine/evd.mli
+++ b/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
diff --git a/library/global.ml b/library/global.ml
index 03d7612a4..ce37dfecf 100644
--- a/library/global.ml
+++ b/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 ()
diff --git a/library/global.mli b/library/global.mli
index 1d68d1082..79c8525c6 100644
--- a/library/global.mli
+++ b/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
diff --git a/library/summary.ml b/library/summary.ml
index 5fe3160e1..6df17476b 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -87,7 +87,7 @@ let unfreeze_single name state =
       Pp.(seq [str "Error unfreezing summary "; str name; fnl (); CErrors.iprint e]);
     iraise e
 
-let unfreeze_summaries { summaries; ml_module } =
+let unfreeze_summaries ?(partial=false) { summaries; ml_module } =
   (* The unfreezing of [ml_modules_summary] has to be anticipated since it
    * may modify the content of [summaries] by loading new ML modules *)
   begin match !sum_mod with
@@ -98,8 +98,10 @@ let unfreeze_summaries { summaries; ml_module } =
   let ufz name decl =
     try decl.unfreeze_function String.Map.(find name summaries)
     with Not_found ->
-      Feedback.msg_warning Pp.(str "Summary was captured out of module scope for entry " ++ str name);
-      decl.init_function ()
+      if not partial then begin
+        Feedback.msg_warning Pp.(str "Summary was captured out of module scope for entry " ++ str name);
+        decl.init_function ()
+      end;
   in
   (* String.Map.iter unfreeze_single !sum_map *)
   String.Map.iter ufz !sum_map
diff --git a/library/summary.mli b/library/summary.mli
index 9fc6df6ad..09447199e 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -80,7 +80,7 @@ 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
 
 (** Typed projection of the summary. Experimental API, use with CARE *)
diff --git a/stm/stm.ml b/stm/stm.ml
index 8aa832da8..0dbe168b7 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -158,9 +158,10 @@ let mkTransCmd cast cids ceff cqueue =
   Cmd { ctac = false; cast; cblock = None; cqueue; cids; ceff }
 
 (* Parts of the system state that are morally part of the proof state *)
-let summary_pstate = [ Evarutil.meta_counter_summary_name;
-                       Evd.evar_counter_summary_name;
-                       "program-tcc-table" ]
+let summary_pstate = Evarutil.meta_counter_summary_tag,
+                     Evd.evar_counter_summary_tag,
+                     Obligations.program_tcc_summary_tag
+
 type cached_state =
   | Empty
   | Error of Exninfo.iexn
@@ -762,15 +763,21 @@ end = struct (* {{{ *)
   let fix_exn_ref = ref (fun x -> x)
 
   type proof_part =
-    Proof_global.t * Summary.frozen_bits (* only meta counters *)
+    Proof_global.t *
+    int *                                   (* Evarutil.meta_counter_summary_tag *)
+    int *                                   (* Evd.evar_counter_summary_tag *)
+    Obligations.program_info Names.Id.Map.t (* Obligations.program_tcc_summary_tag *)
 
   type partial_state =
     [ `Full of Vernacstate.t
     | `ProofOnly of Stateid.t * proof_part ]
 
   let proof_part_of_frozen { Vernacstate.proof; system } =
+    let st = States.summary_of_state system in
     proof,
-    Summary.project_summary (States.summary_of_state system) summary_pstate
+    Summary.project_from_summary st Util.(pi1 summary_pstate),
+    Summary.project_from_summary st Util.(pi2 summary_pstate),
+    Summary.project_from_summary st Util.(pi3 summary_pstate)
 
   let freeze marshallable id =
     VCS.set_state id (Valid (Vernacstate.freeze_interp_state marshallable))
@@ -830,16 +837,21 @@ end = struct (* {{{ *)
             else s
            with VCS.Expired -> s in
          VCS.set_state id (Valid s)
-    | `ProofOnly(ontop,(pstate,counters)) ->
+    | `ProofOnly(ontop,(pstate,c1,c2,c3)) ->
          if is_cached_and_valid ontop then
            let s = get_cached ontop in
            let s = { s with proof =
              Proof_global.copy_terminators ~src:s.proof ~tgt:pstate } in
            let s = { s with system =
              States.replace_summary s.system
-               (Summary.surgery_summary
-                 (States.summary_of_state s.system)
-               counters) } in
+               begin
+                 let st = States.summary_of_state s.system in
+                 let st = Summary.modify_summary st Util.(pi1 summary_pstate) c1 in
+                 let st = Summary.modify_summary st Util.(pi2 summary_pstate) c2 in
+                 let st = Summary.modify_summary st Util.(pi3 summary_pstate) c3 in
+                 st
+               end
+                } in
            VCS.set_state id (Valid s)
     with VCS.Expired -> ()
 
@@ -854,10 +866,10 @@ end = struct (* {{{ *)
 
   let same_env { Vernacstate.system = s1 } { Vernacstate.system = s2 } =
     let s1 = States.summary_of_state s1 in
-    let e1 = Summary.project_summary s1 [Global.global_env_summary_name] in
+    let e1 = Summary.project_from_summary s1 Global.global_env_summary_tag in
     let s2 = States.summary_of_state s2 in
-    let e2 = Summary.project_summary s2 [Global.global_env_summary_name] in
-    Summary.pointer_equal e1 e2
+    let e2 = Summary.project_from_summary s2 Global.global_env_summary_tag in
+    e1 == e2
 
   let define ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true)
         f id
@@ -2040,8 +2052,6 @@ and Reach : sig
 
 end = struct (* {{{ *)
 
-let pstate = summary_pstate
-
 let async_policy () =
   let open Flags in
   if is_universe_polymorphism () then false
@@ -2254,10 +2264,14 @@ let known_state ?(redefine_qed=false) ~cache id =
   (* ugly functions to process nested lemmas, i.e. hard to reproduce
    * side effects *)
   let cherry_pick_non_pstate () =
-    Summary.freeze_summary ~marshallable:`No ~complement:true pstate,
-    Lib.freeze ~marshallable:`No in
+    let st = Summary.freeze_summaries ~marshallable:`No in
+    let st = Summary.remove_from_summary st Util.(pi1 summary_pstate) in
+    let st = Summary.remove_from_summary st Util.(pi2 summary_pstate) in
+    let st = Summary.remove_from_summary st Util.(pi3 summary_pstate) in
+    st, Lib.freeze ~marshallable:`No in
+
   let inject_non_pstate (s,l) =
-    Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env ()
+    Summary.unfreeze_summaries ~partial:true s; Lib.unfreeze l; update_global_env ()
   in
   let rec pure_cherry_pick_non_pstate safe_id id =
     stm_purify (fun id ->
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 24d664951..bdae27e5b 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -429,8 +429,8 @@ let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m)
 
 let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m []
 
-let from_prg : program_info ProgMap.t ref =
-  Summary.ref ProgMap.empty ~name:"program-tcc-table"
+let from_prg, program_tcc_summary_tag =
+  Summary.ref_tag ProgMap.empty ~name:"program-tcc-table"
 
 let close sec =
   if not (ProgMap.is_empty !from_prg) then
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 0602e52e9..bdc97d48c 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -104,3 +104,6 @@ exception NoObligations of Names.Id.t option
 val explain_no_obligations : Names.Id.t option -> Pp.t
 
 val set_program_mode : bool -> unit
+
+type program_info
+val program_tcc_summary_tag : program_info Id.Map.t Summary.Dyn.tag