package coq-core

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

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

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.

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

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

type inline = int option

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

type ('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

    *)
type universes =
  1. | Monomorphic
  2. | Polymorphic of Univ.AbstractContext.t
type 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. impredicative_set : bool;
    (*

    Predicativity of the Set universe.

    *)
  10. sprop_allowed : bool;
    (*

    If false, error when encountering SProp.

    *)
  11. 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.

Representation of definitions/assumptions in the kernel
type 'opaque pconstant_body = {
  1. const_hyps : Constr.named_context;
    (*

    younger hyp at top

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

    The typing options which were used for type-checking.

    *)
}
type constant_body = Opaqueproof.opaque pconstant_body
type nested_type =
  1. | NestedInd of Names.inductive
  2. | NestedPrimitive of Names.Constant.t

Representation of mutual inductive types in the kernel

type recarg =
  1. | Norec
  2. | Mrec of Names.inductive
  3. | Nested of nested_type
type 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.

type record_info =
  1. | NotRecord
  2. | FakeRecord
  3. | PrimRecord of (Names.Id.t * Names.Label.t array * Sorts.relevance array * Constr.types array) array
type regular_inductive_arity = {
  1. mind_user_arity : Constr.types;
  2. mind_sort : Sorts.t;
}
type 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. It includes the context of parameters, that is, it has the form paramdecls, realdecls_i such that Ui (see above) is forall realdecls_i, si for some sort si and such that Ii has thus type forall paramdecls, forall realdecls_i, si. The context itself is represented internally as a list in reverse order [realdecl_i{r_i};...;realdecl_i1;paramdecl_m;...;paramdecl_1].

    *)
  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 recursive occurrences of the inductive types in Tij (i.e. in the type of the j-th constructor of the i-th types of the block a shown above) have the form Ind ((mind,0),u), ..., Ind ((mind,n-1),u) for u the canonical abstract instance associated to mind_universes and mind the name to which the inductive block is bound in the environment.

    *)
  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. It includes the parameters, i.e. each component of the array has the form (decls_ij, Ii params realargs_ij) where decls_ij is the concatenation of the context of parameters (possibly with let-ins) and of the arguments of the constructor (possibly with let-ins). This context is internally represented as a list [cstrdecl_ij{q_ij};...;cstrdecl_ij1;paramdecl_m;...;paramdecl_1] such that the constructor in fine has type forall paramdecls, forall cstrdecls_ij, Ii params realargs_ij] with params referring to the assumptions of paramdecls and realargs_ij being the "indices" specific to the constructor.

    *)
  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;
}

Datas specific to a single type of a block of mutually inductive type

type recursivity_kind =
  1. | Finite
    (*

    = inductive

    *)
  2. | CoFinite
    (*

    = coinductive

    *)
  3. | BiFinite
    (*

    = non-recursive, like in "Record" definitions

    *)
Datas associated to a full block of mutually inductive types
type 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_univ_hyps : Univ.Instance.t;
    (*

    Section polymorphic universes.

    *)
  7. mind_nparams : int;
    (*

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

    *)
  8. mind_nparams_rec : int;
    (*

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

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

    The context of parameters (includes let-in declaration)

    *)
  10. mind_universes : universes;
    (*

    Information about monomorphic/polymorphic/cumulative inductives and their universes

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

    Variance info, None when non-cumulative.

    *)
  13. 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.

    *)
  14. mind_private : bool option;
    (*

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

    *)
  15. 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

type ('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.

type 'uconstr with_declaration =
  1. | WithMod of Names.Id.t list * Names.ModPath.t
  2. | WithDef of Names.Id.t list * 'uconstr
type 'uconstr module_alg_expr =
  1. | MEident of Names.ModPath.t
  2. | MEapply of 'uconstr module_alg_expr * Names.ModPath.t
  3. | MEwith of 'uconstr module_alg_expr * 'uconstr with_declaration
type 'uconstr functor_alg_expr =
  1. | MENoFunctor of 'uconstr module_alg_expr
  2. | MEMoreFunctor of 'uconstr functor_alg_expr

A module expression is an algebraic expression, possibly functorized.

type module_expression = (Constr.constr * Univ.AbstractContext.t option) functor_alg_expr

A component of a module structure

type structure_field_body =
  1. | SFBconst of 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)

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

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

and module_signature = (module_type_body, structure_body) functorize
and module_implementation =
  1. | Abstract
    (*

    no accessible implementation

    *)
  2. | Algebraic of module_expression
    (*

    non-interactive algebraic expression

    *)
  3. | Struct of structure_body
    (*

    interactive body living in the parameter context of mod_type

    *)
  4. | FullStruct
    (*

    special case of Struct : the body is exactly mod_type

    *)
and '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.
and 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.

and module_type_body = unit generic_module_body
and _ 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.
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