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. --- vernac/comFixpoint.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/comFixpoint.ml') diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 0b75e7f410..2995df4a66 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -322,7 +322,7 @@ let do_fixpoint_common (fixl : Vernacexpr.fixpoint_expr list) = let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl in fixl, ntns, fix, List.map compute_possible_guardness_evidences info -let do_fixpoint_interactive ~scope ~poly l : Lemmas.t = +let do_fixpoint_interactive ~scope ~poly l : Declare.Proof.t = let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes ~scope ~poly fix ntns in lemma -- cgit v1.2.3 From 2ac5353d24133cbca97a85617942d38aed0cc9a3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 25 May 2020 14:13:54 +0200 Subject: [declare] Remove mutual internals from Info.t structure. We move the advanced proof initialization routine to Declare, and stop exposing implementation internals in `Info.t` constructor. --- vernac/comFixpoint.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/comFixpoint.ml') diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 2995df4a66..5bf3350777 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -271,7 +271,7 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs let init_terms = Some fixdefs in let evd = Evd.from_ctx ctx in let lemma = - Lemmas.start_lemma_with_initialization ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl + Declare.start_proof_with_initialization ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl evd (Some(cofix,indexes,init_terms)) thms None in (* Declare notations *) List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; -- cgit v1.2.3 From 1f121ebf2990dc25899f2f3eb138eddd147483cf Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 15 May 2020 02:42:38 +0200 Subject: [declare] Refactor constant information into a record. This improves the interface, and allows even more sealing of the API. This is yet work in progress. --- vernac/comFixpoint.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'vernac/comFixpoint.ml') diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 5bf3350777..925a2d8389 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -283,9 +283,10 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt let fixdefs = List.map Option.get fixdefs in let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in let fix_kind = Decls.IsDefinition fix_kind in + let info = Declare.CInfo.make ~scope ~opaque:false ~kind:fix_kind ~poly ~udecl () in let _ : GlobRef.t list = - Declare.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx - ~possible_indexes:indexes ~udecl ~ntns ~rec_declaration + Declare.declare_mutually_recursive ~info ~uctx + ~possible_indexes:indexes ~ntns ~rec_declaration fixitems in () -- 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`. --- vernac/comFixpoint.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/comFixpoint.ml') diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 925a2d8389..99db8df803 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -271,7 +271,7 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs let init_terms = Some fixdefs in let evd = Evd.from_ctx ctx in let lemma = - Declare.start_proof_with_initialization ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl + Declare.Proof.start_with_initialization ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl evd (Some(cofix,indexes,init_terms)) thms None in (* Declare notations *) List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; -- cgit v1.2.3 From c7a62d0ee0205dfe5bef4bb874c04f1978d4b5c3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 18 Jun 2020 20:14:19 +0200 Subject: [declare] Refactor analysis and construction of mutual lemmas When declaring a lemma, the code path is quite different depending on whether the lemma is inferred to be a mutually-defined lemma or not. We refactor the code path in declare to reflect that; this will allow to better organize constant information and to reuse the `Recthm.t` type in particular. --- vernac/comFixpoint.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'vernac/comFixpoint.ml') diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 99db8df803..304df6fe93 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -271,8 +271,8 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs let init_terms = Some fixdefs in let evd = Evd.from_ctx ctx in let lemma = - Declare.Proof.start_with_initialization ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl - evd (Some(cofix,indexes,init_terms)) thms None in + Declare.Proof.start_mutual_with_initialization ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl + evd ~mutual_info:(cofix,indexes,init_terms) thms None in (* Declare notations *) List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; lemma -- 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. --- vernac/comFixpoint.ml | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) (limited to 'vernac/comFixpoint.ml') diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 304df6fe93..0f34adf1c7 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -257,11 +257,9 @@ let build_recthms ~indexes fixnames fixtypes fiximps = in let thms = List.map3 (fun name typ (ctx,impargs,_) -> - { Declare.Recthm.name - ; typ - ; args = List.map Context.Rel.Declaration.get_name ctx - ; impargs}) - fixnames fixtypes fiximps + let args = List.map Context.Rel.Declaration.get_name ctx in + Declare.CInfo.make ~name ~typ ~args ~impargs () + ) fixnames fixtypes fiximps in fix_kind, cofix, thms @@ -270,9 +268,10 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs let indexes = Option.default [] indexes in let init_terms = Some fixdefs in let evd = Evd.from_ctx ctx in + let info = Declare.Info.make ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl () in let lemma = - Declare.Proof.start_mutual_with_initialization ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl - evd ~mutual_info:(cofix,indexes,init_terms) thms None in + Declare.Proof.start_mutual_with_initialization ~info + evd ~mutual_info:(cofix,indexes,init_terms) ~cinfo:thms None in (* Declare notations *) List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; lemma @@ -283,11 +282,11 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt let fixdefs = List.map Option.get fixdefs in let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in let fix_kind = Decls.IsDefinition fix_kind in - let info = Declare.CInfo.make ~scope ~opaque:false ~kind:fix_kind ~poly ~udecl () in + let info = Declare.Info.make ~scope ~kind:fix_kind ~poly ~udecl () in + let cinfo = fixitems in let _ : GlobRef.t list = - Declare.declare_mutually_recursive ~info ~uctx + Declare.declare_mutually_recursive ~cinfo ~info ~opaque:false ~uctx ~possible_indexes:indexes ~ntns ~rec_declaration - fixitems in () -- cgit v1.2.3