From 19bbc3fd946555aa1fa1fc23d805a4eb3d13bc45 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 27 May 2017 23:22:04 +0200 Subject: [stm] Move interpretation state to Vernacentries We still don't thread the state there, but this is a start of the needed infrastructure. --- vernac/vernacentries.ml | 19 +++++++++++++++++++ vernac/vernacentries.mli | 13 ++++++++++++- 2 files changed, 31 insertions(+), 1 deletion(-) (limited to 'vernac') diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 66427b7093..7f2985aca7 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2227,3 +2227,22 @@ let interp ?(verbosely=true) ?proof (loc,c) = in 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 diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index a09011d245..5559e6b81b 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -14,11 +14,22 @@ val dump_global : Libnames.reference or_by_notation -> unit val vernac_require : Libnames.reference option -> bool option -> Libnames.reference list -> unit +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) *) +} + +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 : ?verbosely:bool -> ?proof:Proof_global.closed_proof -> - Vernacexpr.vernac_expr Loc.located -> unit + interp_state -> + Vernacexpr.vernac_expr Loc.located -> interp_state (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name -- cgit v1.2.3 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 a1a87d54e0..f095a5d6cf 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 d45665dd4c..9ab89c8832 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 7f2985aca7..13b6eafc22 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 5559e6b81b..56635c8011 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 From 286d387082fb0f86858dce661c789bdcb802c295 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 25 Sep 2017 21:38:44 +0200 Subject: [vernac] [state] Cache freeze/unfreeze Users need to be careful wrt global state modification outside `Vernacentries` without registering the functions. In particular, our fail implementation also has to invalidate the cache. --- vernac/vernacentries.ml | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) (limited to 'vernac') diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 13b6eafc22..b7a8612148 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2154,16 +2154,21 @@ type interp_state = { (* TODO: inline records in OCaml 4.03 *) 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 s_cache = ref (States.freeze ~marshallable:`No) +let s_proof = ref (Proof_global.freeze ~marshallable:`No) + +let invalidate_cache () = + s_cache := Obj.magic 0; + s_proof := Obj.magic 0 + let freeze_interp_state marshallable = - { system = States.freeze ~marshallable; - proof = Proof_global.freeze ~marshallable; + { system = (s_cache := States.freeze ~marshallable; !s_cache); + proof = (s_proof := Proof_global.freeze ~marshallable; !s_proof); shallow = marshallable = `Shallow } let unfreeze_interp_state { system; proof } = - States.unfreeze system; - Proof_global.unfreeze proof + if (!s_cache != system) then (s_cache := system; States.unfreeze system); + if (!s_proof != proof) then (s_proof := proof; Proof_global.unfreeze proof) (* XXX STATE: this type hints that restoring the state should be the caller's responsibility *) @@ -2182,7 +2187,8 @@ let with_fail st b f = raise (HasFailed (CErrors.iprint (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e))) with e when CErrors.noncritical e -> - (* Restore the previous state *) + (* Restore the previous state XXX Careful here with the cache! *) + invalidate_cache (); unfreeze_interp_state st; let (e, _) = CErrors.push e in match e with -- cgit v1.2.3