diff options
Diffstat (limited to 'kernel/subtyping.ml')
| -rw-r--r-- | kernel/subtyping.ml | 114 |
1 files changed, 54 insertions, 60 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 99c1b8483..6cedb6ad2 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -319,10 +319,9 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = check_conv error cst conv env ty1 ty2 let rec check_modules cst env msb1 msb2 subst1 subst2 = - let mty1 = module_type_of_module None msb1 in - let mty2 = module_type_of_module None msb2 in - let cst = check_modtypes cst env mty1 mty2 subst1 subst2 false in - cst + let mty1 = module_type_of_module msb1 in + let mty2 = module_type_of_module msb2 in + check_modtypes cst env mty1 mty2 subst1 subst2 false and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2= let map1 = make_labmap mp1 sig1 in @@ -344,67 +343,62 @@ and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2= | 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 - check_modtypes cst env mtb1 mtb2 subst1 subst2 true + let env = + add_module_type mtb2.typ_mp mtb2 + (add_module_type mtb1.typ_mp mtb1 env) + in + check_modtypes cst env mtb1 mtb2 subst1 subst2 true in List.fold_left check_one_body cst sig2 -and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv = - if mtb1==mtb2 then cst else - let mtb1',mtb2'=mtb1.typ_expr,mtb2.typ_expr in - let rec check_structure cst env str1 str2 equiv subst1 subst2 = - match str1,str2 with - | SEBstruct (list1), - SEBstruct (list2) -> - if equiv then - let subst2 = - add_mp mtb2.typ_mp mtb1.typ_mp mtb1.typ_delta subst2 in - Univ.union_constraints - (check_signatures cst env - mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2 - mtb1.typ_delta mtb2.typ_delta) - (check_signatures cst env - mtb2.typ_mp list2 mtb1.typ_mp list1 subst2 subst1 - mtb2.typ_delta mtb1.typ_delta) - else - check_signatures cst env - mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2 - mtb1.typ_delta mtb2.typ_delta - | SEBfunctor (arg_id1,arg_t1,body_t1), - SEBfunctor (arg_id2,arg_t2,body_t2) -> - let subst1 = - (join (map_mbid arg_id1 (MPbound arg_id2) arg_t2.typ_delta) subst1) in - let cst = check_modtypes cst env - arg_t2 arg_t1 subst2 subst1 - equiv in - (* contravariant *) - let env = add_module - (module_body_of_type (MPbound arg_id2) arg_t2) env - in - let env = match body_t1 with - SEBstruct str -> - add_module {mod_mp = mtb1.typ_mp; - mod_expr = None; - mod_type = subst_struct_expr subst1 body_t1; - mod_type_alg= None; - mod_constraints=mtb1.typ_constraints; - mod_retroknowledge = []; - mod_delta = mtb1.typ_delta} env - | _ -> env - in - check_structure cst env body_t1 body_t2 equiv - subst1 - subst2 - | _ , _ -> error_incompatible_modtypes mtb1 mtb2 - in - if mtb1'== mtb2' then cst - else check_structure cst env mtb1' mtb2' equiv subst1 subst2 +and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv = + if mtb1==mtb2 || mtb1.typ_expr == mtb2.typ_expr then cst + else + let rec check_structure cst env str1 str2 equiv subst1 subst2 = + match str1,str2 with + |NoFunctor list1, + NoFunctor list2 -> + if equiv then + let subst2 = add_mp mtb2.typ_mp mtb1.typ_mp mtb1.typ_delta subst2 in + let cst1 = check_signatures cst env + mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2 + mtb1.typ_delta mtb2.typ_delta + in + let cst2 = check_signatures cst env + mtb2.typ_mp list2 mtb1.typ_mp list1 subst2 subst1 + mtb2.typ_delta mtb1.typ_delta + in + Univ.union_constraints cst1 cst2 + else + check_signatures cst env + mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2 + mtb1.typ_delta mtb2.typ_delta + |MoreFunctor (arg_id1,arg_t1,body_t1), + MoreFunctor (arg_id2,arg_t2,body_t2) -> + let mp2 = MPbound arg_id2 in + let subst1 = join (map_mbid arg_id1 mp2 arg_t2.typ_delta) subst1 in + let cst = check_modtypes cst env arg_t2 arg_t1 subst2 subst1 equiv in + (* contravariant *) + let env = add_module_type mp2 arg_t2 env in + let env = + if Modops.is_functor body_t1 then env + else add_module + {mod_mp = mtb1.typ_mp; + mod_expr = Abstract; + mod_type = subst_signature subst1 body_t1; + mod_type_alg = None; + mod_constraints = mtb1.typ_constraints; + mod_retroknowledge = []; + mod_delta = mtb1.typ_delta} env + in + check_structure cst env body_t1 body_t2 equiv subst1 subst2 + | _ , _ -> error_incompatible_modtypes mtb1 mtb2 + in + check_structure cst env mtb1.typ_expr mtb2.typ_expr equiv subst1 subst2 let check_subtypes env sup super = - let env = add_module - (module_body_of_type sup.typ_mp sup) env in - check_modtypes empty_constraint env + let env = add_module_type sup.typ_mp sup env in + check_modtypes empty_constraint env (strengthen sup sup.typ_mp) super empty_subst (map_mp super.typ_mp sup.typ_mp sup.typ_delta) false |