diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-28 00:35:57 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-10-17 02:19:11 +0200 |
commit | 280be11cb4706e039cf4e9f68a5ae38b0aef9340 (patch) | |
tree | e1e1a1a8465076e0fe6e95566f14d7ea0f960813 /kernel | |
parent | 19bbc3fd946555aa1fa1fc23d805a4eb3d13bc45 (diff) |
[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
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/opaqueproof.ml | 16 | ||||
-rw-r--r-- | kernel/term_typing.ml | 6 |
2 files changed, 11 insertions, 11 deletions
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 5e20c1b51..400f9feee 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -78,12 +78,12 @@ let subst_opaque sub = function let iter_direct_opaque f = function | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") | Direct (d,cu) -> - Direct (d,Future.chain ~pure:true cu (fun (c, u) -> f c; c, u)) + Direct (d,Future.chain cu (fun (c, u) -> f c; c, u)) let discharge_direct_opaque ~cook_constr ci = function | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") | Direct (d,cu) -> - Direct (ci::d,Future.chain ~pure:true cu (fun (c, u) -> cook_constr c, u)) + Direct (ci::d,Future.chain cu (fun (c, u) -> cook_constr c, u)) let join_opaque { opaque_val = prfs; opaque_dir = odp } = function | Direct (_,cu) -> ignore(Future.join cu) @@ -105,7 +105,7 @@ let force_proof { opaque_val = prfs; opaque_dir = odp } = function | Indirect (l,dp,i) -> let pt = if DirPath.equal dp odp - then Future.chain ~pure:true (snd (Int.Map.find i prfs)) fst + then Future.chain (snd (Int.Map.find i prfs)) fst else !get_opaque dp i in let c = Future.force pt in force_constr (List.fold_right subst_substituted l (from_val c)) @@ -120,20 +120,20 @@ let force_constraints { opaque_val = prfs; opaque_dir = odp } = function | Some u -> Future.force u let get_constraints { opaque_val = prfs; opaque_dir = odp } = function - | Direct (_,cu) -> Some(Future.chain ~pure:true cu snd) + | Direct (_,cu) -> Some(Future.chain cu snd) | Indirect (_,dp,i) -> if DirPath.equal dp odp - then Some(Future.chain ~pure:true (snd (Int.Map.find i prfs)) snd) + then Some(Future.chain (snd (Int.Map.find i prfs)) snd) else !get_univ dp i let get_proof { opaque_val = prfs; opaque_dir = odp } = function - | Direct (_,cu) -> Future.chain ~pure:true cu fst + | Direct (_,cu) -> Future.chain cu fst | Indirect (l,dp,i) -> let pt = if DirPath.equal dp odp - then Future.chain ~pure:true (snd (Int.Map.find i prfs)) fst + then Future.chain (snd (Int.Map.find i prfs)) fst else !get_opaque dp i in - Future.chain ~pure:true pt (fun c -> + Future.chain pt (fun c -> force_constr (List.fold_right subst_substituted l (from_val c))) module FMap = Future.UUIDMap diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 22e109b01..f93b24b3e 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -266,7 +266,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let tyj = infer_type env typ in let proofterm = - Future.chain ~pure:true body (fun ((body,uctx),side_eff) -> + Future.chain body (fun ((body,uctx),side_eff) -> let j, uctx = match trust with | Pure -> let env = push_context_set uctx env in @@ -535,7 +535,7 @@ let export_side_effects mb env ce = let { const_entry_body = body } = c in let _, eff = Future.force body in let ce = DefinitionEntry { c with - const_entry_body = Future.chain ~pure:true body + const_entry_body = Future.chain body (fun (b_ctx, _) -> b_ctx, ()) } in let not_exists (c,_,_,_) = try ignore(Environ.lookup_constant c env); false @@ -628,7 +628,7 @@ let translate_local_def mb env id centry = let translate_mind env kn mie = Indtypes.check_inductive env kn mie let inline_entry_side_effects env ce = { ce with - const_entry_body = Future.chain ~pure:true + const_entry_body = Future.chain ce.const_entry_body (fun ((body, ctx), side_eff) -> let body, ctx',_ = inline_side_effects env body ctx side_eff in (body, ctx'), ()); |