diff options
| -rw-r--r-- | plugins/funind/gen_principle.ml | 2 | ||||
| -rw-r--r-- | stm/stm.ml | 10 | ||||
| -rw-r--r-- | tactics/declare.ml | 10 | ||||
| -rw-r--r-- | tactics/declare.mli | 5 | ||||
| -rw-r--r-- | tactics/pfedit.ml | 2 | ||||
| -rw-r--r-- | tactics/proof_global.ml | 111 | ||||
| -rw-r--r-- | tactics/proof_global.mli | 2 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacstate.ml | 4 | ||||
| -rw-r--r-- | vernac/vernacstate.mli | 2 |
10 files changed, 73 insertions, 77 deletions
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 45c46c56f4..0ed04d262a 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -199,7 +199,7 @@ let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_ (* end; *) let open Proof_global in - let { entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)) lemma in + let { entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false) lemma in match entries with | [entry] -> entry, hook diff --git a/stm/stm.ml b/stm/stm.ml index 62556d38ff..ba8eba0eed 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1668,7 +1668,7 @@ end = struct (* {{{ *) (* The original terminator, a hook, has not been saved in the .vio*) let proof, _info = - PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in + PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true in let info = Lemmas.Info.make () in @@ -2518,9 +2518,11 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = | VtKeepOpaque -> Opaque | VtKeepDefined -> Transparent | VtKeepAxiom -> assert false in - Some(PG_compat.close_proof ~opaque - ~keep_body_ucst_separate:false - (State.exn_on id ~valid:eop)) in + try Some (PG_compat.close_proof ~opaque ~keep_body_ucst_separate:false) + with exn -> + let iexn = Exninfo.capture exn in + Exninfo.iraise (State.exn_on id ~valid:eop iexn) + in if keep <> VtKeep VtKeepAxiom then reach view.next; let wall_clock2 = Unix.gettimeofday () in diff --git a/tactics/declare.ml b/tactics/declare.ml index 5e6f78be6f..a149850a64 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -187,14 +187,14 @@ let record_aux env s_ty s_bo = let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty -let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types - ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body = - { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); - proof_entry_secctx = None; +let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types + ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) ?(univc=Univ.ContextSet.empty) body = + { proof_entry_body = Future.from_val ?fix_exn ((body,univc), eff); + proof_entry_secctx = section_vars; proof_entry_type = types; proof_entry_universes = univs; proof_entry_opaque = opaque; - proof_entry_feedback = None; + proof_entry_feedback = feedback_id; proof_entry_inline_code = inline} let pure_definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types diff --git a/tactics/declare.mli b/tactics/declare.mli index 0068b9842a..6ea08d5b0e 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -59,9 +59,14 @@ val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool + -> ?feedback_id:Stateid.t + -> ?section_vars:Id.Set.t -> ?types:types -> ?univs:Entries.universes_entry -> ?eff:Evd.side_effects + -> ?univc:Univ.ContextSet.t + (** Universe-constraints attached to the body-only, used in vio / + vio-delayed opaque constants *) -> constr -> Evd.side_effects proof_entry diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index b228a04298..22d0ce5328 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -122,7 +122,7 @@ let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ~uctx ~sig let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in let pf, status = by tac pf in let open Proof_global in - let { entries; uctx } = close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pf in + let { entries; uctx } = close_proof ~opaque ~keep_body_ucst_separate:false pf in match entries with | [entry] -> entry, status, uctx diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml index b97acdafa6..8d62d1635d 100644 --- a/tactics/proof_global.ml +++ b/tactics/proof_global.ml @@ -142,78 +142,73 @@ let private_poly_univs = fun () -> !b let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id - (fpl : closed_proof_output Future.computation) ps = + ((elist, uctx) : closed_proof_output) ps = let { section_vars; proof; udecl; initial_euctx } = ps in - let Proof.{ name; poly; entry } = Proof.data proof in + let Proof.{ name; poly; entry; sigma } = Proof.data proof in let opaque = match opaque with Opaque -> true | Transparent -> false in let constrain_variables ctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx in - let fpl, univs = Future.split2 fpl in - let uctx = Future.force univs in (* Because of dependent subgoals at the beginning of proofs, we could have existential variables in the initial types of goals, we need to normalise them for the kernel. *) - let subst_evar k = - let { Proof.sigma } = Proof.data proof in - Evd.existential_opt_value0 sigma k in - let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar - (UState.subst uctx) in + let subst_evar k = Evd.existential_opt_value0 sigma k in + let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar (UState.subst uctx) in - let make_body t (c, eff) = + let make_body typ (c, eff) : + Constr.types Entries.in_universes_entry * Evd.side_effects Entries.proof_output = let body = c in let allow_deferred = not poly && (keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff.Evd.seff_private)) in - let typ = if allow_deferred then t else nf t in + let typ = if allow_deferred then typ else nf typ in let used_univs_body = Vars.universes_of_constr body in let used_univs_typ = Vars.universes_of_constr typ in - if allow_deferred then - let initunivs = UState.univ_entry ~poly initial_euctx in - let ctx = constrain_variables uctx in - (* For vi2vo compilation proofs are computed now but we need to - complement the univ constraints of the typ with the ones of - the body. So we keep the two sets distinct. *) - let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let ctx_body = UState.restrict ctx used_univs in - let univs = UState.check_mono_univ_decl ctx_body udecl in - (initunivs, typ), ((body, univs), eff) - else if poly && opaque && private_poly_univs () then - let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let universes = UState.restrict uctx used_univs in - let typus = UState.restrict universes used_univs_typ in - let udecl = UState.check_univ_decl ~poly typus udecl in - let ubody = Univ.ContextSet.diff - (UState.context_set universes) - (UState.context_set typus) - in - (udecl, typ), ((body, ubody), eff) - else - (* Since the proof is computed now, we can simply have 1 set of - constraints in which we merge the ones for the body and the ones - for the typ. We recheck the declaration after restricting with - the actually used universes. - TODO: check if restrict is really necessary now. *) - let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let ctx = UState.restrict uctx used_univs in - let univs = UState.check_univ_decl ~poly ctx udecl in - (univs, typ), ((body, Univ.ContextSet.empty), eff) + let used_univs = Univ.LSet.union used_univs_body used_univs_typ in + let utyp, ubody = + if allow_deferred then + let utyp = UState.univ_entry ~poly initial_euctx in + let ctx = constrain_variables uctx in + (* For vi2vo compilation proofs are computed now but we need to + complement the univ constraints of the typ with the ones of + the body. So we keep the two sets distinct. *) + let ctx_body = UState.restrict ctx used_univs in + let univs = UState.check_mono_univ_decl ctx_body udecl in + utyp, univs + else if poly && opaque && private_poly_univs () then + let universes = UState.restrict uctx used_univs in + let typus = UState.restrict universes used_univs_typ in + let utyp = UState.check_univ_decl ~poly typus udecl in + let ubody = Univ.ContextSet.diff + (UState.context_set universes) + (UState.context_set typus) + in + utyp, ubody + else + (* Since the proof is computed now, we can simply have 1 set of + constraints in which we merge the ones for the body and the ones + for the typ. We recheck the declaration after restricting with + the actually used universes. + TODO: check if restrict is really necessary now. *) + let ctx = UState.restrict uctx used_univs in + let utyp = UState.check_univ_decl ~poly ctx udecl in + utyp, Univ.ContextSet.empty + in + (typ, utyp), ((body, ubody), eff) in - let make_body t p = Future.split2 (Future.chain p (make_body t)) in let entry_fn p (_, t) = let t = EConstr.Unsafe.to_constr t in - let univstyp, body = make_body t p in - let univs, typ = Future.force univstyp in - Declare.delayed_definition_entry ~opaque ?feedback_id ?section_vars ~univs ~types:typ body + let (typ, univs), ((body,univc),eff) = make_body t p in + Declare.definition_entry ~opaque ?feedback_id ?section_vars ~univs ~univc ~types:typ ~eff body in - let entries = Future.map2 entry_fn fpl (Proofview.initial_goals entry) in - { name; entries; uctx; udecl } + let entries = CList.map2 entry_fn elist (Proofview.initial_goals entry) in + { name; entries; uctx } let close_proof_delayed ~opaque ~keep_body_ucst_separate ?feedback_id (fpl : closed_proof_output Future.computation) ps = let { section_vars; proof; udecl; initial_euctx } = ps in - let Proof.{ name; poly; entry } = Proof.data proof in + let Proof.{ name; poly; entry; sigma } = Proof.data proof in (* We don't allow poly = true in this path *) if poly then @@ -228,18 +223,14 @@ let close_proof_delayed ~opaque ~keep_body_ucst_separate ?feedback_id (* Because of dependent subgoals at the beginning of proofs, we could have existential variables in the initial types of goals, we need to normalise them for the kernel. *) - let subst_evar k = - let { Proof.sigma } = Proof.data proof in - Evd.existential_opt_value0 sigma k in - - let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar - (UState.subst uctx) in + let subst_evar k = Evd.existential_opt_value0 sigma k in + let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar (UState.subst uctx) in let make_body t p = (* Already checked the univ_decl for the type universes when starting the proof. *) let univctx = UState.univ_entry ~poly:false uctx in let t = nf t in - Future.from_val (univctx, t), + (t, univctx), Future.chain p (fun (pt,eff) -> (* Deferred proof, we already checked the universe declaration with the initial universes, ensure that the final universes respect @@ -257,9 +248,8 @@ let close_proof_delayed ~opaque ~keep_body_ucst_separate ?feedback_id in let entry_fn p (_, t) = let t = EConstr.Unsafe.to_constr t in - let univstyp, body = make_body t p in - let univs, typ = Future.force univstyp in - Declare.delayed_definition_entry ~opaque ?feedback_id ?section_vars ~univs ~types:typ body + let (typ, utyp), body = make_body t p in + Declare.delayed_definition_entry ~opaque ?feedback_id ?section_vars ~univs:utyp ~types:typ body in let entries = Future.map2 entry_fn fpl (Proofview.initial_goals entry) in { name; entries; uctx } @@ -304,9 +294,8 @@ let return_proof ?(allow_partial=false) ps = let close_future_proof ~opaque ~feedback_id ps proof = close_proof_delayed ~opaque ~keep_body_ucst_separate:true ~feedback_id proof ps -let close_proof ~opaque ~keep_body_ucst_separate fix_exn ps = - close_proof ~opaque ~keep_body_ucst_separate - (Future.from_val ~fix_exn (return_proof ps)) ps +let close_proof ~opaque ~keep_body_ucst_separate ps = + close_proof ~opaque ~keep_body_ucst_separate (return_proof ps) ps let update_global_env = map_proof (fun p -> diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli index d820fc8b40..44b78ee911 100644 --- a/tactics/proof_global.mli +++ b/tactics/proof_global.mli @@ -67,7 +67,7 @@ val update_global_env : t -> t (* Takes a function to add to the exceptions data relative to the state in which the proof was built *) -val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> t -> proof_object +val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> t -> proof_object (* Intermediate step necessary to delegate the future. * Both access the current proof state. The former is supposed to be diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index feedf4d71d..7f7340bb34 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -403,7 +403,7 @@ let process_idopt_for_save ~idopt info = let save_lemma_proved ~lemma ~opaque ~idopt = (* Env and sigma are just used for error printing in save_remaining_recthms *) - let proof_obj = Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) lemma.proof in + let proof_obj = Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false lemma.proof in let proof_info = process_idopt_for_save ~idopt lemma.info in finalize_proof proof_obj proof_info diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 6846826bfa..7c191a1f86 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -170,8 +170,8 @@ module Proof_global = struct cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~opaque ~feedback_id st pf) pt, Internal.get_info pt) - let close_proof ~opaque ~keep_body_ucst_separate f = - cc_lemma (fun pt -> pf_fold ((close_proof ~opaque ~keep_body_ucst_separate f)) pt, + let close_proof ~opaque ~keep_body_ucst_separate = + cc_lemma (fun pt -> pf_fold ((close_proof ~opaque ~keep_body_ucst_separate)) pt, Internal.get_info pt) let discard_all () = s_lemmas := None diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index 7607f8373a..2c9c7ecc6f 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -74,7 +74,7 @@ module Proof_global : sig feedback_id:Stateid.t -> Proof_global.closed_proof_output Future.computation -> closed_proof - val close_proof : opaque:Proof_global.opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof + val close_proof : opaque:Proof_global.opacity_flag -> keep_body_ucst_separate:bool -> closed_proof val discard_all : unit -> unit val update_global_env : unit -> unit |