From 280be11cb4706e039cf4e9f68a5ae38b0aef9340 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 28 May 2017 00:35:57 +0200 Subject: [stm] Remove state-handling from Futures. We make Vernacentries.interp functional wrt state, and thus remove state-handling from `Future`. Now, a future needs a closure if it wants to preserve state. Consequently, `Vernacentries.interp` takes a state, and returns the new one. We don't explicitly thread the state in the STM yet, instead, we recover the state that was used before and pass it explicitly to `interp`. I have tested the commit with the files in interactive, but we aware that some new bugs may appear or old ones be made more apparent. However, I am confident that this step will improve our understanding of bugs. In some cases, we perform a bit more summary wrapping/unwrapping. This will go away in future commits; informal timings for a full make: - master: real 2m11,027s user 8m30,904s sys 1m0,000s - no_futures: real 2m8,474s user 8m34,380s sys 0m59,156s --- vernac/command.ml | 2 +- vernac/lemmas.ml | 2 +- vernac/vernacentries.ml | 67 ++++++++++++++++++++++++++---------------------- vernac/vernacentries.mli | 5 ++-- 4 files changed, 41 insertions(+), 35 deletions(-) (limited to 'vernac') diff --git a/vernac/command.ml b/vernac/command.ml index a1a87d54e..f095a5d6c 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -79,7 +79,7 @@ let red_constant_entry n ce sigma = function let (_, c) = redfun env sigma c in EConstr.Unsafe.to_constr c in - { ce with const_entry_body = Future.chain ~pure:true proof_out + { ce with const_entry_body = Future.chain proof_out (fun ((body,ctx),eff) -> (under_binders env sigma redfun n body,ctx),eff) } let warn_implicits_in_term = diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index d45665dd4..9ab89c883 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -60,7 +60,7 @@ let adjust_guardness_conditions const = function (* Try all combinations... not optimal *) let env = Global.env() in { const with const_entry_body = - Future.chain ~pure:true const.const_entry_body + Future.chain const.const_entry_body (fun ((body, ctx), eff) -> match kind_of_term body with | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 7f2985aca..13b6eafc2 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2148,23 +2148,42 @@ let locate_if_not_already ?loc (e, info) = exception HasNotFailed exception HasFailed of Pp.t -let with_fail b f = - if not b then f () +type interp_state = { (* TODO: inline records in OCaml 4.03 *) + system : States.state; (* summary + libstack *) + proof : Proof_global.state; (* proof state *) + shallow : bool (* is the state trimmed down (libstack) *) +} + +(* Unfortunately we cannot cache here due to some bits in the STM not + being fully pure. *) +let freeze_interp_state marshallable = + { system = States.freeze ~marshallable; + proof = Proof_global.freeze ~marshallable; + shallow = marshallable = `Shallow } + +let unfreeze_interp_state { system; proof } = + States.unfreeze system; + Proof_global.unfreeze proof + +(* XXX STATE: this type hints that restoring the state should be the + caller's responsibility *) +let with_fail st b f = + if not b + then f () else begin try (* If the command actually works, ignore its effects on the state. * Note that error has to be printed in the right state, hence * within the purified function *) - Future.purify - (fun v -> - try f v; raise HasNotFailed - with - | HasNotFailed as e -> raise e - | e -> - let e = CErrors.push e in - raise (HasFailed (CErrors.iprint - (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e)))) - () + try f (); raise HasNotFailed + with + | HasNotFailed as e -> raise e + | e -> + let e = CErrors.push e in + raise (HasFailed (CErrors.iprint + (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e))) with e when CErrors.noncritical e -> + (* Restore the previous state *) + unfreeze_interp_state st; let (e, _) = CErrors.push e in match e with | HasNotFailed -> @@ -2175,7 +2194,7 @@ let with_fail b f = | _ -> assert false end -let interp ?(verbosely=true) ?proof (loc,c) = +let interp ?(verbosely=true) ?proof st (loc,c) = let orig_program_mode = Flags.is_program_mode () in let rec aux ?locality ?polymorphism isprogcmd = function @@ -2188,7 +2207,7 @@ let interp ?(verbosely=true) ?proof (loc,c) = | VernacPolymorphic (b, c) -> user_err Pp.(str "Polymorphism specified twice") | VernacLocal _ -> user_err Pp.(str "Locality specified twice") | VernacFail v -> - with_fail true (fun () -> aux ?locality ?polymorphism isprogcmd v) + with_fail st true (fun () -> aux ?locality ?polymorphism isprogcmd v) | VernacTimeout (n,v) -> current_timeout := Some n; aux ?locality ?polymorphism isprogcmd v @@ -2228,21 +2247,7 @@ let interp ?(verbosely=true) ?proof (loc,c) = if verbosely then Flags.verbosely (aux false) c else aux false c -type interp_state = { (* TODO: inline records in OCaml 4.03 *) - system : States.state; (* summary + libstack *) - proof : Proof_global.state; (* proof state *) - shallow : bool (* is the state trimmed down (libstack) *) -} - -let freeze_interp_state marshallable = - { system = States.freeze ~marshallable; - proof = Proof_global.freeze ~marshallable; - shallow = (marshallable = `Shallow) } - -let unfreeze_interp_state { system; proof } = - States.unfreeze system; Proof_global.unfreeze proof - -let _dummy_interp_state = { system = Obj.magic 0; proof = Obj.magic 0; shallow = false } - let interp ?verbosely ?proof st cmd = - interp ?verbosely ?proof cmd; st + unfreeze_interp_state st; + interp ?verbosely ?proof st cmd; + freeze_interp_state `No diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 5559e6b81..56635c801 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -22,7 +22,6 @@ type interp_state = { (* TODO: inline records in OCaml 4.03 *) val freeze_interp_state : Summary.marshallable -> interp_state val unfreeze_interp_state : interp_state -> unit -val _dummy_interp_state : interp_state (** The main interpretation function of vernacular expressions *) val interp : @@ -39,7 +38,9 @@ val interp : val make_cases : string -> string list list -val with_fail : bool -> (unit -> unit) -> unit +(* XXX STATE: this type hints that restoring the state should be the + caller's responsibility *) +val with_fail : interp_state -> bool -> (unit -> unit) -> unit val command_focus : unit Proof.focus_kind -- cgit v1.2.3