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/funind/functional_principles_proofs.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'plugins/funind/functional_principles_proofs.ml') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index b864b18887..652f942cb9 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -856,9 +856,10 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num let lemma = Lemmas.start_lemma ~name:(mk_equation_id f_id) ~poly:false evd lemma_type in - let lemma, _ = Lemmas.by (Proofview.V82.tactic prove_replacement) lemma in + let lemma, _ = Declare.by (Proofview.V82.tactic prove_replacement) lemma in let () = - Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent ~idopt:None + Declare.save_lemma_proved ~proof:lemma ~opaque:Declare.Transparent + ~idopt:None in evd -- 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/funind/functional_principles_proofs.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'plugins/funind/functional_principles_proofs.ml') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 652f942cb9..c0d7c1e8e6 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -853,8 +853,10 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num (*i The next call to mk_equation_id is valid since we are constructing the lemma Ensures by: obvious i*) + let info = Declare.Info.make () in let lemma = - Lemmas.start_lemma ~name:(mk_equation_id f_id) ~poly:false evd lemma_type + Declare.start_proof ~name:(mk_equation_id f_id) ~poly:false ~info + ~impargs:[] ~udecl:UState.default_univ_decl evd lemma_type in let lemma, _ = Declare.by (Proofview.V82.tactic prove_replacement) lemma in let () = -- cgit v1.2.3 From a6d663c85d71b3cce007af23419e8030b8c5ac88 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 25 May 2020 14:57:44 +0200 Subject: [declare] [api] Removal of duplicated type aliases. --- plugins/funind/functional_principles_proofs.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind/functional_principles_proofs.ml') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index c0d7c1e8e6..6ec12db952 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -860,7 +860,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num in let lemma, _ = Declare.by (Proofview.V82.tactic prove_replacement) lemma in let () = - Declare.save_lemma_proved ~proof:lemma ~opaque:Declare.Transparent + Declare.save_lemma_proved ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None in evd -- 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/funind/functional_principles_proofs.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind/functional_principles_proofs.ml') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 6ec12db952..2c85ae079f 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -856,7 +856,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num let info = Declare.Info.make () in let lemma = Declare.start_proof ~name:(mk_equation_id f_id) ~poly:false ~info - ~impargs:[] ~udecl:UState.default_univ_decl evd lemma_type + ~impargs:[] evd lemma_type in let lemma, _ = Declare.by (Proofview.V82.tactic prove_replacement) lemma in let () = -- 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/funind/functional_principles_proofs.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'plugins/funind/functional_principles_proofs.ml') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 2c85ae079f..79f311e282 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -855,13 +855,14 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num constructing the lemma Ensures by: obvious i*) let info = Declare.Info.make () in let lemma = - Declare.start_proof ~name:(mk_equation_id f_id) ~poly:false ~info + Declare.Proof.start ~name:(mk_equation_id f_id) ~poly:false ~info ~impargs:[] evd lemma_type in - let lemma, _ = Declare.by (Proofview.V82.tactic prove_replacement) lemma in + let lemma, _ = + Declare.Proof.by (Proofview.V82.tactic prove_replacement) lemma + in let () = - Declare.save_lemma_proved ~proof:lemma ~opaque:Vernacexpr.Transparent - ~idopt:None + Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None in evd -- 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/funind/functional_principles_proofs.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/funind/functional_principles_proofs.ml') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 79f311e282..afe89aef6e 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -854,10 +854,10 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num (*i The next call to mk_equation_id is valid since we are constructing the lemma Ensures by: obvious i*) let info = Declare.Info.make () in - let lemma = - Declare.Proof.start ~name:(mk_equation_id f_id) ~poly:false ~info - ~impargs:[] evd lemma_type + let cinfo = + Declare.CInfo.make ~name:(mk_equation_id f_id) ~typ:lemma_type () in + let lemma = Declare.Proof.start ~cinfo ~info evd in let lemma, _ = Declare.Proof.by (Proofview.V82.tactic prove_replacement) lemma in -- cgit v1.2.3 From a5a65ddcf0e476384c827cdf2445bc554eae825a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 24 Jun 2020 14:22:57 +0200 Subject: [declare] Return list of declared global in Proof.save This is needed in rewriter as to avoid hack; indeed it makes sense to propagate this information to the callers of save. --- plugins/funind/functional_principles_proofs.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind/functional_principles_proofs.ml') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index afe89aef6e..2151ad7873 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -861,7 +861,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num let lemma, _ = Declare.Proof.by (Proofview.V82.tactic prove_replacement) lemma in - let () = + let (_ : _ list) = Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None in evd -- cgit v1.2.3