From 77cf18eb844b45776b2ec67be9f71e8dd4ca002c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 30 Oct 2015 11:48:40 -0400 Subject: Add a way to get the right fix_exn in external vernacular commands involving Futures. --- library/declare.ml | 4 ++-- library/declare.mli | 3 ++- stm/stm.ml | 8 ++++++-- stm/stm.mli | 1 + toplevel/obligations.ml | 14 ++++++++------ 5 files changed, 19 insertions(+), 11 deletions(-) diff --git a/library/declare.ml b/library/declare.ml index 63e5a7224..5968fbf38 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -225,9 +225,9 @@ let declare_constant_common id cst = update_tables c; c -let definition_entry ?(opaque=false) ?(inline=false) ?types +let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body = - { const_entry_body = Future.from_val ((body,Univ.ContextSet.empty), eff); + { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); const_entry_secctx = None; const_entry_type = types; const_entry_polymorphic = poly; diff --git a/library/declare.mli b/library/declare.mli index fdbd23561..c6119a58a 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -48,7 +48,8 @@ type internal_flag = | UserIndividualRequest (* Defaut definition entries, transparent with no secctx or proj information *) -val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types -> +val definition_entry : ?fix_exn:Future.fix_exn -> + ?opaque:bool -> ?inline:bool -> ?types:types -> ?poly:polymorphic -> ?univs:Univ.universe_context -> ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry diff --git a/stm/stm.ml b/stm/stm.ml index 02361c738..42be4fca7 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -596,6 +596,7 @@ module State : sig ?safe_id:Stateid.t -> ?redefine:bool -> ?cache:Summary.marshallable -> ?feedback_processed:bool -> (unit -> unit) -> Stateid.t -> unit + val fix_exn_ref : (iexn -> iexn) ref val install_cached : Stateid.t -> unit val is_cached : ?cache:Summary.marshallable -> Stateid.t -> bool @@ -619,6 +620,7 @@ end = struct (* {{{ *) (* 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 + let fix_exn_ref = ref (fun x -> x) (* helpers *) let freeze_global_state marshallable = @@ -726,8 +728,10 @@ end = struct (* {{{ *) try prerr_endline("defining "^str_id^" (cache="^ if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)"); - (* set id and good id *) + let good_id = match safe_id with None -> !cur_id | Some id -> id in + fix_exn_ref := exn_on id ~valid:good_id; f (); + fix_exn_ref := (fun x -> x); if cache = `Yes then freeze `No id else if cache = `Shallow then freeze `Shallow id; prerr_endline ("setting cur id to "^str_id); @@ -2559,5 +2563,5 @@ let process_error_hook = Hooks.process_error_hook let interp_hook = Hooks.interp_hook let with_fail_hook = Hooks.with_fail_hook let unreachable_state_hook = Hooks.unreachable_state_hook - +let get_fix_exn () = !State.fix_exn_ref (* vim:set foldmethod=marker: *) diff --git a/stm/stm.mli b/stm/stm.mli index 18ed6fc2e..0c05c93d4 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -136,3 +136,4 @@ val process_error_hook : Future.fix_exn Hook.t val interp_hook : (?verbosely:bool -> ?proof:Proof_global.closed_proof -> Loc.t * Vernacexpr.vernac_expr -> unit) Hook.t val with_fail_hook : (bool -> (unit -> unit) -> unit) Hook.t +val get_fix_exn : unit -> (Exninfo.iexn -> Exninfo.iexn) diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index e488f84f8..9019f486b 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -508,16 +508,17 @@ let declare_definition prg = let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None) (Evd.evar_universe_context_subst prg.prg_ctx) in let opaque = prg.prg_opaque in + let fix_exn = Stm.get_fix_exn () in let ce = - definition_entry ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind) - ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body) + definition_entry ~fix_exn + ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind) + ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body) in progmap_remove prg; !declare_definition_ref prg.prg_name prg.prg_kind ce prg.prg_implicits - (Lemmas.mk_hook (fun l r -> - Lemmas.call_hook (fun exn -> exn) prg.prg_hook l r; r)) - + (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r; r)) + open Pp let rec lam_index n t acc = @@ -618,8 +619,9 @@ let declare_obligation prg obl body ty uctx = if get_shrink_obligations () && not poly then shrink_body body else [], body, [||] in + let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in let ce = - { const_entry_body = Future.from_val((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants); + { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body; const_entry_secctx = None; const_entry_type = if List.is_empty ctx then ty else None; const_entry_polymorphic = poly; -- cgit v1.2.3