aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/mod_subst.ml16
-rw-r--r--kernel/mod_typing.ml16
-rw-r--r--kernel/modops.ml9
-rw-r--r--kernel/safe_typing.ml3
-rw-r--r--library/declaremods.ml14
-rw-r--r--test-suite/output/TranspModtype.out6
6 files changed, 38 insertions, 26 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index ea477d6a1..3b3d28090 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -320,16 +320,14 @@ let update_subst_alias subst1 subst2 =
let subst_inv key (mp,resolve) sub =
let newmp =
match key with
- | MBI msid -> Some (MPbound msid)
- | MSI msid -> Some (MPself msid)
- | _ -> None
+ | MBI msid -> MPbound msid
+ | MSI msid -> MPself msid
+ | MPI mp -> mp
in
- match newmp with
- | None -> sub
- | Some mpi -> match mp with
- | MPbound mbid -> Umap.add (MBI mbid) (mpi,None) sub
- | MPself msid -> Umap.add (MSI msid) (mpi,None) sub
- | _ -> Umap.add (MPI mp) (mpi,None) sub
+ match mp with
+ | MPbound mbid -> Umap.add (MBI mbid) (newmp,None) sub
+ | MPself msid -> Umap.add (MSI msid) (newmp,None) sub
+ | _ -> Umap.add (MPI mp) (newmp,None) sub
in
let subst_mbi = Umap.fold subst_inv subst2 empty_subst in
let alias_subst key (mp,resolve) sub=
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 3ae9293c7..36ef0c5e6 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -243,16 +243,22 @@ and translate_struct_entry env mse = match mse with
let feb'= eval_struct env feb
in
let farg_id, farg_b, fbody_b = destr_functor env feb' in
- let mtb =
+ let mtb,mp =
try
- lookup_modtype (path_of_mexpr mexpr) env
+ let mp = path_of_mexpr mexpr in
+ lookup_modtype mp env,mp
with
| Not_path -> error_application_to_not_path mexpr
(* place for nondep_supertype *) in
let meb,sub2= translate_struct_entry env mexpr in
- let sub = join sub1 sub2 in
- let sub = join_alias sub (map_mbid farg_id (path_of_mexpr mexpr) None) in
- let sub = update_subst_alias sub (map_mbid farg_id (path_of_mexpr mexpr) None) in
+ let sub2 = match eval_struct env (SEBident mp) with
+ | SEBstruct (msid,sign) -> subst_key (map_msid msid mp) sub2
+ | _ -> sub2 in
+ let sub3 = 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
| MSEwith(mte, with_decl) ->
diff --git a/kernel/modops.ml b/kernel/modops.ml
index dc339af52..8d74c4c30 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -271,6 +271,9 @@ let rec eval_struct env = function
| SEBwith (mtb, (With_module_body (_,mp,_) as wdb)) ->
let alias_in_mp =
(lookup_modtype mp env).typ_alias in
+ let alias_in_mp = match eval_struct env (SEBident mp) with
+ | SEBstruct (msid,sign) -> subst_key (map_msid msid mp) alias_in_mp
+ | _ -> alias_in_mp in
merge_with env mtb wdb alias_in_mp
(* | SEBfunctor(mbid,mtb,body) ->
let env = add_module (MPbound mbid) (module_body_of_type mtb) env in
@@ -308,8 +311,9 @@ and merge_with env mtb with_decl alias=
SFBconst c,None
| With_module_body ([id], mp,cst) ->
let mp' = scrape_alias mp env in
+ let new_alias = update_subst_alias alias (map_mp (mp_rec [id]) mp') in
SFBalias (mp,Some cst),
- Some(join (map_mp (mp_rec [id]) mp') alias)
+ Some(join (map_mp (mp_rec [id]) mp') new_alias)
| With_definition_body (_::_,_)
| With_module_body (_::_,_,_) ->
let old = match spec with
@@ -323,6 +327,9 @@ and merge_with env mtb with_decl alias=
With_module_body (idl,mp,cst),
Some(map_mp (mp_rec idc) mp)
in
+ let subst1 = match subst1 with
+ | None -> None
+ | Some s -> Some (update_subst_alias alias s) in
let subst = Option.fold_right join subst1 alias in
let modtype =
merge_with env (type_of_mb env old) new_with_decl alias in
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index b1eea3bbd..a895e68ce 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -311,7 +311,8 @@ let add_alias l mp senv =
(* we get all alias substitutions that comes from mp *)
let _,sub = translate_struct_entry senv.env (MSEident mp) in
(* we add the new one *)
- let sub = join (map_mp mp' mp) sub in
+ let mp1 = scrape_alias mp senv.env in
+ let sub = join (map_mp mp' mp1) sub in
let env' = register_alias mp' mp senv.env in
mp', { old = senv.old;
env = env';
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 01450599a..80944b2e6 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -568,7 +568,7 @@ let rec get_modtype_substobjs env = function
Modops.resolver_of_environment farg_id farg_b mp sub_alias env in
(* application outside the kernel, only for substitutive
objects (that are all non-logical objects) *)
- (join (join (map_mbid mbid mp (Some resolve)) subst ) sub_alias
+ (join (join subst (map_mbid mbid mp (Some resolve))) sub_alias
, mbids, msid, objs)
| [] -> match mexpr with
| MSEident _ -> error "Application of a non-functor"
@@ -661,20 +661,19 @@ let end_module id =
anomaly "Funsig cannot be here..."
| Some (MSEapply _ as mty) ->
abstract_substobjs mbids (get_modtype_substobjs (Global.env()) mty), [], []
- with
+ with
Not_found -> anomaly "Module objects not found..."
in
-
(* must be called after get_modtype_substobjs, because of possible
dependencies on functor arguments *)
let mp = Global.end_module id res_o in
-
+
begin match sub_o with
None -> ()
| Some sub_mtb -> check_subtypes mp sub_mtb
end;
-
+
Summary.module_unfreeze_summaries fs;
let substituted = subst_substobjs dir mp substobjs in
@@ -875,7 +874,7 @@ let rec get_module_substobjs env = function
(* application outside the kernel, only for substitutive
objects (that are all non-logical objects) *)
((join
- (join (map_mbid mbid mp (Some resolve)) subst)
+ (join subst (map_mbid mbid mp (Some resolve)))
sub_alias)
, mbids, msid, objs)
| [] -> match mexpr with
@@ -940,11 +939,12 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
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 prefix = dir,(mp',empty_dirpath) in
+ let mp1 = Environ.scrape_alias mp env in
let substituted =
match mbids with
| [] ->
Some (subst_objects prefix
- (join sub (join (map_msid msid mp') (map_mp mp' mp))) objs)
+ (join sub (join (map_msid msid mp') (map_mp mp' mp1))) objs)
| _ -> None in
ignore (add_leaf
id
diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out
index 009d7fc35..f94ed6423 100644
--- a/test-suite/output/TranspModtype.out
+++ b/test-suite/output/TranspModtype.out
@@ -1,7 +1,7 @@
-TrM.A = N.A
+TrM.A = M.A
: Set
-OpM.A = N.A
+OpM.A = M.A
: Set
-TrM.B = N.B
+TrM.B = M.B
: Set
*** [ OpM.B : Set ]
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 01:23:08 +0000