summaryrefslogtreecommitdiff
path: root/kernel/declarations.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/declarations.ml')
-rw-r--r--kernel/declarations.ml103
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}