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/comProgramFixpoint.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'vernac/comProgramFixpoint.ml') diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 4aa46e0a86..e51a786cb0 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -314,8 +314,8 @@ let do_program_recursive ~scope ~poly fixkind fixl = end in let uctx = Evd.evar_universe_context evd in let kind = match fixkind with - | Declare.Obls.IsFixpoint _ -> Decls.Fixpoint - | Declare.Obls.IsCoFixpoint -> Decls.CoFixpoint + | Declare.Obls.IsFixpoint _ -> Decls.(IsDefinition Fixpoint) + | Declare.Obls.IsCoFixpoint -> Decls.(IsDefinition CoFixpoint) in let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~udecl ~uctx ntns fixkind -- 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/comProgramFixpoint.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'vernac/comProgramFixpoint.ml') diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index e51a786cb0..87aa5d9b2d 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -290,7 +290,8 @@ let do_program_recursive ~scope ~poly fixkind fixl = let evars, _, def, typ = RetrieveObl.retrieve_obligations env name evm (List.length rec_sign) def typ in - ({ Declare.Recthm.name; typ; impargs; args = [] }, def, evars) + let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in + (cinfo, def, evars) in let (fixnames,fixrs,fixdefs,fixtypes) = fix in let fiximps = List.map pi2 info in -- cgit v1.2.3 From 06159c53e84ab1cff0299890767576972eaf83c2 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 23 Jun 2020 22:18:23 +0200 Subject: [obligation] Switch to new declare info API. --- vernac/comProgramFixpoint.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'vernac/comProgramFixpoint.ml') diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 87aa5d9b2d..381b6cb9fa 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -260,8 +260,10 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = RetrieveObl.retrieve_obligations env recname sigma 0 def typ in let uctx = Evd.evar_universe_context sigma in - ignore(Obligations.add_definition ~name:recname ~term:evars_def ~udecl - ~poly evars_typ ~uctx evars ~hook) + let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ () in + let info = Declare.Info.make ~udecl ~poly ~hook () in + let _ : Declare.progress = Obligations.add_definition ~cinfo ~info ~term:evars_def ~uctx evars in + () let out_def = function | Some def -> def @@ -319,7 +321,8 @@ let do_program_recursive ~scope ~poly fixkind fixl = | Declare.Obls.IsCoFixpoint -> Decls.(IsDefinition CoFixpoint) in let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in - Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~udecl ~uctx ntns fixkind + let info = Declare.Info.make ~poly ~scope ~kind ~udecl () in + Obligations.add_mutual_definitions defs ~info ~uctx ~ntns fixkind let do_fixpoint ~scope ~poly l = let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in -- cgit v1.2.3 From 4a2c8653c0b2f5e73db769a8ea6bf79b76086524 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 23 Jun 2020 22:36:22 +0200 Subject: [declare] Merge remaining obligations bits into Declare This allows us to remove a large chunk of the internal API, and is the pre-requisite to get rid of [Proof_ending], and even more refactoring on the declare path. --- vernac/comProgramFixpoint.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'vernac/comProgramFixpoint.ml') diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 381b6cb9fa..b04aaa7e6f 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -262,7 +262,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = let uctx = Evd.evar_universe_context sigma in let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ () in let info = Declare.Info.make ~udecl ~poly ~hook () in - let _ : Declare.progress = Obligations.add_definition ~cinfo ~info ~term:evars_def ~uctx evars in + let _ : Declare.progress = Declare.Obls.add_definition ~cinfo ~info ~term:evars_def ~uctx evars in () let out_def = function @@ -322,7 +322,7 @@ let do_program_recursive ~scope ~poly fixkind fixl = in let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in let info = Declare.Info.make ~poly ~scope ~kind ~udecl () in - Obligations.add_mutual_definitions defs ~info ~uctx ~ntns fixkind + Declare.Obls.add_mutual_definitions defs ~info ~uctx ~ntns fixkind let do_fixpoint ~scope ~poly l = let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in -- cgit v1.2.3 From 4ad9fa2b257184f9955216fc8345508c217c762d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 23 Jun 2020 23:07:04 +0200 Subject: [declare] Some more cleanup on unused functions after the last commits. --- vernac/comProgramFixpoint.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'vernac/comProgramFixpoint.ml') diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index b04aaa7e6f..37615fa09c 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -262,7 +262,8 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = let uctx = Evd.evar_universe_context sigma in let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ () in let info = Declare.Info.make ~udecl ~poly ~hook () in - let _ : Declare.progress = Declare.Obls.add_definition ~cinfo ~info ~term:evars_def ~uctx evars in + let _ : Declare.Obls.progress = + Declare.Obls.add_definition ~cinfo ~info ~term:evars_def ~uctx evars in () let out_def = function -- cgit v1.2.3