Merge PR coq#19193: [vernacstate] Remove Vernacstate.Parser.t

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <[email protected]>

dev/ci/user-overlays/19193-ejgallego-vernacstate_remove_parsing.sh

@@ -0,0 +1,5 @@
+overlay coq_lsp https://github.com/ejgallego/coq-lsp vernacstate_remove_parsing 19193
+
+overlay serapi https://github.com/ejgallego/coq-serapi vernacstate_remove_parsing 19193
+
+overlay vscoq https://github.com/ejgallego/vscoq vernacstate_remove_parsing 19193

stm/stm.ml

@@ -191,9 +191,9 @@ let mkTransCmd cast cids ceff cqueue =
 
 type cached_state =
   | EmptyState
-  | ParsingState of Vernacstate.Parser.t
+  | ParsingState of Pcoq.frozen_t
   | FullState of Vernacstate.t
-  | ErrorState of Vernacstate.Parser.t option * Exninfo.iexn
+  | ErrorState of Pcoq.frozen_t option * Exninfo.iexn
 type branch = Vcs_.Branch.t * Vcs_.branch_info
 type backup = { mine : branch; others : branch list }
 
@@ -309,7 +309,7 @@ module VCS : sig
     mutable vcs_backup : vcs option * backup option;
   }
 
-  val init : stm_doc_type -> id -> Vernacstate.Parser.t -> doc
+  val init : stm_doc_type -> id -> Pcoq.frozen_t -> doc
   (* val get_type : unit -> stm_doc_type *)
   val set_ldir : Names.DirPath.t -> unit
   val get_ldir : unit -> Names.DirPath.t
@@ -339,8 +339,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.t -> unit
-  val get_parsing_state : id -> Vernacstate.Parser.t option
+  val set_parsing_state : id -> Pcoq.frozen_t -> unit
+  val get_parsing_state : id -> Pcoq.frozen_t option
   val get_proof_mode : id -> Pvernac.proof_mode option
 
   (* cuts from start -> stop, raising Expired if some nodes are not there *)
@@ -2214,7 +2214,10 @@ let new_doc { doc_type ; injections } =
   (* We must reset the whole state before creating a document! *)
   State.restore_root_state ();
 
-  let doc = VCS.init doc_type Stateid.initial (Vernacstate.Parser.init ()) in
+  let doc =
+    let ps = Pcoq.freeze () in
+    VCS.init doc_type Stateid.initial ps
+  in
 
   Safe_typing.allow_delayed_constants := (cur_opt()).async_proofs_mode <> APoff;
 
@@ -2508,7 +2511,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) x c =
               | VtNow ->
                 (* We need to execute to get the new parsing state *)
                 let () = observe ~doc:dummy_doc (VCS.get_branch_pos (VCS.current_branch ())) in
-                let parsing = Vernacstate.Parser.cur_state () in
+                let parsing = Pcoq.freeze () in
                 (* If execution has not been put in cache, we need to save the parsing state *)
                 if (VCS.get_info id).state == EmptyState then VCS.set_parsing_state id parsing;
                 parsing
@@ -2553,7 +2556,8 @@ let stop_worker n = Slaves.cancel_worker n
 let parse_sentence ~doc sid ~entry pa =
   let ps = Option.get @@ VCS.get_parsing_state sid in
   let proof_mode = VCS.get_proof_mode sid in
-  Vernacstate.Parser.parse ps (entry proof_mode) pa
+  Pcoq.unfreeze ps;
+  Pcoq.Entry.parse (entry proof_mode) pa
 
 (* You may need to know the len + indentation of previous command to compute
  * the indentation of the current one.

vernac/vernacstate.ml

@@ -8,20 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-module Parser = struct
-
-  type t = Pcoq.frozen_t
-
-  let init () = Pcoq.freeze ()
-
-  let cur_state () = Pcoq.freeze ()
-
-  let parse ps entry pa =
-    Pcoq.unfreeze ps;
-    Pcoq.Entry.parse entry pa
-
-end
-
 module Synterp = struct
 
   type t = Lib.Synterp.frozen * Summary.Synterp.frozen
@@ -33,10 +19,10 @@ module Synterp = struct
     Lib.Synterp.unfreeze fl;
     Summary.Synterp.unfreeze_summaries fs
 
-  let init () = freeze ()
+  let parsing (_fl, fs) =
+    Summary.Synterp.project_from_summary fs Pcoq.parser_summary_tag
 
-  let parsing (_, sum) =
-    Summary.Synterp.project_from_summary sum Pcoq.parser_summary_tag
+  let init () = freeze ()
 
   module Stm = struct
     let make_shallow (lib, summary) = Lib.Synterp.drop_objects lib, Summary.Synterp.make_marshallable summary
@@ -68,7 +54,6 @@ end = struct
     Lib.Interp.unfreeze fl;
     Summary.Interp.unfreeze_summaries fs
 
-  (* STM-specific state manipulations *)
   module Stm = struct
     let make_shallow (lib, summary) = Lib.Interp.drop_objects lib, Summary.Interp.make_marshallable summary
     let lib = fst

vernac/vernacstate.mli

@@ -8,18 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-module Parser : sig
-
-  (** Subset of [Synterp.t] needed to parse *)
-  type t
-
-  val init : unit -> t
-  val cur_state : unit -> t
-
-  val parse : t -> 'a Pcoq.Entry.t -> Pcoq.Parsable.t -> 'a
-
-end
-
 (** Synterp State, includes parser state, etc... ; as of today the
     parsing state has no functional components. *)
 module Synterp : sig
@@ -29,8 +17,7 @@ module Synterp : sig
   val init : unit -> t
   val freeze : unit -> t
   val unfreeze : t -> unit
-  val parsing : t -> Parser.t
-
+  val parsing : t -> Pcoq.frozen_t
 end
 
 module System : sig