Module Declarations

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 = {
template_level : Sorts.t;
}
type template_universes = {
template_param_levels : Univ.Level.t option list;
template_context : Univ.ContextSet.t;
}
type ('a, 'b) declaration_arity =
| RegularArity of 'a
| 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, 'rules) 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

*)
| Symbol of 'rules(*

or a symbol

*)
type universes =
| Monomorphic
| Polymorphic of UVars.AbstractContext.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.

*)
impredicative_set : bool;(*

Predicativity of the Set universe.

*)
sprop_allowed : bool;(*

If false, error when encountering SProp.

*)
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, 'bytecode) pconstant_body = {
const_hyps : Constr.named_context;(*

younger hyp at top

*)
const_univ_hyps : UVars.Instance.t;
const_body : (Constr.t, 'opaque, bool) constant_def;(*

bool is for unfold_fix in symbols

*)
const_type : Constr.types;
const_relevance : Sorts.relevance;
const_body_code : 'bytecode;
const_universes : universes;
const_inline_code : bool;
const_typing_flags : typing_flags;(*

The typing options which were used for type-checking.

*)
}
type constant_body = (Opaqueproof.opaque, Vmlibrary.indirect_code option) pconstant_body
Representation of mutual inductive types in the kernel
type recarg_type =
| RecArgInd of Names.inductive
| RecArgPrim of Names.Constant.t
type recarg =
| Norec
| Mrec of recarg_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 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 =
| 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 squash_info =
| AlwaysSquashed
| SometimesSquashed of Sorts.Quality.Set.t(*

A sort polymorphic inductive I@{...|...|...} : ... -> Type@{ s|...} is squashed at a given instantiation if any quality in the list is not smaller than s.

NB: if s is a variable SometimesSquashed contains SProp ie non ground instantiations are squashed.

*)
type one_inductive_body = {
mind_typename : Names.Id.t;(*

Name of the type: Ii

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

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

*)
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_squashed : squash_info option;(*

Is elimination restricted to the inductive's sort?

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

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

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

type recursivity_kind =
| Finite(*

= inductive

*)
| CoFinite(*

= coinductive

*)
| BiFinite(*

= non-recursive, like in "Record" definitions

*)
Datas associated to a full block of mutually inductive types
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, coinductive or non-recursive

*)
mind_ntypes : int;(*

Number of types in the block

*)
mind_hyps : Constr.named_context;(*

Section hypotheses on which the block depends

*)
mind_univ_hyps : UVars.Instance.t;(*

Section polymorphic universes.

*)
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_template : template_universes option;
mind_variance : UVars.Variance.t array option;(*

Variance info, None when non-cumulative.

*)
mind_sec_variance : UVars.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.

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

*)
}
Rewrite rules
type quality_pattern = Sorts.Quality.pattern =
| PQVar of int option
| PQConstant of Sorts.Quality.constant
type instance_mask = UVars.Instance.mask
type sort_pattern = Sorts.pattern =
| PSProp
| PSSProp
| PSSet
| PSType of int option
| PSQSort of int option * int option
type 'arg head_pattern =
| PHRel of int
| PHSort of sort_pattern
| PHSymbol of Names.Constant.t * instance_mask
| PHInd of Names.inductive * instance_mask
| PHConstr of Names.constructor * instance_mask
| PHInt of Uint63.t
| PHFloat of Float64.t
| PHLambda of 'arg array * 'arg
| PHProd of 'arg array * 'arg

Patterns are internally represented as pairs of a head-pattern and a list of eliminations Eliminations correspond to elements of the stack in a reduction machine, they represent a pattern with a hole, to be filled with the head-pattern

type pattern_elimination =
| PEApp of pattern_argument array
| PECase of Names.inductive * instance_mask * pattern_argument * pattern_argument array
| PEProj of Names.Projection.t
and head_elimination = pattern_argument head_pattern * pattern_elimination list
and pattern_argument =
| EHole of int
| EHoleIgnored
| ERigid of head_elimination
type rewrite_rule = {
nvars : int * int * int;
lhs_pat : instance_mask * pattern_elimination list;
rhs : Constr.constr;
}
Representation of rewrite rules in the kernel
type rewrite_rules_body = {
rewrules_rules : (Names.Constant.t * rewrite_rule) list;
}

(c, { lhs_pat = (u, elims); rhs }) in this list stands for (PHSymbol (c,u), elims) ==> rhs

Module declarations

Functor expressions are forced to be on top of other expressions

type ('ty, 'a) functorize =
| NoFunctor of 'a
| 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 =
| WithMod of Names.Id.t list * Names.ModPath.t
| WithDef of Names.Id.t list * 'uconstr
type 'uconstr module_alg_expr =
| MEident of Names.ModPath.t
| MEapply of 'uconstr module_alg_expr * Names.ModPath.t
| MEwith of 'uconstr module_alg_expr * 'uconstr with_declaration
type 'uconstr functor_alg_expr =
| MENoFunctor of 'uconstr module_alg_expr
| MEMoreFunctor of 'uconstr functor_alg_expr

A module expression is an algebraic expression, possibly functorized.

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

A component of a module structure

type structure_field_body =
| SFBconst of constant_body
| SFBmind of mutual_inductive_body
| SFBrules of rewrite_rules_body
| SFBmodule of module_body
| 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 =
| Abstract(*

no accessible implementation

*)
| Algebraic of module_expression(*

non-interactive algebraic expression

*)
| Struct of structure_body(*

interactive body living in the parameter context of mod_type

*)
| 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_delta : Mod_subst.delta_resolver;(*

quotiented set of equivalent constants and inductive names

*)
mod_retroknowledge : 'a module_retroknowledge;
}

For a module, there are five possible situations:

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 =
| ModBodyRK : Retroknowledge.action list -> module_implementation module_retroknowledge
| ModTypeRK : unit module_retroknowledge

Extra invariants :