diff options
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/mod_subst.ml | 42 | ||||
-rw-r--r-- | kernel/mod_subst.mli | 2 | ||||
-rw-r--r-- | kernel/mod_typing.ml | 30 | ||||
-rw-r--r-- | kernel/modops.ml | 3 | ||||
-rw-r--r-- | kernel/subtyping.ml | 19 |
5 files changed, 73 insertions, 23 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 0df3e6631..040d7f811 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -347,6 +347,48 @@ let update_subst_alias subst1 subst2 = in Umap.fold alias_subst subst1 empty_subst +let update_subst subst1 subst2 = + let subst_inv key (mp,resolve) l = + let newmp = + match key with + | MBI msid -> MPbound msid + | MSI msid -> MPself msid + | MPI mp -> mp + in + match mp with + | MPbound mbid -> ((MBI mbid),newmp)::l + | MPself msid -> ((MSI msid),newmp)::l + | _ -> ((MPI mp),newmp)::l + in + let subst_mbi = Umap.fold subst_inv subst2 [] in + let alias_subst key (mp,resolve) sub= + let newsetkey = + match key with + | MPI mp1 -> + let compute_set_newkey l (k,mp') = + let mp_from_key = match k with + | MBI msid -> MPbound msid + | MSI msid -> MPself msid + | MPI mp -> mp + in + let new_mp1 = replace_mp_in_mp mp_from_key mp' mp1 in + if new_mp1 == mp1 then l else (MPI new_mp1)::l + in + begin + match List.fold_left compute_set_newkey [] subst_mbi with + | [] -> None + | l -> Some (l) + end + | _ -> None + in + match newsetkey with + | None -> sub + | Some l -> + List.fold_left (fun s k -> Umap.add k (mp,resolve) s) + sub l + in + Umap.fold alias_subst subst1 empty_subst + let join_alias (subst1 : substitution) (subst2 : substitution) = let apply_subst (sub : substitution) key (mp,resolve) = let mp',resolve' = diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index 5384d0f85..6ae9649d6 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -85,6 +85,8 @@ val occur_mbid : mod_bound_id -> substitution -> bool val update_subst_alias : substitution -> substitution -> substitution +val update_subst : substitution -> substitution -> substitution + val subst_key : substitution -> substitution -> substitution val join_alias : substitution -> substitution -> substitution diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 09edc63f6..4a2dd9afc 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -263,27 +263,25 @@ and translate_struct_entry env mse = match mse with | Not_path -> error_application_to_not_path mexpr (* place for nondep_supertype *) in let meb,sub2= translate_struct_entry env (MSEident mp) in - let sub2 = match eval_struct env (SEBident mp) with - | SEBstruct (msid,sign) -> subst_key (map_msid msid mp) sub2 - | _ -> sub2 in - let sub3= - if sub1 = empty_subst then - update_subst_alias sub2 (map_mbid farg_id mp None) + if sub1 = empty_subst then + let cst = check_subtypes env mtb farg_b in + SEBapply(feb,meb,cst),sub1 else - update_subst_alias sub2 - (join_alias sub1 (map_mbid farg_id mp None)) - in - let sub = if sub2 = sub3 then - join sub1 sub2 else join (join sub1 sub2) sub3 in - let sub = join_alias sub (map_mbid farg_id mp None) in - let sub = update_subst_alias sub (map_mbid farg_id mp None) in - let cst = check_subtypes env mtb farg_b in - SEBapply(feb,meb,cst),sub + let sub2 = match eval_struct env (SEBident mp) with + | SEBstruct (msid,sign) -> + join_alias + (subst_key (map_msid msid mp) sub2) + (map_msid msid mp) + | _ -> sub2 in + let sub3 = join_alias sub1 (map_mbid farg_id mp None) in + let sub4 = update_subst sub2 sub3 in + let cst = check_subtypes env mtb farg_b in + SEBapply(feb,meb,cst),(join sub3 sub4) | MSEwith(mte, with_decl) -> let mtb,sub1 = translate_struct_entry env mte in let mtb',sub2 = check_with env mtb with_decl in mtb',join sub1 sub2 - + let rec add_struct_expr_constraints env = function | SEBident _ -> env diff --git a/kernel/modops.ml b/kernel/modops.ml index 590db2727..49e49f573 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -329,8 +329,9 @@ and merge_with env mtb with_decl alias= match with_decl with With_definition_body (_,c) -> With_definition_body (idl,c),None | With_module_body (idc,mp,cst) -> + let mp' = scrape_alias mp env in With_module_body (idl,mp,cst), - Some(map_mp (mp_rec (List.rev idc)) mp) + Some(map_mp (mp_rec (List.rev idc)) mp') in let subst = match subst1 with | None -> None diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index a24f835d9..0c31d7962 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -289,9 +289,16 @@ let check_constant cst env msid1 l info1 cb2 spec2 = check_conv cst conv env ty1 ty2 | _ -> error () -let rec check_modules cst env msid1 l msb1 msb2 = +let rec check_modules cst env msid1 l msb1 msb2 alias = let mp = (MPdot(MPself msid1,l)) in let mty1 = module_type_of_module (Some mp) msb1 in + let alias1,struct_expr = match eval_struct env mty1.typ_expr with + | SEBstruct (msid,sign) as str -> + update_subst alias (map_msid msid mp),str + | _ as str -> empty_subst,str in + let mty1 = {mty1 with + typ_expr = struct_expr; + typ_alias = join alias1 mty1.typ_alias } in let mty2 = module_type_of_module None msb2 in let cst = check_modtypes cst env mty1 mty2 false in cst @@ -301,8 +308,8 @@ and check_signatures cst env (msid1,sig1) alias (msid2,sig2') = let mp1 = MPself msid1 in let env = add_signature mp1 sig1 env in let sig1 = subst_structure alias sig1 in - let alias = update_subst_alias alias (map_msid msid2 mp1) in - let sig2 = subst_structure alias sig2' in + let alias1 = update_subst_alias alias (map_msid msid2 mp1) in + let sig2 = subst_structure alias1 sig2' in let sig2 = subst_signature_msid msid2 mp1 sig2 in let map1 = make_label_map mp1 sig1 in let check_one_body cst (l,spec2) = @@ -321,14 +328,14 @@ and check_signatures cst env (msid1,sig1) alias (msid2,sig2') = | SFBmodule msb2 -> begin match info1 with - | Module msb -> check_modules cst env msid1 l msb msb2 + | Module msb -> check_modules cst env msid1 l msb msb2 alias | Alias mp ->let msb = {mod_expr = Some (SEBident mp); mod_type = Some (eval_struct env (SEBident mp)); mod_constraints = Constraint.empty; mod_alias = (lookup_modtype mp env).typ_alias; mod_retroknowledge = []} in - check_modules cst env msid1 l msb msb2 + check_modules cst env msid1 l msb msb2 alias | _ -> error_not_match l spec2 end | SFBalias (mp,_) -> @@ -342,7 +349,7 @@ and check_signatures cst env (msid1,sig1) alias (msid2,sig2') = mod_constraints = Constraint.empty; mod_alias = (lookup_modtype mp env).typ_alias; mod_retroknowledge = []} in - check_modules cst env msid1 l msb msb1 + check_modules cst env msid1 l msb msb1 alias | _ -> error_not_match l spec2 end | SFBmodtype mtb2 -> |