From a8b3c907cb2d6da16bdeea10b943552dc9efc0ed Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 5 Jun 2019 17:48:46 +0200 Subject: [proof] Move proofs that have an associated constant to `Lemmas` The main idea of this PR is to distinguish the types of "proof object" `Proof_global.t` and the type of "proof object associated to a constant, the new `Lemmas.t`. This way, we can move the terminator setup to the higher layer in `vernac`, which is the one that really knows about constants, paving the way for further simplification and in particular for a unified handling of constant saving by removal of the control inversion here. Terminators are now internal to `Lemmas`, as it is the only part of the code applying them. As a consequence, proof nesting is now handled by `Lemmas`, and `Proof_global.t` is just a single `Proof.t` plus some environmental meta-data. We are also enable considerable simplification in a future PR, as this patch makes `Proof.t` and `Proof_global.t` essentially the same, so we should expect to handle them under a unified interface. --- plugins/derive/derive.ml | 24 +++++++++++------------- 1 file changed, 11 insertions(+), 13 deletions(-) (limited to 'plugins/derive/derive.ml') diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 7c0f269481..fd5b3a7e48 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -22,7 +22,7 @@ let map_const_entry_body (f:constr->constr) (x:Safe_typing.private_constants Ent (which can contain references to [f]) in the context extended by [f:=?x]. When the proof ends, [f] is defined as the value of [?x] and [lemma] as the proof. *) -let start_deriving f suchthat lemma = +let start_deriving f suchthat name : Lemmas.t = let env = Global.env () in let sigma = Evd.from_env env in @@ -48,7 +48,6 @@ let start_deriving f suchthat lemma = (* The terminator handles the registering of constants when the proof is closed. *) let terminator com = - let open Proof_global in (* Extracts the relevant information from the proof. [Admitted] and [Save] result in user errors. [opaque] is [true] if the proof was concluded by [Qed], and [false] if [Defined]. [f_def] @@ -56,10 +55,10 @@ let start_deriving f suchthat lemma = [suchthat], respectively. *) let (opaque,f_def,lemma_def) = match com with - | Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.") - | Proved (_,Some _,_) -> + | Lemmas.Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.") + | Lemmas.Proved (_,Some _,_) -> CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name.") - | Proved (opaque, None, obj) -> + | Lemmas.Proved (opaque, None, obj) -> match Proof_global.(obj.entries) with | [_;f_def;lemma_def] -> opaque <> Proof_global.Transparent , f_def , lemma_def @@ -97,12 +96,11 @@ let start_deriving f suchthat lemma = Entries.DefinitionEntry lemma_def , Decl_kinds.(IsProof Proposition) in - ignore (Declare.declare_constant lemma lemma_def) - in + ignore (Declare.declare_constant name lemma_def) + in - let terminator = Proof_global.make_terminator terminator in - let pstate = Proof_global.start_dependent_proof lemma kind goals terminator in - Proof_global.modify_proof begin fun p -> - let p,_,() = Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p in - p - end pstate + let terminator ?hook _ = Lemmas.make_terminator terminator in + let lemma = Lemmas.start_dependent_lemma name kind goals ~terminator in + Lemmas.simple_with_proof begin fun _ p -> + Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p + end lemma -- cgit v1.2.3 From cb84805a1758ab52506f74207dacd80a8f07224e Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 14 Feb 2019 12:45:49 +0100 Subject: [save_proof] Make terminator API internal. We refactor the terminator API to make it more internal. Indeed we remove `set_terminator` and `get_terminator` is only there due to access to internals in the STM `save_proof` path by the infamous `?proof` parameter. After this only 2 non-standard terminators remain: obligations and derive. We will refactor those in next PRs. --- plugins/derive/derive.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/derive/derive.ml') diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index fd5b3a7e48..cff8214438 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -99,7 +99,7 @@ let start_deriving f suchthat name : Lemmas.t = ignore (Declare.declare_constant name lemma_def) in - let terminator ?hook _ = Lemmas.make_terminator terminator in + let terminator ?hook _ = Lemmas.Internal.make_terminator terminator in let lemma = Lemmas.start_dependent_lemma name kind goals ~terminator in Lemmas.simple_with_proof begin fun _ p -> Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p -- cgit v1.2.3 From 879475156ccbfb14687ed9a02b04f8cf2422d698 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 22 May 2019 17:29:22 +0200 Subject: [proof] Uniformize Proof_global API We rename modify to map [more in line with the rest of the system] and make the endline function specific, as it is only used in one case. --- plugins/derive/derive.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/derive/derive.ml') diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index cff8214438..79d1c7520f 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -101,6 +101,6 @@ let start_deriving f suchthat name : Lemmas.t = let terminator ?hook _ = Lemmas.Internal.make_terminator terminator in let lemma = Lemmas.start_dependent_lemma name kind goals ~terminator in - Lemmas.simple_with_proof begin fun _ p -> + Lemmas.pf_map (Proof_global.map_proof begin fun p -> Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p - end lemma + end) lemma -- cgit v1.2.3