From 43f3634a0e75381ca473aea08415e3d262e4c066 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 11 Feb 2019 23:25:31 +0100 Subject: [vernac] Allow path for `save_proof` where no proof state is present. In that case the terminator and proof object have to be supplied in the ?proof argument, or else we get an anomaly. Co-authored-by: Maxime Dénès --- plugins/funind/functional_principles_proofs.ml | 2 +- plugins/funind/invfun.ml | 4 +- plugins/funind/recdef.ml | 8 +- vernac/lemmas.ml | 117 +++++++++++++------------ vernac/lemmas.mli | 12 ++- vernac/vernacentries.ml | 13 +-- 6 files changed, 86 insertions(+), 70 deletions(-) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 499005a4db..287a374ab1 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1000,7 +1000,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num lemma_type in let pstate,_ = Pfedit.by (Proofview.V82.tactic prove_replacement) pstate in - let pstate = Lemmas.save_proof ~pstate (Vernacexpr.(Proved(Proof_global.Transparent,None))) in + let pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None in pstate, evd diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 136848eb67..edb698280f 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -811,7 +811,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let pstate = fst @@ Pfedit.by (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") (proving_tac i))) pstate in - let _ = Lemmas.save_proof ~pstate (Vernacexpr.(Proved(Proof_global.Transparent,None))) in + let _ = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None in let finfo = find_Function_infos (fst f_as_constant) in (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *) let _,lem_cst_constr = Evd.fresh_global @@ -871,7 +871,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let pstate = fst (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") (proving_tac i))) pstate) in - let _pstate = Lemmas.save_proof ~pstate (Vernacexpr.(Proved(Proof_global.Transparent,None))) in + let _pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None in let finfo = find_Function_infos (fst f_as_constant) in let _,lem_cst_constr = Evd.fresh_global (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 43073fe07c..0b1ae90237 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -72,7 +72,7 @@ let declare_fun f_id kind ?univs value = let ce = definition_entry ?univs value (*FIXME *) in ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; -let defined pstate = Lemmas.save_proof ~pstate (Vernacexpr.(Proved (Proof_global.Transparent,None))) +let defined pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None let def_of_const t = match (Constr.kind t) with @@ -1367,7 +1367,7 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type ) g) in - let _pstate = Lemmas.save_proof ~pstate (Vernacexpr.Proved(opacity,None)) in + let _pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:opacity ~idopt:None in () in let pstate = Lemmas.start_proof ~ontop:(Some pstate) @@ -1401,8 +1401,6 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type with UserError _ -> defined pstate - - let com_terminate tcc_lemma_name tcc_lemma_ref @@ -1501,7 +1499,7 @@ let (com_eqn : int -> Id.t -> )) pstate in (* (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *) (* Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *) - let _ = Flags.silently (fun () -> Lemmas.save_proof ~pstate (Vernacexpr.Proved(opacity,None))) () in + let _ = Flags.silently (fun () -> Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:opacity ~idopt:None) () in () (* Pp.msgnl (fun _ _ -> str "eqn finished"); *) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 19b0856015..1c7cc5e636 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -448,60 +448,65 @@ let () = optread = (fun () -> !keep_admitted_vars); optwrite = (fun b -> keep_admitted_vars := b) } -let save_proof ?proof ~pstate = function - | Vernacexpr.Admitted -> - let pe = - let open Proof_global in - match proof with - | Some ({ id; entries; persistence = k; universes }, _) -> - if List.length entries <> 1 then - user_err Pp.(str "Admitted does not support multiple statements"); - let { const_entry_secctx; const_entry_type } = List.hd entries in - if const_entry_type = None then - user_err Pp.(str "Admitted requires an explicit statement"); - let typ = Option.get const_entry_type in - let ctx = UState.univ_entry ~poly:(pi2 k) universes in - let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in - Admitted(id, k, (sec_vars, (typ, ctx), None), universes) - | None -> - let pftree = Proof_global.give_me_the_proof pstate in - let gk = Proof_global.get_current_persistence pstate in - let Proof.{ name; poly; entry } = Proof.data pftree in - let typ = match Proofview.initial_goals entry with - | [typ] -> snd typ - | _ -> - CErrors.anomaly - ~label:"Lemmas.save_proof" (Pp.str "more than one statement.") - in - let typ = EConstr.Unsafe.to_constr typ in - let universes = Proof.((data pftree).initial_euctx) in - (* This will warn if the proof is complete *) - let pproofs, _univs = - Proof_global.return_proof ~allow_partial:true pstate in - let sec_vars = - if not !keep_admitted_vars then None - else match Proof_global.get_used_variables pstate, pproofs with - | Some _ as x, _ -> x - | None, (pproof, _) :: _ -> - let env = Global.env () in - let ids_typ = Environ.global_vars_set env typ in - let ids_def = Environ.global_vars_set env pproof in - Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def)) - | _ -> None in - let decl = Proof_global.get_universe_decl pstate in - let ctx = UState.check_univ_decl ~poly universes decl in - Admitted(name,gk,(sec_vars, (typ, ctx), None), universes) - in - Proof_global.apply_terminator (Proof_global.get_terminator pstate) pe; - Some pstate - | Vernacexpr.Proved (opaque,idopt) -> - let (proof_obj,terminator) = - match proof with - | None -> - Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pstate - | Some proof -> proof +let save_proof_admitted ?proof ~pstate = + let pe = + let open Proof_global in + match proof with + | Some ({ id; entries; persistence = k; universes }, _) -> + if List.length entries <> 1 then + user_err Pp.(str "Admitted does not support multiple statements"); + let { const_entry_secctx; const_entry_type } = List.hd entries in + if const_entry_type = None then + user_err Pp.(str "Admitted requires an explicit statement"); + let typ = Option.get const_entry_type in + let ctx = UState.univ_entry ~poly:(pi2 k) universes in + let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in + Admitted(id, k, (sec_vars, (typ, ctx), None), universes) + | None -> + let pftree = Proof_global.give_me_the_proof pstate in + let gk = Proof_global.get_current_persistence pstate in + let Proof.{ name; poly; entry } = Proof.data pftree in + let typ = match Proofview.initial_goals entry with + | [typ] -> snd typ + | _ -> + CErrors.anomaly + ~label:"Lemmas.save_proof" (Pp.str "more than one statement.") in - (* if the proof is given explicitly, nothing has to be deleted *) - let pstate = if Option.is_empty proof then Proof_global.discard_current pstate else Some pstate in - Proof_global.(apply_terminator terminator (Proved (opaque,idopt,proof_obj))); - pstate + let typ = EConstr.Unsafe.to_constr typ in + let universes = Proof.((data pftree).initial_euctx) in + (* This will warn if the proof is complete *) + let pproofs, _univs = + Proof_global.return_proof ~allow_partial:true pstate in + let sec_vars = + if not !keep_admitted_vars then None + else match Proof_global.get_used_variables pstate, pproofs with + | Some _ as x, _ -> x + | None, (pproof, _) :: _ -> + let env = Global.env () in + let ids_typ = Environ.global_vars_set env typ in + let ids_def = Environ.global_vars_set env pproof in + Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def)) + | _ -> None in + let decl = Proof_global.get_universe_decl pstate in + let ctx = UState.check_univ_decl ~poly universes decl in + Admitted(name,gk,(sec_vars, (typ, ctx), None), universes) + in + Proof_global.apply_terminator (Proof_global.get_terminator pstate) pe + +let save_proof_proved ?proof ?pstate ~opaque ~idopt = + (* Invariant (uh) *) + if Option.is_empty pstate && Option.is_empty proof then + user_err (str "No focused proof (No proof-editing in progress)."); + let (proof_obj,terminator) = + match proof with + | None -> + (* XXX: The close_proof and proof state API should be refactored + so it is possible to insert proofs properly into the state *) + let pstate = Option.get pstate in + Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pstate + | Some proof -> proof + in + (* if the proof is given explicitly, nothing has to be deleted *) + let pstate = if Option.is_empty proof then Proof_global.discard_current Option.(get pstate) else pstate in + Proof_global.(apply_terminator terminator (Proved (opaque,idopt,proof_obj))); + pstate diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 9b5c84e0d1..1f70cfa1ad 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -71,4 +71,14 @@ val initialize_named_context_for_proof : unit -> Environ.named_context_val (** {6 ... } *) -val save_proof : ?proof:Proof_global.closed_proof -> pstate:Proof_global.t -> Vernacexpr.proof_end -> Proof_global.t option +val save_proof_admitted + : ?proof:Proof_global.closed_proof + -> pstate:Proof_global.t + -> unit + +val save_proof_proved + : ?proof:Proof_global.closed_proof + -> ?pstate:Proof_global.t + -> opaque:Proof_global.opacity_flag + -> idopt:Names.lident option + -> Proof_global.t option diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 3ead8663ce..284df19b4c 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -616,15 +616,18 @@ let vernac_start_proof ~atts ~pstate kind l = List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l; Some (start_proof_and_print ~pstate ~program_mode:atts.program (local, atts.polymorphic, Proof kind) l) -let vernac_end_proof ~pstate ?proof = function - | Admitted -> save_proof ~pstate ?proof Admitted - | Proved (_,_) as e -> save_proof ~pstate ?proof e +let vernac_end_proof ?pstate ?proof = function + | Admitted -> + vernac_require_open_proof ~pstate (save_proof_admitted ?proof); + pstate + | Proved (opaque,idopt) -> + save_proof_proved ?pstate ?proof ~opaque ~idopt let vernac_exact_proof ~pstate c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is called only at the begining of a proof. *) let pstate, status = Pfedit.by (Tactics.exact_proof c) pstate in - let pstate = save_proof ~pstate (Vernacexpr.(Proved(Proof_global.Opaque,None))) in + let pstate = save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Opaque ~idopt:None in if not status then Feedback.feedback Feedback.AddedAxiom; pstate @@ -2270,7 +2273,7 @@ let interp ?proof ~atts ~st c : Proof_global.t option = with_def_attributes ~atts vernac_start_proof ~pstate k l | VernacEndProof e -> unsupported_attributes atts; - vernac_require_open_proof ~pstate (vernac_end_proof ?proof e) + vernac_end_proof ?proof ?pstate e | VernacExactProof c -> unsupported_attributes atts; vernac_require_open_proof ~pstate (vernac_exact_proof c) -- cgit v1.2.3