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 --- proofs/proof_global.ml | 92 ++++--------------------------------------------- proofs/proof_global.mli | 45 ------------------------ 2 files changed, 6 insertions(+), 131 deletions(-) (limited to 'proofs') diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 4cc73f419e..9ee9e7ae2c 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -22,51 +22,6 @@ open Names module NamedDecl = Context.Named.Declaration -(*** Proof Modes ***) - -(* Type of proof modes : - - A function [set] to set it *from standard mode* - - A function [reset] to reset the *standard mode* from it *) -type proof_mode_name = string -type proof_mode = { - name : proof_mode_name ; - set : unit -> unit ; - reset : unit -> unit -} - -let proof_modes = Hashtbl.create 6 -let find_proof_mode n = - try Hashtbl.find proof_modes n - with Not_found -> - CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." n)) - -let register_proof_mode ({name = n} as m) = - Hashtbl.add proof_modes n (CEphemeron.create m) - -(* initial mode: standard mode *) -let standard = { name = "No" ; set = (fun ()->()) ; reset = (fun () -> ()) } -let _ = register_proof_mode standard - -(* Default proof mode, to be set at the beginning of proofs. *) -let default_proof_mode = ref (find_proof_mode "No") - -let get_default_proof_mode_name () = - (CEphemeron.default !default_proof_mode standard).name - -let proof_mode_opt_name = ["Default";"Proof";"Mode"] -let () = - Goptions.(declare_string_option { - optdepr = false; - optname = "default proof mode" ; - optkey = proof_mode_opt_name ; - optread = begin fun () -> - (CEphemeron.default !default_proof_mode standard).name - end; - optwrite = begin fun n -> - default_proof_mode := find_proof_mode n - end - }) - (*** Proof Global Environment ***) (* Extra info on proofs. *) @@ -95,7 +50,6 @@ type pstate = { endline_tactic : Genarg.glob_generic_argument option; section_vars : Constr.named_context option; proof : Proof.t; - mode : proof_mode CEphemeron.key; universe_decl: UState.universe_decl; strength : Decl_kinds.goal_kind; } @@ -109,23 +63,8 @@ let apply_terminator f = f to be resumed when the current proof is closed or aborted. *) let pstates = ref ([] : pstate list) -(* Current proof_mode, for bookkeeping *) -let current_proof_mode = ref !default_proof_mode - -(* combinators for proof modes *) -let update_proof_mode () = - match !pstates with - | { mode = m } :: _ -> - CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); - current_proof_mode := m; - CEphemeron.iter_opt !current_proof_mode (fun x -> x.set ()) - | _ -> - CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); - current_proof_mode := find_proof_mode "No" - (* combinators for the current_proof lists *) -let push a l = l := a::!l; - update_proof_mode () +let push a l = l := a::!l exception NoSuchProof let () = CErrors.register_handler begin function @@ -221,25 +160,8 @@ let discard {CAst.loc;v=id} = let discard_current () = if List.is_empty !pstates then raise NoCurrentProof else pstates := List.tl !pstates - let discard_all () = pstates := [] -(* [set_proof_mode] sets the proof mode to be used after it's called. It is - typically called by the Proof Mode command. *) -let set_proof_mode m id = - pstates := List.map - (fun ps -> if pf_name_eq id ps then { ps with mode = m } else ps) - !pstates; - update_proof_mode () - -let set_proof_mode mn = - set_proof_mode (find_proof_mode mn) (get_current_proof_name ()) - -let activate_proof_mode mode = - CEphemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ()) -let disactivate_current_proof_mode () = - CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()) - (** [start_proof sigma id pl str goals terminator] starts a proof of name [id] with goals [goals] (a list of pairs of environment and conclusion); [str] describes what kind of theorem/definition this @@ -254,9 +176,8 @@ let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals terminator proof = Proof.start ~name ~poly:(pi2 kind) sigma goals; endline_tactic = None; section_vars = None; - mode = find_proof_mode "No"; - universe_decl = pl; - strength = kind } in + strength = kind; + universe_decl = pl } in push initial_state pstates let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals terminator = @@ -265,9 +186,8 @@ let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals termina proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals; endline_tactic = None; section_vars = None; - mode = find_proof_mode "No"; - universe_decl = pl; - strength = kind } in + strength = kind; + universe_decl = pl } in push initial_state pstates let get_used_variables () = (cur_pstate ()).section_vars @@ -478,7 +398,7 @@ end let freeze ~marshallable = if marshallable then CErrors.anomaly (Pp.str"full marshalling of proof state not supported.") else !pstates -let unfreeze s = pstates := s; update_proof_mode () +let unfreeze s = pstates := s let proof_of_state = function { proof }::_ -> proof | _ -> raise NoCurrentProof let copy_terminators ~src ~tgt = assert(List.length src = List.length tgt); diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index e762f3b7dc..40920f51a3 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -13,7 +13,6 @@ environment. *) type t - val there_are_pending_proofs : unit -> bool val check_no_pending_proof : unit -> unit @@ -139,47 +138,3 @@ val freeze : marshallable:bool -> t val unfreeze : t -> unit val proof_of_state : t -> Proof.t val copy_terminators : src:t -> tgt:t -> t - - -(**********************************************************) -(* Proof Mode API *) -(* The current Proof Mode API is deprecated and a new one *) -(* will be (hopefully) defined in 8.8 *) -(**********************************************************) - -(** Type of proof modes : - - A name - - A function [set] to set it *from standard mode* - - A function [reset] to reset the *standard mode* from it - -*) -type proof_mode_name = string -type proof_mode = { - name : proof_mode_name ; - set : unit -> unit ; - reset : unit -> unit -} - -(** Registers a new proof mode which can then be adressed by name - in [set_default_proof_mode]. - One mode is already registered - the standard mode - named "No", - It corresponds to Coq default setting are they are set when coqtop starts. *) -val register_proof_mode : proof_mode -> unit -(* Can't make this deprecated due to limitations of camlp5 *) -(* [@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] *) - -val proof_mode_opt_name : string list - -val get_default_proof_mode_name : unit -> proof_mode_name -[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] - -(** [set_proof_mode] sets the proof mode to be used after it's called. It is - typically called by the Proof Mode command. *) -val set_proof_mode : proof_mode_name -> unit -[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] - -val activate_proof_mode : proof_mode_name -> unit -[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] - -val disactivate_current_proof_mode : unit -> unit -[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] -- cgit v1.2.3