Module DeclarationsSource

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.

Sourcetype template_arity = {
  1. template_level : Sorts.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
  2. | Polymorphic of Univ.AbstractContext.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. impredicative_set : bool;
    (*

    Predicativity of the Set universe.

    *)
  10. sprop_allowed : bool;
    (*

    If false, error when encountering SProp.

    *)
  11. cumulative_sprop : bool;
    (*

    SProp <= Type

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

    *)
}
Sourcetype constant_body = Opaqueproof.opaque pconstant_body
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 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. 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

Sourcetype 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
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_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

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 'uconstr with_declaration =
  1. | WithMod of Names.Id.t list * Names.ModPath.t
  2. | WithDef of Names.Id.t list * 'uconstr
Sourcetype '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

A component of a module structure

Sourcetype 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)

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:

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 :