diff options
| -rw-r--r-- | checker/values.ml | 6 | ||||
| -rw-r--r-- | kernel/cooking.ml | 2 | ||||
| -rw-r--r-- | kernel/declareops.ml | 16 | ||||
| -rw-r--r-- | kernel/declareops.mli | 1 | ||||
| -rw-r--r-- | kernel/modops.ml | 28 | ||||
| -rw-r--r-- | kernel/modops.mli | 4 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 22 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 2 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 9 | ||||
| -rw-r--r-- | lib/future.ml | 108 | ||||
| -rw-r--r-- | lib/future.mli | 48 | ||||
| -rw-r--r-- | library/global.ml | 5 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 14 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 6 | ||||
| -rw-r--r-- | toplevel/command.ml | 3 | ||||
| -rw-r--r-- | toplevel/lemmas.ml | 3 | ||||
| -rw-r--r-- | toplevel/stm.ml | 36 |
17 files changed, 121 insertions, 192 deletions
diff --git a/checker/values.ml b/checker/values.ml index 55c6367a7..9a0d9922f 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -69,10 +69,8 @@ let v_map vk vd = let v_computation f = Annot ("Future.computation", v_ref - (v_sum "computation" 2 - [| [| Fail "Closure" |]; - [| f ; v_sum "option" 1 [| [| Fail "Val(_,Some _)" |] |] |]; - [| Fail "Exn" |] |])) + (v_sum "Future.comput" 0 + [| [| Fail "Ongoing" |]; [| f |] |])) (** kernel/names *) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 4c2f22199..dbe83a856 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -126,7 +126,7 @@ let on_body f = function | Undef _ as x -> x | Def cs -> Def (Lazyconstr.from_val (f (Lazyconstr.force cs))) | OpaqueDef lc -> - OpaqueDef (Future.chain ~id:"Cooking.on_body" ~pure:true lc (fun lc -> + OpaqueDef (Future.chain lc (fun lc -> (Lazyconstr.opaque_from_val (f (Lazyconstr.force_opaque lc))))) let constr_of_def = function diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 973859ede..3083c1738 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -52,8 +52,7 @@ let subst_const_type sub arity = match arity with let subst_const_def sub def = match def with | Undef _ -> def | Def c -> Def (subst_constr_subst sub c) - | OpaqueDef lc -> - OpaqueDef (Future.chain ~pure:true lc (subst_lazy_constr sub)) + | OpaqueDef lc -> OpaqueDef (Future.chain lc (subst_lazy_constr sub)) (* TODO : the native compiler seems to rely on a fresh (ref NotLinked) being created at each substitution. Quite ugly... For the moment, @@ -100,7 +99,7 @@ let hcons_const_def = function Def (from_val (Term.hcons_constr constr)) | OpaqueDef lc -> OpaqueDef - (Future.chain ~pure:true lc + (Future.chain lc (fun lc -> opaque_from_val (Term.hcons_constr (force_opaque lc)))) let hcons_const_body cb = @@ -242,17 +241,6 @@ let join_constant_body cb = | OpaqueDef d -> ignore(Future.join d) | _ -> () -let prune_constant_body cb = - let cst, cbo = cb.const_constraints, cb.const_body in - let cst' = Future.drop cst in - let cbo' = match cbo with - | OpaqueDef d -> - let d' = Future.drop d in - if d' == d then cbo else OpaqueDef d' - | _ -> cbo in - if cst' == cst && cbo' == cbo then cb - else {cb with const_constraints = cst'; const_body = cbo'} - let string_of_side_effect = function | SEsubproof (c,_) -> Names.string_of_con c | SEscheme (cl,_) -> diff --git a/kernel/declareops.mli b/kernel/declareops.mli index f593b4547..177ae9d45 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -59,7 +59,6 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body val join_constant_body : constant_body -> unit -val prune_constant_body : constant_body -> constant_body (** {6 Hash-consing} *) diff --git a/kernel/modops.ml b/kernel/modops.ml index 76feb8498..6a0a952f7 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -592,7 +592,7 @@ let rec collect_mbid l sign = match sign with let clean_bounded_mod_expr sign = if is_functor sign then collect_mbid MBIset.empty sign else sign -(** {6 Stm machinery : join and prune } *) +(** {6 Stm machinery } *) let rec join_module mb = implem_iter join_signature join_expression mb.mod_expr; @@ -610,29 +610,3 @@ and join_structure struc = List.iter join_field struc and join_signature sign = functor_iter join_modtype join_structure sign and join_expression me = functor_iter join_modtype (fun _ -> ()) me -let rec prune_module mb = - let me, mta, mt = mb.mod_expr, mb.mod_type_alg, mb.mod_type in - let mt' = prune_signature mt in - let me' = implem_smartmap prune_signature prune_expression me in - let mta' = Option.smartmap prune_expression mta in - if me' == me && mta' == mta && mt' == mt then mb - else {mb with mod_expr = me'; mod_type_alg = mta'; mod_type = mt'} -and prune_modtype mt = - let te, ta = mt.typ_expr, mt.typ_expr_alg in - let te' = prune_signature te in - let ta' = Option.smartmap prune_expression ta in - if te==te' && ta==ta' then mt else { mt with typ_expr=te'; typ_expr_alg=ta' } -and prune_field (l,body as orig) = match body with - |SFBconst sb -> - let sb' = prune_constant_body sb in - if sb == sb' then orig else (l, SFBconst sb') - |SFBmind _ -> orig - |SFBmodule m -> - let m' = prune_module m in - if m == m' then orig else (l, SFBmodule m') - |SFBmodtype m -> - let m' = prune_modtype m in - if m == m' then orig else (l, SFBmodtype m') -and prune_structure struc = List.smartmap prune_field struc -and prune_signature sign = functor_smartmap prune_modtype prune_structure sign -and prune_expression me = functor_smartmap prune_modtype (fun me -> me) me diff --git a/kernel/modops.mli b/kernel/modops.mli index 6aed95988..11eb876ad 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -76,13 +76,11 @@ val subst_modtype_and_resolver : module_type_body -> module_path -> val clean_bounded_mod_expr : module_signature -> module_signature -(** {6 Stm machinery : join and prune } *) +(** {6 Stm machinery } *) val join_module : module_body -> unit val join_structure : structure_body -> unit -val prune_structure : structure_body -> structure_body - (** {6 Errors } *) type signature_mismatch_error = diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 57e44a322..90d52572a 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -197,28 +197,6 @@ let join_safe_environment e = (fun e fc -> add_constraints (Now (Future.join fc)) e) {e with future_cst = []} e.future_cst -(* TODO : out of place and maybe incomplete w.r.t. modules *) -(* this is there to explore the opaque pre-env structure but is - * not part of the trusted code base *) -let prune_env env = - let open Pre_env in - let prune_ckey (cb,k) = Declareops.prune_constant_body cb, k in - let prune_globals glob = - { glob with env_constants = Cmap_env.map prune_ckey glob.env_constants } - in - let env = Environ.pre_env env in - Environ.env_of_pre_env {env with - env_globals = prune_globals env.env_globals; - env_named_vals = []; - env_rel_val = []} -let prune_safe_environment e = - { e with - modvariant = (match e.modvariant with LIBRARY -> LIBRARY | _ -> NONE); - revstruct = Modops.prune_structure e.revstruct; - future_cst = []; - env = prune_env e.env } - - (** {6 Various checks } *) let exists_modlabel l senv = Label.Set.mem l senv.modlabels diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index a56bb8578..b16d5b63d 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -43,8 +43,6 @@ val is_curmod_library : safe_environment -> bool (* safe_environment has functional data affected by lazy computations, * thus this function returns a new safe_environment *) val join_safe_environment : safe_environment -> safe_environment -(* future computations are just dropped by this function *) -val prune_safe_environment : safe_environment -> safe_environment (** {6 Enriching a safe environment } *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 567511c93..987621619 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -84,9 +84,8 @@ let infer_declaration ?(what="UNKNOWN") env dcl = | DefinitionEntry c -> let ctx, entry_body = c.const_entry_secctx, c.const_entry_body in if c.const_entry_opaque && not (Option.is_empty c.const_entry_type) then - let id = "infer_declaration " ^ what in let body_cst = - Future.chain ~id entry_body (fun (body, side_eff) -> + Future.chain entry_body (fun (body, side_eff) -> let body = handle_side_effects env body side_eff in let j, cst = infer env body in let j = @@ -163,7 +162,7 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) = check declared inferred; x | OpaqueDef lc -> (* In this case we can postpone the check *) - OpaqueDef (Future.chain ~id:(string_of_con kn) lc (fun lc -> + OpaqueDef (Future.chain lc (fun lc -> let ids_typ = global_vars_set_constant_type env typ in let ids_def = global_vars_set env (Lazyconstr.force_opaque lc) in @@ -198,7 +197,7 @@ let translate_local_def env id centry = let translate_mind env kn mie = Indtypes.check_inductive env kn mie let handle_side_effects env ce = { ce with - const_entry_body = Future.chain ~id:"handle_side_effects" + const_entry_body = Future.chain ce.const_entry_body (fun (body, side_eff) -> - handle_side_effects env body side_eff, Declareops.no_seff); + handle_side_effects env body side_eff, Declareops.no_seff); } diff --git a/lib/future.ml b/lib/future.ml index c1fb176df..b93d33640 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* to avoid side effects *) +(* To deal with side effects we have to save/restore the system state *) let freeze = ref (fun () -> assert false : unit -> Dyn.t) let unfreeze = ref (fun _ -> () : Dyn.t -> unit) let set_freeze f g = freeze := f; unfreeze := g @@ -26,59 +26,73 @@ let _ = Errors.register_handler (function "asynchronous script processing.") | _ -> raise Errors.Unhandled) +type fix_exn = exn -> exn +let id x = prerr_endline "no fix_exn"; x + (* Val is not necessarily a final state, so the computation restarts from the state stocked into Val *) type 'a comp = | Delegated - | Dropped + (* TODO in some cases one would like to block, sock here + a mutex and a condition to make this possible *) | Closure of (unit -> 'a) | Val of 'a * Dyn.t option | Exn of exn + (* Invariant: this exception is always "fixed" as in fix_exn *) + +type 'a comput = + | Ongoing of (fix_exn * 'a comp ref) Ephemeron.key + | Finished of 'a -type 'a computation = 'a comp ref +type 'a computation = 'a comput ref + +let create f x = ref (Ongoing (Ephemeron.create (f, Pervasives.ref x))) +let get x = + match !x with + | Finished v -> (fun x -> x), ref( Val (v,None)) + | Ongoing x -> + try Ephemeron.get x + with Ephemeron.InvalidKey -> (fun x -> x), ref (Exn NotHere) type 'a value = [ `Val of 'a | `Exn of exn ] -let is_over x = match !x with +let is_over kx = let _, x = get kx in match !x with | Val _ | Exn _ -> true - | Closure _ | Delegated | Dropped -> false + | Closure _ | Delegated -> false -let is_val x = match !x with +let is_val kx = let _, x = get kx in match !x with | Val _ -> true - | Exn _ | Closure _ | Delegated | Dropped -> false + | Exn _ | Closure _ | Delegated -> false -let is_exn x = match !x with +let is_exn kx = let _, x = get kx in match !x with | Exn _ -> true - | Val _ | Closure _ | Delegated | Dropped -> false + | Val _ | Closure _ | Delegated -> false -let peek_val x = match !x with +let peek_val kx = let _, x = get kx in match !x with | Val (v, _) -> Some v - | Exn _ | Closure _ | Delegated | Dropped -> None - -let from_val v = ref (Val (v, None)) -let from_here v = ref (Val (v, Some (!freeze ()))) -let proj = function - | `Val (x, _ ) -> `Val x - | `Exn e -> `Exn e + | Exn _ | Closure _ | Delegated -> None -let create f = ref (Closure f) +let from_val ?(fix_exn=id) v = create fix_exn (Val (v, None)) +let from_here ?(fix_exn=id) v = create fix_exn (Val (v, Some (!freeze ()))) type 'a assignement = [ `Val of 'a | `Exn of exn | `Comp of 'a computation] -let create_delegate () = - let c = ref Delegated in - c, (fun v -> - assert (!c == Delegated); - match v with - | `Val v -> c := Val (v, None) - | `Exn e -> c := Exn e - | `Comp f -> c := !f) - -(* TODO: get rid of try/catch *) -let compute ~pure c : 'a value = match !c with +let create_delegate fix_exn = + let ck = create fix_exn Delegated in + ck, fun v -> + let fix_exn, c = get ck in + assert (!c == Delegated); + match v with + | `Val v -> c := Val (v, None) + | `Exn e -> c := Exn (fix_exn e) + | `Comp f -> let _, comp = get f in c := !comp + +(* TODO: get rid of try/catch to be stackless *) +let compute ~pure ck : 'a value = + let fix_exn, c = get ck in + match !c with | Val (x, _) -> `Val x | Exn e -> `Exn e | Delegated -> `Exn NotReady - | Dropped -> `Exn NotHere | Closure f -> try let data = f () in @@ -86,6 +100,7 @@ let compute ~pure c : 'a value = match !c with c := Val (data, state); `Val data with e -> let e = Errors.push e in + let e = fix_exn e in match e with | NotReady -> `Exn e | _ -> c := Exn e; `Exn e @@ -94,20 +109,19 @@ let force ~pure x = match compute ~pure x with | `Val v -> v | `Exn e -> raise e -let drop c = match !c with Closure _ | Val (_,Some _) -> ref Dropped | _ -> c - -let chain ?(id="none") ?(pure=false) c f = ref (match !c with - | Closure _ | Delegated | Dropped -> Closure (fun () -> f (force ~pure c)) +let chain ?(pure=false) ck f = + let fix_exn, c = get ck in + create fix_exn (match !c with + | Closure _ | Delegated -> Closure (fun () -> f (force ~pure ck)) | Exn _ as x -> x | Val (v, None) -> Closure (fun () -> f v) | Val (v, Some _) when pure -> Closure (fun () -> f v) - | Val (v, Some state) -> -(* prerr_endline ("Future: restarting (check if optimizable): " ^ id); *) - Closure (fun () -> !unfreeze state; f v)) + | Val (v, Some state) -> Closure (fun () -> !unfreeze state; f v)) -let create_here f = chain ~pure:false (from_here ()) f +let create fix_exn f = create fix_exn (Closure f) -let replace x y = +let replace kx y = + let _, x = get kx in match !x with | Exn _ -> x := Closure (fun () -> force ~pure:false y) | _ -> Errors.anomaly (Pp.str "Only Exn futures can be replaced") @@ -125,19 +139,13 @@ let transactify f x = try f x with e -> let e = Errors.push e in !unfreeze state; raise e -let purify_future f x = - match !x with - | Val _ | Exn _ | Delegated | Dropped -> f x - | Closure _ -> purify f x - +let purify_future f x = if is_over x then f x else purify f x let compute x = purify_future (compute ~pure:false) x let force x = purify_future (force ~pure:false) x -let join x = - let v = force x in - (x := match !x with - | Val (x,_) -> Val (x, None) - | Exn _ | Delegated | Dropped | Closure _ -> assert false); +let join kx = + let v = force kx in + kx := Finished v; v let split2 x = @@ -156,3 +164,5 @@ let map2 f x l = with Failure _ | Invalid_argument _ -> Errors.anomaly (Pp.str "Future.map2 length mismatch")) in f xi y) 0 l + +let chain f g = chain f g diff --git a/lib/future.mli b/lib/future.mli index a1535b13d..4ba601976 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -6,48 +6,51 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Futures: for now lazy computations with some purity enforcing *) -(* TODO: it may be worth separating in the type pure and inpure computations *) +(* Futures: asynchronous computations with some purity enforcing *) exception NotReady type 'a computation type 'a value = [ `Val of 'a | `Exn of exn ] +type fix_exn = exn -> exn -(* Build a computation *) -val create : (unit -> 'a) -> 'a computation -val from_val : 'a -> 'a computation +(* Build a computation. fix_exn is used to enrich any exception raised + by forcing the computations or any computation that is chained after + it. It is used by STM to attach errors to their corresponding states, + and to communicate to the code catching the exception a valid state id. *) +val create : fix_exn -> (unit -> 'a) -> 'a computation + +(* Usually from_val is used to create "fake" futures, to use the same API + as if a real asynchronous computations was there. In this case fixing + the exception is not needed, but *if* the future is chained, the fix_exn + argument should really be given *) +val from_val : ?fix_exn:fix_exn -> 'a -> 'a computation + +(* Like from_val, but also takes a snapshot of the global state. Morally + the value is not just the 'a but also the global system state *) +val from_here : ?fix_exn:fix_exn -> 'a -> 'a computation (* Run remotely, returns the function to assign *) type 'a assignement = [ `Val of 'a | `Exn of exn | `Comp of 'a computation] -val create_delegate : unit -> 'a computation * ('a assignement -> unit) +val create_delegate : fix_exn -> 'a computation * ('a assignement -> unit) (* Given a computation that is_exn, replace it by another one *) val replace : 'a computation -> 'a computation -> unit -(* Variants to stock a copy of the current environment *) -val create_here : (unit -> 'a) -> 'a computation -val from_here : 'a -> 'a computation - (* Inspect a computation *) val is_over : 'a computation -> bool val is_val : 'a computation -> bool val is_exn : 'a computation -> bool val peek_val : 'a computation -> 'a option -(* Chain computations. - Note that in [chain c f], f will execute in an environment modified by c - unless ~pure:true *) -val chain : - ?id:string -> ?pure:bool -> 'a computation -> ('a -> 'b) -> 'b computation +(* Chain computations. *) +val chain : 'a computation -> ('a -> 'b) -> 'b computation (* Forcing a computation *) val force : 'a computation -> 'a val compute : 'a computation -> 'a value -val drop : 'a computation -> 'a computation - -(* Final call, no more impure chain allowed since the state is lost *) +(* Final call, no more chain allowed since the state is lost *) val join : 'a computation -> 'a (* Utility *) @@ -58,11 +61,14 @@ val map2 : ('a computation -> 'b -> 'c) -> 'a list computation -> 'b list -> 'c list -(* These functions are needed to get rid of side effects *) -val set_freeze : (unit -> Dyn.t) -> (Dyn.t -> unit) -> unit - (* Once set_freeze is called we can purify a computation *) val purify : ('a -> 'b) -> 'a -> 'b (* And also let a function alter the state but backtrack if it raises exn *) val transactify : ('a -> 'b) -> 'a -> 'b +(* These functions are needed to get rid of side effects. + Thy are set for the outermos layer of the system, since they have to + deal with the whole system state. *) +val set_freeze : (unit -> Dyn.t) -> (Dyn.t -> unit) -> unit + + diff --git a/library/global.ml b/library/global.ml index fd6cce46f..3b0e504d8 100644 --- a/library/global.ml +++ b/library/global.ml @@ -26,15 +26,12 @@ let global_env = ref Safe_typing.empty_environment let join_safe_environment () = global_env := Safe_typing.join_safe_environment !global_env -let prune_safe_environment env = Safe_typing.prune_safe_environment env -(* XXX TODO pass args so that these functions can stop at the current - * file boundaries *) let () = Summary.declare_summary "Global environment" { Summary.freeze_function = (function | `Yes -> join_safe_environment (); !global_env | `No -> !global_env - | `Shallow -> prune_safe_environment !global_env); + | `Shallow -> !global_env); unfreeze_function = (fun fr -> global_env := fr); init_function = (fun () -> global_env := Safe_typing.empty_environment) } diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 81bfcacce..08eaa30f5 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -277,18 +277,18 @@ let close_proof ~now fpl = List.iter (fun x -> ignore(Future.compute x.Entries.const_entry_body)) entries; (pid, (entries, compute_guard, strength, hook)) -let return_proof ~fix_exn = +let return_proof () = let { proof } = cur_pstate () in let initial_goals = Proof.initial_goals proof in let evd = try Proof.return proof with | Proof.UnfinishedProof -> - raise (fix_exn(Errors.UserError("last tactic before Qed", - str"Attempt to save an incomplete proof"))) + raise (Errors.UserError("last tactic before Qed", + str"Attempt to save an incomplete proof")) | Proof.HasUnresolvedEvar -> - raise (fix_exn(Errors.UserError("last tactic before Qed", + raise (Errors.UserError("last tactic before Qed", str"Attempt to save a proof with existential " ++ - str"variables still non-instantiated"))) + str"variables still non-instantiated")) in let eff = Evd.eval_side_effects evd in (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate @@ -297,8 +297,8 @@ let return_proof ~fix_exn = List.map (fun (c, _) -> (Evarutil.nf_evar evd c, eff)) initial_goals let close_future_proof proof = close_proof ~now:false proof -let close_proof () = - close_proof ~now:true (Future.from_here (return_proof ~fix_exn:(fun x -> x))) +let close_proof fix_exn = + close_proof ~now:true (Future.from_here ~fix_exn (return_proof ())) (**********************************************************) (* *) diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 5922075ec..9d7407010 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -64,12 +64,14 @@ type closed_proof = (Entries.definition_entry list * lemma_possible_guards * Decl_kinds.goal_kind * unit Tacexpr.declaration_hook) -val close_proof : unit -> closed_proof +(* Takes a function to add to the exceptions data relative to the + state in which the proof was built *) +val close_proof : (exn -> exn) -> closed_proof (* Intermediate step necessary to delegate the future. * Both access the current proof state. The formes is supposed to be * chained with a computation that completed the proof *) -val return_proof : fix_exn:(exn -> exn) -> Entries.proof_output list +val return_proof : unit -> Entries.proof_output list val close_future_proof : Entries.proof_output list Future.computation -> closed_proof diff --git a/toplevel/command.ml b/toplevel/command.ml index 308bdc07d..9efe4eefc 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -68,8 +68,7 @@ let red_constant_entry n ce = function | None -> ce | Some red -> let proof_out = ce.const_entry_body in - { ce with const_entry_body = Future.chain ~id:"red_constant_entry" - proof_out (fun (body,eff) -> + { ce with const_entry_body = Future.chain proof_out (fun (body,eff) -> under_binders (Global.env()) (fst (reduction_of_red_expr red)) n body,eff) } diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 43aefc722..5a936e623 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -48,9 +48,8 @@ let adjust_guardness_conditions const = function | [] -> const (* Not a recursive statement *) | possible_indexes -> (* Try all combinations... not optimal *) - (* XXX bug ignore(Future.join const.const_entry_body); *) { const with const_entry_body = - Future.chain ~id:"adjust_guardness_conditions" const.const_entry_body + Future.chain const.const_entry_body (fun (body, eff) -> match kind_of_term body with | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 789b56914..487120b27 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -201,9 +201,8 @@ module VCS : sig val set_state : id -> state -> unit val forget_state : id -> unit - (* TODO: move elsewhere if possible, so that purify can be just called *) (* cuts from start -> stop, raising Expired if some nodes are not there *) - val slice : start:id -> stop:id -> purify:(state -> state) -> vcs + val slice : start:id -> stop:id -> vcs val create_cluster : id list -> tip:id -> unit val cluster_of : id -> id option @@ -391,7 +390,7 @@ end = struct (* {{{ *) let visit id = Vcs_aux.visit !vcs id - let slice ~start ~stop ~purify = + let slice ~start ~stop = let l = let rec aux id = if Stateid.equal id stop then [] else @@ -408,9 +407,7 @@ end = struct (* {{{ *) (* Stm should have reached the beginning of proof *) assert (not (Option.is_empty info.state)); (* This may be expensive *) - let info = { info with - state = Some (purify (Option.get info.state)); - vcs_backup = None,None } in + let info = { info with vcs_backup = None, None } in let v = Vcs_.set_info v stop info in List.fold_right (fun (id,tr) v -> let v = Vcs_.commit v id tr in @@ -499,10 +496,6 @@ module State : sig val exn_on : Stateid.t -> ?valid:Stateid.t -> exn -> exn - (* projects a state so that it can be marshalled and its content is - * sufficient for the execution of Coq on a proof branch *) - val make_shallow : state -> state - end = struct (* {{{ *) (* cur_id holds Stateid.dummy in case the last attempt to define a state @@ -523,15 +516,6 @@ end = struct (* {{{ *) (fun () -> in_t (freeze_global_state `No, !cur_id)) (fun t -> let s,i = out_t t in unfreeze_global_state s; cur_id := i) - let make_shallow s = - if s.shallow then s - else - Future.purify (fun s -> - Printf.eprintf - "make_shallow & define should be protected by a lock!\n"; - unfreeze_global_state s; - freeze_global_state `Shallow) s - let is_cached id = Stateid.equal id !cur_id || match VCS.get_info id with @@ -734,16 +718,15 @@ end = struct (* {{{ *) match task with | TaskBuildProof (exn_info,bop,eop,_,_) -> ReqBuildProof(exn_info,eop, - VCS.slice ~start:eop ~stop:bop ~purify:State.make_shallow) + VCS.slice ~start:eop ~stop:bop) let cancel_switch_of_task = function | TaskBuildProof (_,_,_,_,c) -> c let build_proof_here (id,valid) eop = - Future.create (fun () -> + Future.create (State.exn_on id ~valid) (fun () -> !reach_known_state ~cache:`No eop; - let p = Proof_global.return_proof ~fix_exn:(State.exn_on id ~valid) in - p) + Proof_global.return_proof ()) let slave_respond msg = match msg with @@ -811,12 +794,12 @@ end = struct (* {{{ *) TQueue.wait_until_n_are_waiting_and_queue_empty (SlavesPool.n_slaves ()) queue - let build_proof ~exn_info ~start ~stop = + let build_proof ~exn_info:(id,valid as exn_info) ~start ~stop = let cancel_switch = ref false in if SlavesPool.is_empty () then build_proof_here exn_info stop, cancel_switch else - let f, assign = Future.create_delegate () in + let f, assign = Future.create_delegate (State.exn_on id ~valid) in Pp.feedback (Interface.InProgress 1); TQueue.push queue (TaskBuildProof(exn_info,start,stop,assign,cancel_switch)); @@ -1120,7 +1103,8 @@ let known_state ?(redefine_qed=false) ~cache id = reach eop; begin match keep with | VtKeep -> - let proof = Proof_global.close_proof () in + let proof = + Proof_global.close_proof (State.exn_on id ~valid:eop) in reach view.next; vernac_interp id ~proof x | VtDrop -> |