diff options
| -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 | ||||
| -rw-r--r-- | library/declaremods.ml | 20 |
6 files changed, 85 insertions, 31 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 -> diff --git a/library/declaremods.ml b/library/declaremods.ml index 5f7daa9b5..59da90e66 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -332,7 +332,9 @@ let subst_module ((sp,kn),subst,(entry,substobjs,_)) = check_empty "subst_module" entry; let dir,mp = dir_of_sp sp, mp_of_kn kn in let (sub,mbids,msid,objs) = substobjs in + let sub = subst_key subst sub in let sub' = update_subst_alias subst sub in + let sub' = update_subst_alias sub' (map_msid msid mp) in let sub = join sub' sub in let subst' = join sub subst in (* substitutive_objects get the new substitution *) @@ -346,6 +348,7 @@ let subst_module ((sp,kn),subst,(entry,substobjs,_)) = let subst_module_alias ((sp,kn),subst,(entry,substobjs,_)) = let dir,mp = dir_of_sp sp, mp_of_kn kn in let (sub,mbids,msid,objs) = substobjs in + let sub = update_subst_alias subst (map_msid msid mp) in let subst' = join sub subst in (* substitutive_objects get the new substitution *) let substobjs = (subst',mbids,msid,objs) in @@ -365,8 +368,8 @@ let subst_module_alias ((sp,kn),subst,(entry,substobjs,_)) = substobjs, match mbids with | [] -> Some (subst_objects prefix - (join (map_mp mp mp') - (join (map_msid msid mp') subst)) objs) + (join subst' (join (map_msid msid mp') + (map_mp mp mp'))) objs) | _ -> None) | _ -> anomaly "Modops: Not an alias" @@ -886,12 +889,10 @@ let rec get_module_substobjs env = function if sub1 = empty_subst then update_subst_alias sub_alias (map_mbid farg_id mp None) else - update_subst_alias sub_alias - (join_alias sub1 (map_mbid farg_id mp None)) + let sub1' = join_alias sub1 (map_mbid farg_id mp None) in + let sub_alias' = update_subst_alias sub_alias sub1' in + join sub1' sub_alias' in - let sub = if sub_alias = sub3 then - join sub1 sub_alias else join (join sub1 sub_alias) sub3 in - let sub = join_alias sub (map_mbid farg_id mp None) in let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in (match mbids with | mbid::mbids -> @@ -901,7 +902,7 @@ let rec get_module_substobjs env = function objects (that are all non-logical objects) *) ((join (join subst (map_mbid mbid mp (Some resolve))) - sub) + sub3) , mbids, msid, objs) | [] -> match mexpr with | MSEident _ -> error "Application of a non-functor" @@ -1072,6 +1073,9 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = (in_module_alias (Some (entry, mty_sub_o), substobjs, substituted))) | _ -> let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in + let (sub,mbids,msid,objs) = substobjs in + let sub' = subst_key (map_msid msid mp) sub in + let substobjs = (join sub sub',mbids,msid,objs) in let substituted = subst_substobjs dir mp substobjs in ignore (add_leaf id |