Merge PR #9263: [STM] explicit handling of parsing states

Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: maximedenes

9 files changed, 144 insertions, 33 deletions

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 8f155adb8a..0dfbba0e83 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -340,7 +340,7 @@ let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c
   | None -> standard_proof_terminator ?hook compute_guard
   | Some terminator -> terminator ?hook compute_guard
   in
-  let sign = 
+  let sign =
     match sign with
     | Some sign -> sign
     | None -> initialize_named_context_for_proof ()
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index a647b2ef73..0e46df2320 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -12,6 +12,27 @@ open Pcoq
 
 let uvernac = create_universe "vernac"
 
+type proof_mode = string
+
+(* Tactic parsing modes *)
+let register_proof_mode, find_proof_mode, lookup_proof_mode =
+  let proof_mode : (string, Vernacexpr.vernac_expr Entry.t) Hashtbl.t =
+    Hashtbl.create 19 in
+  let register_proof_mode ename e = Hashtbl.add proof_mode ename e; ename in
+  let find_proof_mode ename =
+    try Hashtbl.find proof_mode ename
+    with Not_found ->
+      CErrors.anomaly Pp.(str "proof mode not found: " ++ str ename) in
+  let lookup_proof_mode name =
+    if Hashtbl.mem proof_mode name then Some name
+    else None
+  in
+  register_proof_mode, find_proof_mode, lookup_proof_mode
+
+let proof_mode_to_string name = name
+
+let command_entry_ref = ref None
+
 module Vernac_ =
   struct
     let gec_vernac s = Entry.create ("vernac:" ^ s)
@@ -39,17 +60,24 @@ module Vernac_ =
       ] in
       Pcoq.grammar_extend main_entry None (None, [None, None, rule])
 
-    let command_entry_ref = ref noedit_mode
+    let select_tactic_entry spec =
+      match spec with
+      | None -> noedit_mode
+      | Some ename -> find_proof_mode ename
+
     let command_entry =
       Pcoq.Entry.of_parser "command_entry"
-        (fun strm -> Pcoq.Entry.parse_token_stream !command_entry_ref strm)
+        (fun strm -> Pcoq.Entry.parse_token_stream (select_tactic_entry !command_entry_ref) strm)
 
   end
 
-let main_entry = Vernac_.main_entry
+module Unsafe = struct
+  let set_tactic_entry oname = command_entry_ref := oname
+end
 
-let set_command_entry e = Vernac_.command_entry_ref := e
-let get_command_entry () = !Vernac_.command_entry_ref
+let main_entry proof_mode =
+  Unsafe.set_tactic_entry proof_mode;
+  Vernac_.main_entry
 
 let () =
   register_grammar Genredexpr.wit_red_expr (Vernac_.red_expr);
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
index b2f8f71462..fa251281dc 100644
--- a/vernac/pvernac.mli
+++ b/vernac/pvernac.mli
@@ -14,6 +14,8 @@ open Vernacexpr
 
 val uvernac : gram_universe
 
+type proof_mode
+
 module Vernac_ :
   sig
     val gallina : vernac_expr Entry.t
@@ -24,13 +26,31 @@ module Vernac_ :
     val rec_definition : (fixpoint_expr * decl_notation list) Entry.t
     val noedit_mode : vernac_expr Entry.t
     val command_entry : vernac_expr Entry.t
+    val main_entry : (Loc.t * vernac_control) option Entry.t
     val red_expr : raw_red_expr Entry.t
     val hint_info : Hints.hint_info_expr Entry.t
   end
 
+(* To be removed when the parser is made functional wrt the tactic
+ * non terminal *)
+module Unsafe : sig
+  (* To let third party grammar entries reuse Vernac_ and
+   * do something with the proof mode *)
+  val set_tactic_entry : proof_mode option -> unit
+end
+
 (** The main entry: reads an optional vernac command *)
-val main_entry : (Loc.t * vernac_control) option Entry.t
+val main_entry : proof_mode option -> (Loc.t * vernac_control) option Entry.t
+
+(** Grammar entry for tactics: proof mode(s).
+  By default Coq's grammar has an empty entry (non-terminal) for
+  tactics.  A plugin can register its non-terminal by providing a name
+  and a grammar entry.
+
+  For example the Ltac plugin register the "Classic" grammar
+  entry for parsing its tactics.
+  *)
 
-(** Handling of the proof mode entry *)
-val get_command_entry : unit -> vernac_expr Entry.t
-val set_command_entry : vernac_expr Entry.t -> unit
+val register_proof_mode : string -> Vernacexpr.vernac_expr Entry.t -> proof_mode
+val lookup_proof_mode : string -> proof_mode option
+val proof_mode_to_string : proof_mode -> string
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 26859cd2cf..996fe320f9 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -489,6 +489,28 @@ let vernac_notation ~module_local =
 let vernac_custom_entry ~module_local s =
   Metasyntax.declare_custom_entry module_local s
 
+(* Default proof mode, to be set at the beginning of proofs for
+   programs that cannot be statically classified. *)
+let default_proof_mode = ref (Pvernac.register_proof_mode "Noedit" Pvernac.Vernac_.noedit_mode)
+let get_default_proof_mode () = !default_proof_mode
+
+let get_default_proof_mode_opt () = Pvernac.proof_mode_to_string !default_proof_mode
+let set_default_proof_mode_opt name =
+  default_proof_mode :=
+    match Pvernac.lookup_proof_mode name with
+    | Some pm -> pm
+    | None -> CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." name))
+
+let proof_mode_opt_name = ["Default";"Proof";"Mode"]
+let () =
+  Goptions.declare_string_option Goptions.{
+    optdepr = false;
+    optname = "default proof mode" ;
+    optkey = proof_mode_opt_name;
+    optread = get_default_proof_mode_opt;
+    optwrite = set_default_proof_mode_opt;
+  }
+
 (***********)
 (* Gallina *)
 
@@ -2115,13 +2137,9 @@ exception End_of_input
 let vernac_load interp fname =
   if Proof_global.there_are_pending_proofs () then
     CErrors.user_err Pp.(str "Load is not supported inside proofs.");
-  let interp x =
-    let proof_mode = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] in
-    Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"];
-    interp x in
-  let parse_sentence = Flags.with_option Flags.we_are_parsing
+  let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing
     (fun po ->
-    match Pcoq.Entry.parse Pvernac.main_entry po with
+    match Pcoq.Entry.parse (Pvernac.main_entry proof_mode) po with
       | Some x -> x
       | None -> raise End_of_input) in
   let fname =
@@ -2132,7 +2150,15 @@ let vernac_load interp fname =
     let in_chan = open_utf8_file_in longfname in
     Pcoq.Parsable.make ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in
   begin
-    try while true do interp (snd (parse_sentence input)) done
+    try while true do
+        let proof_mode =
+          if Proof_global.there_are_pending_proofs () then
+            Some (get_default_proof_mode ())
+          else
+            None
+        in
+        interp (snd (parse_sentence proof_mode input));
+      done
     with End_of_input -> ()
   end;
   (* If Load left a proof open, we fail too. *)
@@ -2312,8 +2338,7 @@ let interp ?proof ~atts ~st c =
     Aux_file.record_in_aux_at "VernacProof" (tacs^" "^usings);
     Option.iter vernac_set_end_tac tac;
     Option.iter vernac_set_used_variables using
-  | VernacProofMode mn -> unsupported_attributes atts;
-    Proof_global.set_proof_mode mn [@ocaml.warning "-3"]
+  | VernacProofMode mn -> unsupported_attributes atts; ()
 
   (* Extensions *)
   | VernacExtend (opn,args) ->
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 8d8d7cfcf0..4fbd3849b0 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -10,6 +10,11 @@
 
 val dump_global : Libnames.qualid Constrexpr.or_by_notation -> unit
 
+(** Default proof mode set by `start_proof` *)
+val get_default_proof_mode : unit -> Pvernac.proof_mode
+
+val proof_mode_opt_name : string list
+
 (** Vernacular entries *)
 val vernac_require :
   Libnames.qualid option -> bool option -> Libnames.qualid list -> unit
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 05687afd8b..f5cf3401d0 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -29,15 +29,15 @@ type vernac_type =
       parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ];
       proof_block_detection : proof_block_name option
     }
-  (* To be removed *)
-  | VtProofMode of string
   (* Queries are commands assumed to be "pure", that is to say, they
      don't modify the interpretation state. *)
   | VtQuery
+  (* Commands that change the current proof mode *)
+  | VtProofMode of string
   (* To be removed *)
   | VtMeta
   | VtUnknown
-and vernac_start = string * opacity_guarantee * Names.Id.t list
+and vernac_start = opacity_guarantee * Names.Id.t list
 and vernac_sideff_type = Names.Id.t list
 and opacity_guarantee =
   | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 0d43eb1ee8..118907c31b 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -45,15 +45,15 @@ type vernac_type =
       parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ];
       proof_block_detection : proof_block_name option
     }
-  (* To be removed *)
-  | VtProofMode of string
   (* Queries are commands assumed to be "pure", that is to say, they
      don't modify the interpretation state. *)
   | VtQuery
+  (* Commands that change the current proof mode *)
+  | VtProofMode of string
   (* To be removed *)
   | VtMeta
   | VtUnknown
-and vernac_start = string * opacity_guarantee * Names.Id.t list
+and vernac_start = opacity_guarantee * Names.Id.t list
 and vernac_sideff_type = Names.Id.t list
 and opacity_guarantee =
   | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 61540024ef..c691dc8559 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -8,10 +8,30 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+module Parser = struct
+
+  type state = Pcoq.frozen_t
+
+  let init () = Pcoq.freeze ~marshallable:false
+
+  let cur_state () = Pcoq.freeze ~marshallable:false
+
+  let parse ps entry pa =
+    Pcoq.unfreeze ps;
+    Flags.with_option Flags.we_are_parsing (fun () ->
+      try Pcoq.Entry.parse entry pa
+      with e when CErrors.noncritical e ->
+        let (e, info) = CErrors.push e in
+        Exninfo.iraise (e, info))
+    ()
+
+end
+
 type t = {
-  system  : States.state;        (* summary + libstack *)
-  proof   : Proof_global.t;      (* proof state *)
-  shallow : bool                 (* is the state trimmed down (libstack) *)
+  parsing: Parser.state;
+  system : States.state; (* summary + libstack *)
+  proof : Proof_global.t; (* proof state *)
+  shallow : bool; (* is the state trimmed down (libstack) *)
 }
 
 let s_cache = ref None
@@ -37,11 +57,13 @@ let freeze_interp_state ~marshallable =
   { system = update_cache s_cache (States.freeze ~marshallable);
     proof  = update_cache s_proof (Proof_global.freeze ~marshallable);
     shallow = false;
+    parsing = Parser.cur_state ();
   }
 
-let unfreeze_interp_state { system; proof } =
+let unfreeze_interp_state { system; proof; parsing } =
   do_if_not_cached s_cache States.unfreeze system;
-  do_if_not_cached s_proof Proof_global.unfreeze proof
+  do_if_not_cached s_proof Proof_global.unfreeze proof;
+  Pcoq.unfreeze parsing
 
 let make_shallow st =
   let lib = States.lib_of_state st.system in
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index ed20cb935a..581c23386a 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -8,10 +8,21 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+module Parser : sig
+  type state
+
+  val init : unit -> state
+  val cur_state : unit -> state
+
+  val parse : state -> 'a Pcoq.Entry.t -> Pcoq.Parsable.t -> 'a
+
+end
+
 type t = {
-  system  : States.state;        (* summary + libstack *)
-  proof   : Proof_global.t;      (* proof state *)
-  shallow : bool                 (* is the state trimmed down (libstack) *)
+  parsing: Parser.state;
+  system : States.state; (* summary + libstack *)
+  proof : Proof_global.t; (* proof state *)
+  shallow : bool; (* is the state trimmed down (libstack) *)
 }
 
 val freeze_interp_state : marshallable:bool -> t