aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--intf/tacexpr.mli2
-rw-r--r--lib/future.ml7
-rw-r--r--lib/future.mli12
-rw-r--r--plugins/funind/functional_principles_proofs.ml2
-rw-r--r--plugins/funind/functional_principles_types.ml4
-rw-r--r--plugins/funind/indfun.ml2
-rw-r--r--plugins/funind/indfun_common.ml3
-rw-r--r--plugins/funind/indfun_common.mli2
-rw-r--r--plugins/funind/invfun.ml4
-rw-r--r--plugins/funind/recdef.ml8
-rw-r--r--stm/lemmas.ml11
-rw-r--r--stm/stm.ml3
-rw-r--r--tactics/rewrite.ml1
-rw-r--r--toplevel/class.ml4
-rw-r--r--toplevel/classes.ml4
-rw-r--r--toplevel/command.ml15
-rw-r--r--toplevel/obligations.ml13
-rw-r--r--toplevel/vernacentries.ml5
18 files changed, 68 insertions, 34 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 4b4a54a035..7895ddbf47 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -273,4 +273,4 @@ type raw_tactic_arg =
type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
type glob_red_expr = (g_trm, g_cst, g_pat) red_expr_gen
-type 'a declaration_hook = locality -> global_reference -> 'a
+type 'a declaration_hook = 'a Future.hook
diff --git a/lib/future.ml b/lib/future.ml
index 77386a1a9f..960363e252 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -91,6 +91,13 @@ 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 ())))
let fix_exn_of ck = let _, fix_exn, _ = get ck in fix_exn
+type 'a hook = Decl_kinds.locality -> Globnames.global_reference -> 'a
+let mk_hook hook = hook
+let call_hook fix_exn hook l c =
+ try hook l c
+ with e when Errors.noncritical e ->
+ let e = Errors.push e in
+ raise (fix_exn e)
let default_force () = raise NotReady
let assignement ck = fun v ->
diff --git a/lib/future.mli b/lib/future.mli
index b4eced06a9..41f5e185c9 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -84,8 +84,18 @@ val from_val : ?fix_exn:fix_exn -> 'a -> 'a computation
the value is not just the 'a but also the global system state *)
val from_here : ?fix_exn:fix_exn -> 'a -> 'a computation
-(* To get the fix_exn of a computation *)
+(* To get the fix_exn of a computation and build a Tacexpr.declaration_hook.
+ * When a future enters the environment a corresponding hook is run to perform
+ * some work. If this fails, then its failure has to be annotated with the
+ * same state id that corresponds to the future computation end. I.e. Qed
+ * is split into two parts, the lazy one (the future) and the eagher one
+ * (the hook), both performing some computations for the same state id. *)
val fix_exn_of : 'a computation -> fix_exn
+type 'a hook
+val mk_hook :
+ (Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a hook
+val call_hook :
+ fix_exn -> 'a hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a
(* Run remotely, returns the function to assign. Optionally tekes a function
that is called when forced. The default one is to raise NotReady.
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f0c7b5a7f7..714192f530 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -988,7 +988,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
(mk_equation_id f_id)
(Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem))
(lemma_type, (*FIXME*) Univ.ContextSet.empty)
- (fun _ _ -> ());
+ (Future.mk_hook (fun _ _ -> ()));
ignore (Pfedit.by (Proofview.V82.tactic prove_replacement));
Lemmas.save_proof (Vernacexpr.Proved(false,None))
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index a8876c75b1..65a2627070 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -290,7 +290,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
let new_princ_name =
next_ident_away_in_goal (Id.of_string "___________princ_________") []
in
- let hook = hook new_principle_type in
+ let hook = Future.mk_hook (hook new_principle_type) in
begin
Lemmas.start_proof
new_princ_name
@@ -305,7 +305,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
(* let dur1 = System.time_difference tim1 tim2 in *)
(* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *)
(* end; *)
- get_proof_clean true,Ephemeron.create hook
+ get_proof_clean true, Ephemeron.create hook
end
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 70a892a3bb..8c8d7a667e 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -352,7 +352,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
| [((_,fname),_,bl,ret_type,body),_] when not is_rec ->
let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in
Command.do_definition fname (Decl_kinds.Global,(*FIXME*)false,Decl_kinds.Definition)
- bl None body (Some ret_type) (fun _ _ -> ())
+ bl None body (Some ret_type) (Future.mk_hook (fun _ _ -> ()))
| _ ->
Command.do_fixpoint Global false(*FIXME*) fixpoint_exprl
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 0d1e600ee6..b923260c24 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -147,6 +147,7 @@ let get_locality = function
| Global -> false
let save with_clean id const (locality,_,kind) hook =
+ let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
let l,r = match locality with
| Discharge when Lib.sections_are_opened () ->
let k = Kindops.logical_kind_of_goal_kind kind in
@@ -160,7 +161,7 @@ let save with_clean id const (locality,_,kind) hook =
(locality, ConstRef kn)
in
if with_clean then Pfedit.delete_current_proof ();
- Ephemeron.iter_opt hook (fun f -> f l r);
+ Ephemeron.iter_opt hook (fun f -> Future.call_hook fix_exn f l r);
definition_message id
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 6e8b79a6be..3fafeadc1c 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -46,7 +46,7 @@ val const_of_id: Id.t -> constant
val jmeq : unit -> Term.constr
val jmeq_refl : unit -> Term.constr
-val save : bool -> Id.t -> Entries.definition_entry -> Decl_kinds.goal_kind ->
+val save : bool -> Id.t -> Entries.definition_entry -> Decl_kinds.goal_kind ->
unit Tacexpr.declaration_hook Ephemeron.key -> unit
(* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d5640798e2..9558923f6b 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1080,7 +1080,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
Lemmas.start_proof lem_id
(Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem))
(fst lemmas_types_infos.(i), (*FIXME*)Univ.ContextSet.empty)
- (fun _ _ -> ());
+ (Future.mk_hook (fun _ _ -> ()));
ignore (Pfedit.by
(Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
(proving_tac i))));
@@ -1133,7 +1133,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
Lemmas.start_proof lem_id
(Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem))
(fst lemmas_types_infos.(i), (*FIXME*)Univ.ContextSet.empty)
- (fun _ _ -> ());
+ (Future.mk_hook (fun _ _ -> ()));
ignore (Pfedit.by
(Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
(proving_tac i))));
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 4390143619..08d8ca3914 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1320,7 +1320,7 @@ let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompos
na
(Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma)
(gls_type, ctx)
- hook;
+ (Future.mk_hook hook);
if Indfun_common.is_strict_tcc ()
then
ignore (by (Proofview.V82.tactic (tclIDTAC)))
@@ -1415,7 +1415,9 @@ let (com_eqn : int -> Id.t ->
let f_constr = constr_of_global f_ref in
let equation_lemma_type = subst1 f_constr equation_lemma_type in
(Lemmas.start_proof eq_name (Global, false, Proof Lemma)
- ~sign:(Environ.named_context_val env) (equation_lemma_type, (*FIXME*)Univ.ContextSet.empty) (fun _ _ -> ());
+ ~sign:(Environ.named_context_val env)
+ (equation_lemma_type, (*FIXME*)Univ.ContextSet.empty)
+ (Future.mk_hook (fun _ _ -> ()));
ignore (by
(Proofview.V82.tactic (start_equation f_ref terminate_ref
(fun x ->
@@ -1535,5 +1537,5 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
term_id
using_lemmas
(List.length res_vars)
- ctx hook)
+ ctx (Future.mk_hook hook))
()
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 0668af2c50..493b874aed 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -168,6 +168,7 @@ let look_for_possibly_mutual_statements = function
(* Saving a goal *)
let save id const cstrs do_guard (locality,poly,kind) hook =
+ let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
let const = adjust_guardness_conditions const do_guard in
let k = Kindops.logical_kind_of_goal_kind kind in
let l,r = match locality with
@@ -183,7 +184,7 @@ let save id const cstrs do_guard (locality,poly,kind) hook =
let kn = declare_constant id ~local (DefinitionEntry const, k) in
(locality, ConstRef kn) in
definition_message id;
- hook l r
+ Future.call_hook fix_exn hook l r
let default_thm_id = Id.of_string "Unnamed_thm"
@@ -224,7 +225,7 @@ let save_remaining_recthms (locality,p,kind) body opaq i (id,((t_i,ctx_i),(_,imp
let body_i = match kind_of_term body with
| Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
| CoFix (0,decls) -> mkCoFix (i,decls)
- | _ -> anomaly (Pp.str "Not a proof by induction") in
+ | _ -> anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr body) in
match locality with
| Discharge ->
let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p
@@ -285,7 +286,7 @@ let admit hook () =
str "declared as an axiom.")
in
let () = assumption_message id in
- hook Global (ConstRef kn)
+ Future.call_hook (fun exn -> exn) hook Global (ConstRef kn)
(* Starting a goal *)
@@ -400,8 +401,8 @@ let start_proof_with_initialization kind recguard thms snl hook =
let thms_data = (strength,ref,imps)::other_thms_data in
List.iter (fun (strength,ref,imps) ->
maybe_declare_manual_implicits false ref imps;
- hook strength ref) thms_data in
- start_proof id kind t ?init_tac hook ~compute_guard:guard
+ Future.call_hook (fun exn -> exn) hook strength ref) thms_data in
+ start_proof id kind t ?init_tac (Future.mk_hook hook) ~compute_guard:guard
let start_proof_com kind thms hook =
let env0 = Global.env () in
diff --git a/stm/stm.ml b/stm/stm.ml
index b6143df528..c708389908 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -763,7 +763,8 @@ end = struct
!reach_known_state ~cache:`No eop;
(* The original terminator, a hook, has not been saved in the .vi*)
Proof_global.set_terminator
- (Lemmas.standard_proof_terminator [] (fun _ _ -> ()));
+ (Lemmas.standard_proof_terminator []
+ (Future.mk_hook (fun _ _ -> ())));
let proof = Proof_global.close_proof (fun x -> x) in
vernac_interp eop ~proof
{ verbose = false; loc;
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 1e88456f36..1c98ec21dd 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1878,6 +1878,7 @@ let add_morphism_infer glob m n =
declare_projection n instance_id (ConstRef cst)
| _ -> assert false
in
+ let hook = Future.mk_hook hook in
Flags.silently
(fun () ->
Lemmas.start_proof instance_id kind (instance, ctx) hook;
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 9ca75d1737..1d85290511 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -304,6 +304,8 @@ let add_coercion_hook poly local ref =
let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
Flags.if_verbose msg_info msg
+let add_coercion_hook poly = Future.mk_hook (add_coercion_hook poly)
+
let add_subclass_hook poly local ref =
let stre = match local with
| Local -> true
@@ -312,3 +314,5 @@ let add_subclass_hook poly local ref =
in
let cl = class_of_global ref in
try_add_new_coercion_subclass cl stre poly
+
+let add_subclass_hook poly = Future.mk_hook (add_subclass_hook poly)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index b9c4a42943..5d1a0a43b6 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -294,6 +294,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
in obls, Some constr, typ
| None -> [||], None, termtype
in
+ let hook = Future.mk_hook hook in
let ctx = Evd.universe_context_set evm in
ignore (Obligations.add_definition id ?term:constr
typ ctx ~kind:(Global,poly,Instance) ~hook obls);
@@ -302,7 +303,8 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
(Flags.silently
(fun () ->
Lemmas.start_proof id kind (termtype, Evd.universe_context_set evm)
- (fun _ -> instance_hook k pri global imps ?hook);
+ (Future.mk_hook
+ (fun _ -> instance_hook k pri global imps ?hook));
(* spiwack: I don't know what to do with the status here. *)
if not (Option.is_empty term) then
ignore (Pfedit.by (!refine_ref (evm, Option.get term)))
diff --git a/toplevel/command.ml b/toplevel/command.ml
index c1283fb1f4..b49fe40a09 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -163,7 +163,7 @@ let declare_definition ident (local, p, k) ce imps hook =
VarRef ident
| Discharge | Local | Global ->
declare_global_definition ident ce local k imps in
- hook local r
+ Future.call_hook (Future.fix_exn_of ce.Entries.const_entry_body) hook local r
let _ = Obligations.declare_definition_ref := declare_definition
@@ -183,10 +183,12 @@ let do_definition ident k bl red_option c ctypopt hook =
Obligations.eterm_obligations env ident evd 0 c typ
in
let ctx = Evd.universe_context_set evd in
- ignore(Obligations.add_definition ident ~term:c cty ctx ~implicits:imps ~kind:k ~hook obls)
+ ignore(Obligations.add_definition
+ ident ~term:c cty ctx ~implicits:imps ~kind:k ~hook obls)
else let ce = check_definition def in
ignore(declare_definition ident k ce imps
- (fun l r -> hook l r;r))
+ (Future.mk_hook
+ (fun l r -> Future.call_hook (fun exn -> exn) hook l r;r)))
(* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
@@ -690,7 +692,7 @@ let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
let declare_fix (_,poly,_ as kind) ctx f ((def,_),eff) t imps =
let ce = definition_entry ~types:t ~poly ~univs:ctx ~eff def in
- declare_definition f kind ce imps (fun _ r -> r)
+ declare_definition f kind ce imps (Future.mk_hook (fun _ r -> r))
let _ = Obligations.declare_fix_ref := declare_fix
@@ -898,6 +900,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
Impargs.declare_manual_implicits false gr [impls]
in hook, recname, typ
in
+ let hook = Future.mk_hook hook in
let fullcoqc = Evarutil.nf_evar !evdref def in
let fullctyp = Evarutil.nf_evar !evdref typ in
Obligations.check_evars env !evdref;
@@ -991,7 +994,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexe
Option.map (List.map Proofview.V82.tactic) init_tac
in
Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint)
- (Some(false,indexes,init_tac)) thms None (fun _ _ -> ())
+ (Some(false,indexes,init_tac)) thms None (Future.mk_hook (fun _ _ -> ()))
else begin
(* We shortcut the proof process *)
let fixdefs = List.map Option.get fixdefs in
@@ -1025,7 +1028,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns
Option.map (List.map Proofview.V82.tactic) init_tac
in
Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
- (Some(true,[],init_tac)) thms None (fun _ _ -> ())
+ (Some(true,[],init_tac)) thms None (Future.mk_hook (fun _ _ -> ()))
else begin
(* We shortcut the proof process *)
let fixdefs = List.map Option.get fixdefs in
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index f8247c4ed6..00fc3e0ce1 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -535,7 +535,8 @@ let declare_definition prg =
progmap_remove prg;
!declare_definition_ref prg.prg_name
prg.prg_kind ce prg.prg_implicits
- (fun l r -> prg.prg_hook l r; r)
+ (Future.mk_hook (fun l r ->
+ Future.call_hook (fun exn -> exn) prg.prg_hook l r; r))
open Pp
@@ -606,7 +607,7 @@ let declare_mutual_definition l =
Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
let gr = List.hd kns in
let kn = match gr with ConstRef kn -> kn | _ -> assert false in
- first.prg_hook local gr;
+ Future.call_hook (fun exn -> exn) first.prg_hook local gr;
List.iter progmap_remove l; kn
let shrink_body c =
@@ -815,7 +816,7 @@ let rec solve_obligation prg num tac =
let kind = kind_of_obligation (pi2 prg.prg_kind) obl.obl_status in
Lemmas.start_proof_univs obl.obl_name kind
(Universes.subst_opt_univs_constr prg.prg_subst obl.obl_type, ctx)
- (fun (subst, ctx) strength gr ->
+ (fun (subst, ctx) -> Future.mk_hook (fun strength gr ->
let cst = match gr with ConstRef cst -> cst | _ -> assert false in
let obl =
let transparent = evaluable_constant cst (Global.env ()) in
@@ -851,7 +852,7 @@ let rec solve_obligation prg num tac =
let deps = dependencies obls num in
if not (Int.Set.is_empty deps) then
ignore(auto_solve_obligations (Some prg.prg_name) None ~oblset:deps)
- | _ -> ());
+ | _ -> ()));
trace (str "Started obligation " ++ int user_num ++ str " proof: " ++
Printer.pr_constr_env (Global.env ()) obl.obl_type);
ignore (Pfedit.by (snd (get_default_tactic ())));
@@ -976,7 +977,7 @@ let show_term n =
++ Printer.pr_constr_env (Global.env ()) prg.prg_body)
let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
- ?(reduce=reduce) ?(hook=fun _ _ -> ()) obls =
+ ?(reduce=reduce) ?(hook=Future.mk_hook (fun _ _ -> ())) obls =
let info = str (Id.to_string n) ++ str " has type-checked" in
let prg = init_prog_info n term t ctx [] None [] obls implicits kind reduce hook in
let obls,_ = prg.prg_obligations in
@@ -994,7 +995,7 @@ let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition)
| _ -> res)
let add_mutual_definitions l ctx ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
- ?(hook=fun _ _ -> ()) notations fixkind =
+ ?(hook=Future.mk_hook (fun _ _ -> ())) notations fixkind =
let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
List.iter
(fun (n, b, t, imps, obls) ->
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 007ab52388..1fdf95c0f5 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -452,11 +452,12 @@ let start_proof_and_print k l hook =
start_proof_com k l hook;
print_subgoals ()
-let no_hook _ _ = ()
+let no_hook = Future.mk_hook (fun _ _ -> ())
let vernac_definition_hook p = function
| Coercion -> Class.add_coercion_hook p
-| CanonicalStructure -> fun _ -> Recordops.declare_canonical_structure
+| CanonicalStructure ->
+ Future.mk_hook (fun _ -> Recordops.declare_canonical_structure)
| SubClass -> Class.add_subclass_hook p
| _ -> no_hook
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 16:39:16 +0000