Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

1 files changed, 81 insertions, 34 deletions

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 =