diff options
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 103 |
1 files changed, 53 insertions, 50 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index f4827029..51500979 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declarations.ml 11417 2008-09-17 15:06:57Z soubiran $ i*) +(*i $Id$ i*) (*i*) open Util @@ -38,7 +38,7 @@ type constr_substituted = constr substituted let from_val = from_val -let force = force subst_mps +let force = force subst_mps let subst_constr_subst = subst_substituted @@ -49,7 +49,7 @@ type constant_body = { const_body_code : Cemitcodes.to_patch_substituted; (* const_type_code : Cemitcodes.to_patch; *) const_constraints : constraints; - const_opaque : bool; + const_opaque : bool; const_inline : bool} (*s Inductive types (internal representation with redundant @@ -62,14 +62,14 @@ let subst_rel_declaration sub (id,copt,t as x) = let subst_rel_context sub = list_smartmap (subst_rel_declaration sub) -type recarg = - | Norec - | Mrec of int +type recarg = + | Norec + | Mrec of int | Imbr of inductive let subst_recarg sub r = match r with | Norec | Mrec _ -> r - | Imbr (kn,i) -> let kn' = subst_kn sub kn in + | Imbr (kn,i) -> let kn' = subst_ind sub kn in if kn==kn' then r else Imbr (kn',i) type wf_paths = recarg Rtree.t @@ -86,7 +86,7 @@ let dest_subterms p = let (_,cstrs) = Rtree.dest_node p in Array.map (fun t -> Array.to_list (snd (Rtree.dest_node t))) cstrs -let recarg_length p j = +let recarg_length p j = let (_,cstrs) = Rtree.dest_node p in Array.length (snd (Rtree.dest_node cstrs.(j-1))) @@ -105,7 +105,7 @@ type monomorphic_inductive_arity = { mind_sort : sorts; } -type inductive_arity = +type inductive_arity = | Monomorphic of monomorphic_inductive_arity | Polymorphic of polymorphic_arity @@ -135,6 +135,9 @@ 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; @@ -155,7 +158,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 = { @@ -187,25 +190,25 @@ 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 } -let subst_arity sub = function -| NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s) -| PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s) - +let subst_arity sub arity = + if sub = empty_subst then arity + else match arity with + | NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s) + | PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s) + (* TODO: should be changed to non-coping after Term.subst_mps *) let subst_const_body sub cb = { - const_hyps = (assert (cb.const_hyps=[]); []); - const_body = Option.map (subst_constr_subst sub) cb.const_body; - const_type = subst_arity sub cb.const_type; - const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code; - (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*) - const_constraints = cb.const_constraints; - const_opaque = cb.const_opaque; - const_inline = cb.const_inline} - + const_hyps = (assert (cb.const_hyps=[]); []); + const_body = Option.map (subst_constr_subst sub) cb.const_body; + const_type = subst_arity sub cb.const_type; + const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code; + (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*) + const_constraints = cb.const_constraints; + const_opaque = cb.const_opaque; + const_inline = cb.const_inline} + let subst_arity sub = function | Monomorphic s -> Monomorphic { @@ -214,7 +217,7 @@ let subst_arity sub = function } | Polymorphic s as x -> x -let subst_mind_packet sub mbp = +let subst_mind_packet sub mbp = { mind_consnames = mbp.mind_consnames; mind_consnrealdecls = mbp.mind_consnrealdecls; mind_typename = mbp.mind_typename; @@ -223,61 +226,61 @@ let subst_mind_packet sub mbp = mind_arity = subst_arity sub mbp.mind_arity; mind_user_lc = array_smartmap (subst_mps sub) mbp.mind_user_lc; mind_nrealargs = mbp.mind_nrealargs; + mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt; mind_kelim = mbp.mind_kelim; - mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*); + mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*); mind_nb_constant = mbp.mind_nb_constant; mind_nb_args = mbp.mind_nb_args; mind_reloc_tbl = mbp.mind_reloc_tbl } -let subst_mind sub mib = - { mind_record = mib.mind_record ; +let subst_mind sub mib = + { mind_record = mib.mind_record ; mind_finite = mib.mind_finite ; mind_ntypes = mib.mind_ntypes ; mind_hyps = (assert (mib.mind_hyps=[]); []) ; mind_nparams = mib.mind_nparams; mind_nparams_rec = mib.mind_nparams_rec; - mind_params_ctxt = + mind_params_ctxt = map_rel_context (subst_mps sub) mib.mind_params_ctxt; mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ; - mind_constraints = mib.mind_constraints ; - mind_equiv = Option.map (subst_kn sub) mib.mind_equiv } + mind_constraints = mib.mind_constraints } (*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 = + { mod_mp : module_path; + mod_expr : struct_expr_body option; + mod_type : struct_expr_body; + mod_type_alg : struct_expr_body option; mod_constraints : constraints; - mod_alias : substitution; + 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 = + { typ_mp : module_path; + typ_expr : struct_expr_body; + typ_expr_alg : struct_expr_body option ; + typ_constraints : constraints; + typ_delta :delta_resolver} |