diff --git a/master/api/rocq-runtime/Coq_checklib/Mod_checking/index.html b/master/api/rocq-runtime/Coq_checklib/Mod_checking/index.html index a0773566d6..78397183b7 100644 --- a/master/api/rocq-runtime/Coq_checklib/Mod_checking/index.html +++ b/master/api/rocq-runtime/Coq_checklib/Mod_checking/index.html @@ -1,2 +1,2 @@ -
Coq_checklib.Mod_checking
val set_indirect_accessor : (Opaqueproof.opaque -> Opaqueproof.opaque_proofterm) -> unit
val check_module : Environ.env -> Names.Cset.t Names.Cmap.t -> Names.ModPath.t -> Declarations.module_body -> Names.Cset.t Names.Cmap.t
exception BadConstant of Names.Constant.t * Pp.t
Coq_checklib.Mod_checking
val set_indirect_accessor : (Opaqueproof.opaque -> Opaqueproof.opaque_proofterm) -> unit
val check_module : Environ.env -> Names.Cset.t Names.Cmap.t -> Names.ModPath.t -> Mod_declarations.module_body -> Names.Cset.t Names.Cmap.t
exception BadConstant of Names.Constant.t * Pp.t
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 inductive_arity = (regular_inductive_arity, template_arity) declaration_arity
type squash_info =
| AlwaysSquashed | |
| SometimesSquashed of Sorts.Quality.Set.t | (* A sort polymorphic inductive NB: if |
type one_inductive_body = {
mind_typename : Names.Id.t; | (* Name of the type: |
mind_arity_ctxt : Constr.rel_context; | (* Arity context of |
mind_arity : inductive_arity; | (* Arity sort and original user arity *) |
mind_consnames : Names.Id.t array; | (* Names of the constructors: |
mind_user_lc : Constr.types array; | (* Types of the constructors with parameters: |
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 |
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 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, |
mind_sec_variance : UVars.Variance.t array option; | (* Variance info for section polymorphic universes. |
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 *) |
}
type mind_specif = mutual_inductive_body * one_inductive_body
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 |
| PHString of Pstring.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.Repr.t |
and head_elimination = pattern_argument head_pattern * pattern_elimination list
type rewrite_rule = {
nvars : int * int * int; |
lhs_pat : instance_mask * pattern_elimination list; |
rhs : Constr.constr; |
}
(c, { lhs_pat = (u, elims); rhs })
in this list stands for (PHSymbol (c,u), elims) ==> rhs
type (_, 'v) when_mod_body =
| ModBodyVal : 'v -> (mod_body, 'v) when_mod_body |
| ModTypeNul : (mod_type, 'v) when_mod_body |
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 |
| FullStruct | (* special case of |
and 'a generic_module_body = {
mod_mp : Names.ModPath.t; | (* absolute path of the module *) |
mod_expr : ('a, module_implementation) when_mod_body; | (* 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, Retroknowledge.action list) when_mod_body; |
}
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 = mod_body 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 = mod_type generic_module_body
type 'a module_retroknowledge = ('a, Retroknowledge.action list) when_mod_body
Extra invariants :
MEwith
inside a mod_expr
implementation : the 'with' syntax is only supported for module typesMEapply
can only be another MEapply
or a MEident
* the argument of MEapply
is now directly forced to be a ModPath.t
.