From 43d381ab20035f64ce2edea8639fcd9e1d0453bc Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 25 May 2020 14:09:30 +0200 Subject: [declare] Move proof information to declare. At this point the record in lemmas was just a stub; next commit will stop exposing the internals of mutual information, and pave the way for the refactoring of `Info.t` handling in the Declare interface. --- plugins/derive/derive.ml | 9 ++++----- plugins/derive/derive.mli | 2 +- 2 files changed, 5 insertions(+), 6 deletions(-) (limited to 'plugins/derive') diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index e5665c59b8..633d5dfe3b 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -15,7 +15,7 @@ open Context.Named.Declaration (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 name : Lemmas.t = +let start_deriving f suchthat name : Declare.Proof.t = let env = Global.env () in let sigma = Evd.from_env env in @@ -40,8 +40,7 @@ let start_deriving f suchthat name : Lemmas.t = TNil sigma)))))) in - let info = Lemmas.Info.make ~proof_ending:(Declare.Proof_ending.(End_derive {f; name})) ~kind () in + let info = Declare.Info.make ~proof_ending:(Declare.Proof_ending.(End_derive {f; name})) ~kind () in let lemma = Lemmas.start_dependent_lemma ~name ~poly ~info goals in - Lemmas.pf_map (Declare.Proof.map_proof begin fun p -> - Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p - end) lemma + Declare.Proof.map lemma ~f:(fun p -> + Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p) diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli index ef94c7e78f..06e7dacd36 100644 --- a/plugins/derive/derive.mli +++ b/plugins/derive/derive.mli @@ -16,4 +16,4 @@ val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t - -> Lemmas.t + -> Declare.Proof.t -- cgit v1.2.3 From 671004aac9f9d3b70ef41f81e7b3ea8f190971ec Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 25 May 2020 14:20:24 +0200 Subject: [declare] Remove Lemmas module The module is now a stub. We choose to be explicit on the parameters for now, this will improve in next commits with the refactoring of proof / constant information. --- plugins/derive/derive.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/derive') diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 633d5dfe3b..c4f7638fb9 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -41,6 +41,6 @@ let start_deriving f suchthat name : Declare.Proof.t = in let info = Declare.Info.make ~proof_ending:(Declare.Proof_ending.(End_derive {f; name})) ~kind () in - let lemma = Lemmas.start_dependent_lemma ~name ~poly ~info goals in + let lemma = Declare.start_dependent_proof ~name ~poly ~info ~udecl:UState.default_univ_decl goals in Declare.Proof.map lemma ~f:(fun p -> Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p) -- cgit v1.2.3 From b143d124e140628e5974da4af1b8a70a4d534598 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 25 May 2020 16:30:20 +0200 Subject: [declare] Move udecl to Info structure. --- plugins/derive/derive.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/derive') diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index c4f7638fb9..7779e4f4c7 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -41,6 +41,6 @@ let start_deriving f suchthat name : Declare.Proof.t = in let info = Declare.Info.make ~proof_ending:(Declare.Proof_ending.(End_derive {f; name})) ~kind () in - let lemma = Declare.start_dependent_proof ~name ~poly ~info ~udecl:UState.default_univ_decl goals in + let lemma = Declare.start_dependent_proof ~name ~poly ~info goals in Declare.Proof.map lemma ~f:(fun p -> Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p) -- cgit v1.2.3 From 030bb57d4b7e70d45379cab61903b75bf7a41b19 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 25 May 2020 16:43:01 +0200 Subject: [declare] Reify Proof.t API into the Proof module. This is in preparation for the next commit which will clean-up the current API flow in `Declare`. --- plugins/derive/derive.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/derive') diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 7779e4f4c7..d85d3bd744 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -41,6 +41,6 @@ let start_deriving f suchthat name : Declare.Proof.t = in let info = Declare.Info.make ~proof_ending:(Declare.Proof_ending.(End_derive {f; name})) ~kind () in - let lemma = Declare.start_dependent_proof ~name ~poly ~info goals in + let lemma = Declare.Proof.start_dependent ~name ~poly ~info goals in Declare.Proof.map lemma ~f:(fun p -> Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p) -- cgit v1.2.3 From ea8b9e060dfba9cc8706677e29c26dabaaa87551 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 22 Jun 2020 20:42:39 +0200 Subject: [declare] Improve organization of proof/constant information. We unify information about constants so it is shared among all the paths [interactive, NI, obligations]. IMHO the current setup looks pretty good, with information split into a per-constant record `CInfo.t` and variables affecting mutual definitions at once, which live in `Info.t`. Main information outside our `Info` record is `opaque`, which is provided at different moments in several cases. There are a few nits regarding interactive proofs, which will go away in the next commits. --- plugins/derive/derive.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'plugins/derive') diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index d85d3bd744..27df963e98 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -40,7 +40,8 @@ let start_deriving f suchthat name : Declare.Proof.t = TNil sigma)))))) in - let info = Declare.Info.make ~proof_ending:(Declare.Proof_ending.(End_derive {f; name})) ~kind () in - let lemma = Declare.Proof.start_dependent ~name ~poly ~info goals in + let info = Declare.Info.make ~poly ~kind () in + let proof_ending = Declare.Proof_ending.(End_derive {f; name}) in + let lemma = Declare.Proof.start_dependent ~name ~info ~proof_ending goals in Declare.Proof.map lemma ~f:(fun p -> Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p) -- cgit v1.2.3 From d9dca86f798ce11861f1a4715763cad1aae28e5a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 23 Jun 2020 22:47:53 +0200 Subject: [declare] Remove Proof_ending from the public API This completes the refactoring [for now] of the core `Declare` interface, and will allow much internal refactoring in the future. In particular, we remove the low-level Proof_ending type, and instead introduce higher-level constructors for the several declare users. Future PRs will change the internal representation of proof handling to better enforce some invariants that should hold for specific proofs. --- plugins/derive/derive.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'plugins/derive') diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 27df963e98..027064b75f 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -41,7 +41,6 @@ let start_deriving f suchthat name : Declare.Proof.t = in let info = Declare.Info.make ~poly ~kind () in - let proof_ending = Declare.Proof_ending.(End_derive {f; name}) in - let lemma = Declare.Proof.start_dependent ~name ~info ~proof_ending goals in + let lemma = Declare.Proof.start_derive ~name ~f ~info goals in Declare.Proof.map lemma ~f:(fun p -> Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p) -- cgit v1.2.3