package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

This module provides the functions to declare new variables, parameters, constants and inductive types in the global environment. It also updates some accesory tables such as Nametab (name resolution), Impargs, and Notations.

We provide three main entry points:

  • one-go functions, that will register a constant in one go, suited for non-interactive definitions where the term is given.
  • two-phase start/save functions which will create an interactive proof, allow its modification using tactics, and saving when complete.
  • program mode API, that allow to declare a constant with holes, to be fullfilled later.

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 ... end

Declaration hooks, to be run when a constant is saved. Use with care, as imperative effects may become not supported in the future.

One-go, non-interactive declaration API

module CInfo : sig ... end

Information for a single top-level named constant

module Info : sig ... end

Information 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 -> Evd.evar_map -> Names.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

type lemma_possible_guards = int list list
val declare_mutually_recursive : info:Info.t -> cinfo:Constr.t CInfo.t list -> opaque:bool -> ntns:Metasyntax.notation_interpretation_decl list -> uctx:UState.t -> rec_declaration:Constr.rec_declaration -> possible_indexes:lemma_possible_guards option -> Names.GlobRef.t list

Declaration of interactive constants

module OblState : sig ... end

save / save_admitted can update obligations state, so we need to expose the state here

module Proof : sig ... end

Declare.Proof.t Construction of constants using interactive proofs.

low-level, internal API, avoid using unless you have special needs

type proof_entry

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

type parameter_entry
type primitive_entry
val definition_entry : ?opaque:bool -> ?using:Names.Id.Set.t -> ?inline:bool -> ?types:Constr.types -> ?univs:UState.named_universes_entry -> Constr.constr -> proof_entry
val parameter_entry : ?inline:int -> ?univs:UState.named_universes_entry -> Constr.constr -> parameter_entry
val primitive_entry : ?types:(Constr.types * UState.named_universes_entry) -> CPrimitives.op_or_type -> primitive_entry
val declare_entry : name:Names.Id.t -> ?scope:Locality.definition_scope -> kind:Decls.logical_kind -> ?deprecation:Deprecation.t -> ?hook:Hook.t -> impargs:Impargs.manual_implicits -> uctx:UState.t -> proof_entry -> Names.GlobRef.t

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_variable : name:Names.variable -> kind:Decls.logical_kind -> typ:Constr.types -> impl:Glob_term.binding_kind -> univs:UState.named_universes_entry -> unit

Declaration of local constructions (Variable/Hypothesis/Local)

type constant_entry =
  1. | DefinitionEntry of proof_entry
  2. | ParameterEntry of parameter_entry
  3. | PrimitiveEntry of primitive_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_entry
val declare_constant : ?local:Locality.import_status -> name:Names.Id.t -> kind:Decls.logical_kind -> ?typing_flags:Declarations.typing_flags -> ?deprecation:Deprecation.t -> constant_entry -> Names.Constant.t

declare_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

Declaration messages, for internal use

val definition_message : Names.Id.t -> unit

XXX: Scheduled for removal from public API, do not use

val assumption_message : Names.Id.t -> unit
val fixpoint_message : int array option -> Names.Id.t list -> unit
val check_exists : Names.Id.t -> unit
val 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.t

Semantics of this function is a bit dubious, use with care

Program mode API

Coq'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 ... end
val is_local_constant : Names.Constant.t -> bool
For internal support, do not use
module Internal : sig ... end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct