summaryrefslogtreecommitdiff
path: root/kernel/subtyping.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/subtyping.ml')
-rw-r--r--kernel/subtyping.ml74
1 files changed, 39 insertions, 35 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index c141a02a..08ee67b4 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -32,15 +32,18 @@ type namedobject =
| Constant of constant_body
| IndType of inductive * mutual_inductive_body
| IndConstr of constructor * mutual_inductive_body
+
+type namedmodule =
| Module of module_body
| Modtype of module_type_body
(* adds above information about one mutual inductive: all types and
constructors *)
-let add_nameobjects_of_mib ln mib map =
- let add_nameobjects_of_one j oib map =
- let ip = (ln,j) in
+let add_mib_nameobjects mp l mib map =
+ let ind = make_mind mp empty_dirpath l in
+ let add_mip_nameobjects j oib map =
+ let ip = (ind,j) in
let map =
array_fold_right_i
(fun i id map ->
@@ -50,22 +53,33 @@ let add_nameobjects_of_mib ln mib map =
in
Labmap.add (label_of_id oib.mind_typename) (IndType (ip, mib)) map
in
- array_fold_right_i add_nameobjects_of_one mib.mind_packets map
+ array_fold_right_i add_mip_nameobjects mib.mind_packets map
+
+
+(* creates (namedobject/namedmodule) map for the whole signature *)
+
+type labmap = { objs : namedobject Labmap.t; mods : namedmodule Labmap.t }
+let empty_labmap = { objs = Labmap.empty; mods = Labmap.empty }
-(* creates namedobject map for the whole signature *)
+let get_obj mp map l =
+ try Labmap.find l map.objs
+ with Not_found -> error_no_such_label_sub l (string_of_mp mp)
-let make_label_map mp list =
+let get_mod mp map l =
+ try Labmap.find l map.mods
+ with Not_found -> error_no_such_label_sub l (string_of_mp mp)
+
+let make_labmap mp list =
let add_one (l,e) map =
- let add_map obj = Labmap.add l obj map in
match e with
- | SFBconst cb -> add_map (Constant cb)
- | SFBmind mib ->
- add_nameobjects_of_mib (make_mind mp empty_dirpath l) mib map
- | SFBmodule mb -> add_map (Module mb)
- | SFBmodtype mtb -> add_map (Modtype mtb)
+ | SFBconst cb -> { map with objs = Labmap.add l (Constant cb) map.objs }
+ | SFBmind mib -> { map with objs = add_mib_nameobjects mp l mib map.objs }
+ | SFBmodule mb -> { map with mods = Labmap.add l (Module mb) map.mods }
+ | SFBmodtype mtb -> { map with mods = Labmap.add l (Modtype mtb) map.mods }
in
- List.fold_right add_one list Labmap.empty
+ List.fold_right add_one list empty_labmap
+
let check_conv_error error why cst f env a1 a2 =
try
@@ -299,7 +313,6 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in
let ty2 = Typeops.type_of_constant_type env cb2.const_type in
check_conv NotConvertibleTypeField cst conv env ty1 ty2
- | _ -> error DefinitionFieldExpected
let rec check_modules cst env msb1 msb2 subst1 subst2 =
let mty1 = module_type_of_module None msb1 in
@@ -308,33 +321,24 @@ let rec check_modules cst env msb1 msb2 subst1 subst2 =
cst
and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2=
- let map1 = make_label_map mp1 sig1 in
+ let map1 = make_labmap mp1 sig1 in
let check_one_body cst (l,spec2) =
- let info1 =
- try
- Labmap.find l map1
- with
- Not_found -> error_no_such_label_sub l
- (string_of_mp mp1)
- in
- match spec2 with
+ match spec2 with
| SFBconst cb2 ->
- check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2
+ check_constant cst env mp1 l (get_obj mp1 map1 l)
+ cb2 spec2 subst1 subst2
| SFBmind mib2 ->
- check_inductive cst env
- mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
+ check_inductive cst env mp1 l (get_obj mp1 map1 l)
+ mp2 mib2 spec2 subst1 subst2 reso1 reso2
| SFBmodule msb2 ->
- begin
- match info1 with
- | Module msb -> check_modules cst env msb msb2
- subst1 subst2
- | _ -> error_signature_mismatch l spec2 ModuleFieldExpected
+ begin match get_mod mp1 map1 l with
+ | Module msb -> check_modules cst env msb msb2 subst1 subst2
+ | _ -> error_signature_mismatch l spec2 ModuleFieldExpected
end
| SFBmodtype mtb2 ->
- let mtb1 =
- match info1 with
- | Modtype mtb -> mtb
- | _ -> error_signature_mismatch l spec2 ModuleTypeFieldExpected
+ let mtb1 = match get_mod mp1 map1 l with
+ | Modtype mtb -> mtb
+ | _ -> error_signature_mismatch l spec2 ModuleTypeFieldExpected
in
let env = add_module (module_body_of_type mtb2.typ_mp mtb2)
(add_module (module_body_of_type mtb1.typ_mp mtb1) env) in