diff options
Diffstat (limited to 'kernel/declarations.mli')
| -rw-r--r-- | kernel/declarations.mli | 179 |
1 files changed, 98 insertions, 81 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index db706a0c..5b800ede 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -1,30 +1,25 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declarations.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Names open Univ open Term open Cemitcodes open Sign open Mod_subst -(*i*) -(* This module defines the internal representation of global +(** This module defines the internal representation of global declarations. This includes global constants/axioms, mutual inductive definitions, modules and module types *) type engagement = ImpredicativeSet -(**********************************************************************) -(*s Representation of constants (Definition/Axiom) *) +(** {6 Representation of constants (Definition/Axiom) } *) type polymorphic_arity = { poly_param_levels : universe option list; @@ -40,24 +35,58 @@ 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. *) + +type lazy_constr + +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 + +val force_opaque : lazy_constr -> constr +val opaque_from_val : constr -> lazy_constr + +(** 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 constant_def = + | Undef of inline + | Def of constr_substituted + | OpaqueDef of lazy_constr + type constant_body = { - const_hyps : section_context; (* New: younger hyp at top *) - const_body : constr_substituted option; + const_hyps : section_context; (** New: younger hyp at top *) + const_body : constant_def; const_type : constant_type; const_body_code : to_patch_substituted; - (*i const_type_code : to_patch;i*) - const_constraints : constraints; - const_opaque : bool; - const_inline : bool} + const_constraints : constraints } +val subst_const_def : substitution -> constant_def -> constant_def val subst_const_body : substitution -> constant_body -> constant_body -(**********************************************************************) -(*s Representation of mutual inductive types in the kernel *) +(** 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 + +(** {6 Representation of mutual inductive types in the kernel } *) type recarg = | Norec - | Mrec of int + | Mrec of inductive | Imbr of inductive val subst_recarg : substitution -> recarg -> recarg @@ -72,12 +101,12 @@ val recarg_length : wf_paths -> int -> int val subst_wf_paths : substitution -> wf_paths -> wf_paths -(* -\begin{verbatim} +(** +{v Inductive I1 (params) : U1 := c11 : T11 | ... | c1p1 : T1p1 ... with In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpn -\end{verbatim} +v} *) type monomorphic_inductive_arity = { @@ -90,94 +119,72 @@ type inductive_arity = | Polymorphic of polymorphic_arity type one_inductive_body = { +(** {8 Primitive datas } *) -(* Primitive datas *) + mind_typename : identifier; (** Name of the type: [Ii] *) - (* Name of the type: [Ii] *) - mind_typename : identifier; + mind_arity_ctxt : rel_context; (** Arity context of [Ii] with parameters: [forall params, Ui] *) - (* Arity context of [Ii] with parameters: [forall params, Ui] *) - mind_arity_ctxt : rel_context; + mind_arity : inductive_arity; (** Arity sort and original user arity if monomorphic *) - (* Arity sort and original user arity if monomorphic *) - mind_arity : inductive_arity; + mind_consnames : identifier array; (** Names of the constructors: [cij] *) - (* Names of the constructors: [cij] *) - mind_consnames : identifier array; - - (* Types of the constructors with parameters: [forall params, Tij], - where the Ik are replaced by de Bruijn index in the context - I1:forall params, U1 .. In:forall params, Un *) mind_user_lc : types array; + (** Types of the constructors with parameters: [forall params, Tij], + where the Ik are replaced by de Bruijn index in the + context I1:forall params, U1 .. In:forall params, Un *) -(* Derived datas *) +(** {8 Derived datas } *) - (* Number of expected real arguments of the type (no let, no params) *) - mind_nrealargs : int; + mind_nrealargs : int; (** Number of expected real arguments of the type (no let, no params) *) - (* Length of realargs context (with let, no params) *) - mind_nrealargs_ctxt : int; + mind_nrealargs_ctxt : int; (** Length of realargs context (with let, no params) *) - (* List of allowed elimination sorts *) - mind_kelim : sorts_family list; + mind_kelim : sorts_family list; (** List of allowed elimination sorts *) - (* Head normalized constructor types so that their conclusion is atomic *) - mind_nf_lc : types array; + mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion is atomic *) - (* Length of the signature of the constructors (with let, 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) *) - (* Signature of recursive arguments in the constructors *) - mind_recargs : wf_paths; + mind_recargs : wf_paths; (** Signature of recursive arguments in the constructors *) -(* Datas for bytecode compilation *) +(** {8 Datas for bytecode compilation } *) - (* number of constant constructor *) - mind_nb_constant : int; + mind_nb_constant : int; (** number of constant constructor *) - (* number of no constant constructor *) - mind_nb_args : int; + mind_nb_args : int; (** number of no constant constructor *) mind_reloc_tbl : Cbytecodes.reloc_table; } type mutual_inductive_body = { - (* The component of the mutual inductive block *) - mind_packets : one_inductive_body array; + mind_packets : one_inductive_body array; (** The component of the mutual inductive block *) - (* Whether the inductive type has been declared as a record *) - mind_record : bool; + mind_record : bool; (** Whether the inductive type has been declared as a record *) - (* Whether the type is inductive or coinductive *) - mind_finite : bool; + mind_finite : bool; (** Whether the type is inductive or coinductive *) - (* Number of types in the block *) - mind_ntypes : int; + mind_ntypes : int; (** Number of types in the block *) - (* Section hypotheses on which the block depends *) - mind_hyps : section_context; + mind_hyps : section_context; (** Section hypotheses on which the block depends *) - (* Number of expected parameters *) - mind_nparams : int; + mind_nparams : int; (** Number of expected parameters *) - (* Number of recursively uniform (i.e. ordinary) parameters *) - mind_nparams_rec : int; + mind_nparams_rec : int; (** Number of recursively uniform (i.e. ordinary) parameters *) - (* The context of parameters (includes let-in declaration) *) - mind_params_ctxt : rel_context; + mind_params_ctxt : rel_context; (** The context of parameters (includes let-in declaration) *) - (* Universes constraints enforced by the inductive declaration *) - mind_constraints : constraints; + mind_constraints : constraints; (** Universes constraints enforced by the inductive declaration *) } val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body -(**********************************************************************) -(*s Modules: signature component specifications, module types, and - module declarations *) +(** {6 Modules: signature component specifications, module types, and + module declarations } *) type structure_field_body = | SFBconst of constant_body @@ -199,29 +206,39 @@ and with_declaration_body = | With_definition_body of identifier list * constant_body and module_body = - { (*absolute path of the module*) + { (** absolute path of the module *) mod_mp : module_path; - (* Implementation *) + (** Implementation *) mod_expr : struct_expr_body option; - (* Signature *) + (** Signature *) mod_type : struct_expr_body; - (* algebraic structure expression is kept + (** 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 *) + (** set of all constraint in the module *) mod_constraints : constraints; - (* quotiented set of equivalent constant and inductive name *) + (** 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*) + (** Path of the module type *) typ_mp : module_path; typ_expr : struct_expr_body; - (* algebraic structure expression is kept + (** 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 *) + (** 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 |