From dc664b3b0c6f6f5eeba0c1092efc3f4537cdf657 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 19 Nov 2017 03:40:45 +0100 Subject: [plugins] Prepare plugin API for functional handling of state. To this purpose we allow plugins to register functions that will modify the state. This is not used yet, but will be used soon when we remove the global handling of the proof state. --- stm/proofBlockDelimiter.ml | 2 +- stm/stm.ml | 79 +++++++++++++++++++++++----------------------- stm/stm.mli | 2 +- 3 files changed, 41 insertions(+), 42 deletions(-) (limited to 'stm') diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index 01b75e496..77642946c 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -46,7 +46,7 @@ let simple_goal sigma g gs = let is_focused_goal_simple ~doc id = match state_of_id ~doc id with | `Expired | `Error _ | `Valid None -> `Not - | `Valid (Some { Vernacentries.proof }) -> + | `Valid (Some { Vernacstate.proof }) -> let proof = Proof_global.proof_of_state proof in let focused, r1, r2, r3, sigma = Proof.proof proof in let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in diff --git a/stm/stm.ml b/stm/stm.ml index b394c3a13..a3a14a840 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -25,14 +25,14 @@ open Vernacexpr (* Protect against state changes *) let stm_purify f x = - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in try let res = f x in - Vernacentries.unfreeze_interp_state st; + Vernacstate.unfreeze_interp_state st; res with e -> let e = CErrors.push e in - Vernacentries.unfreeze_interp_state st; + Vernacstate.unfreeze_interp_state st; Exninfo.iraise e let execution_error ?loc state_id msg = @@ -165,7 +165,7 @@ let summary_pstate = [ Evarutil.meta_counter_summary_name; type cached_state = | Empty | Error of Exninfo.iexn - | Valid of Vernacentries.interp_state + | Valid of Vernacstate.t type branch = Vcs_.Branch.t * branch_type Vcs_.branch_info type backup = { mine : branch; others : branch list } @@ -735,16 +735,16 @@ module State : sig val exn_on : Stateid.t -> valid:Stateid.t -> Exninfo.iexn -> Exninfo.iexn (* to send states across worker/master *) - val get_cached : Stateid.t -> Vernacentries.interp_state - val same_env : Vernacentries.interp_state -> Vernacentries.interp_state -> bool + val get_cached : Stateid.t -> Vernacstate.t + val same_env : Vernacstate.t -> Vernacstate.t -> bool type proof_part type partial_state = - [ `Full of Vernacentries.interp_state + [ `Full of Vernacstate.t | `ProofOnly of Stateid.t * proof_part ] - val proof_part_of_frozen : Vernacentries.interp_state -> proof_part + val proof_part_of_frozen : Vernacstate.t -> proof_part val assign : Stateid.t -> partial_state -> unit (* Handlers for initial state, prior to document creation. *) @@ -757,8 +757,6 @@ module State : sig end = struct (* {{{ *) - open Vernacentries - (* cur_id holds Stateid.dummy in case the last attempt to define a state * failed, so the global state may contain garbage *) let cur_id = ref Stateid.dummy @@ -768,15 +766,15 @@ end = struct (* {{{ *) Proof_global.state * Summary.frozen_bits (* only meta counters *) type partial_state = - [ `Full of Vernacentries.interp_state + [ `Full of Vernacstate.t | `ProofOnly of Stateid.t * proof_part ] - let proof_part_of_frozen { Vernacentries.proof; system } = + let proof_part_of_frozen { Vernacstate.proof; system } = proof, Summary.project_summary (States.summary_of_state system) summary_pstate let freeze marshallable id = - VCS.set_state id (Valid (Vernacentries.freeze_interp_state marshallable)) + VCS.set_state id (Valid (Vernacstate.freeze_interp_state marshallable)) let freeze_invalid id iexn = VCS.set_state id (Error iexn) @@ -800,7 +798,7 @@ end = struct (* {{{ *) let install_cached id = match VCS.get_info id with | { state = Valid s } -> - Vernacentries.unfreeze_interp_state s; + Vernacstate.unfreeze_interp_state s; cur_id := id | { state = Error ie } -> @@ -819,6 +817,7 @@ end = struct (* {{{ *) with VCS.Expired -> anomaly Pp.(str "not a cached state (expired).") let assign id what = + let open Vernacstate in if VCS.get_state id <> Empty then () else try match what with | `Full s -> @@ -826,7 +825,7 @@ end = struct (* {{{ *) try let prev = (VCS.visit id).next in if is_cached_and_valid prev - then { s with Vernacentries.proof = + then { s with proof = Proof_global.copy_terminators ~src:(get_cached prev).proof ~tgt:s.proof } else s @@ -854,7 +853,7 @@ end = struct (* {{{ *) execution_error ?loc id (iprint (e, info)); (e, Stateid.add info ~valid id) - let same_env { system = s1 } { system = s2 } = + let same_env { Vernacstate.system = s1 } { Vernacstate.system = s2 } = let s1 = States.summary_of_state s1 in let e1 = Summary.project_summary s1 [Global.global_env_summary_name] in let s2 = States.summary_of_state s2 in @@ -902,11 +901,11 @@ end = struct (* {{{ *) let init_state = ref None let register_root_state () = - init_state := Some (Vernacentries.freeze_interp_state `No) + init_state := Some (Vernacstate.freeze_interp_state `No) let restore_root_state () = cur_id := Stateid.dummy; - Vernacentries.unfreeze_interp_state (Option.get !init_state); + Vernacstate.unfreeze_interp_state (Option.get !init_state); end (* }}} *) @@ -1001,7 +1000,7 @@ end (* Wrapper for Vernacentries.interp to set the feedback id *) (* It is currently called 19 times, this number should be certainly reduced... *) -let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacentries.interp_state = +let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t = (* The Stm will gain the capability to interpret commmads affecting the whole document state, such as backtrack, etc... so we start to design the stm command interpreter now *) @@ -1437,19 +1436,19 @@ end = struct (* {{{ *) * a bad fixpoint *) let fix_exn = Future.fix_exn_of future_proof in (* STATE: We use the current installed imperative state *) - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in if not drop then begin let checked_proof = Future.chain future_proof (fun p -> (* Unfortunately close_future_proof and friends are not pure so we need to set the state manually here *) - Vernacentries.unfreeze_interp_state st; + Vernacstate.unfreeze_interp_state st; let pobject, _ = Proof_global.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in let terminator = (* The one sent by master is an InvalidKey *) Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in stm_vernac_interp stop ~proof:(pobject, terminator) st { verbose = false; loc; indentation = 0; strlen = 0; @@ -1457,7 +1456,7 @@ end = struct (* {{{ *) ignore(Future.join checked_proof); end; (* STATE: Restore the state XXX: handle exn *) - Vernacentries.unfreeze_interp_state st; + Vernacstate.unfreeze_interp_state st; RespBuiltProof(proof,time) with | e when CErrors.noncritical e || e = Stack_overflow -> @@ -1598,7 +1597,7 @@ end = struct (* {{{ *) * => takes nothing from the itermediate states. *) (* STATE We use the state resulting from reaching start. *) - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp stop ~proof st { verbose = false; loc; indentation = 0; strlen = 0; expr = (VernacEndProof (Proved (Opaque,None))) }); @@ -1855,7 +1854,7 @@ end = struct (* {{{ *) * => captures state id in a future closure, which will discard execution state but for the proof + univs. *) - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp r_state_fb st ast); let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in match Evd.(evar_body (find sigma r_goal)) with @@ -1895,7 +1894,7 @@ end = struct (* {{{ *) | VernacRedirect (_,(_,e)) -> find ~time ~fail e | VernacFail e -> find ~time ~fail:true e | e -> e, time, fail in find ~time:false ~fail:false e in - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in Vernacentries.with_fail st fail (fun () -> (if time then System.with_time !Flags.time else (fun x -> x)) (fun () -> ignore(TaskQueue.with_n_workers nworkers (fun queue -> @@ -1989,7 +1988,7 @@ end = struct (* {{{ *) VCS.print (); Reach.known_state ~cache:`No r_where; (* STATE *) - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in try (* STATE SPEC: * - start: r_where @@ -2203,7 +2202,7 @@ let known_state ?(redefine_qed=false) ~cache id = Proofview.give_up else Proofview.tclUNIT () end in match (VCS.get_info base_state).state with - | Valid { Vernacentries.proof } -> + | Valid { Vernacstate.proof } -> Proof_global.unfreeze proof; Proof_global.with_current_proof (fun _ p -> feedback ~id:id Feedback.AddedAxiom; @@ -2213,7 +2212,7 @@ let known_state ?(redefine_qed=false) ~cache id = * - end : maybe after recovery command. *) (* STATE: We use an updated state with proof *) - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in Option.iter (fun expr -> ignore(stm_vernac_interp id st { verbose = true; loc = None; expr; indentation = 0; strlen = 0 } )) @@ -2293,7 +2292,7 @@ let known_state ?(redefine_qed=false) ~cache id = resilient_tactic id cblock (fun () -> reach view.next; (* State resulting from reach *) - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x) ); if eff then update_global_env () @@ -2303,13 +2302,13 @@ let known_state ?(redefine_qed=false) ~cache id = | Flags.APon | Flags.APonLazy -> resilient_command reach view.next | Flags.APoff -> reach view.next); - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); if eff then update_global_env () ), (if eff then `Yes else cache), true | `Fork ((x,_,_,_), None) -> (fun () -> resilient_command reach view.next; - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); wall_clock_last_fork := Unix.gettimeofday () ), `Yes, true @@ -2318,7 +2317,7 @@ let known_state ?(redefine_qed=false) ~cache id = reach view.next; (try - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); with e when CErrors.noncritical e -> let (e, info) = CErrors.push e in @@ -2369,7 +2368,7 @@ let known_state ?(redefine_qed=false) ~cache id = Proof_global.close_future_proof ~feedback_id:id fp in if not delegate then ignore(Future.compute fp); reach view.next; - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id ~proof st x); feedback ~id:id Incomplete | { VCS.kind = `Master }, _ -> assert false @@ -2378,7 +2377,7 @@ let known_state ?(redefine_qed=false) ~cache id = ), (if redefine_qed then `No else `Yes), true | `Sync (name, `Immediate) -> (fun () -> reach eop; - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); Proof_global.discard_all () ), `Yes, true @@ -2401,7 +2400,7 @@ let known_state ?(redefine_qed=false) ~cache id = if keep != VtKeepAsAxiom then reach view.next; let wall_clock2 = Unix.gettimeofday () in - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id ?proof st x); let wall_clock3 = Unix.gettimeofday () in Aux_file.record_in_aux_at ?loc:x.loc "proof_check_time" @@ -2419,7 +2418,7 @@ let known_state ?(redefine_qed=false) ~cache id = aux (collect_proof keep (view.next, x) brname brinfo eop) | `Sideff (ReplayCommand x,_) -> (fun () -> reach view.next; - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); update_global_env () ), cache, true @@ -2688,7 +2687,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) | VtQuery (false,route), VtNow -> let query_sid = VCS.cur_tip () in (try - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp ~route query_sid st x) with e -> let e = CErrors.push e in @@ -2762,7 +2761,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) (* Side effect on all branches *) | VtUnknown, _ when expr = VernacToplevelControl Drop -> - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp (VCS.get_branch_pos head) st x); `Ok @@ -2790,7 +2789,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) VCS.checkout VCS.Branch.master; let mid = VCS.get_branch_pos VCS.Branch.master in let _st' = Reach.known_state ~cache:(VCS.is_interactive ()) mid in - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); (* Vernac x may or may not start a proof *) if not in_proof && Proof_global.there_are_pending_proofs () then diff --git a/stm/stm.mli b/stm/stm.mli index 31f4599d3..9fd35a0d3 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -220,7 +220,7 @@ val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t val get_doc : Feedback.doc_id -> doc val state_of_id : doc:doc -> - Stateid.t -> [ `Valid of Vernacentries.interp_state option | `Expired | `Error of exn ] + Stateid.t -> [ `Valid of Vernacstate.t option | `Expired | `Error of exn ] (* Queries for backward compatibility *) val current_proof_depth : doc:doc -> int -- cgit v1.2.3