package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (40)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors.

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.14.1.tar.gz
sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3

doc/coq-core.kernel/Declarations/index.html

Module DeclarationsSource

This module defines the internal representation of global declarations. This includes global constants/axioms, mutual inductive definitions, modules and module types

Sourcetype set_predicativity =
  1. | ImpredicativeSet
  2. | PredicativeSet
Sourcetype engagement = set_predicativity
Representation of constants (Definition/Axiom)

Non-universe polymorphic mode polymorphism (Coq 8.2+): inductives and constants hiding inductives are implicitly polymorphic when applied to parameters, on the universes appearing in the whnf of their parameters and their conclusion, in a template style.

In truly universe polymorphic mode, we always use RegularArity.

Sourcetype template_arity = {
  1. template_level : Univ.Universe.t;
}
Sourcetype template_universes = {
  1. template_param_levels : Univ.Level.t option list;
  2. template_context : Univ.ContextSet.t;
}
Sourcetype ('a, 'b) declaration_arity =
  1. | RegularArity of 'a
  2. | TemplateArity of 'b

Inlining level of parameters at functor applications. None means no inlining

Sourcetype inline = int option

A constant can have no body (axiom/parameter), or a transparent body, or an opaque one

Sourcetype ('a, 'opaque) constant_def =
  1. | Undef of inline
    (*

    a global assumption

    *)
  2. | Def of 'a
    (*

    or a transparent global definition

    *)
  3. | OpaqueDef of 'opaque
    (*

    or an opaque global definition

    *)
  4. | Primitive of CPrimitives.t
    (*

    or a primitive operation

    *)
Sourcetype universes =
  1. | Monomorphic of Univ.ContextSet.t
  2. | Polymorphic of Univ.AUContext.t
Sourcetype typing_flags = {
  1. check_guarded : bool;
    (*

    If false then fixed points and co-fixed points are assumed to be total.

    *)
  2. check_positive : bool;
    (*

    If false then inductive types are assumed positive and co-inductive types are assumed productive.

    *)
  3. check_universes : bool;
    (*

    If false universe constraints are not checked

    *)
  4. conv_oracle : Conv_oracle.oracle;
    (*

    Unfolding strategies for conversion

    *)
  5. share_reduction : bool;
    (*

    Use by-need reduction algorithm

    *)
  6. enable_VM : bool;
    (*

    If false, all VM conversions fall back to interpreted ones

    *)
  7. enable_native_compiler : bool;
    (*

    If false, all native conversions fall back to VM ones

    *)
  8. indices_matter : bool;
    (*

    The universe of an inductive type must be above that of its indices.

    *)
  9. cumulative_sprop : bool;
    (*

    SProp <= Type

    *)
  10. allow_uip : bool;
    (*

    Allow definitional UIP (breaks termination)

    *)
}

The typing_flags are instructions to the type-checker which modify its behaviour. The typing flags used in the type-checking of a constant are tracked in their constant_body so that they can be displayed to the user.

Sourcetype 'opaque constant_body = {
  1. const_hyps : Constr.named_context;
    (*

    New: younger hyp at top

    *)
  2. const_body : (Constr.t, 'opaque) constant_def;
  3. const_type : Constr.types;
  4. const_relevance : Sorts.relevance;
  5. const_body_code : Vmemitcodes.body_code option;
  6. const_universes : universes;
  7. const_inline_code : bool;
  8. const_typing_flags : typing_flags;
    (*

    The typing options which were used for type-checking.

    *)
}
Sourcetype nested_type =
  1. | NestedInd of Names.inductive
  2. | NestedPrimitive of Names.Constant.t

Representation of mutual inductive types in the kernel

Sourcetype recarg =
  1. | Norec
  2. | Mrec of Names.inductive
  3. | Nested of nested_type
Sourcetype wf_paths = recarg Rtree.t
   Inductive I1 (params) : U1 := c11 : T11 | ... | c1p1 : T1p1
   ...
   with      In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpn

Record information: If the type is not a record, then NotRecord If the type is a non-primitive record, then FakeRecord If it is a primitive record, for every type in the block, we get:

  • The identifier for the binder name of the record in primitive projections.
  • The constants associated to each projection.
  • The projection types (under parameters).

The kernel does not exploit the difference between NotRecord and FakeRecord. It is mostly used by extraction, and should be extruded from the kernel at some point.

Sourcetype record_info =
  1. | NotRecord
  2. | FakeRecord
  3. | PrimRecord of (Names.Id.t * Names.Label.t array * Sorts.relevance array * Constr.types array) array
Sourcetype regular_inductive_arity = {
  1. mind_user_arity : Constr.types;
  2. mind_sort : Sorts.t;
}
Sourcetype one_inductive_body = {
  1. mind_typename : Names.Id.t;
    (*

    Name of the type: Ii

    *)
  2. mind_arity_ctxt : Constr.rel_context;
    (*

    Arity context of Ii with parameters: forall params, Ui

    *)
  3. mind_arity : inductive_arity;
    (*

    Arity sort and original user arity

    *)
  4. mind_consnames : Names.Id.t array;
    (*

    Names of the constructors: cij

    *)
  5. mind_user_lc : Constr.types array;
    (*

    Types of the constructors with parameters: forall params, Tij, where the Ik are replaced by de Bruijn index in the context I1:forall params, U1 .. In:forall params, Un

    *)
  6. mind_nrealargs : int;
    (*

    Number of expected real arguments of the type (no let, no params)

    *)
  7. mind_nrealdecls : int;
    (*

    Length of realargs context (with let, no params)

    *)
  8. mind_kelim : Sorts.family;
    (*

    Highest allowed elimination sort

    *)
  9. mind_nf_lc : (Constr.rel_context * Constr.types) array;
    (*

    Head normalized constructor types so that their conclusion exposes the inductive type

    *)
  10. mind_consnrealargs : int array;
    (*

    Number of expected proper arguments of the constructors (w/o params)

    *)
  11. mind_consnrealdecls : int array;
    (*

    Length of the signature of the constructors (with let, w/o params)

    *)
  12. mind_recargs : wf_paths;
    (*

    Signature of recursive arguments in the constructors

    *)
  13. mind_relevance : Sorts.relevance;
  14. mind_nb_constant : int;
    (*

    number of constant constructor

    *)
  15. mind_nb_args : int;
    (*

    number of no constant constructor

    *)
  16. mind_reloc_tbl : Vmvalues.reloc_table;
}
Sourcetype recursivity_kind =
  1. | Finite
    (*

    = inductive

    *)
  2. | CoFinite
    (*

    = coinductive

    *)
  3. | BiFinite
    (*

    = non-recursive, like in "Record" definitions

    *)
Sourcetype mutual_inductive_body = {
  1. mind_packets : one_inductive_body array;
    (*

    The component of the mutual inductive block

    *)
  2. mind_record : record_info;
    (*

    The record information

    *)
  3. mind_finite : recursivity_kind;
    (*

    Whether the type is inductive or coinductive

    *)
  4. mind_ntypes : int;
    (*

    Number of types in the block

    *)
  5. mind_hyps : Constr.named_context;
    (*

    Section hypotheses on which the block depends

    *)
  6. mind_nparams : int;
    (*

    Number of expected parameters including non-uniform ones (i.e. length of mind_params_ctxt w/o let-in)

    *)
  7. mind_nparams_rec : int;
    (*

    Number of recursively uniform (i.e. ordinary) parameters

    *)
  8. mind_params_ctxt : Constr.rel_context;
    (*

    The context of parameters (includes let-in declaration)

    *)
  9. mind_universes : universes;
    (*

    Information about monomorphic/polymorphic/cumulative inductives and their universes

    *)
  10. mind_template : template_universes option;
  11. mind_variance : Univ.Variance.t array option;
    (*

    Variance info, None when non-cumulative.

    *)
  12. mind_sec_variance : Univ.Variance.t array option;
    (*

    Variance info for section polymorphic universes. None outside sections. The final variance once all sections are discharged is mind_sec_variance ++ mind_variance.

    *)
  13. mind_private : bool option;
    (*

    allow pattern-matching: Some true ok, Some false blocked

    *)
  14. mind_typing_flags : typing_flags;
    (*

    typing flags at the time of the inductive creation

    *)
}
Module declarations

Functor expressions are forced to be on top of other expressions

Sourcetype ('ty, 'a) functorize =
  1. | NoFunctor of 'a
  2. | MoreFunctor of Names.MBId.t * 'ty * ('ty, 'a) functorize

The fully-algebraic module expressions : names, applications, 'with ...'. They correspond to the user entries of non-interactive modules. They will be later expanded into module structures in Mod_typing, and won't play any role into the kernel after that : they are kept only for short module printing and for extraction.

Sourcetype with_declaration =
  1. | WithMod of Names.Id.t list * Names.ModPath.t
  2. | WithDef of Names.Id.t list * Constr.constr * Univ.AUContext.t option
Sourcetype module_alg_expr =
  1. | MEident of Names.ModPath.t
  2. | MEapply of module_alg_expr * Names.ModPath.t
  3. | MEwith of module_alg_expr * with_declaration

A component of a module structure

Sourcetype structure_field_body =
  1. | SFBconst of Opaqueproof.opaque constant_body
  2. | SFBmind of mutual_inductive_body
  3. | SFBmodule of module_body
  4. | SFBmodtype of module_type_body

A module structure is a list of labeled components.

Note : we may encounter now (at most) twice the same label in a structure_body, once for a module (SFBmodule or SFBmodtype) and once for an object (SFBconst or SFBmind)

Sourceand structure_body = (Names.Label.t * structure_field_body) list

A module signature is a structure, with possibly functors on top of it

A module expression is an algebraic expression, possibly functorized.

Sourceand module_implementation =
  1. | Abstract
    (*

    no accessible implementation

    *)
  2. | Algebraic of module_expression
    (*

    non-interactive algebraic expression

    *)
  3. | Struct of module_signature
    (*

    interactive body

    *)
  4. | FullStruct
    (*

    special case of Struct : the body is exactly mod_type

    *)
Sourceand 'a generic_module_body = {
  1. mod_mp : Names.ModPath.t;
    (*

    absolute path of the module

    *)
  2. mod_expr : 'a;
    (*

    implementation

    *)
  3. mod_type : module_signature;
    (*

    expanded type

    *)
  4. mod_type_alg : module_expression option;
    (*

    algebraic type

    *)
  5. mod_delta : Mod_subst.delta_resolver;
    (*

    quotiented set of equivalent constants and inductive names

    *)
  6. mod_retroknowledge : 'a module_retroknowledge;
}

For a module, there are five possible situations:

  • Declare Module M : T then mod_expr = Abstract; mod_type_alg = Some T
  • Module M := E then mod_expr = Algebraic E; mod_type_alg = None
  • Module M : T := E then mod_expr = Algebraic E; mod_type_alg = Some T
  • Module M. ... End M then mod_expr = FullStruct; mod_type_alg = None
  • Module M : T. ... End M then mod_expr = Struct; mod_type_alg = Some T And of course, all these situations may be functors or not.
Sourceand module_body = module_implementation generic_module_body

A module_type_body is just a module_body with no implementation and also an empty mod_retroknowledge. Its mod_type_alg contains the algebraic definition of this module type, or None if it has been built interactively.

Sourceand module_type_body = unit generic_module_body
Sourceand _ module_retroknowledge =
  1. | ModBodyRK : Retroknowledge.action list -> module_implementation module_retroknowledge
  2. | ModTypeRK : unit module_retroknowledge

Extra invariants :

  • No MEwith inside a mod_expr implementation : the 'with' syntax is only supported for module types
  • A module application is atomic, for instance ((M N) P) : * the head of MEapply can only be another MEapply or a MEident * the argument of MEapply is now directly forced to be a ModPath.t.