From 7929ce046f6d10b3ad3ddbc9460172e13be55e29 Mon Sep 17 00:00:00 2001 From: soubiran Date: Tue, 22 Apr 2008 14:29:51 +0000 Subject: correction bug 1839 -is line, and those below, will be ignored-- M kernel/mod_typing.ml M kernel/subtyping.ml M kernel/modops.ml M library/declaremods.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10829 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/mod_typing.ml | 26 +++++++++++++++++++------- kernel/modops.ml | 29 +++++++++++++++++------------ kernel/subtyping.ml | 1 + library/declaremods.ml | 34 ++++++++++++++++++++-------------- 4 files changed, 57 insertions(+), 33 deletions(-) diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 662841cdf..b1daea228 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -43,7 +43,7 @@ let rec check_with env mtb with_decl = let cb = check_with_aux_def env mtb with_decl in SEBwith(mtb,With_definition_body(id,cb)),empty_subst | With_Module (id,mp) -> - let cst,sub = check_with_aux_mod env mtb with_decl in + let cst,sub = check_with_aux_mod env mtb with_decl true in SEBwith(mtb,With_module_body(id,mp,cst)),sub and check_with_aux_def env mtb with_decl = @@ -116,7 +116,7 @@ and check_with_aux_def env mtb with_decl = Not_found -> error_no_such_label l | Reduction.NotConvertible -> error_with_incorrect l -and check_with_aux_mod env mtb with_decl = +and check_with_aux_mod env mtb with_decl now = let initmsid,msid,sig_b = match (eval_struct env mtb) with | SEBstruct(msid,sig_b) ->let msid'=(refresh_msid msid) in msid,msid',(subst_signature_msid msid (MPself(msid')) sig_b) @@ -162,7 +162,12 @@ and check_with_aux_mod env mtb with_decl = | _,_ -> anomaly "Mod_typing:no implementation and no alias" in - cst,join (map_mp (mp_rec [id]) mp) mtb'.typ_alias + if now then + let mp' = scrape_alias mp env' in + let up_subst = update_subst_alias mtb'.typ_alias (map_mp (mp_rec [id]) mp') in + cst, (join (map_mp (mp_rec [id]) mp') up_subst) + else + cst,empty_subst | With_Module (_::_,mp) -> let old = match spec with SFBmodule msb -> msb @@ -175,11 +180,18 @@ and check_with_aux_mod env mtb with_decl = With_Definition (_,c) -> With_Definition (idl,c) | With_Module (_,c) -> With_Module (idl,c) in - let cst,sub = + let cst,_ = check_with_aux_mod env' - (type_of_mb env old) new_with_decl in - cst,(join (map_mp (mp_rec idl) mp) sub) - | Some msb -> + (type_of_mb env old) new_with_decl false in + if now then + let mtb' = lookup_modtype mp env' in + let mp' = scrape_alias mp env' in + let up_subst = update_subst_alias + mtb'.typ_alias (map_mp (mp_rec (List.rev (id::idl))) mp') in + cst, (join (map_mp (mp_rec (List.rev (id::idl))) mp') up_subst) + else + cst,empty_subst + | Some msb -> error_a_generative_module_expected l end | _ -> anomaly "Modtyping:incorrect use of with" diff --git a/kernel/modops.ml b/kernel/modops.ml index 4d0af4fee..0d0af00f0 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -270,17 +270,19 @@ let rec eval_struct env = function (join sub_alias (map_mbid farg_id mp (Some resolve))) fbody_b) | SEBwith (mtb,(With_definition_body _ as wdb)) -> - merge_with env mtb wdb empty_subst + let mtb',_ = merge_with env mtb wdb empty_subst in + mtb' | 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 + let mtb',_ = merge_with env mtb wdb alias_in_mp in + mtb' (* | SEBfunctor(mbid,mtb,body) -> - let env = add_module (MPbound mbid) (module_body_of_type mtb) env in - SEBfunctor(mbid,mtb,eval_struct env body) *) + let env = add_module (MPbound mbid) (module_body_of_type mtb) env in + SEBfunctor(mbid,mtb,eval_struct env body) *) | mtb -> mtb and type_of_mb env mb = @@ -328,25 +330,28 @@ and merge_with env mtb with_decl alias= With_definition_body (_,c) -> With_definition_body (idl,c),None | With_module_body (idc,mp,cst) -> With_module_body (idl,mp,cst), - Some(map_mp (mp_rec idc) mp) + Some(map_mp (mp_rec (List.rev idc)) mp) in - let subst1 = match subst1 with + let subst = 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 = + | Some s -> Some (join s (update_subst_alias alias s)) in + let modtype,subst_msb = merge_with env (type_of_mb env old) new_with_decl alias in let msb = { mod_expr = None; mod_type = Some modtype; mod_constraints = old.mod_constraints; - mod_alias = subst; + mod_alias = begin + match subst_msb with + |None -> empty_subst + |Some s -> s + end; mod_retroknowledge = old.mod_retroknowledge} in - (SFBmodule msb),Some subst + (SFBmodule msb),subst in SEBstruct(msid, before@(l,new_spec):: - (Option.fold_right subst_structure subst after)) + (Option.fold_right subst_structure subst after)),subst with Not_found -> error_no_such_label l diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index e4b1f7045..a24f835d9 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -300,6 +300,7 @@ let rec check_modules cst env msid1 l msb1 msb2 = 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 sig2 = subst_signature_msid msid2 mp1 sig2 in diff --git a/library/declaremods.ml b/library/declaremods.ml index 3907ab21b..93e322e2c 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -538,7 +538,7 @@ let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs mp = else error "MODULE expected!" | idl,lobj::tail -> lobj::replace_idl (idl,tail) in - (join (map_mp (mp_rec idl) mp) subst, mbids, msid, replace_idl (idl,lib_stack)) + (join (map_mp (mp_rec (List.rev idl)) mp) subst, mbids, msid, replace_idl (idl,lib_stack)) let abstract_substobjs mbids1 (subst, mbids2, msid, lib_stack) = (subst, mbids1@mbids2, msid, lib_stack) @@ -554,7 +554,7 @@ let rec get_modtype_substobjs env = function let modobjs = MPmap.find mp !modtab_substobjs in replace_module_object idl substobjs modobjs mp | MSEapply (mexpr, MSEident mp) -> - let ftb,_ = Mod_typing.translate_struct_entry env mexpr in + let ftb,sub1 = Mod_typing.translate_struct_entry env mexpr in let farg_id, farg_b, fbody_b = Modops.destr_functor env (Modops.eval_struct env ftb) in let mp = Environ.scrape_alias mp env in @@ -564,18 +564,22 @@ let rec get_modtype_substobjs env = function (subst_key (map_msid msid mp) sub_alias) (map_msid msid mp) | _ -> sub_alias in - let sub_alias = join_alias sub_alias (map_mbid farg_id mp None) in - let sub_alias = update_subst_alias sub_alias - (map_mbid farg_id mp (None)) in - let (subst, mbids, msid, objs) = get_modtype_substobjs env mexpr in + let sub3 = update_subst_alias sub_alias + (join_alias sub1 (map_mbid farg_id mp None)) 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_modtype_substobjs env mexpr in (match mbids with | mbid::mbids -> let resolve = 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 subst (map_mbid mbid mp (Some resolve))) sub_alias - , mbids, msid, objs) + ((join + (join subst (map_mbid mbid mp (Some resolve))) + sub) + , mbids, msid, objs) | [] -> match mexpr with | MSEident _ -> error "Application of a non-functor" | _ -> error "Application of a functor with too few arguments") @@ -862,7 +866,7 @@ let rec get_module_substobjs env = function let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in (subst, mbid::mbids, msid, objs) | MSEapply (mexpr, MSEident mp) -> - let ftb,_ = Mod_typing.translate_struct_entry env mexpr in + let ftb,sub1 = Mod_typing.translate_struct_entry env mexpr in let farg_id, farg_b, fbody_b = Modops.destr_functor env (Modops.eval_struct env ftb) in let mp = Environ.scrape_alias mp env in @@ -872,10 +876,12 @@ let rec get_module_substobjs env = function (subst_key (map_msid msid mp) sub_alias) (map_msid msid mp) | _ -> sub_alias in - let sub_alias = join_alias sub_alias (map_mbid farg_id mp None) in - let sub_alias = update_subst_alias sub_alias - (map_mbid farg_id mp (None)) in - let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in + let sub3 = update_subst_alias sub_alias + (join_alias sub1 (map_mbid farg_id mp None)) 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 -> let resolve = @@ -884,7 +890,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_alias) + sub) , mbids, msid, objs) | [] -> match mexpr with | MSEident _ -> error "Application of a non-functor" -- cgit v1.2.3