Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)
open Namesopen Constr
(** This module defines the internal representation of global declarations. This includes global constants/axioms, mutual inductive definitions, modules and module types *)
(** {6 Representation of constants (Definition/Axiom) } *)
(** Template polymorphism: provides universe polymorphism and sort polymorphism (restricted to above prop qualities), with implicit instances and inferring the universes from the types of parameters instead.
The data other than [mind_template] in the inductive bodies is instantiated to the default universes (e.g. [mind_user_arity], [mind_sort], the constructor data, etc).*)
type template_universes = { (** For each LocalAssum parameter (in regular order, not rel_context order), tell whether it binds a quality or a universe level (read from the sort, NB it is possible to bind a qvar next to a constant universe) (the binders are DeBruijn levels as with universe polymorphism, but may be instantiated with algebraics) *) template_param_arguments : Sorts.t option list; (** Inductive sort with abstracted universes. *) template_concl : Sorts.t; template_context : UVars.AbstractContext.t; (** Template_defaults qualities are all QType. Also the universes are all levels so we can use Instance. *) template_defaults : UVars.Instance.t;}
(** 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 *)
(* Global declarations (i.e. constants) can be either: *)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
(** 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 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 *)
check_eliminations : bool; (** If [false] sort elimination constraints are not checked. Breaks the system *)
conv_oracle : Conv_oracle.oracle; (** Unfolding strategies for conversion *)
share_reduction : bool; (** Use by-need reduction algorithm *)
unfold_dep_heuristic : bool; (** If [true], use dependency heuristic when unfolding constants during conversion *)
unfold_height_heuristic : bool; (** If [true], use definitional height heuristic when unfolding constants during conversion. A strategy level is assigned to each constant when it's defined. The level is [-h] where [h] is the definitional height of the constant. *)
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) *)
}
(** {6 Representation of definitions/assumptions in the kernel } *)
(* some contraints are in constant_constraints, some other may be in * the OpaqueDef *)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 : 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. *) const_def_height : int option}
type constant_body = (Opaqueproof.opaque, Vmlibrary.indirect_code) pconstant_body
(** {6 Representation of mutual inductive types in the kernel } *)
type recarg_type =| RecArgInd of inductive| RecArgPrim of Constant.t
type recarg =| Norec| Mrec of recarg_type
type wf_paths = recarg Rtree.t
(**{v Inductive I1 (params) : U1 := c11 : T11 | ... | c1p1 : T1p1 ... with In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpnv}*)
(** 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, PrimRecord of: - The identifier for the binder name of the record in primitive projections. - The constants associated to each projection. - The projection types (under parameters). - The recheck at eta conversion flag
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 has_eta = AlwaysEta | MaybeEta | NoEta
type record_info =| NotRecord| FakeRecord| PrimRecord of { id : Id.t; projections : Id.t array; relevances : Sorts.relevance array; tys : types array; has_eta : has_eta; }
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. *)
(** {7 Datas specific to a single type of a block of mutually inductive type } *)type one_inductive_body = {(** {8 Primitive datas } *)
mind_typename : 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_sort : Sorts.t; (** Arity sort *)
mind_user_arity : types; (** Original user arity, convertible to [mkArity (mind_arity_ctxt, mind_sort)]. As such it contains the parameters. (not necessarily a syntactic arity, eg [relation A] instead of [A -> A -> Prop]) *)
mind_record : record_info; (** The record information *)
mind_consnames : Id.t array; (** Names of the constructors: [cij] *)
mind_user_lc : 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. *)
(** {8 Derived datas } *)
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 : (rel_context * 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_automaton : recarg Rtree.Automaton.t; (** Minimal automaton generated from the inductive tree *)
mind_relevance : Sorts.relevance; (* XXX this is redundant with mind_sort, is it actually worth keeping? *)
mind_relies_on_indices_not_mattering : bool; (** true if this inductive relies on indices not mattering, i.e. its behavior would change under -indices-matter. *)
(** {8 Datas for bytecode compilation } *)
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 *)
(** {7 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_finite : recursivity_kind; (** Whether the type is inductive, coinductive or non-recursive *)
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 *)}
type mind_specif = mutual_inductive_body * one_inductive_body
(** {6 Rewrite rules } *)
type 'q quality_pattern = 'q Sorts.Quality.pattern = | PQVar of 'q | PQConstant of Sorts.Quality.constant | PQGlobal of Sorts.QGlobal.t
type ('q, 'u) instance_mask = ('q, 'u) UVars.Instance.mask
type ('q, 'u) sort_pattern = ('q, 'u) Sorts.pattern = | PSProp | PSSProp | PSSet | PSType of 'u | PSGlobal of Sorts.QGlobal.t * 'u | PSQSort of 'q * 'u
(** 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 head_pattern = | PHRel of int | PHSort of (int option, int option) sort_pattern | PHSymbol of Constant.t * (int option, int option) instance_mask | PHInd of inductive * (int option, int option) instance_mask | PHConstr of constructor * (int option, int option) instance_mask | PHInt of Uint63.t | PHFloat of Float64.t | PHString of Pstring.t | PHLambda of pattern_argument array * head_elimination | PHProd of pattern_argument array * pattern_argument
and pattern_elimination = | PEApp of pattern_argument array | PECase of inductive * pattern_argument * pattern_argument array | PEProj of Projection.Repr.t
and head_elimination = head_pattern * pattern_elimination list
and pattern_argument = | EHole of int | EHoleIgnored | ERigid of head_elimination
type machine_rewrite_rule = { nvars : int * int * int; lhs_pat : (int option, int option) instance_mask * pattern_elimination list; rhs : constr;}
(** {6 Representation of rewrite rules in the kernel } *)
(** [(c, { lhs_pat = (u, elims); rhs })] in this list stands for [(PHSymbol (c,u), elims) ==> rhs] *)type rewrite_rules_body = { rewrules_rules : (Constant.t * machine_rewrite_rule) list;}
(** {6 Module declarations } *)
type mod_body = [ `ModBody ]type mod_type = [ `ModType ]
(** Functor expressions are forced to be on top of other expressions *)
type ('ty,'a) functorize = | NoFunctor of 'a | MoreFunctor of 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 Id.t list * ModPath.t | WithDef of Id.t list * 'uconstr
type 'uconstr module_alg_expr = | MEident of ModPath.t | MEapply of 'uconstr module_alg_expr * 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 * UVars.AbstractContext.t option) functor_alg_expr
(** A component of a module structure *)
type ('mod_body, 'mod_type) structure_field_body = | SFBconst of constant_body | SFBmind of mutual_inductive_body | SFBrules of rewrite_rules_body | SFBmodule of 'mod_body | SFBmodtype of 'mod_type
(** 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 ('mod_body, 'mod_type) structure_body = (Id.t * ('mod_body, 'mod_type) structure_field_body) list