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/comDefinition.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/comDefinition.ml') diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index d56917271c..a791e67bb1 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -127,7 +127,7 @@ let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c c interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in let term, ty, uctx, obls = Declare.prepare_obligation ~name ~body ~types evd in - let _ : Declare.Obls.progress = + let _ : Declare.progress = Obligations.add_definition ~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls in () -- 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/comDefinition.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'vernac/comDefinition.ml') diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index a791e67bb1..c89de88e95 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -116,9 +116,9 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in let kind = Decls.IsDefinition kind in + let info = Declare.CInfo.make ~scope ~kind ?hook ~opaque:false ~impargs ~udecl ~poly () in let _ : Names.GlobRef.t = - Declare.declare_definition ~name ~scope ~kind ?hook ~impargs - ~opaque:false ~poly evd ~udecl ~types ~body + Declare.declare_definition ~name ~info ~types ~body evd in () let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = -- 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/comDefinition.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'vernac/comDefinition.ml') diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index c89de88e95..d5ab9f03be 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -116,9 +116,10 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in let kind = Decls.IsDefinition kind in - let info = Declare.CInfo.make ~scope ~kind ?hook ~opaque:false ~impargs ~udecl ~poly () in + let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types () in + let info = Declare.Info.make ~scope ~kind ?hook ~udecl ~poly () in let _ : Names.GlobRef.t = - Declare.declare_definition ~name ~info ~types ~body evd + Declare.declare_definition ~info ~cinfo ~opaque:false ~body evd in () let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = -- 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/comDefinition.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'vernac/comDefinition.ml') diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index d5ab9f03be..537f713e82 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -127,8 +127,10 @@ let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c c let (body, types), evd, udecl, impargs = interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in - let term, ty, uctx, obls = Declare.prepare_obligation ~name ~body ~types evd in + let term, typ, uctx, obls = Declare.prepare_obligation ~name ~body ~types evd in let _ : Declare.progress = + let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in + let info = Declare.Info.make ~udecl ~scope ~poly ~kind ?hook () in Obligations.add_definition - ~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls + ~cinfo ~info ~term ~uctx obls 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/comDefinition.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'vernac/comDefinition.ml') diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 537f713e82..5860626917 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -127,10 +127,9 @@ let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c c let (body, types), evd, udecl, impargs = interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in - let term, typ, uctx, obls = Declare.prepare_obligation ~name ~body ~types evd in + let term, typ, uctx, obls = Declare.Obls.prepare_obligation ~name ~body ~types evd in let _ : Declare.progress = let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in let info = Declare.Info.make ~udecl ~scope ~poly ~kind ?hook () in - Obligations.add_definition - ~cinfo ~info ~term ~uctx obls + Declare.Obls.add_definition ~cinfo ~info ~term ~uctx obls 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/comDefinition.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/comDefinition.ml') diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 5860626917..f9b2d8b1d1 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -128,7 +128,7 @@ let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c c interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in let term, typ, uctx, obls = Declare.Obls.prepare_obligation ~name ~body ~types evd in - let _ : Declare.progress = + let _ : Declare.Obls.progress = let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in let info = Declare.Info.make ~udecl ~scope ~poly ~kind ?hook () in Declare.Obls.add_definition ~cinfo ~info ~term ~uctx obls -- cgit v1.2.3