From e43c35ba795520fe111ac39a834f334753491b28 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 17 Apr 2017 10:31:29 +0200 Subject: [STM] explicit handling of parsing states DAG nodes hold now a system state and a parsing state. The latter is always passed to the parser. This paves the way to decoupling the effect of commands on the parsing state and the system state, and hence never force to interpret, say, Notation. Handling proof modes is now done explicitly in the STM, not by interpreting VernacStartLemma. Similarly Notation execution could be split in two phases in order to obtain a parsing state without fully executing it (that requires executing all commands before it). Co-authored-by: Maxime Dénès Co-authored-by: Emilio Jesus Gallego Arias --- vernac/lemmas.ml | 2 +- vernac/pvernac.ml | 38 +++++++++++++++++++++++++++++++++----- vernac/pvernac.mli | 28 ++++++++++++++++++++++++---- vernac/vernacentries.ml | 43 ++++++++++++++++++++++++++++++++++--------- vernac/vernacentries.mli | 5 +++++ vernac/vernacextend.ml | 6 +++--- vernac/vernacextend.mli | 6 +++--- vernac/vernacstate.ml | 32 +++++++++++++++++++++++++++----- vernac/vernacstate.mli | 17 ++++++++++++++--- 9 files changed, 144 insertions(+), 33 deletions(-) (limited to 'vernac') 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 -- cgit v1.2.3