From 17ba18d81e5fe3dc153b1c12ac1b8daeb5474d48 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 2 May 2019 06:10:29 +0200 Subject: [lemmas] Turn Lemmas.info into a proper type with constructor. Lemmas.info was a bit out of hand, as well as the parameters to the `start_*` family. Most of the info is not needed and should hopefully remain constrained to special cases, most callers only set the hook, and obligations should be better served by a `start_obligation` function soon. --- plugins/funind/invfun.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'plugins/funind/invfun.ml') diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 2020881c7c..48b5e56635 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -804,10 +804,10 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let lem_id = mk_correct_id f_id in let (typ,_) = lemmas_types_infos.(i) in let lemma = Lemmas.start_lemma - lem_id - Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) - !evd - typ in + ~name:lem_id + ~kind:Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) + !evd + typ in let lemma = fst @@ Lemmas.by (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") (proving_tac i))) lemma in @@ -865,8 +865,8 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list Ensures by: obvious i*) let lem_id = mk_complete_id f_id in - let lemma = Lemmas.start_lemma lem_id - Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) sigma + let lemma = Lemmas.start_lemma ~name:lem_id + ~kind:Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) sigma (fst lemmas_types_infos.(i)) in let lemma = fst (Lemmas.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") -- cgit v1.2.3 From fd2d2a8178d78e441fb3191cf112ed517dc791af Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 22 May 2019 05:33:10 +0200 Subject: [proof] Remove duplicated universe polymorphic from decl_kinds This information is already present on `Proof.t`, so we extract it form there. Moreover, this information is essential to the lower-level proof, as opposed to the "kind" information which is only relevant to the vernac layer; we will move it thus to its proper layer in subsequent commits. --- plugins/funind/invfun.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'plugins/funind/invfun.ml') diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 48b5e56635..e5b0a5d032 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -805,7 +805,8 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let (typ,_) = lemmas_types_infos.(i) in let lemma = Lemmas.start_lemma ~name:lem_id - ~kind:Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) + ~poly:false + ~kind:Decl_kinds.(Global ImportDefaultBehavior,Proof Theorem) !evd typ in let lemma = fst @@ Lemmas.by @@ -866,8 +867,9 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list i*) let lem_id = mk_complete_id f_id in let lemma = Lemmas.start_lemma ~name:lem_id - ~kind:Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) sigma - (fst lemmas_types_infos.(i)) in + ~poly:false + ~kind:Decl_kinds.(Global ImportDefaultBehavior,Proof Theorem) sigma + (fst lemmas_types_infos.(i)) in let lemma = fst (Lemmas.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") (proving_tac i))) lemma) in -- cgit v1.2.3 From 8b903319eae4d645f9385e8280d04d18a4f3a2bc Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 6 Jun 2019 06:09:24 +0200 Subject: [lemmas] [proof] Split proof kinds into per-layer components. We split `{goal,declaration,assumption}_kind` into their components. This makes sense as each part of this triple is handled by a different layer, namely: - `polymorphic` status: necessary for the lower engine layers; - `locality`: only used in `vernac` top-level constants - `kind`: merely used for cosmetic purposes [could indeed be removed / pushed upwards] We also profit from this refactoring to add some named parameters to the top-level definition API which is quite parameter-hungry. More refactoring is possible and will come in further commits, in particular this is a step towards unifying the definition / lemma save path. --- plugins/funind/invfun.ml | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) (limited to 'plugins/funind/invfun.ml') diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index e5b0a5d032..1ab64ac1b2 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -803,10 +803,13 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list i*) let lem_id = mk_correct_id f_id in let (typ,_) = lemmas_types_infos.(i) in + let info = Lemmas.Info.make + ~scope:Decl_kinds.(Global ImportDefaultBehavior) + ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false - ~kind:Decl_kinds.(Global ImportDefaultBehavior,Proof Theorem) + ~info !evd typ in let lemma = fst @@ Lemmas.by @@ -866,13 +869,14 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list Ensures by: obvious i*) let lem_id = mk_complete_id f_id in - let lemma = Lemmas.start_lemma ~name:lem_id - ~poly:false - ~kind:Decl_kinds.(Global ImportDefaultBehavior,Proof Theorem) sigma - (fst lemmas_types_infos.(i)) in + let info = Lemmas.Info.make + ~scope:Decl_kinds.(Global ImportDefaultBehavior) + ~kind:Decl_kinds.(Proof Theorem) () in + let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false ~info + sigma (fst lemmas_types_infos.(i)) in let lemma = fst (Lemmas.by - (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") - (proving_tac i))) lemma) in + (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") + (proving_tac i))) lemma) in let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in let finfo = find_Function_infos (fst f_as_constant) in let _,lem_cst_constr = Evd.fresh_global -- cgit v1.2.3 From b2aae7ba35a90e695d34f904c74f5156385344a9 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 6 Jun 2019 13:21:48 +0200 Subject: [api] Move `locality` from `library` to `vernac`. This datatype does belong to this layer. --- plugins/funind/invfun.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/funind/invfun.ml') diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 1ab64ac1b2..587e1fc2e8 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -804,7 +804,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let lem_id = mk_correct_id f_id in let (typ,_) = lemmas_types_infos.(i) in let info = Lemmas.Info.make - ~scope:Decl_kinds.(Global ImportDefaultBehavior) + ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in let lemma = Lemmas.start_lemma ~name:lem_id @@ -870,7 +870,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list i*) let lem_id = mk_complete_id f_id in let info = Lemmas.Info.make - ~scope:Decl_kinds.(Global ImportDefaultBehavior) + ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:Decl_kinds.(Proof Theorem) () in let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false ~info sigma (fst lemmas_types_infos.(i)) in -- cgit v1.2.3