From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 1 Feb 2009 00:54:40 +0100 Subject: Imported Upstream version 8.2~rc2+dfsg --- kernel/mod_typing.ml | 115 ++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 81 insertions(+), 34 deletions(-) (limited to 'kernel/mod_typing.ml') diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 6840febd..4a9fb606 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: mod_typing.ml 11170 2008-06-25 08:31:04Z soubiran $ i*) +(*i $Id: mod_typing.ml 11514 2008-10-28 13:39:02Z soubiran $ i*) open Util open Names @@ -37,14 +37,46 @@ let rec list_fold_map2 f e = function let e'',t1',t2' = list_fold_map2 f e' t in e'',h1'::t1',h2'::t2' +let rec rebuild_mp mp l = + match l with + []-> mp + | i::r -> rebuild_mp (MPdot(mp,i)) r + +let type_of_struct env b meb = + let rec aux env = function + | SEBfunctor (mp,mtb,body) -> + let env = add_module (MPbound mp) (module_body_of_type mtb) env in + SEBfunctor(mp,mtb, aux env body) + | SEBident mp -> + strengthen env (lookup_modtype mp env).typ_expr mp + | SEBapply _ as mtb -> eval_struct env mtb + | str -> str + in + if b then + Some (aux env meb) + else + None + +let rec bounded_str_expr = function + | SEBfunctor (mp,mtb,body) -> bounded_str_expr body + | SEBident mp -> (check_bound_mp mp) + | SEBapply (f,a,_)->(bounded_str_expr f) + | _ -> false + +let return_opt_type mp env mtb = + if (check_bound_mp mp) then + Some (strengthen env mtb.typ_expr mp) + else + None + let rec check_with env mtb with_decl = match with_decl with | With_Definition (id,_) -> 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 true in - SEBwith(mtb,With_module_body(id,mp,cst)),sub + let cst,sub,typ_opt = check_with_aux_mod env mtb with_decl true in + SEBwith(mtb,With_module_body(id,mp,typ_opt,cst)),sub and check_with_aux_def env mtb with_decl = let msid,sig_b = match (eval_struct env mtb) with @@ -140,7 +172,7 @@ and check_with_aux_mod env mtb with_decl now = | With_Module ([id], mp) -> let old,alias = match spec with SFBmodule msb -> Some msb,None - | SFBalias (mp',cst) -> None,Some (mp',cst) + | SFBalias (mp',_,cst) -> None,Some (mp',cst) | _ -> error_not_a_module (string_of_label l) in let mtb' = lookup_modtype mp env' in @@ -164,35 +196,48 @@ and check_with_aux_mod env mtb with_decl now = in if now then let mp' = scrape_alias mp env' in - let up_subst = update_subst mtb'.typ_alias (map_mp (mp_rec [id]) mp') in - cst, (join (map_mp (mp_rec [id]) mp') up_subst) + let _,sub = Modops.update_subst env' (module_body_of_type mtb') mp' in + let up_subst = update_subst sub (map_mp (mp_rec [id]) mp') in + cst, (join (map_mp (mp_rec [id]) mp') up_subst),(return_opt_type mp env' mtb') else - cst,empty_subst + cst,empty_subst,(return_opt_type mp env' mtb') | With_Module (_::_,mp) -> - let old = match spec with - SFBmodule msb -> msb + let old,alias = match spec with + SFBmodule msb -> Some msb, None + | SFBalias (mpold,typ_opt,cst)->None, Some mpold | _ -> error_not_a_module (string_of_label l) in begin - match old.mod_expr with - None -> - let new_with_decl = match with_decl with - With_Definition (_,c) -> - With_Definition (idl,c) - | With_Module (_,c) -> With_Module (idl,c) in - let cst,_ = - check_with_aux_mod env' - (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 - 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) + if alias = None then + let old = Option.get old in + match old.mod_expr with + None -> + let new_with_decl = match with_decl with + With_Definition (_,c) -> + With_Definition (idl,c) + | With_Module (_,c) -> With_Module (idl,c) in + let cst,_,typ_opt = + check_with_aux_mod env' + (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 _,sub = Modops.update_subst env' (module_body_of_type mtb') mp' in + let up_subst = update_subst + sub (map_mp (mp_rec (List.rev (id::idl))) mp') in + cst, + (join (map_mp (mp_rec (List.rev (id::idl))) mp') up_subst), + typ_opt + else + cst,empty_subst,typ_opt + | Some msb -> + error_a_generative_module_expected l else - cst,empty_subst - | Some msb -> - error_a_generative_module_expected l + let mpold = Option.get alias in + let mpnew = rebuild_mp mpold (List.map label_of_id idl) in + check_modpath_equiv env' mpnew mp; + let mtb' = lookup_modtype mp env' in + Constraint.empty,empty_subst,(return_opt_type mp env' mtb') end | _ -> anomaly "Modtyping:incorrect use of with" with @@ -214,7 +259,9 @@ and translate_module env me = let meb,sub1 = translate_struct_entry env mexpr in let mod_typ,sub,cst = match me.mod_entry_type with - | None -> None,sub1,Constraint.empty + | None -> + (type_of_struct env (bounded_str_expr meb) meb) + ,sub1,Constraint.empty | Some mte -> let mtb2,sub2 = translate_struct_entry env mte in let cst = check_subtypes env @@ -304,7 +351,7 @@ let rec add_struct_expr_constraints env = function | SEBwith(meb,With_definition_body(_,cb))-> Environ.add_constraints cb.const_constraints (add_struct_expr_constraints env meb) - | SEBwith(meb,With_module_body(_,_,cst))-> + | SEBwith(meb,With_module_body(_,_,_,cst))-> Environ.add_constraints cst (add_struct_expr_constraints env meb) @@ -312,8 +359,8 @@ and add_struct_elem_constraints env = function | SFBconst cb -> Environ.add_constraints cb.const_constraints env | SFBmind mib -> Environ.add_constraints mib.mind_constraints env | SFBmodule mb -> add_module_constraints env mb - | SFBalias (mp,Some cst) -> Environ.add_constraints cst env - | SFBalias (mp,None) -> env + | SFBalias (mp,_,Some cst) -> Environ.add_constraints cst env + | SFBalias (mp,_,None) -> env | SFBmodtype mtb -> add_modtype_constraints env mtb and add_module_constraints env mb = @@ -352,15 +399,15 @@ let rec struct_expr_constraints cst = function | SEBwith(meb,With_definition_body(_,cb))-> struct_expr_constraints (Univ.Constraint.union cb.const_constraints cst) meb - | SEBwith(meb,With_module_body(_,_,cst1))-> + | SEBwith(meb,With_module_body(_,_,_,cst1))-> struct_expr_constraints (Univ.Constraint.union cst1 cst) meb and struct_elem_constraints cst = function | SFBconst cb -> cst | SFBmind mib -> cst | SFBmodule mb -> module_constraints cst mb - | SFBalias (mp,Some cst1) -> Univ.Constraint.union cst1 cst - | SFBalias (mp,None) -> cst + | SFBalias (mp,_,Some cst1) -> Univ.Constraint.union cst1 cst + | SFBalias (mp,_,None) -> cst | SFBmodtype mtb -> modtype_constraints cst mtb and module_constraints cst mb = -- cgit v1.2.3