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, 'rules) 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

    *)
  5. | Symbol of 'rules
    (*

    or a symbol

    *)
type universes =
  1. | Monomorphic
  2. | Polymorphic of UVars.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, 'bytecode) pconstant_body = {
  1. const_hyps : Constr.named_context;
    (*

    younger hyp at top

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

    bool is for unfold_fix in symbols

    *)
  4. const_type : Constr.types;
  5. const_relevance : Sorts.relevance;
  6. const_body_code : 'bytecode;
  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, Vmlibrary.indirect_code option) pconstant_body
Representation of mutual inductive types in the kernel
type recarg_type =
  1. | RecArgInd of Names.inductive
  2. | RecArgPrim of Names.Constant.t
type recarg =
  1. | Norec
  2. | 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 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 squash_info =
  1. | AlwaysSquashed
  2. | 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 = {
  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_squashed : squash_info option;
    (*

    Is elimination restricted to the inductive's 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, coinductive or non-recursive

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

    Variance info, None when non-cumulative.

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

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

    *)
}
Rewrite rules
type quality_pattern = Sorts.Quality.pattern =
  1. | PQVar of int option
  2. | PQConstant of Sorts.Quality.constant
type instance_mask = UVars.Instance.mask
type sort_pattern = Sorts.pattern =
  1. | PSProp
  2. | PSSProp
  3. | PSSet
  4. | PSType of int option
  5. | PSQSort of int option * int option
type 'arg head_pattern =
  1. | PHRel of int
  2. | PHSort of sort_pattern
  3. | PHSymbol of Names.Constant.t * instance_mask
  4. | PHInd of Names.inductive * instance_mask
  5. | PHConstr of Names.constructor * instance_mask
  6. | PHInt of Uint63.t
  7. | PHFloat of Float64.t
  8. | PHString of Pstring.t
  9. | PHLambda of 'arg array * 'arg
  10. | 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 =
  1. | PEApp of pattern_argument array
  2. | PECase of Names.inductive * instance_mask * pattern_argument * pattern_argument array
  3. | PEProj of Names.Projection.t
and head_elimination = pattern_argument head_pattern * pattern_elimination list
and pattern_argument =
  1. | EHole of int
  2. | EHoleIgnored
  3. | ERigid of head_elimination
type rewrite_rule = {
  1. nvars : int * int * int;
  2. lhs_pat : instance_mask * pattern_elimination list;
  3. rhs : Constr.constr;
}
Representation of rewrite rules in the kernel
type rewrite_rules_body = {
  1. 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 =
  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 * UVars.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. | SFBrules of rewrite_rules_body
  4. | SFBmodule of module_body
  5. | 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