diff options
Diffstat (limited to 'kernel/declarations.mli')
| -rw-r--r-- | kernel/declarations.mli | 70 |
1 files changed, 42 insertions, 28 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index b4f5f1f7..adf1d14e 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declarations.mli 11417 2008-09-17 15:06:57Z soubiran $ i*) +(*i $Id$ i*) (*i*) open Names @@ -55,9 +55,9 @@ val subst_const_body : substitution -> constant_body -> constant_body (**********************************************************************) (*s Representation of mutual inductive types in the kernel *) -type recarg = - | Norec - | Mrec of int +type recarg = + | Norec + | Mrec of int | Imbr of inductive val subst_recarg : substitution -> recarg -> recarg @@ -85,7 +85,7 @@ type monomorphic_inductive_arity = { mind_sort : sorts; } -type inductive_arity = +type inductive_arity = | Monomorphic of monomorphic_inductive_arity | Polymorphic of polymorphic_arity @@ -115,13 +115,17 @@ type one_inductive_body = { (* Number of expected real arguments of the type (no let, no params) *) mind_nrealargs : int; + (* Length of realargs context (with let, no params) *) + mind_nrealargs_ctxt : int; + (* List of allowed elimination sorts *) mind_kelim : sorts_family list; (* Head normalized constructor types so that their conclusion is atomic *) mind_nf_lc : types array; - (* Length of the signature of the constructors (with let, w/o params) *) + (* Length of the signature of the constructors (with let, w/o params) + (not used in the kernel) *) mind_consnrealdecls : int array; (* Signature of recursive arguments in the constructors *) @@ -135,7 +139,7 @@ type one_inductive_body = { (* number of no constant constructor *) mind_nb_args : int; - mind_reloc_tbl : Cbytecodes.reloc_table; + mind_reloc_tbl : Cbytecodes.reloc_table; } type mutual_inductive_body = { @@ -167,8 +171,6 @@ type mutual_inductive_body = { (* Universes constraints enforced by the inductive declaration *) mind_constraints : constraints; - (* Source of the inductive block when aliased in a module *) - mind_equiv : kernel_name option } val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body @@ -177,37 +179,49 @@ val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body (*s Modules: signature component specifications, module types, and module declarations *) -type structure_field_body = +type structure_field_body = | SFBconst of constant_body | SFBmind of mutual_inductive_body | SFBmodule of module_body - | SFBalias of module_path * struct_expr_body option - *constraints option | SFBmodtype of module_type_body and structure_body = (label * structure_field_body) list and struct_expr_body = | SEBident of module_path - | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body - | SEBstruct of mod_self_id * structure_body - | SEBapply of struct_expr_body * struct_expr_body - * constraints + | 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 and with_declaration_body = - With_module_body of identifier list * module_path - * struct_expr_body option * constraints + With_module_body of identifier list * module_path | With_definition_body of identifier list * constant_body - -and module_body = - { mod_expr : struct_expr_body option; - mod_type : struct_expr_body option; + +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; - mod_alias : substitution; + (* quotiented set of equivalent constant and inductive name *) + mod_delta : delta_resolver; mod_retroknowledge : Retroknowledge.action list} - -and module_type_body = - { typ_expr : struct_expr_body; - typ_strength : module_path option; - typ_alias : substitution} + +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} |