From 5f937b2f8532b2ccf36c62557934cc2c9150005b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 9 Mar 2020 06:32:00 -0400 Subject: [proof] Miscellaneous cleanup on proof info handling After the refactorings proof information is organized in a slightly different way thus the lower layers don't need to pass info back anymore. --- vernac/declareDef.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/declareDef.mli') diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 1d7fd3a3bf..e999027b44 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -36,7 +36,7 @@ module Hook : sig end val make : (S.t -> unit) -> t - val call : ?hook:t -> ?fix_exn:Future.fix_exn -> S.t -> unit + val call : ?hook:t -> S.t -> unit end val declare_definition -- cgit v1.2.3 From 56ffe818ab7706a82d79b538fdf3af8b23d95f40 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 14 Mar 2020 03:07:42 -0400 Subject: [declare] [obligations] Refactor preparation of obligation entry Preparation of obligation/program entries requires low-level manipulation that does break the abstraction over `proof_entry`; we thus introduce `prepare_obligation`, and move the code that prepares the obligation entry to its own module. This seems to improve separation of concerns, and helps clarify the two of three current models in which Coq operates w.r.t. definitions: - single, ground entries with possibly mutual definitions [regular lemmas] - single, non-ground entries with possibly mutual definitions [obligations] - multiple entries [equations] --- vernac/declareDef.mli | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) (limited to 'vernac/declareDef.mli') diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index e999027b44..27d9460382 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -89,8 +89,7 @@ val declare_mutually_recursive -> Names.GlobRef.t list val prepare_definition - : allow_evars:bool - -> ?opaque:bool + : ?opaque:bool -> ?inline:bool -> poly:bool -> udecl:UState.universe_decl @@ -99,6 +98,17 @@ val prepare_definition -> Evd.evar_map -> Evd.evar_map * Evd.side_effects Declare.proof_entry +val prepare_obligation + : ?opaque:bool + -> ?inline:bool + -> name:Id.t + -> poly:bool + -> udecl:UState.universe_decl + -> types:EConstr.t option + -> body:EConstr.t + -> Evd.evar_map + -> Constr.constr * Constr.types * UState.t * RetrieveObl.obligation_info + val prepare_parameter : allow_evars:bool -> poly:bool -- cgit v1.2.3 From d507679b5b6dfac944e038b6a3ebd9fb8e6998ff Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 14 Mar 2020 03:19:15 -0400 Subject: [declareDef] Cleanup of allow_evars and check_evars We don't the parameter anymore as the paths are too different now. Note that this removes a duplicate `check_evars` that has been in `master` quite some time [double check in `ComDefinition` and in `DeclareDef.prepare_definition`] --- vernac/declareDef.mli | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'vernac/declareDef.mli') diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 27d9460382..f72954d8c2 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -110,8 +110,7 @@ val prepare_obligation -> Constr.constr * Constr.types * UState.t * RetrieveObl.obligation_info val prepare_parameter - : allow_evars:bool - -> poly:bool + : poly:bool -> udecl:UState.universe_decl -> types:EConstr.types -> Evd.evar_map -- cgit v1.2.3 From 8ac27a8261f5f3fb5d4bf2a207a144df07477910 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 14 Mar 2020 03:42:57 -0400 Subject: [declare] Make the type of closed entries opaque. This is a step in forcing all entry creation go thru the preparation functions. We still need to handle plain `Declare.` calls, but this will be next step. We need to leave a backdoor for interactive proofs until we unify proof preparation happening in `Proof_global` with the one happening in `DeclareDef`, but we are getting there. TODO: see how to avoid the normalization problems in DeclareObl --- vernac/declareDef.mli | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) (limited to 'vernac/declareDef.mli') diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index f72954d8c2..9c5cd6fc2a 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -39,6 +39,13 @@ module Hook : sig val call : ?hook:t -> S.t -> unit end +module ClosedDef : sig + type t + + (* Don't use for non-interactive proofs *) + val of_proof_entry : Evd.side_effects Declare.proof_entry -> t +end + val declare_definition : name:Id.t -> scope:locality @@ -46,7 +53,7 @@ val declare_definition -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) -> ubind:UnivNames.universe_binders -> impargs:Impargs.manual_implicits - -> Evd.side_effects Declare.proof_entry + -> ClosedDef.t -> GlobRef.t val declare_assumption @@ -88,15 +95,19 @@ val declare_mutually_recursive -> Recthm.t list -> Names.GlobRef.t list +(* The common use of the returned evar_map is to obtain the universe + binders and context for the hook; we should refactor that soon by + merging prepare and declare. *) val prepare_definition : ?opaque:bool -> ?inline:bool + -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) -> poly:bool -> udecl:UState.universe_decl -> types:EConstr.t option -> body:EConstr.t -> Evd.evar_map - -> Evd.evar_map * Evd.side_effects Declare.proof_entry + -> Evd.evar_map * ClosedDef.t val prepare_obligation : ?opaque:bool -- cgit v1.2.3 From 8fbc927ac40cc707b1a940d8339a2a289755d533 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 14 Mar 2020 16:34:30 -0400 Subject: [declareDef] More consistent handling of universe binders The only reasons that `prepare_definition` returned a sigma were: - to obtain the universe binders to be passed to declare - to obtain the UState.t to be passed to the equations hook We handle this automatically now; it seems like a reasonably good API improvement. However, it is not clear what we do now is right for all cases; must check. --- vernac/declareDef.mli | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) (limited to 'vernac/declareDef.mli') diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 9c5cd6fc2a..8f3db59ba9 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -43,15 +43,17 @@ module ClosedDef : sig type t (* Don't use for non-interactive proofs *) - val of_proof_entry : Evd.side_effects Declare.proof_entry -> t + val of_proof_entry + : uctx:UState.t + -> Evd.side_effects Declare.proof_entry -> t end val declare_definition : name:Id.t -> scope:locality -> kind:Decls.logical_kind - -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) - -> ubind:UnivNames.universe_binders + -> ?hook:Hook.t + -> ?obls:(Id.t * Constr.t) list -> impargs:Impargs.manual_implicits -> ClosedDef.t -> GlobRef.t @@ -95,9 +97,6 @@ val declare_mutually_recursive -> Recthm.t list -> Names.GlobRef.t list -(* The common use of the returned evar_map is to obtain the universe - binders and context for the hook; we should refactor that soon by - merging prepare and declare. *) val prepare_definition : ?opaque:bool -> ?inline:bool @@ -107,7 +106,7 @@ val prepare_definition -> types:EConstr.t option -> body:EConstr.t -> Evd.evar_map - -> Evd.evar_map * ClosedDef.t + -> ClosedDef.t val prepare_obligation : ?opaque:bool -- cgit v1.2.3 From 7d46a32dc928af64e3e111d6d62caa00f93c427c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 18 Mar 2020 05:35:41 -0400 Subject: [declare] Fuse prepare and declare for the non-interactive path. This will allow to share the definition metadata for example with obligations; a bit more work is needed to finally move the preparation of interactive proofs from Proof_global to `prepare_entry`. --- vernac/declareDef.mli | 47 ++++++++++++++++++++++++++--------------------- 1 file changed, 26 insertions(+), 21 deletions(-) (limited to 'vernac/declareDef.mli') diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 8f3db59ba9..3bc1e25f19 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -39,23 +39,39 @@ module Hook : sig val call : ?hook:t -> S.t -> unit end -module ClosedDef : sig - type t - - (* Don't use for non-interactive proofs *) - val of_proof_entry - : uctx:UState.t - -> Evd.side_effects Declare.proof_entry -> t -end +(** Declare an interactively-defined constant *) +val declare_entry + : name:Id.t + -> scope:locality + -> kind:Decls.logical_kind + -> ?hook:Hook.t + -> ?obls:(Id.t * Constr.t) list + -> impargs:Impargs.manual_implicits + -> uctx:UState.t + -> Evd.side_effects Declare.proof_entry + -> GlobRef.t +(** Declares a non-interactive constant; [body] and [types] will be + normalized w.r.t. the passed [evar_map] [sigma]. Universes should + be handled properly, including minimization and restriction. Note + that [sigma] is checked for unresolved evars, thus you should be + careful not to submit open terms or evar maps with stale, + unresolved existentials *) val declare_definition : name:Id.t -> scope:locality -> kind:Decls.logical_kind + -> opaque:bool + -> impargs:Impargs.manual_implicits + -> udecl:UState.universe_decl -> ?hook:Hook.t -> ?obls:(Id.t * Constr.t) list - -> impargs:Impargs.manual_implicits - -> ClosedDef.t + -> poly:bool + -> ?inline:bool + -> types:EConstr.t option + -> body:EConstr.t + -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) + -> Evd.evar_map -> GlobRef.t val declare_assumption @@ -97,17 +113,6 @@ val declare_mutually_recursive -> Recthm.t list -> Names.GlobRef.t list -val prepare_definition - : ?opaque:bool - -> ?inline:bool - -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) - -> poly:bool - -> udecl:UState.universe_decl - -> types:EConstr.t option - -> body:EConstr.t - -> Evd.evar_map - -> ClosedDef.t - val prepare_obligation : ?opaque:bool -> ?inline:bool -- cgit v1.2.3