DeclareThis module provides the functions to declare new variables, parameters, constants and inductive types in the global environment. It also updates some accessory tables such as Nametab (name resolution), Impargs, and Notations.
We provide three main entry points:
start/save functions which will create an interactive proof, allow its modification using tactics, and saving when complete.Note that the API in this file is still in a state of flux, don't hesitate to contact the maintainers if you have any question.
Additionally, this file does contain some low-level functions, marked as such; these functions are unstable and should not be used unless you already know what they are doing.
module Hook : sig ... endDeclaration hooks, to be run when a constant is saved. Use with care, as imperative effects may become not supported in the future.
module CInfo : sig ... endInformation for a single top-level named constant
module Info : sig ... endInformation for a declaration, interactive or not, includes parameters shared by mutual constants
val declare_definition : info:Info.t -> cinfo:EConstr.t option CInfo.t -> opaque:bool -> body:EConstr.t -> ?using:Vernacexpr.section_subset_expr ->
Evd.evar_map -> Names.GlobRef.tDeclares 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
val declare_mutual_definitions : info:Info.t -> cinfo:Constr.t CInfo.t list -> opaque:bool -> uctx:UState.t ->
bodies:Constr.t list -> possible_guard:(Pretyping.possible_guard * Sorts.relevance list) -> ?using:Vernacexpr.section_subset_expr -> unit -> Names.GlobRef.t listmodule OblState : sig ... endsave / save_admitted can update obligations state, so we need to expose the state here
module Proof : sig ... endDeclare.Proof.t Construction of constants using interactive proofs.
Proof entries represent a proof that has been finished, but still not registered with the kernel.
XXX: This is an internal, low-level API and could become scheduled for removal from the public API, use higher-level declare APIs instead
val definition_entry : ?opaque:bool -> ?using:Names.Id.Set.t -> ?inline:bool -> ?types:Constr.types -> ?univs:UState.named_universes_entry ->
Constr.constr -> proof_entryval parameter_entry : ?inline:int -> ?univs:UState.named_universes_entry -> Constr.constr -> parameter_entryval primitive_entry : ?types:(Constr.types * UState.named_universes_entry) -> CPrimitives.op_or_type -> primitive_entryval symbol_entry : ?univs:UState.named_universes_entry -> unfold_fix:bool -> Constr.types -> symbol_entryval declare_entry : ?loc:Loc.t -> name:Names.Id.t -> ?scope:Locality.definition_scope -> kind:Decls.logical_kind -> ?user_warns:Globnames.extended_global_reference UserWarn.with_qf -> ?hook:Hook.t ->
impargs:Impargs.manual_implicits -> uctx:UState.t -> proof_entry -> Names.GlobRef.tXXX: This is an internal, low-level API and could become scheduled for removal from the public API, use higher-level declare APIs instead
type variable_declaration = | SectionLocalDef of {
} | |||
| SectionLocalAssum of {
} |
Declaration of section variables and local definitions
val declare_variable : name:Names.variable -> kind:Decls.logical_kind -> typing_flags:Declarations.typing_flags option -> variable_declaration -> unitDeclaration of local constructions (Variable/Hypothesis/Local)
type constant_entry = | DefinitionEntry of proof_entry |
| ParameterEntry of parameter_entry |
| PrimitiveEntry of primitive_entry |
| SymbolEntry of symbol_entry |
Declaration of global constructions i.e. Definition/Theorem/Axiom/Parameter/...
XXX: This is an internal, low-level API and could become scheduled for removal from the public API, use higher-level declare APIs instead
val prepare_parameter : poly:bool -> udecl:UState.universe_decl -> types:EConstr.types -> Evd.evar_map -> Evd.evar_map * parameter_entryval declare_constant : ?loc:Loc.t -> ?local:Locality.import_status -> name:Names.Id.t -> kind:Decls.logical_kind -> ?typing_flags:Declarations.typing_flags ->
?user_warns:Globnames.extended_global_reference UserWarn.with_qf -> constant_entry -> Names.Constant.tdeclare_constant id cd declares a global declaration (constant/parameter) with name id in the current section; it returns the full path of the declaration
XXX: This is an internal, low-level API and could become scheduled for removal from the public API, use higher-level declare APIs instead
val declare_definition_full : info:Info.t -> cinfo:EConstr.t option CInfo.t -> opaque:bool -> body:EConstr.t ->
?using:Vernacexpr.section_subset_expr -> Evd.evar_map -> Names.GlobRef.t * Univ.ContextSet.tLike declare_definition but also returns the universes and universe constraints added to the global environment
Declaration messages, for internal use
val definition_message : Names.Id.t -> unitXXX: Scheduled for removal from public API, do not use
val assumption_message : Names.Id.t -> unitval fixpoint_message : int array option -> Names.Id.t list -> unitval check_exists : Names.Id.t -> unitval build_by_tactic : Environ.env -> uctx:UState.t -> poly:bool -> typ:EConstr.types ->
unit Proofview.tactic -> Constr.constr * Constr.types option * UState.named_universes_entry * bool * UState.tSemantics of this function is a bit dubious, use with care
Rocq's Program mode support. This mode extends declarations of constants and fixpoints with Program Definition and Program
Fixpoint to support incremental construction of terms using delayed proofs, called "obligations"
The mode also provides facilities for managing and auto-solving sets of obligations.
The basic code flow of programs/obligations is as follows:
add_definition / add_mutual_definitions are called from the respective Program vernacular command interpretation; at this point the only extra work we do is to prepare the new definition d using RetrieveObl, which consists in turning unsolved evars into obligations. d is not sent to the kernel yet, as it is not complete and cannot be typchecked, but saved in a special data-structure. Auto-solving of obligations is tried at this stage (see below)next_obligation will retrieve the next obligation (RetrieveObl sorts them by topological order) and will try to solve it. When all obligations are solved, the original constant d is grounded and sent to the kernel for addition to the global environment. Auto-solving of obligations is also triggered on obligation completion.Solving of obligations: Solved obligations are stored as regular global declarations in the global environment, usually with name constant_obligation_number where constant is the original constant and number is the corresponding (internal) number.
Solving an obligation can trigger a bit of a complex cascaded callback path; closing an obligation can indeed allow all other obligations to be closed, which in turn may trigged the declaration of the original constant. Care must be taken, as this can modify Global.env in arbitrarily ways. Current code takes some care to refresh the env in the proper boundaries, but the invariants remain delicate.
Saving of obligations: as open obligations use the regular proof mode, a `Qed` will call `Lemmas.save_lemma` first. For this reason obligations code is split in two: this file, Obligations, taking care of the top-level vernac commands, and Declare, which is called by `Lemmas` to close an obligation proof and eventually to declare the top-level Programed constant.
module Obls : sig ... endval is_local_constant : Names.Constant.t -> boolmodule Internal : sig ... end