diff options
| -rw-r--r-- | kernel/mod_subst.ml | 48 | ||||
| -rw-r--r-- | kernel/mod_typing.ml | 3 | ||||
| -rw-r--r-- | kernel/modops.ml | 53 | ||||
| -rw-r--r-- | kernel/modops.mli | 2 | ||||
| -rw-r--r-- | kernel/subtyping.ml | 2 |
5 files changed, 89 insertions, 19 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 640aecb98..b7bf1ba8b 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -526,20 +526,20 @@ let replace_mp_in_kn mpfrom mpto kn = if mp==mp'' then kn else make_kn mp'' dir l +let rec mp_in_mp mp mp1 = + match mp1 with + | _ when mp1 = mp -> true + | MPdot (mp2,l) -> mp_in_mp mp mp2 + | _ -> false + let mp_in_key mp key = - let rec mp_rec mp1 = - match mp1 with - | _ when mp1 = mp -> true - | MPdot (mp2,l) -> mp_rec mp2 - | _ -> false - in - match key with + match key with | MP mp1 -> - mp_rec mp1 + mp_in_mp mp mp1 | KN kn -> let mp1,dir,l = repr_kn kn in - mp_rec mp1 - + mp_in_mp mp mp1 + let subset_prefixed_by mp resolver = let prefixmp key hint resolv = match hint with @@ -652,10 +652,23 @@ let add_delta_resolver resolver1 resolver2 = Deltamap.fold Deltamap.add (update_delta_resolver resolver1 resolver2) resolver2 +let substition_prefixed_by k mp subst = + let prefixmp key (mp_to,reso) sub = + match key with + | MPI mpk -> + if mp_in_mp mp mpk then + let new_key = replace_mp_in_mp mp k mpk in + Umap.add (MPI new_key) (mp_to,reso) sub + else + sub + | _ -> sub + in + Umap.fold prefixmp subst empty_subst + let join (subst1 : substitution) (subst2 : substitution) = - let apply_subst (sub : substitution) (mp,resolve) = + let apply_subst key (mp,resolve) res = let mp',resolve' = - match subst_mp0 sub mp with + match subst_mp0 subst2 mp with None -> mp, None | Some (mp',resolve') -> mp' ,Some resolve' in @@ -663,12 +676,15 @@ let join (subst1 : substitution) (subst2 : substitution) = match resolve' with Some res -> add_delta_resolver - (subst_dom_codom_delta_resolver sub resolve) res + (subst_dom_codom_delta_resolver subst2 resolve) res | None -> - subst_codom_delta_resolver sub resolve + subst_codom_delta_resolver subst2 resolve in - mp',resolve'' in - let subst = Umap.map (apply_subst subst2) subst1 in + let k = match key with MBI mp -> MPbound mp | MPI mp -> mp in + let prefixed_subst = substition_prefixed_by k mp subst2 in + Umap.fold Umap.add prefixed_subst + (Umap.add key (mp',resolve'') res) in + let subst = Umap.fold apply_subst subst1 empty_subst in (Umap.fold Umap.add subst2 subst) diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index cfa256888..c9d9ac924 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -361,7 +361,8 @@ let rec translate_struct_include_module_entry env mp inl mse = match mse with | MSEident mp1 -> let mb = lookup_module mp1 env in let mb' = strengthen_and_subst_mb mb mp env true in - mb'.mod_type, mb'.mod_delta,Univ.Constraint.empty + let mb_typ = clean_bounded_mod_expr mb'.mod_type in + mb_typ, mb'.mod_delta,Univ.Constraint.empty | MSEapply (fexpr,mexpr) -> let sign,resolver,cst1 = translate_struct_include_module_entry env mp inl fexpr in diff --git a/kernel/modops.ml b/kernel/modops.ml index 80ce482bc..2d9c92afc 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -532,3 +532,56 @@ let subst_modtype_and_resolver mtb mp env = let full_subst = (map_mp mtb.typ_mp mp new_delta) in subst_modtype full_subst (fun resolver subst -> subst_dom_codom_delta_resolver subst resolver) mtb + +let rec is_bounded_expr l = function + | SEBident mp -> List.mem mp l + | SEBapply (fexpr,mexpr,_) -> + is_bounded_expr l mexpr || is_bounded_expr l fexpr + | _ -> false + +let rec clean_struct l = function + | (lab,SFBmodule mb) as field -> + let clean_typ = clean_expr l mb.mod_type in + let clean_impl = + begin try + if (is_bounded_expr l (Option.get mb.mod_expr)) then + Some clean_typ + else Some (clean_expr l (Option.get mb.mod_expr)) + with + Option.IsNone -> None + end in + if clean_typ==mb.mod_type && clean_impl==mb.mod_expr then + field + else + (lab,SFBmodule {mb with + mod_type=clean_typ; + mod_expr=clean_impl}) + | field -> field + +and clean_expr l = function + | SEBfunctor (mbid,sigt,str) as s-> + let str_clean = clean_expr l str in + let sig_clean = clean_expr l sigt.typ_expr in + if str_clean == str && sig_clean = sigt.typ_expr then + s else SEBfunctor (mbid,{sigt with typ_expr=sig_clean},str_clean) + | SEBstruct str as s-> + let str_clean = Util.list_smartmap (clean_struct l) str in + if str_clean == str then s else SEBstruct(str_clean) + | str -> str + +let rec collect_mbid l = function + | SEBfunctor (mbid,sigt,str) as s-> + let str_clean = collect_mbid ((MPbound mbid)::l) str in + if str_clean == str then s else + SEBfunctor (mbid,sigt,str_clean) + | SEBstruct str as s-> + let str_clean = Util.list_smartmap (clean_struct l) str in + if str_clean == str then s else SEBstruct(str_clean) + | _ -> anomaly "Modops:the evaluation of the structure failed " + + +let clean_bounded_mod_expr = function + | SEBfunctor _ as str -> + let str_clean = collect_mbid [] str in + if str_clean == str then str else str_clean + | str -> str diff --git a/kernel/modops.mli b/kernel/modops.mli index 435c196f9..3488a312f 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -53,6 +53,8 @@ val strengthen_and_subst_mb : module_body -> module_path -> env -> bool val subst_modtype_and_resolver : module_type_body -> module_path -> env -> module_type_body +val clean_bounded_mod_expr : struct_expr_body -> struct_expr_body + val error_existing_label : label -> 'a val error_declaration_not_path : module_struct_entry -> 'a diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 2a5f35f1a..e07af3ba3 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -390,8 +390,6 @@ and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv = let env = add_module (module_body_of_type (MPbound arg_id2) arg_t2) env in - let subst1 = - (join (map_mbid arg_id1 (MPbound arg_id2) arg_t2.typ_delta) subst1) in let env = match body_t1 with SEBstruct str -> add_module {mod_mp = mtb1.typ_mp; |