Module Declarations

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

type set_predicativity =
| ImpredicativeSet
| PredicativeSet
type engagement = set_predicativity
Representation of constants (Definition/Axiom)
type template_arity = {
template_param_levels : Univ.Level.t option list;
template_level : Univ.Universe.t;
}
type ('a, 'b) declaration_arity =
| RegularArity of 'a
| TemplateArity of 'b
type inline = int option
type ('a, 'opaque) constant_def =
| Undef of inline

a global assumption

| Def of 'a

or a transparent global definition

| OpaqueDef of 'opaque

or an opaque global definition

| Primitive of CPrimitives.t

or a primitive operation

type universes =
| Monomorphic of Univ.ContextSet.t
| Polymorphic of Univ.AUContext.t
type typing_flags = {
check_guarded : bool;

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

check_positive : bool;

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

check_universes : bool;

If false universe constraints are not checked

conv_oracle : Conv_oracle.oracle;

Unfolding strategies for conversion

share_reduction : bool;

Use by-need reduction algorithm

enable_VM : bool;

If false, all VM conversions fall back to interpreted ones

enable_native_compiler : bool;

If false, all native conversions fall back to VM ones

indices_matter : bool;

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

check_template : bool;
}

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.

type 'opaque constant_body = {
const_hyps : Constr.named_context;

New: younger hyp at top

const_body : (Constr.t Mod_subst.substituted, 'opaque) constant_def;
const_type : Constr.types;
const_relevance : Sorts.relevance;
const_body_code : Cemitcodes.to_patch_substituted option;
const_universes : universes;
const_inline_code : bool;
const_typing_flags : typing_flags;

The typing options which were used for type-checking.

}
Representation of mutual inductive types in the kernel
type recarg =
| Norec
| Mrec of Names.inductive
| Imbr of Names.inductive
type wf_paths = recarg Rtree.t
type record_info =
| NotRecord
| FakeRecord
| PrimRecord of (Names.Id.t * Names.Label.t array * Sorts.relevance array * Constr.types array) array
type regular_inductive_arity = {
mind_user_arity : Constr.types;
mind_sort : Sorts.t;
}
type inductive_arity = (regular_inductive_arity, template_arity) declaration_arity
type one_inductive_body = {
mind_typename : Names.Id.t;

Name of the type: Ii

mind_arity_ctxt : Constr.rel_context;

Arity context of Ii with parameters: forall params, Ui

mind_arity : inductive_arity;

Arity sort and original user arity

mind_consnames : Names.Id.t array;

Names of the constructors: cij

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

mind_nrealargs : int;

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

mind_nrealdecls : int;

Length of realargs context (with let, no params)

mind_kelim : Sorts.family;

Highest allowed elimination sort

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

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

mind_consnrealargs : int array;

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

mind_consnrealdecls : int array;

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

mind_recargs : wf_paths;

Signature of recursive arguments in the constructors

mind_relevance : Sorts.relevance;
mind_nb_constant : int;

number of constant constructor

mind_nb_args : int;

number of no constant constructor

mind_reloc_tbl : Vmvalues.reloc_table;
}
type recursivity_kind =
| Finite

= inductive

| CoFinite

= coinductive

| BiFinite

= non-recursive, like in "Record" definitions

type mutual_inductive_body = {
mind_packets : one_inductive_body array;

The component of the mutual inductive block

mind_record : record_info;

The record information

mind_finite : recursivity_kind;

Whether the type is inductive or coinductive

mind_ntypes : int;

Number of types in the block

mind_hyps : Constr.named_context;

Section hypotheses on which the block depends

mind_nparams : int;

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

mind_nparams_rec : int;

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

mind_params_ctxt : Constr.rel_context;

The context of parameters (includes let-in declaration)

mind_universes : universes;

Information about monomorphic/polymorphic/cumulative inductives and their universes

mind_variance : Univ.Variance.t array option;

Variance info, None when non-cumulative.

mind_private : bool option;

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

mind_typing_flags : typing_flags;

typing flags at the time of the inductive creation

}
Module declarations
type ('ty, 'a) functorize =
| NoFunctor of 'a
| MoreFunctor of Names.MBId.t * 'ty * ('ty, 'a) functorize
type with_declaration =
| WithMod of Names.Id.t list * Names.ModPath.t
| WithDef of Names.Id.t list * Constr.constr * Univ.AUContext.t option
type module_alg_expr =
| MEident of Names.ModPath.t
| MEapply of module_alg_expr * Names.ModPath.t
| MEwith of module_alg_expr * with_declaration
type structure_field_body =
| SFBconst of Opaqueproof.opaque constant_body
| SFBmind of mutual_inductive_body
| SFBmodule of module_body
| SFBmodtype of module_type_body
and structure_body = (Names.Label.t * structure_field_body) list
and module_signature = (module_type_body, structure_body) functorize
and module_expression = (module_type_body, module_alg_expr) functorize
and module_implementation =
| Abstract

no accessible implementation

| Algebraic of module_expression

non-interactive algebraic expression

| Struct of module_signature

interactive body

| FullStruct

special case of Struct : the body is exactly mod_type

and 'a generic_module_body = {
mod_mp : Names.ModPath.t;

absolute path of the module

mod_expr : 'a;

implementation

mod_type : module_signature;

expanded type

mod_type_alg : module_expression option;

algebraic type

mod_constraints : Univ.ContextSet.t;

set of all universes constraints in the module

mod_delta : Mod_subst.delta_resolver;

quotiented set of equivalent constants and inductive names

mod_retroknowledge : 'a module_retroknowledge;
}
and module_body = module_implementation generic_module_body
and module_type_body = unit generic_module_body
and _ module_retroknowledge =
| ModBodyRK : Retroknowledge.action list -> module_implementation module_retroknowledge
| ModTypeRK : unit module_retroknowledge