diff options
Diffstat (limited to 'kernel/declarations.mli')
| -rw-r--r-- | kernel/declarations.mli | 264 |
1 files changed, 142 insertions, 122 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 4ee2fe57..bec52122 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -1,17 +1,14 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Names -open Univ open Term -open Cemitcodes -open Sign -open Mod_subst +open Context (** This module defines the internal representation of global declarations. This includes global constants/axioms, mutual @@ -21,33 +18,24 @@ type engagement = ImpredicativeSet (** {6 Representation of constants (Definition/Axiom) } *) -type polymorphic_arity = { - poly_param_levels : universe option list; - poly_level : universe; -} - -type constant_type = - | NonPolymorphicType of types - | PolymorphicArity of rel_context * polymorphic_arity - -type constr_substituted - -val from_val : constr -> constr_substituted -val force : constr_substituted -> constr - -(** Opaque proof terms are not loaded immediately, but are there - in a lazy form. Forcing this lazy may trigger some unmarshal of - the necessary structure. *) +(** Non-universe polymorphic mode polymorphism (Coq 8.2+): inductives + and constants hiding inductives are implicitely polymorphic when + applied to parameters, on the universes appearing in the whnf of + their parameters and their conclusion, in a template style. + + In truely universe polymorphic mode, we always use RegularArity. +*) -type lazy_constr +type template_arity = { + template_param_levels : Univ.universe_level option list; + template_level : Univ.universe; +} -val subst_lazy_constr : substitution -> lazy_constr -> lazy_constr -val force_lazy_constr : lazy_constr -> constr_substituted -val make_lazy_constr : constr_substituted Lazy.t -> lazy_constr -val lazy_constr_is_val : lazy_constr -> bool +type ('a, 'b) declaration_arity = + | RegularArity of 'a + | TemplateArity of 'b -val force_opaque : lazy_constr -> constr -val opaque_from_val : constr -> lazy_constr +type constant_type = (types, rel_context * template_arity) declaration_arity (** Inlining level of parameters at functor applications. None means no inlining *) @@ -57,31 +45,43 @@ type inline = int option (** A constant can have no body (axiom/parameter), or a transparent body, or an opaque one *) +(** Projections are a particular kind of constant: + always transparent. *) + +type projection_body = { + proj_ind : mutual_inductive; + proj_npars : int; + proj_arg : int; + proj_type : types; (* Type under params *) + proj_eta : constr * types; (* Eta-expanded term and type *) + proj_body : constr; (* For compatibility with VMs only, the match version *) +} + type constant_def = | Undef of inline - | Def of constr_substituted - | OpaqueDef of lazy_constr + | Def of constr Mod_subst.substituted + | OpaqueDef of Opaqueproof.opaque +type constant_universes = Univ.universe_context + +(* some contraints are in constant_constraints, some other may be in + * the OpaueDef *) type constant_body = { - const_hyps : section_context; (** New: younger hyp at top *) + const_hyps : Context.section_context; (** New: younger hyp at top *) const_body : constant_def; const_type : constant_type; - const_body_code : to_patch_substituted; - const_constraints : constraints } - -val subst_const_def : substitution -> constant_def -> constant_def -val subst_const_body : substitution -> constant_body -> constant_body - -(** Is there a actual body in const_body or const_body_opaque ? *) - -val constant_has_body : constant_body -> bool - -(** Accessing const_body_opaque or const_body *) - -val body_of_constant : constant_body -> constr_substituted option - -val is_opaque : constant_body -> bool - + const_body_code : Cemitcodes.to_patch_substituted; + const_polymorphic : bool; (** Is it polymorphic or not *) + const_universes : constant_universes; + const_proj : projection_body option; + const_inline_code : bool } + +type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ] + +type side_effect = + | SEsubproof of constant * constant_body * seff_env + | SEscheme of (inductive * constant * constant_body * seff_env) list * string + (** {6 Representation of mutual inductive types in the kernel } *) type recarg = @@ -89,18 +89,8 @@ type recarg = | Mrec of inductive | Imbr of inductive -val subst_recarg : substitution -> recarg -> recarg - type wf_paths = recarg Rtree.t -val mk_norec : wf_paths -val mk_paths : recarg -> wf_paths list array -> wf_paths -val dest_recarg : wf_paths -> recarg -val dest_subterms : wf_paths -> wf_paths list array -val recarg_length : wf_paths -> int -> int - -val subst_wf_paths : substitution -> wf_paths -> wf_paths - (** {v Inductive I1 (params) : U1 := c11 : T11 | ... | c1p1 : T1p1 @@ -109,25 +99,32 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths v} *) -type monomorphic_inductive_arity = { - mind_user_arity : constr; +(** Record information: + If the record is not primitive, then None + Otherwise, we get: + - The identifier for the binder name of the record in primitive projections. + - The constants associated to each projection. + - The checked projection bodies. *) + +type record_body = (Id.t * constant array * projection_body array) option + +type regular_inductive_arity = { + mind_user_arity : types; mind_sort : sorts; } -type inductive_arity = -| Monomorphic of monomorphic_inductive_arity -| Polymorphic of polymorphic_arity +type inductive_arity = (regular_inductive_arity, template_arity) declaration_arity type one_inductive_body = { (** {8 Primitive datas } *) - mind_typename : identifier; (** Name of the type: [Ii] *) + mind_typename : Id.t; (** Name of the type: [Ii] *) mind_arity_ctxt : rel_context; (** Arity context of [Ii] with parameters: [forall params, Ui] *) - mind_arity : inductive_arity; (** Arity sort and original user arity if monomorphic *) + mind_arity : inductive_arity; (** Arity sort and original user arity *) - mind_consnames : identifier array; (** Names of the constructors: [cij] *) + mind_consnames : Id.t array; (** Names of the constructors: [cij] *) mind_user_lc : types array; (** Types of the constructors with parameters: [forall params, Tij], @@ -138,12 +135,16 @@ type one_inductive_body = { mind_nrealargs : int; (** Number of expected real arguments of the type (no let, no params) *) - mind_nrealargs_ctxt : int; (** Length of realargs context (with let, no params) *) + mind_nrealdecls : int; (** Length of realargs context (with let, no params) *) mind_kelim : sorts_family list; (** List of allowed elimination sorts *) mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion is atomic *) + mind_consnrealargs : int array; + (** Number of expected proper arguments of the constructors (w/o params) + (not used in the kernel) *) + mind_consnrealdecls : int array; (** Length of the signature of the constructors (with let, w/o params) (not used in the kernel) *) @@ -163,13 +164,13 @@ type mutual_inductive_body = { mind_packets : one_inductive_body array; (** The component of the mutual inductive block *) - mind_record : bool; (** Whether the inductive type has been declared as a record *) + mind_record : record_body option; (** The record information *) - mind_finite : bool; (** Whether the type is inductive or coinductive *) + mind_finite : Decl_kinds.recursivity_kind; (** Whether the type is inductive or coinductive *) mind_ntypes : int; (** Number of types in the block *) - mind_hyps : section_context; (** Section hypotheses on which the block depends *) + mind_hyps : Context.section_context; (** Section hypotheses on which the block depends *) mind_nparams : int; (** Number of expected parameters *) @@ -177,14 +178,38 @@ type mutual_inductive_body = { mind_params_ctxt : rel_context; (** The context of parameters (includes let-in declaration) *) - mind_constraints : constraints; (** Universes constraints enforced by the inductive declaration *) + mind_polymorphic : bool; (** Is it polymorphic or not *) - } + mind_universes : Univ.universe_context; (** Local universe variables and constraints *) + + mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) + +} + +(** {6 Module declarations } *) -val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body +(** Functor expressions are forced to be on top of other expressions *) -(** {6 Modules: signature component specifications, module types, and - module declarations } *) +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 with_declaration = + | WithMod of Id.t list * module_path + | WithDef of Id.t list * constr + +type module_alg_expr = + | MEident of module_path + | MEapply of module_alg_expr * module_path + | MEwith of module_alg_expr * with_declaration + +(** A component of a module structure *) type structure_field_body = | SFBconst of constant_body @@ -192,57 +217,52 @@ type structure_field_body = | SFBmodule of module_body | SFBmodtype of module_type_body -(** NB: we may encounter now (at most) twice the same label in +(** 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 = (label * structure_field_body) list +and structure_body = (Label.t * structure_field_body) list -and struct_expr_body = - | SEBident of module_path - | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body - | SEBapply of struct_expr_body * struct_expr_body * constraints - | SEBstruct of structure_body - | SEBwith of struct_expr_body * with_declaration_body +(** A module signature is a structure, with possibly functors on top of it *) -and with_declaration_body = - With_module_body of identifier list * module_path - | With_definition_body of identifier list * constant_body +and module_signature = (module_type_body,structure_body) functorize + +(** A module expression is an algebraic expression, possibly functorized. *) + +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 module_body = - { (** absolute path of the module *) - mod_mp : module_path; - (** Implementation *) - mod_expr : struct_expr_body option; - (** Signature *) - mod_type : struct_expr_body; - (** algebraic structure expression is kept - if it's relevant for extraction *) - mod_type_alg : struct_expr_body option; - (** set of all constraint in the module *) - mod_constraints : constraints; - (** quotiented set of equivalent constant and inductive name *) - mod_delta : delta_resolver; - mod_retroknowledge : Retroknowledge.action list} - -and module_type_body = - { - (** Path of the module type *) - typ_mp : module_path; - typ_expr : struct_expr_body; - (** algebraic structure expression is kept - if it's relevant for extraction *) - typ_expr_alg : struct_expr_body option ; - typ_constraints : constraints; - (** quotiented set of equivalent constant and inductive name *) - typ_delta :delta_resolver} - - -(** Hash-consing *) - -(** Here, strictly speaking, we don't perform true hash-consing - of the structure, but simply hash-cons all inner constr - and other known elements *) - -val hcons_const_body : constant_body -> constant_body -val hcons_mind : mutual_inductive_body -> mutual_inductive_body + { mod_mp : module_path; (** absolute path of the module *) + mod_expr : module_implementation; (** implementation *) + mod_type : module_signature; (** expanded type *) + (** algebraic type, kept if it's relevant for extraction *) + mod_type_alg : module_expression option; + (** set of all constraints in the module *) + mod_constraints : Univ.constraints; + (** quotiented set of equivalent constants and inductive names *) + mod_delta : Mod_subst.delta_resolver; + mod_retroknowledge : Retroknowledge.action list } + +(** A [module_type_body] is just a [module_body] with no + implementation ([mod_expr] always [Abstract]) and also + an empty [mod_retroknowledge] *) + +and module_type_body = module_body + +(** 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 [module_path]. +*) |