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

Reviewed-by: SkySkimmer
Reviewed-by: gares

15 files changed, 176 insertions, 162 deletions

diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 167cf37026..dcca694200 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -70,7 +70,7 @@ let build_newrecursive lnameargsardef =
         CErrors.user_err ~hdr:"Function"
           (Pp.str "Body of Function must be given")
     in
-    States.with_state_protection (List.map f) lnameargsardef
+    Vernacstate.System.protect (List.map f) lnameargsardef
   in
   (recdef, rec_impls)
 
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index e6c59f446d..f8c25d5dd0 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -489,7 +489,7 @@ let register_ltac local ?deprecation tacl =
   in
   (* STATE XXX: Review what is going on here. Why does this needs
      protection? Why is not the STM level protection enough? Fishy *)
-  let defs = States.with_state_protection defs () in
+  let defs = Vernacstate.System.protect defs () in
   let iter (def, tac) = match def with
   | NewTac id ->
     Tacenv.register_ltac false local id tac ?deprecation;
diff --git a/stm/stm.ml b/stm/stm.ml
index 652d064b83..3b7921f638 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -199,16 +199,11 @@ let mkTransTac cast cblock cqueue =
 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_tag,
-                     Evd.evar_counter_summary_tag,
-                     Declare.Obls.State.prg_tag
-
 type cached_state =
   | EmptyState
-  | ParsingState of Vernacstate.Parser.state
+  | ParsingState of Vernacstate.Parser.t
   | FullState of Vernacstate.t
-  | ErrorState of Vernacstate.Parser.state option * Exninfo.iexn
+  | ErrorState of Vernacstate.Parser.t option * Exninfo.iexn
 type branch = Vcs_.Branch.t * branch_type Vcs_.branch_info
 type backup = { mine : branch; others : branch list }
 
@@ -334,7 +329,7 @@ module VCS : sig
 
   type vcs = (branch_type, transaction, vcs state_info, box) Vcs_.t
 
-  val init : stm_doc_type -> id -> Vernacstate.Parser.state -> doc
+  val init : stm_doc_type -> id -> Vernacstate.Parser.t -> doc
   (* val get_type : unit -> stm_doc_type *)
   val set_ldir : Names.DirPath.t -> unit
   val get_ldir : unit -> Names.DirPath.t
@@ -364,8 +359,8 @@ module VCS : sig
   val goals : id -> int -> unit
   val set_state : id -> cached_state -> unit
   val get_state : id -> cached_state
-  val set_parsing_state : id -> Vernacstate.Parser.state -> unit
-  val get_parsing_state : id -> Vernacstate.Parser.state option
+  val set_parsing_state : id -> Vernacstate.Parser.t -> unit
+  val get_parsing_state : id -> Vernacstate.Parser.t option
   val get_proof_mode : id -> Pvernac.proof_mode option
 
   (* cuts from start -> stop, raising Expired if some nodes are not there *)
@@ -678,7 +673,7 @@ end = struct (* {{{ *)
         { info with state = EmptyState;
                     vcs_backup = None,None } in
     let make_shallow = function
-      | FullState st -> FullState (Vernacstate.make_shallow st)
+      | FullState st -> FullState (Vernacstate.Stm.make_shallow st)
       | x -> x
     in
     let copy_info_w_state v id =
@@ -870,22 +865,13 @@ end = struct (* {{{ *)
 
   let invalidate_cur_state () = cur_id := Stateid.dummy
 
-  type proof_part =
-    Vernacstate.LemmaStack.t option *
-    int *                                   (* Evarutil.meta_counter_summary_tag *)
-    int *                                   (* Evd.evar_counter_summary_tag *)
-    Declare.Obls.State.t
+  type proof_part = Vernacstate.Stm.pstate
 
   type partial_state =
     [ `Full of Vernacstate.t
     | `ProofOnly of Stateid.t * proof_part ]
 
-  let proof_part_of_frozen { Vernacstate.lemmas; system } =
-    let st = States.summary_of_state system in
-    lemmas,
-    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 proof_part_of_frozen st = Vernacstate.Stm.pstate st
 
   let cache_state ~marshallable id =
     VCS.set_state id (FullState (Vernacstate.freeze_interp_state ~marshallable))
@@ -952,21 +938,10 @@ end = struct (* {{{ *)
             else s
            with VCS.Expired -> s in
          VCS.set_state id (FullState s)
-    | `ProofOnly(ontop,(pstate,c1,c2,c3)) ->
+    | `ProofOnly(ontop,pstate) ->
          if is_cached_and_valid ontop then
            let s = get_cached ontop in
-           let s = { s with lemmas =
-             PG_compat.copy_terminators ~src:s.lemmas ~tgt:pstate } in
-           let s = { s with system =
-             States.replace_summary s.system
-               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
+           let s = Vernacstate.Stm.set_pstate s pstate in
            VCS.set_state id (FullState s)
     with VCS.Expired -> ()
 
@@ -978,12 +953,7 @@ end = struct (* {{{ *)
         execution_error ?loc id (iprint (e, info));
         (e, Stateid.add info ~valid id)
 
-  let same_env { Vernacstate.system = s1 } { Vernacstate.system = s2 } =
-    let s1 = States.summary_of_state s1 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_from_summary s2 Global.global_env_summary_tag in
-    e1 == e2
+  let same_env = Vernacstate.Stm.same_env
 
   (* [define] puts the system in state [id] calling [f ()] *)
   (* [safe_id] is the last known valid state before execution *)
@@ -2373,21 +2343,16 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
 
   (* ugly functions to process nested lemmas, i.e. hard to reproduce
    * side effects *)
-  let cherry_pick_non_pstate () =
-    let st = Summary.freeze_summaries ~marshallable:false 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 () in
-
   let inject_non_pstate (s,l) =
     Summary.unfreeze_summaries ~partial:true s; Lib.unfreeze l; update_global_env ()
   in
+
   let rec pure_cherry_pick_non_pstate safe_id id =
     State.purify (fun id ->
         stm_prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id);
         reach ~safe_id id;
-        cherry_pick_non_pstate ())
+        let st = Vernacstate.freeze_interp_state ~marshallable:false in
+        Vernacstate.Stm.non_pstate st)
       id
 
   (* traverses the dag backward from nodes being already calculated *)
diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml
index c6bb38e005..03c53d6991 100644
--- a/toplevel/coqc.ml
+++ b/toplevel/coqc.ml
@@ -11,7 +11,7 @@
 let outputstate opts =
   Option.iter (fun ostate_file ->
     let fname = CUnix.make_suffix ostate_file ".coq" in
-    Library.extern_state fname) opts.Coqcargs.outputstate
+    Vernacstate.System.dump fname) opts.Coqcargs.outputstate
 
 let coqc_init _copts ~opts =
   Flags.quiet := true;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 2d450d430a..4231915be1 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -52,7 +52,7 @@ let print_memory_stat () =
 let inputstate opts =
   Option.iter (fun istate_file ->
     let fname = Loadpath.locate_file (CUnix.make_suffix istate_file ".coq") in
-    Library.intern_state fname) opts.inputstate
+    Vernacstate.System.load fname) opts.inputstate
 
 (******************************************************************************)
 (* Fatal Errors                                                               *)
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