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/classes.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'vernac/classes.ml') diff --git a/vernac/classes.ml b/vernac/classes.ml index 21e2afe6a9..973c6f8e7c 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -345,7 +345,7 @@ let declare_instance_program env sigma ~global ~poly name pri impargs udecl term let hook = Declare.Hook.make hook in let uctx = Evd.evar_universe_context sigma in let scope, kind = Declare.Global Declare.ImportDefaultBehavior, Decls.Instance in - let _ : Declare.Obls.progress = + let _ : Declare.progress = Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook ~impargs ~uctx typ obls in () @@ -358,7 +358,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id let sigma = Evd.reset_future_goals sigma in let kind = Decls.(IsDefinition Instance) in let hook = Declare.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in - let info = Lemmas.Info.make ~hook ~kind () in + let info = Declare.Info.make ~hook ~kind () in (* XXX: We need to normalize the type, otherwise Admitted / Qed will fails! This is due to a bug in proof_global :( *) let termtype = Evarutil.nf_evar sigma termtype in @@ -374,15 +374,15 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id Tactics.New.reduce_after_refine; ] in - let lemma, _ = Lemmas.by init_refine lemma in + let lemma, _ = Declare.by init_refine lemma in lemma | None -> - let lemma, _ = Lemmas.by (Tactics.auto_intros_tac ids) lemma in + let lemma, _ = Declare.by (Tactics.auto_intros_tac ids) lemma in lemma in match tac with | Some tac -> - let lemma, _ = Lemmas.by tac lemma in + let lemma, _ = Declare.by tac lemma in lemma | None -> lemma -- 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. --- vernac/classes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/classes.ml') diff --git a/vernac/classes.ml b/vernac/classes.ml index 973c6f8e7c..f7d8a4b42f 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -362,7 +362,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id (* XXX: We need to normalize the type, otherwise Admitted / Qed will fails! This is due to a bug in proof_global :( *) let termtype = Evarutil.nf_evar sigma termtype in - let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info ~impargs sigma termtype in + let lemma = Declare.start_proof ~name:id ~poly ~udecl ~info ~impargs sigma termtype in (* spiwack: I don't know what to do with the status here. *) let lemma = match term with -- 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/classes.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'vernac/classes.ml') diff --git a/vernac/classes.ml b/vernac/classes.ml index f7d8a4b42f..c4c6a0fa33 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -311,12 +311,12 @@ let instance_hook info global ?hook cst = declare_instance env sigma (Some info) (not global) cst; (match hook with Some h -> h cst | None -> ()) -let declare_instance_constant info global impargs ?hook name udecl poly sigma term termtype = +let declare_instance_constant iinfo global impargs ?hook name udecl poly sigma term termtype = let kind = Decls.(IsDefinition Instance) in let scope = Declare.Global Declare.ImportDefaultBehavior in - let kn = Declare.declare_definition ~name ~kind ~scope ~impargs - ~opaque:false ~poly sigma ~udecl ~types:(Some termtype) ~body:term in - instance_hook info global ?hook kn + let info = Declare.CInfo.make ~kind ~scope ~impargs ~opaque:false ~poly ~udecl () in + let kn = Declare.declare_definition ~name ~info ~types:(Some termtype) ~body:term sigma in + instance_hook iinfo global ?hook kn let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst name = let subst = List.fold_left2 @@ -344,7 +344,8 @@ let declare_instance_program env sigma ~global ~poly name pri impargs udecl term let obls, _, term, typ = RetrieveObl.retrieve_obligations env name sigma 0 term termtype in let hook = Declare.Hook.make hook in let uctx = Evd.evar_universe_context sigma in - let scope, kind = Declare.Global Declare.ImportDefaultBehavior, Decls.Instance in + let scope, kind = Declare.Global Declare.ImportDefaultBehavior, + Decls.IsDefinition Decls.Instance in let _ : Declare.progress = Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook ~impargs ~uctx typ obls in () -- 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. --- vernac/classes.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'vernac/classes.ml') diff --git a/vernac/classes.ml b/vernac/classes.ml index c4c6a0fa33..b36a6fa3a6 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -313,7 +313,7 @@ let instance_hook info global ?hook cst = let declare_instance_constant iinfo global impargs ?hook name udecl poly sigma term termtype = let kind = Decls.(IsDefinition Instance) in - let scope = Declare.Global Declare.ImportDefaultBehavior in + let scope = Locality.Global Locality.ImportDefaultBehavior in let info = Declare.CInfo.make ~kind ~scope ~impargs ~opaque:false ~poly ~udecl () in let kn = Declare.declare_definition ~name ~info ~types:(Some termtype) ~body:term sigma in instance_hook iinfo global ?hook kn @@ -344,7 +344,7 @@ let declare_instance_program env sigma ~global ~poly name pri impargs udecl term let obls, _, term, typ = RetrieveObl.retrieve_obligations env name sigma 0 term termtype in let hook = Declare.Hook.make hook in let uctx = Evd.evar_universe_context sigma in - let scope, kind = Declare.Global Declare.ImportDefaultBehavior, + let scope, kind = Locality.Global Locality.ImportDefaultBehavior, Decls.IsDefinition Decls.Instance in let _ : Declare.progress = Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook ~impargs ~uctx typ obls -- 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. --- vernac/classes.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'vernac/classes.ml') diff --git a/vernac/classes.ml b/vernac/classes.ml index b36a6fa3a6..1397746dd9 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -359,11 +359,11 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id let sigma = Evd.reset_future_goals sigma in let kind = Decls.(IsDefinition Instance) in let hook = Declare.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in - let info = Declare.Info.make ~hook ~kind () in + let info = Declare.Info.make ~hook ~kind ~udecl () in (* XXX: We need to normalize the type, otherwise Admitted / Qed will fails! This is due to a bug in proof_global :( *) let termtype = Evarutil.nf_evar sigma termtype in - let lemma = Declare.start_proof ~name:id ~poly ~udecl ~info ~impargs sigma termtype in + let lemma = Declare.start_proof ~name:id ~poly ~info ~impargs sigma termtype in (* spiwack: I don't know what to do with the status here. *) let lemma = match term with -- 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/classes.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'vernac/classes.ml') diff --git a/vernac/classes.ml b/vernac/classes.ml index 1397746dd9..c8208cd444 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -363,7 +363,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id (* XXX: We need to normalize the type, otherwise Admitted / Qed will fails! This is due to a bug in proof_global :( *) let termtype = Evarutil.nf_evar sigma termtype in - let lemma = Declare.start_proof ~name:id ~poly ~info ~impargs sigma termtype in + let lemma = Declare.Proof.start ~name:id ~poly ~info ~impargs sigma termtype in (* spiwack: I don't know what to do with the status here. *) let lemma = match term with @@ -375,15 +375,15 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id Tactics.New.reduce_after_refine; ] in - let lemma, _ = Declare.by init_refine lemma in + let lemma, _ = Declare.Proof.by init_refine lemma in lemma | None -> - let lemma, _ = Declare.by (Tactics.auto_intros_tac ids) lemma in + let lemma, _ = Declare.Proof.by (Tactics.auto_intros_tac ids) lemma in lemma in match tac with | Some tac -> - let lemma, _ = Declare.by tac lemma in + let lemma, _ = Declare.Proof.by tac lemma in lemma | None -> 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/classes.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'vernac/classes.ml') diff --git a/vernac/classes.ml b/vernac/classes.ml index c8208cd444..94040a9cef 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -314,8 +314,9 @@ let instance_hook info global ?hook cst = let declare_instance_constant iinfo global impargs ?hook name udecl poly sigma term termtype = let kind = Decls.(IsDefinition Instance) in let scope = Locality.Global Locality.ImportDefaultBehavior in - let info = Declare.CInfo.make ~kind ~scope ~impargs ~opaque:false ~poly ~udecl () in - let kn = Declare.declare_definition ~name ~info ~types:(Some termtype) ~body:term sigma in + let cinfo = Declare.CInfo.make ~name ~impargs ~typ:(Some termtype) () in + let info = Declare.Info.make ~kind ~scope ~poly ~udecl () in + let kn = Declare.declare_definition ~cinfo ~info ~opaque:false ~body:term sigma in instance_hook iinfo global ?hook kn let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst name = @@ -359,11 +360,12 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id let sigma = Evd.reset_future_goals sigma in let kind = Decls.(IsDefinition Instance) in let hook = Declare.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in - let info = Declare.Info.make ~hook ~kind ~udecl () in + let info = Declare.Info.make ~hook ~kind ~udecl ~poly () in (* XXX: We need to normalize the type, otherwise Admitted / Qed will fails! This is due to a bug in proof_global :( *) let termtype = Evarutil.nf_evar sigma termtype in - let lemma = Declare.Proof.start ~name:id ~poly ~info ~impargs sigma termtype in + let cinfo = Declare.CInfo.make ~name:id ~impargs ~typ:termtype () in + let lemma = Declare.Proof.start ~cinfo ~info sigma in (* spiwack: I don't know what to do with the status here. *) let lemma = match term with -- 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/classes.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'vernac/classes.ml') diff --git a/vernac/classes.ml b/vernac/classes.ml index 94040a9cef..04321ed844 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -347,8 +347,10 @@ let declare_instance_program env sigma ~global ~poly name pri impargs udecl term let uctx = Evd.evar_universe_context sigma in let scope, kind = Locality.Global Locality.ImportDefaultBehavior, Decls.IsDefinition Decls.Instance in + let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in + let info = Declare.Info.make ~udecl ~scope ~poly ~kind ~hook () in let _ : Declare.progress = - Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook ~impargs ~uctx typ obls + Obligations.add_definition ~cinfo ~info ~term ~uctx obls in () let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl ids term termtype = -- 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/classes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/classes.ml') diff --git a/vernac/classes.ml b/vernac/classes.ml index 04321ed844..f02474a405 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -350,7 +350,7 @@ let declare_instance_program env sigma ~global ~poly name pri impargs udecl term let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in let info = Declare.Info.make ~udecl ~scope ~poly ~kind ~hook () in let _ : Declare.progress = - Obligations.add_definition ~cinfo ~info ~term ~uctx obls + Declare.Obls.add_definition ~cinfo ~info ~term ~uctx obls in () let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl ids term termtype = -- 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/classes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/classes.ml') diff --git a/vernac/classes.ml b/vernac/classes.ml index f02474a405..ba08aa2b94 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -349,7 +349,7 @@ let declare_instance_program env sigma ~global ~poly name pri impargs udecl term Decls.IsDefinition Decls.Instance in let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in let info = Declare.Info.make ~udecl ~scope ~poly ~kind ~hook () in - let _ : Declare.progress = + let _ : Declare.Obls.progress = Declare.Obls.add_definition ~cinfo ~info ~term ~uctx obls in () -- cgit v1.2.3