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. --- plugins/ltac/extratactics.mlg | 4 ++-- plugins/ltac/g_ltac.mlg | 2 +- plugins/ltac/rewrite.ml | 6 +++--- plugins/ltac/rewrite.mli | 4 ++-- 4 files changed, 8 insertions(+), 8 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index ffb597d4cb..40c64a1c26 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -918,7 +918,7 @@ END VERNAC COMMAND EXTEND GrabEvars STATE proof | [ "Grab" "Existential" "Variables" ] => { classify_as_proofstep } - -> { fun ~pstate -> Declare.Proof.map_proof (fun p -> Proof.V82.grab_evars p) pstate } + -> { fun ~pstate -> Declare.Proof.map ~f:(fun p -> Proof.V82.grab_evars p) pstate } END (* Shelves all the goals under focus. *) @@ -950,7 +950,7 @@ END VERNAC COMMAND EXTEND Unshelve STATE proof | [ "Unshelve" ] => { classify_as_proofstep } - -> { fun ~pstate -> Declare.Proof.map_proof (fun p -> Proof.unshelve p) pstate } + -> { fun ~pstate -> Declare.Proof.map ~f:(fun p -> Proof.unshelve p) pstate } END (* Gives up on the goals under focus: the goals are considered solved, diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 996f6b3eb3..114acaa412 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -363,7 +363,7 @@ let print_info_trace = let vernac_solve ~pstate n info tcom b = let open Goal_select in - let pstate, status = Declare.Proof.map_fold_proof_endline (fun etac p -> + let pstate, status = Declare.Proof.map_fold_endline ~f:(fun etac p -> let with_end_tac = if b then Some etac else None in let global = match n with SelectAll | SelectList _ -> true | _ -> false in let info = Option.append info (print_info_trace ()) in diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 4bc8d61258..e784d6e682 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1978,7 +1978,7 @@ let add_morphism_as_parameter atts m n : unit = (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global cst); declare_projection n instance_id cst -let add_morphism_interactive atts m n : Lemmas.t = +let add_morphism_interactive atts m n : Declare.Proof.t = init_setoid (); let instance_id = add_suffix n "_Proper" in let env = Global.env () in @@ -1996,11 +1996,11 @@ let add_morphism_interactive atts m n : Lemmas.t = | _ -> assert false in let hook = Declare.Hook.make hook in - let info = Lemmas.Info.make ~hook ~kind () in + let info = Declare.Info.make ~hook ~kind () in Flags.silently (fun () -> let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~info evd morph in - fst (Lemmas.by (Tacinterp.interp tac) lemma)) () + fst (Declare.by (Tacinterp.interp tac) lemma)) () let add_morphism atts binders m s n = init_setoid (); diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 1161c84e6a..60a66dd861 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -101,7 +101,7 @@ val add_setoid -> Id.t -> unit -val add_morphism_interactive : rewrite_attributes -> constr_expr -> Id.t -> Lemmas.t +val add_morphism_interactive : rewrite_attributes -> constr_expr -> Id.t -> Declare.Proof.t val add_morphism_as_parameter : rewrite_attributes -> constr_expr -> Id.t -> unit val add_morphism @@ -110,7 +110,7 @@ val add_morphism -> constr_expr -> constr_expr -> Id.t - -> Lemmas.t + -> Declare.Proof.t val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr -- 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. --- plugins/ltac/rewrite.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index e784d6e682..914dc96648 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1999,7 +1999,7 @@ let add_morphism_interactive atts m n : Declare.Proof.t = let info = Declare.Info.make ~hook ~kind () in Flags.silently (fun () -> - let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~info evd morph in + let lemma = Declare.start_proof ~name:instance_id ~poly ~info ~impargs:[] ~udecl:UState.default_univ_decl evd morph in fst (Declare.by (Tacinterp.interp tac) lemma)) () let add_morphism atts binders m s n = -- 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. --- plugins/ltac/rewrite.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 914dc96648..67d09acfda 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1902,8 +1902,9 @@ let declare_projection name instance_id r = let types = Some (it_mkProd_or_LetIn typ ctx) in let kind, opaque, scope = Decls.(IsDefinition Definition), false, Declare.Global Declare.ImportDefaultBehavior in let impargs, udecl = [], UState.default_univ_decl in + let info = Declare.CInfo.make ~scope ~kind ~opaque ~impargs ~udecl ~poly () in let _r : GlobRef.t = - Declare.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma + Declare.declare_definition ~name ~info ~types ~body sigma in () let build_morphism_signature env sigma m = -- 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. --- plugins/ltac/rewrite.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 67d09acfda..0bf97fefa6 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1900,7 +1900,7 @@ let declare_projection name instance_id r = in it_mkProd_or_LetIn ccl ctx in let types = Some (it_mkProd_or_LetIn typ ctx) in - let kind, opaque, scope = Decls.(IsDefinition Definition), false, Declare.Global Declare.ImportDefaultBehavior in + let kind, opaque, scope = Decls.(IsDefinition Definition), false, Locality.Global Locality.ImportDefaultBehavior in let impargs, udecl = [], UState.default_univ_decl in let info = Declare.CInfo.make ~scope ~kind ~opaque ~impargs ~udecl ~poly () in let _r : GlobRef.t = @@ -1968,7 +1968,7 @@ let add_morphism_as_parameter atts m n : unit = let env = Global.env () in let evd = Evd.from_env env in let poly = atts.polymorphic in - let kind, opaque, scope = Decls.(IsAssumption Logical), false, Declare.Global Declare.ImportDefaultBehavior in + let kind, opaque, scope = Decls.(IsAssumption Logical), false, Locality.Global Locality.ImportDefaultBehavior in let impargs, udecl = [], UState.default_univ_decl in let evd, types = build_morphism_signature env evd m in let evd, pe = Declare.prepare_parameter ~poly ~udecl ~types evd in -- 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. --- plugins/ltac/rewrite.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 0bf97fefa6..0c1c763b64 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -2000,7 +2000,7 @@ let add_morphism_interactive atts m n : Declare.Proof.t = let info = Declare.Info.make ~hook ~kind () in Flags.silently (fun () -> - let lemma = Declare.start_proof ~name:instance_id ~poly ~info ~impargs:[] ~udecl:UState.default_univ_decl evd morph in + let lemma = Declare.start_proof ~name:instance_id ~poly ~info ~impargs:[] evd morph in fst (Declare.by (Tacinterp.interp tac) lemma)) () let add_morphism atts binders m s n = -- 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`. --- plugins/ltac/rewrite.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 0c1c763b64..405fe7b844 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -2000,8 +2000,8 @@ let add_morphism_interactive atts m n : Declare.Proof.t = let info = Declare.Info.make ~hook ~kind () in Flags.silently (fun () -> - let lemma = Declare.start_proof ~name:instance_id ~poly ~info ~impargs:[] evd morph in - fst (Declare.by (Tacinterp.interp tac) lemma)) () + let lemma = Declare.Proof.start ~name:instance_id ~poly ~info ~impargs:[] evd morph in + fst (Declare.Proof.by (Tacinterp.interp tac) lemma)) () let add_morphism atts binders m s n = init_setoid (); -- 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. --- plugins/ltac/rewrite.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 405fe7b844..f16d0717df 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1902,9 +1902,10 @@ let declare_projection name instance_id r = let types = Some (it_mkProd_or_LetIn typ ctx) in let kind, opaque, scope = Decls.(IsDefinition Definition), false, Locality.Global Locality.ImportDefaultBehavior in let impargs, udecl = [], UState.default_univ_decl in - let info = Declare.CInfo.make ~scope ~kind ~opaque ~impargs ~udecl ~poly () in + let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types () in + let info = Declare.Info.make ~scope ~kind ~udecl ~poly () in let _r : GlobRef.t = - Declare.declare_definition ~name ~info ~types ~body sigma + Declare.declare_definition ~cinfo ~info ~opaque ~body sigma in () let build_morphism_signature env sigma m = @@ -1997,10 +1998,11 @@ let add_morphism_interactive atts m n : Declare.Proof.t = | _ -> assert false in let hook = Declare.Hook.make hook in - let info = Declare.Info.make ~hook ~kind () in Flags.silently (fun () -> - let lemma = Declare.Proof.start ~name:instance_id ~poly ~info ~impargs:[] evd morph in + let cinfo = Declare.CInfo.make ~name:instance_id ~typ:morph () in + let info = Declare.Info.make ~poly ~hook ~kind () in + let lemma = Declare.Proof.start ~cinfo ~info evd in fst (Declare.Proof.by (Tacinterp.interp tac) lemma)) () let add_morphism atts binders m s n = -- 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. --- plugins/ltac/g_obligations.mlg | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index 498b33d1a8..81ee6ed5bb 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -28,7 +28,7 @@ let () = let tac = Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () -> snd (get_default_tactic ()) end in - Obligations.default_tactic := tac + Declare.Obls.default_tactic := tac let with_tac f tac = let env = Genintern.empty_glob_sign (Global.env ()) in @@ -78,10 +78,10 @@ GRAMMAR EXTEND Gram { -open Obligations +open Declare.Obls -let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac -let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac +let obligation obl tac = with_tac (fun t -> obligation obl t) tac +let next_obligation obl tac = with_tac (fun t -> next_obligation obl t) tac let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[])) -- cgit v1.2.3