Merge PR #12620: [state] Consolidate state handling into Vernacstate

Reviewed-by: SkySkimmer
Reviewed-by: gares

10 files changed, 158 insertions, 109 deletions

diff --git a/vernac/library.ml b/vernac/library.ml
index c30331b221..e580927bfd 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -514,12 +514,3 @@ let get_used_load_paths () =
        String.Set.empty !libraries_loaded_list)
 
 let _ = Nativelib.get_load_paths := get_used_load_paths
-
-(* These commands may not be very safe due to ML-side plugin loading
-   etc... use at your own risk *)
-let extern_state s =
-  System.extern_state Coq_config.state_magic_number s (States.freeze ~marshallable:true)
-
-let intern_state s =
-  States.unfreeze (System.with_magic_number_check (System.intern_state Coq_config.state_magic_number) s);
-  overwrite_library_filenames s
diff --git a/vernac/library.mli b/vernac/library.mli
index 633d266821..d0e9f84691 100644
--- a/vernac/library.mli
+++ b/vernac/library.mli
@@ -76,7 +76,3 @@ val native_name_from_filename : string -> string
 
 (** {6 Opaque accessors} *)
 val indirect_accessor : Opaqueproof.indirect_accessor
-
-(** Low-level state overwriting, not very safe *)
-val intern_state : string -> unit
-val extern_state : string -> unit
diff --git a/vernac/printmod.ml b/vernac/printmod.ml
index 219e445c56..fdf7f6c74a 100644
--- a/vernac/printmod.ml
+++ b/vernac/printmod.ml
@@ -406,11 +406,11 @@ let rec printable_body dir =
     state after the printing *)
 
 let print_expression' is_type extent env mp me =
-  States.with_state_protection
+  Vernacstate.System.protect
     (fun e -> print_expression is_type extent env mp [] e) me
 
 let print_signature' is_type extent env mp me =
-  States.with_state_protection
+  Vernacstate.System.protect
     (fun e -> print_signature is_type extent env mp [] e) me
 
 let unsafe_print_module extent env mp with_body mb =
diff --git a/vernac/record.ml b/vernac/record.ml
index 9d99036273..3468f5fc36 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -710,7 +710,7 @@ let definition_structure udecl kind ~template ~cumulative ~poly finite records =
   let () = check_priorities kind records in
   let ps, data = extract_record_data records in
   let ubinders, univs, auto_template, params, implpars, data =
-    States.with_state_protection (fun () ->
+    Vernacstate.System.protect (fun () ->
       typecheck_params_and_fields (kind = Class true) poly udecl ps data) () in
   let template = template, auto_template in
   match kind with
diff --git a/vernac/states.ml b/vernac/states.ml
deleted file mode 100644
index b6904263df..0000000000
--- a/vernac/states.ml
+++ /dev/null
@@ -1,33 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    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)         *)
-(************************************************************************)
-
-type state = Lib.frozen * Summary.frozen
-
-let lib_of_state = fst
-let summary_of_state = snd
-let replace_summary (lib,_) st = lib, st
-let replace_lib (_,st) lib = lib, st
-
-let freeze ~marshallable =
-  (Lib.freeze (), Summary.freeze_summaries ~marshallable)
-
-let unfreeze (fl,fs) =
-  Lib.unfreeze fl;
-  Summary.unfreeze_summaries fs
-
-(* Rollback. *)
-
-let with_state_protection f x =
-  let st = freeze ~marshallable:false in
-  try
-    let a = f x in unfreeze st; a
-  with reraise ->
-    let reraise = Exninfo.capture reraise in
-    (unfreeze st; Exninfo.iraise reraise)
diff --git a/vernac/states.mli b/vernac/states.mli
deleted file mode 100644
index 51db83ca03..0000000000
--- a/vernac/states.mli
+++ /dev/null
@@ -1,32 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    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)         *)
-(************************************************************************)
-
-(** {6 States of the system} *)
-
-(** In that module, we provide functions to get
-  and set the state of the whole system. Internally, it is done by
-  freezing the states of both [Lib] and [Summary]. We provide functions
-  to write and restore state to and from a given file. *)
-
-type state
-val freeze : marshallable:bool -> state
-val unfreeze : state -> unit
-
-val summary_of_state : state -> Summary.frozen
-val lib_of_state : state -> Lib.frozen
-val replace_summary : state -> Summary.frozen -> state
-val replace_lib : state -> Lib.frozen -> state
-
-(** {6 Rollback } *)
-
-(** [with_state_protection f x] applies [f] to [x] and restores the
-  state of the whole system as it was before applying [f] *)
-
-val with_state_protection : ('a -> 'b) -> 'a -> 'b
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index f357a04668..994592a88a 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -1,9 +1,6 @@
 Vernacexpr
 Attributes
 Pvernac
-States
-Declaremods
-Printmod
 G_vernac
 G_proofs
 Vernacprop
@@ -21,6 +18,7 @@ Declare
 ComHints
 Canonical
 RecLemmas
+Declaremods
 Library
 ComCoercion
 Auto_ind_decl
@@ -32,10 +30,12 @@ ComAssumption
 DeclareInd
 Search
 ComSearch
-Prettyp
 ComInductive
 ComFixpoint
 ComProgramFixpoint
+Vernacstate
+Printmod
+Prettyp
 Record
 Assumptions
 Mltop
@@ -43,5 +43,4 @@ Topfmt
 Loadpath
 ComArguments
 Vernacentries
-Vernacstate
 Vernacinterp
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index f5ef5ee86f..65af66435b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1269,11 +1269,11 @@ let vernac_chdir = function
 
 let vernac_write_state file =
   let file = CUnix.make_suffix file ".coq" in
-  Library.extern_state file
+  Vernacstate.System.dump file
 
 let vernac_restore_state file =
   let file = Loadpath.locate_file (CUnix.make_suffix file ".coq") in
-  Library.intern_state file
+  Vernacstate.System.load file
 
 (************)
 (* Commands *)
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 17c89897fe..073ef1c2d7 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -10,7 +10,7 @@
 
 module Parser = struct
 
-  type state = Pcoq.frozen_t
+  type t = Pcoq.frozen_t
 
   let init () = Pcoq.freeze ~marshallable:false
 
@@ -24,6 +24,58 @@ module Parser = struct
 
 end
 
+module System : sig
+  type t
+  val protect : ('a -> 'b) -> 'a -> 'b
+  val freeze : marshallable:bool -> t
+  val unfreeze : t -> unit
+
+  val dump : string -> unit
+  val load : string -> unit
+
+  module Stm : sig
+    val make_shallow : t -> t
+    val lib : t -> Lib.frozen
+    val summary : t -> Summary.frozen
+    val replace_summary : t -> Summary.frozen -> t
+  end
+end = struct
+  type t = Lib.frozen * Summary.frozen
+
+  let freeze ~marshallable =
+    (Lib.freeze (), Summary.freeze_summaries ~marshallable)
+
+  let unfreeze (fl,fs) =
+    Lib.unfreeze fl;
+    Summary.unfreeze_summaries fs
+
+  let protect f x =
+    let st = freeze ~marshallable:false in
+    try
+      let a = f x in unfreeze st; a
+    with reraise ->
+      let reraise = Exninfo.capture reraise in
+      (unfreeze st; Exninfo.iraise reraise)
+
+  (* These commands may not be very safe due to ML-side plugin loading
+     etc... use at your own risk *)
+  (* XXX: EJGA: this is ignoring parsing state, it works for now? *)
+  let dump s =
+    System.extern_state Coq_config.state_magic_number s (freeze ~marshallable:true)
+
+  let load s =
+    unfreeze (System.with_magic_number_check (System.intern_state Coq_config.state_magic_number) s);
+    Library.overwrite_library_filenames s
+
+  (* STM-specific state manipulations *)
+  module Stm = struct
+    let make_shallow (lib, summary) = Lib.drop_objects lib, summary
+    let lib = fst
+    let summary = snd
+    let replace_summary (lib,_) summary = (lib,summary)
+  end
+end
+
 module LemmaStack = struct
 
   type t = Declare.Proof.t * Declare.Proof.t list
@@ -58,8 +110,8 @@ module LemmaStack = struct
 end
 
 type t = {
-  parsing : Parser.state;
-  system  : States.state;          (* summary + libstack *)
+  parsing : Parser.t;
+  system  : System.t;              (* summary + libstack *)
   lemmas  : LemmaStack.t option;   (* proofs of lemmas currently opened *)
   shallow : bool                   (* is the state trimmed down (libstack) *)
 }
@@ -84,26 +136,19 @@ let do_if_not_cached rf f v =
     ()
 
 let freeze_interp_state ~marshallable =
-  { system = update_cache s_cache (States.freeze ~marshallable);
+  { system = update_cache s_cache (System.freeze ~marshallable);
     lemmas = !s_lemmas;
     shallow = false;
     parsing = Parser.cur_state ();
   }
 
 let unfreeze_interp_state { system; lemmas; parsing } =
-  do_if_not_cached s_cache States.unfreeze system;
+  do_if_not_cached s_cache System.unfreeze system;
   s_lemmas := lemmas;
   Pcoq.unfreeze parsing
 
-let make_shallow st =
-  let lib = States.lib_of_state st.system in
-  { st with
-    system = States.replace_lib st.system @@ Lib.drop_objects lib;
-    shallow = true;
-  }
-
 (* Compatibility module *)
-module Declare = struct
+module Declare_ = struct
 
   let get () = !s_lemmas
   let set x = s_lemmas := x
@@ -182,3 +227,61 @@ module Declare = struct
     | Some src, Some tgt -> Some (LemmaStack.copy_info ~src ~tgt)
 
 end
+
+(* STM-specific state-handling *)
+module Stm = struct
+
+  (* Proof-related state, for workers; ideally the two counters would
+     be contained in the lemmas state themselves, as there is no need
+     for evar / metas to be global among proofs *)
+  type nonrec pstate =
+    LemmaStack.t option *
+    int *                                   (* Evarutil.meta_counter_summary_tag *)
+    int *                                   (* Evd.evar_counter_summary_tag *)
+    Declare.Obls.State.t
+
+  (* Parts of the system state that are morally part of the proof state *)
+  let pstate { lemmas; system } =
+    let st = System.Stm.summary system in
+    lemmas,
+    Summary.project_from_summary st Evarutil.meta_counter_summary_tag,
+    Summary.project_from_summary st Evd.evar_counter_summary_tag,
+    Summary.project_from_summary st Declare.Obls.State.prg_tag
+
+  let set_pstate ({ lemmas; system } as s) (pstate,c1,c2,c3) =
+    { s with
+      lemmas =
+        Declare_.copy_terminators ~src:s.lemmas ~tgt:pstate
+    ; system =
+        System.Stm.replace_summary s.system
+          begin
+            let st = System.Stm.summary s.system in
+            let st = Summary.modify_summary st Evarutil.meta_counter_summary_tag c1 in
+            let st = Summary.modify_summary st Evd.evar_counter_summary_tag c2 in
+            let st = Summary.modify_summary st Declare.Obls.State.prg_tag c3 in
+            st
+          end
+      }
+
+  let non_pstate { system } =
+    let st = System.Stm.summary system in
+    let st = Summary.remove_from_summary st Evarutil.meta_counter_summary_tag in
+    let st = Summary.remove_from_summary st Evd.evar_counter_summary_tag in
+    let st = Summary.remove_from_summary st Declare.Obls.State.prg_tag in
+    st, System.Stm.lib system
+
+  let same_env { system = s1 } { system = s2 } =
+    let s1 = System.Stm.summary s1 in
+    let e1 = Summary.project_from_summary s1 Global.global_env_summary_tag in
+    let s2 = System.Stm.summary s2 in
+    let e2 = Summary.project_from_summary s2 Global.global_env_summary_tag in
+    e1 == e2
+
+  let make_shallow st =
+    { st with
+      system = System.Stm.make_shallow st.system
+    ; shallow = true
+    }
+
+end
+module Declare = Declare_
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index c99db34873..8c23ac0698 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -9,12 +9,27 @@
 (************************************************************************)
 
 module Parser : sig
-  type state
+  type t
+
+  val init : unit -> t
+  val cur_state : unit -> t
+
+  val parse : t -> 'a Pcoq.Entry.t -> Pcoq.Parsable.t -> 'a
+
+end
+
+(** System State *)
+module System : sig
 
-  val init : unit -> state
-  val cur_state : unit -> state
+  (** The system state includes the summary and the libobject  *)
+  type t
+
+  (** [protect f x] runs [f x] and discards changes in the system state  *)
+  val protect : ('a -> 'b) -> 'a -> 'b
 
-  val parse : state -> 'a Pcoq.Entry.t -> Pcoq.Parsable.t -> 'a
+  (** Load / Dump provide unsafe but convenient state dumping from / to disk *)
+  val dump : string -> unit
+  val load : string -> unit
 
 end
 
@@ -31,9 +46,9 @@ module LemmaStack : sig
 end
 
 type t =
-  { parsing : Parser.state
+  { parsing : Parser.t
   (** parsing state [parsing state may not behave 100% functionally yet, beware] *)
-  ; system  : States.state
+  ; system  : System.t
   (** summary + libstack *)
   ; lemmas  : LemmaStack.t option
   (** proofs of lemmas currently opened *)
@@ -44,11 +59,21 @@ type t =
 val freeze_interp_state : marshallable:bool -> t
 val unfreeze_interp_state : t -> unit
 
-val make_shallow : t -> t
-
 (* WARNING: Do not use, it will go away in future releases *)
 val invalidate_cache : unit -> unit
 
+(* STM-specific state handling *)
+module Stm : sig
+  type pstate
+
+  (** Surgery on states related to proof state *)
+  val pstate : t -> pstate
+  val set_pstate : t -> pstate -> t
+  val non_pstate : t -> Summary.frozen * Lib.frozen
+  val same_env : t -> t -> bool
+  val make_shallow : t -> t
+end
+
 (* Compatibility module: Do Not Use *)
 module Declare : sig