diff options
Diffstat (limited to 'kernel/subtyping.ml')
| -rw-r--r-- | kernel/subtyping.ml | 74 |
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 |