Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 412 insertions, 374 deletions

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 34d9e930..b49d34b3 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modops.ml 12234 2009-07-09 09:14:09Z soubiran $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Util
@@ -21,6 +21,7 @@ open Mod_subst
 (*i*)
 
 
+
 let error_existing_label l = 
   error ("The label "^string_of_label l^" is already declared.")
 
@@ -60,6 +61,9 @@ let error_not_a_modtype_loc loc s =
 let error_not_a_module_loc loc s = 
   user_err_loc (loc,"",str ("\""^s^"\" is not a module."))
 
+let error_not_a_module_or_modtype_loc loc s =
+  user_err_loc (loc,"",str ("\""^s^"\" is not a module or module type."))
+
 let error_not_a_module s = error_not_a_module_loc dummy_loc s
 
 let error_not_a_constant l = 
@@ -82,20 +86,12 @@ let error_local_context lo =
 	       (string_of_label l)^" is not empty.")
 
 
-let error_no_such_label_sub l l1 l2 =
-  error (l1^" is not a subtype of "^l2^".\nThe field "^(string_of_label l)^" is missing in "^l1^".")
-
+let error_no_such_label_sub l l1 =
+  error ("The field "^(string_of_label l)^" is missing in "^l1^".")
 
+let error_with_in_module _ = error "The syntax \"with\" is not allowed for modules."
 
-let rec list_split_assoc k rev_before = function
-  | [] -> raise Not_found
-  | (k',b)::after when k=k' -> rev_before,b,after
-  | h::tail -> list_split_assoc k (h::rev_before) tail
-
-let path_of_seb = function
-  | SEBident mp -> mp
-  | _ -> anomaly "Modops: evaluation failed."
-
+let error_application_to_module_type _ = error "Module application to a module type."
 
 let destr_functor env mtb =
   match mtb with
@@ -103,123 +99,126 @@ let destr_functor env mtb =
       	    (arg_id,arg_t,body_t)
   | _ -> error_not_a_functor mtb
 
-(* the constraints are not important here *)
+let is_functor = function
+ | SEBfunctor (arg_id,arg_t,body_t) -> true
+ | _ -> false
 
-let module_body_of_type mtb = 
-  { mod_type = Some mtb.typ_expr;
+let module_body_of_type mp mtb = 
+  { mod_mp = mp;
+    mod_type = mtb.typ_expr;
+    mod_type_alg = mtb.typ_expr_alg;
     mod_expr = None;
-    mod_constraints = Constraint.empty;
-    mod_alias = mtb.typ_alias;
+    mod_constraints = mtb.typ_constraints;
+    mod_delta = mtb.typ_delta;
     mod_retroknowledge = []}
 
-let module_type_of_module mp mb =
-  let mp1,expr = 
-      (match mb.mod_type with
-	| Some expr -> mp,expr
-	| None -> (match mb.mod_expr with
-		     | Some (SEBident mp') ->(Some mp'),(SEBident mp')
-		     | Some expr -> mp,expr
-		     | None -> 
-			 anomaly "Modops: empty expr and type")) in
-    {typ_expr = expr;
-      typ_alias = mb.mod_alias;
-      typ_strength = mp1
-    }
-
-let rec check_modpath_equiv env mp1 mp2 = 
+let check_modpath_equiv env mp1 mp2 = 
   if mp1=mp2 then () else
-  let mp1 = scrape_alias mp1 env in
-  let mp2 = scrape_alias mp2 env in
-    if mp1=mp2 then ()
-    else 
-      error_not_equal mp1 mp2
+    let mb1=lookup_module  mp1 env in
+    let mb2=lookup_module mp2 env in
+      if (delta_of_mp mb1.mod_delta mp1)=(delta_of_mp mb2.mod_delta mp2)
+      then ()
+      else error_not_equal mp1 mp2
 	
 let rec subst_with_body sub = function
-  | With_module_body(id,mp,typ_opt,cst) ->
-      With_module_body(id,subst_mp sub mp,Option.smartmap 
-			 (subst_struct_expr sub) typ_opt,cst)
+  | With_module_body(id,mp) ->
+      With_module_body(id,subst_mp sub mp)
   | With_definition_body(id,cb) ->
       With_definition_body( id,subst_const_body sub cb)
 
-and subst_modtype sub mtb =
-  let typ_expr' = subst_struct_expr sub mtb.typ_expr in
-  let sub_mtb = join_alias mtb.typ_alias sub in
-    if typ_expr'==mtb.typ_expr && sub_mtb==mtb.typ_alias then
-      mtb
+and subst_modtype sub do_delta mtb=
+  let mp = subst_mp sub mtb.typ_mp in
+  let sub = add_mp mtb.typ_mp mp empty_delta_resolver sub in
+  let typ_expr' = subst_struct_expr sub do_delta mtb.typ_expr in
+  let typ_alg' = 
+    Option.smartmap 
+      (subst_struct_expr sub (fun x y-> x)) mtb.typ_expr_alg in
+  let mtb_delta = do_delta mtb.typ_delta sub in
+    if typ_expr'==mtb.typ_expr && 
+      typ_alg'==mtb.typ_expr_alg && mp==mtb.typ_mp then
+	mtb
     else
-      { mtb with 
-	  typ_expr = typ_expr';
-	  typ_alias = sub_mtb}
+      {mtb with 
+	 typ_mp = mp;
+	 typ_expr = typ_expr';
+	 typ_expr_alg = typ_alg';
+	 typ_delta = mtb_delta}
 	
-and subst_structure sub sign = 
-  let subst_body  = function
+and subst_structure sub do_delta sign = 
+  let subst_body = function
       SFBconst cb -> 
 	SFBconst (subst_const_body sub cb)
     | SFBmind mib -> 
 	SFBmind (subst_mind sub mib)
     | SFBmodule mb -> 
-	SFBmodule (subst_module sub mb)
+	SFBmodule (subst_module sub do_delta mb)
     | SFBmodtype mtb -> 
-	SFBmodtype (subst_modtype sub mtb)
-    | SFBalias (mp,typ_opt,cst) ->
-	SFBalias (subst_mp sub mp,Option.smartmap 
-		    (subst_struct_expr sub) typ_opt,cst)
+	SFBmodtype (subst_modtype sub do_delta mtb)
   in
     List.map (fun (l,b) -> (l,subst_body b)) sign
 
-and subst_module  sub mb =
-  let mtb' = Option.smartmap (subst_struct_expr sub) mb.mod_type in
-  (* This is similar to the previous case. In this case we have
-     a module M in a signature that is knows to be equivalent to a module M'
-     (because the signature is "K with Module M := M'") and we are substituting
-     M' with some M''. *)
-  let me' = Option.smartmap (subst_struct_expr sub) mb.mod_expr in
-  let mb_alias = update_subst sub mb.mod_alias in
-   let mb_alias =  if mb_alias = empty_subst then
-     join_alias mb.mod_alias sub 
-   else 
-     join mb_alias (join_alias mb.mod_alias sub)
-   in
-     if mtb'==mb.mod_type && mb.mod_expr == me' 
-      && mb_alias == mb.mod_alias
+and subst_module sub do_delta mb =
+  let mp = subst_mp sub mb.mod_mp in
+  let sub = if is_functor mb.mod_type && not(mp=mb.mod_mp) then
+    add_mp mb.mod_mp mp
+      empty_delta_resolver sub else sub in 
+  let id_delta = (fun x y-> x) in
+  let mtb',me' = 
+    let mtb = subst_struct_expr sub do_delta mb.mod_type in 
+      match mb.mod_expr with
+	  None -> mtb,None
+	| Some me -> if me==mb.mod_type then
+	    mtb,Some mtb
+	  else mtb,Option.smartmap 
+	    (subst_struct_expr sub id_delta) mb.mod_expr
+  in
+  let typ_alg' = Option.smartmap 
+    (subst_struct_expr sub id_delta) mb.mod_type_alg in
+  let mb_delta = do_delta mb.mod_delta sub in
+    if mtb'==mb.mod_type && mb.mod_expr == me' 
+      && mb_delta == mb.mod_delta && mp == mb.mod_mp
     then mb else
-      { mod_expr = me';
-	mod_type=mtb'; 
-	mod_constraints=mb.mod_constraints;
-	mod_alias = mb_alias;
-	mod_retroknowledge=mb.mod_retroknowledge}
-
-
-and subst_struct_expr sub = function
-    | SEBident mp -> SEBident (subst_mp sub  mp)
-    | SEBfunctor (msid, mtb, meb') -> 
-	SEBfunctor(msid,subst_modtype sub mtb,subst_struct_expr sub meb')
-    | SEBstruct (msid,str)->
-	SEBstruct(msid, subst_structure sub str)
+      { mb with
+	  mod_mp = mp;
+	  mod_expr = me';
+	  mod_type_alg = typ_alg';
+	  mod_type=mtb'; 
+	  mod_delta = mb_delta}
+
+and subst_struct_expr sub do_delta = function
+    | SEBident mp -> SEBident (subst_mp sub mp)
+    | SEBfunctor (mbid, mtb, meb') -> 
+	SEBfunctor(mbid,subst_modtype sub do_delta mtb
+		     ,subst_struct_expr sub do_delta meb')
+    | SEBstruct (str)->
+	SEBstruct( subst_structure sub do_delta str)
     | SEBapply (meb1,meb2,cst)->
-	SEBapply(subst_struct_expr sub meb1,
-		 subst_struct_expr sub meb2,
+	SEBapply(subst_struct_expr sub do_delta meb1,
+		 subst_struct_expr sub do_delta meb2,
 		 cst)
     | SEBwith (meb,wdb)-> 
-	SEBwith(subst_struct_expr sub meb,
+	SEBwith(subst_struct_expr sub do_delta meb,
 		subst_with_body sub wdb)
- 
 
-let subst_signature_msid msid mp = 
-  subst_structure (map_msid msid mp)
+let subst_signature subst =
+  subst_structure subst 
+    (fun resolver subst-> subst_codom_delta_resolver subst resolver)
+
+let subst_struct_expr subst = 
+  subst_struct_expr subst
+    (fun resolver subst-> subst_codom_delta_resolver subst resolver)
 
 (* spiwack: here comes the function which takes care of importing 
    the retroknowledge declared in the library *)
 (* lclrk : retroknowledge_action list, rkaction : retroknowledge action *)
-let add_retroknowledge msid mp =
-  let subst = add_msid msid mp empty_subst in
-  let subst_and_perform rkaction env =
+let add_retroknowledge mp =
+  let perform rkaction env =
     match rkaction with
       | Retroknowledge.RKRegister (f, e) ->
 	  Environ.register env f 
 	  (match e with 
-	    | Const kn -> kind_of_term (subst_mps subst (mkConst kn))
-	    | Ind ind -> kind_of_term (subst_mps subst (mkInd ind))
+	    | Const kn -> kind_of_term (mkConst kn)
+	    | Ind ind -> kind_of_term (mkInd ind)
 	    | _ -> anomaly "Modops.add_retroknowledge: had to import an unsupported kind of term")
   in
   fun lclrk env ->
@@ -231,302 +230,341 @@ let add_retroknowledge msid mp =
      for things to go right (the pun is not intented). So we lose 
      tail recursivity, but the world will have exploded before any module
      imports 10 000 retroknowledge registration.*)
-  List.fold_right subst_and_perform lclrk env
-
-
+  List.fold_right perform lclrk env
 
-let strengthen_const env mp l cb = 
-  match cb.const_opaque, cb.const_body with
-  | false, Some _ -> cb
-  | true, Some _ 
-  | _, None -> 
-      let const = mkConst (make_con mp empty_dirpath l) in 
-      let const_subs = Some (Declarations.from_val const) in
-	{cb with 
-      	   const_body = const_subs;
-	   const_opaque = false;
-           const_body_code = Cemitcodes.from_val
-             (compile_constant_body env const_subs false false)
-	}
-
-let strengthen_mind env mp l mib = match mib.mind_equiv with
-  | Some _ -> mib
-  | None -> {mib with mind_equiv = Some (make_kn mp empty_dirpath l)}
-
-
-let rec eval_struct env = function 
-  | SEBident mp -> 
-      begin
-	let mtb =lookup_modtype mp env in
-	match mtb.typ_expr,mtb.typ_strength with
-	    mtb,None -> eval_struct env mtb
-	  | mtb,Some mp -> strengthen_mtb env mp (eval_struct env mtb)
-      end
-  | SEBapply (seb1,seb2,_) -> 
-      let svb1 = eval_struct env seb1 in
-      let farg_id, farg_b, fbody_b = destr_functor env svb1 in
-      let mp = path_of_seb seb2 in
-      let mp = scrape_alias mp env in
-      let sub_alias = (lookup_modtype mp env).typ_alias in
-      let sub_alias = match eval_struct env (SEBident mp) with
-	| SEBstruct (msid,sign) ->
-	    join_alias 
-	      (subst_key (map_msid msid mp) sub_alias)
-	      (map_msid msid mp)
-	| _ -> sub_alias in
-    let resolve = resolver_of_environment farg_id farg_b mp sub_alias env in  
-    let sub_alias1 = update_subst sub_alias 
-	(map_mbid farg_id mp (Some resolve)) in
-	eval_struct env (subst_struct_expr 
-			   (join sub_alias1 
-			      (map_mbid farg_id mp (Some resolve))) fbody_b)
-  | SEBwith (mtb,(With_definition_body _ as wdb)) ->
-      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
-      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) *)
-  | mtb -> mtb
-      
-and type_of_mb env mb =
-  match mb.mod_type,mb.mod_expr with
-      None,Some b -> eval_struct env b
-    | Some t, _ -> eval_struct env t
-    | _,_ -> anomaly 
-	"Modops:  empty type and empty expr" 
-	  
-and merge_with env mtb with_decl alias= 
-  let msid,sig_b = match (eval_struct env mtb) with 
-    | SEBstruct(msid,sig_b) -> msid,sig_b
-    | _ -> error_signature_expected mtb
-  in
-  let id,idl = match with_decl with 
-    | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_,_) -> id,idl
-    | With_definition_body ([],_) | With_module_body ([],_,_,_) -> assert false
-  in
-  let l = label_of_id id in
-    try
-      let rev_before,spec,after = list_split_assoc l [] sig_b in
-      let before = List.rev rev_before in
-      let rec mp_rec = function
-	| [] -> MPself msid
-	| i::r -> MPdot(mp_rec r,label_of_id i)
-      in 
-      let env' = add_signature (MPself msid) before env in
-      let new_spec,subst = match with_decl with
-        | With_definition_body ([],_)
-        | With_module_body ([],_,_,_) -> assert false
-	| With_definition_body ([id],c) -> 
-	    SFBconst c,None
-	| With_module_body ([id], mp,typ_opt,cst) ->
-	    let mp' = scrape_alias mp env' in
-	    let new_alias = update_subst alias (map_mp (mp_rec [id]) mp') in
-	      SFBalias (mp,typ_opt,Some cst),
-	    Some(join (map_mp (mp_rec [id]) mp') new_alias)
-	| With_definition_body (_::_,_) 
-        | With_module_body (_::_,_,_,_) -> 
-	    let old,aliasold = match spec with
-		SFBmodule msb -> Some msb, None
-	      | SFBalias (mpold,typ_opt,cst) ->None, Some (mpold,typ_opt,cst)
-	      | _ -> error_not_a_module (string_of_label l)
-	    in
-	      if aliasold = None then
-		let old = Option.get old in
-		let new_with_decl,subst1 = 
-		  match with_decl with
-                      With_definition_body (_,c) -> With_definition_body (idl,c),None
-		    | With_module_body (idc,mp,typ_opt,cst) -> 
-			let mp' = scrape_alias mp env' in
-			  With_module_body (idl,mp,typ_opt,cst),
-			Some(map_mp (mp_rec (List.rev idc)) mp') 
-		in
-		let subst = match subst1 with
-		  | None -> None
-		  | Some s -> Some (join s (update_subst 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 = begin 
-		      match subst_msb with
-			|None -> empty_subst
-			|Some s -> s
-		    end;
-		    mod_retroknowledge = old.mod_retroknowledge}
-		in
-		  (SFBmodule msb),subst
-	      else 
-		let mpold,typ_opt,cst =  Option.get aliasold in 
-		  SFBalias (mpold,typ_opt,cst),None
-      in
-	SEBstruct(msid,  before@(l,new_spec)::
-		    (Option.fold_right subst_structure subst after)),subst
-    with
-	Not_found -> error_no_such_label l
-
-and add_signature mp sign env = 
+let rec add_signature mp sign resolver env = 
   let add_one env (l,elem) =
     let kn = make_kn mp empty_dirpath l in
-    let con = make_con mp empty_dirpath l in
+    let con = constant_of_kn kn in
+    let mind = mind_of_kn kn in
       match elem with
-	| SFBconst cb -> Environ.add_constant con cb env
-	| SFBmind mib -> Environ.add_mind kn mib env
-	| SFBmodule mb -> 
-	    add_module (MPdot (mp,l)) mb env 
+	| SFBconst cb -> 
+	    let con =  constant_of_delta resolver con in
+	      Environ.add_constant con cb env
+	| SFBmind mib -> 
+	    let mind =  mind_of_delta resolver mind in
+	    Environ.add_mind mind mib env
+	| SFBmodule mb -> add_module mb env
 	      (* adds components as well *)
-	| SFBalias (mp1,_,cst) -> 
-	    Environ.register_alias (MPdot(mp,l)) mp1 env
-	| SFBmodtype mtb -> Environ.add_modtype (MPdot(mp,l)) 
-	    mtb env
+	| SFBmodtype mtb -> Environ.add_modtype mtb.typ_mp mtb env
   in
     List.fold_left add_one env sign
 
-and add_module mp mb env = 
+and add_module mb env = 
+  let mp = mb.mod_mp in
   let env = Environ.shallow_add_module mp mb env in
-  let env =
-    Environ.add_modtype mp (module_type_of_module (Some mp) mb) env
-  in
-  let mod_typ = type_of_mb env mb in
-    match mod_typ with
-      | SEBstruct (msid,sign) -> 
-	  add_retroknowledge msid mp (mb.mod_retroknowledge)
-	    (add_signature mp (subst_signature_msid msid mp sign) env)
+    match mb.mod_type with
+      | SEBstruct (sign) -> 
+	  add_retroknowledge mp mb.mod_retroknowledge 
+	    (add_signature mp sign mb.mod_delta env)
       | SEBfunctor _ -> env
       | _ -> anomaly "Modops:the evaluation of the structure failed "
-	  
-
 
-and  constants_of_specification env mp sign =
- let aux (env,res) (l,elem) =
-  match elem with
-   | SFBconst cb -> env,((make_con mp empty_dirpath l),cb)::res
-   | SFBmind _ -> env,res
-   | SFBmodule mb ->
-       let new_env =  add_module (MPdot (mp,l)) mb env in 
-       new_env,(constants_of_modtype env (MPdot (mp,l))
-		   (type_of_mb env mb)) @ res
-   | SFBalias (mp1,typ_opt,cst) ->
-       let new_env =  register_alias (MPdot (mp,l)) mp1 env in 
-       new_env,(constants_of_modtype env (MPdot (mp,l))
-		   (eval_struct env (SEBident mp1))) @ res
-   | SFBmodtype mtb -> 
-       (* module type dans un module type. 
-	  Il faut au moins mettre mtb dans l'environnement (avec le bon 
-	  kn pour pouvoir continuer aller deplier les modules utilisant ce 
-	  mtb
-	  ex: 
-	  Module Type T1. 
-	  Module Type T2.
-	     ....
-    	    End T2.
-	  .....
-            Declare Module M : T2.
-         End T2 
-	  si on ne rajoute pas T2 dans l'environement de typage 
-	  on va exploser au moment du Declare Module
-       *)
-       let new_env = Environ.add_modtype (MPdot(mp,l)) mtb env in 
-       new_env, (constants_of_modtype env (MPdot(mp,l)) mtb.typ_expr) @ res
- in
- snd (List.fold_left aux (env,[]) sign)
-
-and constants_of_modtype env mp modtype =
-  match (eval_struct env modtype) with
-      SEBstruct (msid,sign) ->
-	constants_of_specification env mp
-	  (subst_signature_msid msid mp sign)
-    | SEBfunctor _ -> []
-    | _ -> anomaly "Modops:the evaluation of the structure failed "
-
-(* returns a resolver for kn that maps mbid to mp. We only keep
-   constants that have the inline flag *)
-and  resolver_of_environment mbid modtype mp alias env =
- let constants = constants_of_modtype env (MPbound mbid) modtype.typ_expr in
- let constants = List.map (fun (l,cb) -> (l,subst_const_body alias cb)) constants in
- let rec make_resolve = function
-   | [] -> []
-   | (con,expecteddef)::r ->
-       let con' = replace_mp_in_con (MPbound mbid) mp con in
-       let con',_ = subst_con alias con' in
-  (*     let con' = replace_mp_in_con (MPbound mbid) mp con' in *)
-	 try
-	   if expecteddef.Declarations.const_inline then
-	     let constant = lookup_constant con' env in
-	     if (not constant.Declarations.const_opaque) then
-	       let constr = Option.map Declarations.force
-		 constant.Declarations.const_body in
-		 (con,constr)::(make_resolve r)
-	     else make_resolve r
-	   else make_resolve r
-	 with Not_found -> error_no_such_label (con_label con')
- in
- let resolve = make_resolve constants in
-   Mod_subst.make_resolver resolve
+let strengthen_const env mp_from l cb resolver = 
+  match cb.const_opaque, cb.const_body with
+  | false, Some _ -> cb
+  | true, Some _ 
+  | _, None ->
+      let con = make_con mp_from empty_dirpath l in
+      let con =  constant_of_delta resolver con in
+      let const = mkConst con in 
+      let const_subs = Some (Declarations.from_val const) in
+	{cb with 
+	   const_body = const_subs;
+	   const_opaque = false;
+	   const_body_code = Cemitcodes.from_val
+            (compile_constant_body env const_subs false false)
+	}
+	  
 
+let rec strengthen_mod env mp_from mp_to mb = 
+  if mp_in_delta mb.mod_mp mb.mod_delta then
+    mb 
+  else
+    match mb.mod_type with
+     | SEBstruct (sign) -> 
+	 let resolve_out,sign_out = 
+	   strengthen_sig env mp_from sign mp_to mb.mod_delta in
+	   { mb with
+	       mod_expr = Some (SEBident mp_to);
+	       mod_type = SEBstruct(sign_out);
+	       mod_type_alg = mb.mod_type_alg;
+	       mod_constraints = mb.mod_constraints;
+	       mod_delta = add_mp_delta_resolver mp_from mp_to 
+	       (add_delta_resolver mb.mod_delta resolve_out);
+	       mod_retroknowledge = mb.mod_retroknowledge}
+     | SEBfunctor _ -> mb
+     | _ -> anomaly "Modops:the evaluation of the structure failed "
+	 
+and strengthen_sig env mp_from sign mp_to resolver =
+  match sign with
+    | [] -> empty_delta_resolver,[]
+    | (l,SFBconst cb) :: rest ->
+	let item' = 
+	  l,SFBconst (strengthen_const env mp_from l cb resolver) in
+	let resolve_out,rest' =
+	  strengthen_sig env mp_from rest mp_to resolver in
+	  resolve_out,item'::rest'
+    | (_,SFBmind _ as item):: rest ->
+	let resolve_out,rest' = 
+	  strengthen_sig env mp_from rest mp_to resolver in
+	  resolve_out,item::rest'
+    | (l,SFBmodule mb) :: rest ->
+	let mp_from' = MPdot (mp_from,l) in
+	let mp_to' = MPdot(mp_to,l) in 
+	let mb_out = 
+	  strengthen_mod env mp_from' mp_to' mb in
+	let item' = l,SFBmodule (mb_out) in
+	let env' = add_module mb_out env in
+	let resolve_out,rest' = 
+	  strengthen_sig env' mp_from rest mp_to resolver in
+	  add_delta_resolver resolve_out mb.mod_delta,
+	item':: rest'
+    | (l,SFBmodtype mty as item) :: rest -> 
+	let env' = add_modtype 
+	  (MPdot(mp_from,l)) mty env
+	in
+	let resolve_out,rest' = 
+	  strengthen_sig env' mp_from rest mp_to resolver in
+	  resolve_out,item::rest'
     
-and strengthen_mtb env mp mtb =
-  let mtb1 = eval_struct env mtb in 
-  match  mtb1 with
-  | SEBfunctor _ -> mtb1
-  | SEBstruct (msid,sign) -> 
-      SEBstruct (msid,strengthen_sig env msid sign mp)
-  | _ -> anomaly "Modops:the evaluation of the structure failed "
-
-and strengthen_mod env mp mb = 
-  let mod_typ = type_of_mb env mb in
-    { mod_expr = mb.mod_expr;
-      mod_type = Some (strengthen_mtb env mp mod_typ);
-      mod_constraints = mb.mod_constraints;
-      mod_alias = mb.mod_alias;
-      mod_retroknowledge = mb.mod_retroknowledge}
-      
-and strengthen_sig env msid sign mp = match sign with
-  | [] -> []
-  | (l,SFBconst cb) :: rest ->
-      let item' = l,SFBconst (strengthen_const env mp l cb) in
-      let rest' = strengthen_sig env msid rest mp in
+let strengthen env mtb mp = 
+  if mp_in_delta mtb.typ_mp mtb.typ_delta then
+    (* in this case mtb has already been strengthened*)
+    mtb 
+  else
+    match mtb.typ_expr with
+      | SEBstruct (sign) -> 
+	  let resolve_out,sign_out =
+	    strengthen_sig env mtb.typ_mp sign mp mtb.typ_delta in
+	    {mtb with
+	       typ_expr = SEBstruct(sign_out);
+	       typ_delta = add_delta_resolver mtb.typ_delta
+		(add_mp_delta_resolver mtb.typ_mp mp resolve_out)}
+      | SEBfunctor _ -> mtb
+      | _ -> anomaly "Modops:the evaluation of the structure failed "
+	  
+let module_type_of_module env mp mb =
+  match mp with
+      Some mp ->
+	strengthen env {
+	  typ_mp = mp;
+	  typ_expr = mb.mod_type;
+	  typ_expr_alg = None;
+	  typ_constraints = mb.mod_constraints;
+	  typ_delta = mb.mod_delta} mp
+	  
+    | None ->
+	{typ_mp = mb.mod_mp;
+	 typ_expr = mb.mod_type;
+	 typ_expr_alg = None;
+	 typ_constraints = mb.mod_constraints;
+	 typ_delta = mb.mod_delta}
+
+let complete_inline_delta_resolver env mp mbid mtb delta =
+  let constants = inline_of_delta mtb.typ_delta in
+  let rec make_inline delta = function
+    | [] -> delta
+    | kn::r -> 
+	let kn = replace_mp_in_kn (MPbound mbid) mp kn in
+	let con = constant_of_kn kn in
+	let con' = constant_of_delta delta con in
+	  try
+	    let constant = lookup_constant con' env in
+	      if (not constant.Declarations.const_opaque) then
+		let constr = Option.map Declarations.force 
+		  constant.Declarations.const_body in
+		  if constr = None then 
+		    (make_inline delta r)
+		  else
+		    add_inline_constr_delta_resolver con (Option.get constr)
+		      (make_inline delta r)
+	      else
+		(make_inline delta r)
+	  with 
+	      Not_found -> error_no_such_label_sub (con_label con) 
+		(string_of_mp (con_modpath con))
+  in
+    make_inline delta constants
+
+let rec strengthen_and_subst_mod
+    mb subst env mp_from mp_to env resolver =
+     match mb.mod_type with
+	 SEBstruct(str) ->
+	   let mb_is_an_alias = mp_in_delta mb.mod_mp mb.mod_delta in
+	   if mb_is_an_alias then 
+	     subst_module subst 
+	       (fun resolver subst-> subst_dom_delta_resolver subst resolver) mb 
+	   else
+	     let resolver,new_sig = 
+	       strengthen_and_subst_struct str subst env
+		 mp_from mp_from mp_to false false mb.mod_delta 
+	     in
+	       {mb with 
+		  mod_mp = mp_to;
+		  mod_expr = Some (SEBident mp_from);
+		  mod_type = SEBstruct(new_sig);
+		  mod_delta = add_mp_delta_resolver mp_to mp_from resolver}
+       | SEBfunctor(arg_id,arg_b,body) ->
+	   let subst = add_mp mb.mod_mp mp_to empty_delta_resolver subst in
+	   subst_module subst 
+	     (fun resolver subst-> subst_dom_codom_delta_resolver subst resolver) mb  
+	
+       | _ -> anomaly "Modops:the evaluation of the structure failed "
+	   
+and strengthen_and_subst_struct 
+    str subst env mp_alias mp_from mp_to alias incl resolver =
+  match str with
+    | [] -> empty_delta_resolver,[]
+    | (l,SFBconst cb) :: rest ->
+	let item' = if alias then
+	  l,SFBconst (subst_const_body subst cb) 
+	else 
+	  l,SFBconst (strengthen_const env mp_from l 
+			(subst_const_body subst cb) resolver)
+	in
+	let con = make_con mp_from empty_dirpath l in
+	let resolve_out,rest' =
+	  strengthen_and_subst_struct rest subst env 
+	    mp_alias mp_from mp_to alias incl resolver in
+	  if incl then
+	    let old_name = constant_of_delta resolver con in
+	    (add_constant_delta_resolver
+	      (constant_of_kn_equiv (make_kn mp_to empty_dirpath l)
+		 (canonical_con old_name)) 
+	      resolve_out),
 	item'::rest'
-  | (l,SFBmind mib) :: rest ->
-      let item' = l,SFBmind (strengthen_mind env mp l mib) in
-      let rest' = strengthen_sig env msid rest mp in
+	  else
+	    resolve_out,item'::rest'
+    | (l,SFBmind mib) :: rest ->
+	let item' = l,SFBmind (subst_mind subst mib) in
+	let mind = make_mind mp_from empty_dirpath l in
+	let resolve_out,rest' =
+	  strengthen_and_subst_struct rest subst env 
+	    mp_alias mp_from mp_to alias incl resolver in
+	  if incl then
+	    let old_name =  mind_of_delta resolver mind in 
+	    (add_mind_delta_resolver
+	      (mind_of_kn_equiv (make_kn mp_to empty_dirpath l) (canonical_mind old_name)) resolve_out),
 	item'::rest'
-  | (l,SFBmodule mb) :: rest ->
-      let mp' = MPdot (mp,l) in
-	let item' = l,SFBmodule (strengthen_mod env mp' mb) in
-	let env' = add_module 
-	  (MPdot (MPself msid,l)) mb env in
-        let rest' = strengthen_sig env' msid rest mp in
+	  else
+	    resolve_out,item'::rest'
+    | (l,SFBmodule mb) :: rest ->
+	let mp_from' = MPdot (mp_from,l) in
+	let mp_to' = MPdot(mp_to,l) in
+	let mb_out = if alias then 
+	  subst_module subst 
+	  (fun resolver subst -> subst_dom_delta_resolver subst resolver) mb 
+	else
+	  strengthen_and_subst_mod
+	    mb subst env mp_from' mp_to' env resolver
+	in
+	let item' = l,SFBmodule (mb_out) in
+	let env' = add_module mb_out env in
+	let resolve_out,rest' = 
+	  strengthen_and_subst_struct rest subst env' 
+	    mp_alias mp_from mp_to alias incl resolver in
+	  if  is_functor mb_out.mod_type then (add_mp_delta_resolver 
+	     mp_to' mp_to' resolve_out),item':: rest' else
+	    add_delta_resolver resolve_out mb_out.mod_delta,
 	item':: rest'
-  | ((l,SFBalias (mp1,_,cst)) as item) :: rest ->
-      let env' = register_alias (MPdot(MPself msid,l)) mp1 env in
-      let rest' = strengthen_sig env' msid rest mp in
-	item::rest'
-  | (l,SFBmodtype mty as item) :: rest -> 
-      let env' = add_modtype 
-		   (MPdot((MPself msid),l)) 
-		   mty
-		   env
-      in
-      let rest' = strengthen_sig env' msid rest mp in
-	item::rest'
-
+    | (l,SFBmodtype mty) :: rest -> 
+	let mp_from' = MPdot (mp_from,l) in
+	let mp_to' = MPdot(mp_to,l) in
+	let subst' = add_mp mp_from' mp_to' empty_delta_resolver subst in
+	let mty = subst_modtype subst' 
+	  (fun resolver subst -> subst_dom_codom_delta_resolver subst' resolver) mty in
+	let env' = add_modtype mp_from' mty env	in
+	let resolve_out,rest' = strengthen_and_subst_struct rest subst env' 
+	    mp_alias mp_from mp_to alias incl resolver in
+	  (add_mp_delta_resolver 
+	     mp_to' mp_to' resolve_out),(l,SFBmodtype mty)::rest'
     
-let strengthen env mtb mp = strengthen_mtb env mp mtb
+let strengthen_and_subst_mb mb mp env include_b =
+    match mb.mod_type with
+	SEBstruct str ->
+	  let mb_is_an_alias = mp_in_delta mb.mod_mp mb.mod_delta in
+	    (*if mb is an alias then the strengthening is useless 
+	      (i.e. it is already done)*)
+	  let mp_alias = delta_of_mp mb.mod_delta mb.mod_mp in
+	  let subst_resolver = map_mp mb.mod_mp mp empty_delta_resolver in
+	  let new_resolver = 
+	    add_mp_delta_resolver mp mp_alias
+	      (subst_dom_delta_resolver subst_resolver mb.mod_delta) in	    
+	  let subst = map_mp mb.mod_mp mp new_resolver in 
+	  let resolver_out,new_sig = 
+	    strengthen_and_subst_struct str subst env
+	     mp_alias mb.mod_mp mp mb_is_an_alias include_b mb.mod_delta
+	  in
+	    {mb with 
+	       mod_mp = mp;
+	       mod_type = SEBstruct(new_sig);
+	       mod_expr = Some (SEBident mb.mod_mp);
+	       mod_delta = if include_b then resolver_out 
+	       else add_delta_resolver new_resolver resolver_out}
+      | SEBfunctor(arg_id,argb,body) ->
+	  let subst = map_mp mb.mod_mp mp empty_delta_resolver in
+	  subst_module subst 
+	    (fun resolver subst -> subst_dom_codom_delta_resolver subst resolver) mb 
+      | _ -> anomaly "Modops:the evaluation of the structure failed "
 
 
-let update_subst env mb mp =
-  match type_of_mb env mb with
-    | SEBstruct(msid,str) -> false, join_alias 
-	(subst_key (map_msid msid mp) mb.mod_alias)
-	(map_msid msid mp)
-    | _ -> true, mb.mod_alias
+let subst_modtype_and_resolver mtb mp env =
+  let subst = (map_mp mtb.typ_mp mp empty_delta_resolver) in
+  let new_delta = subst_dom_codom_delta_resolver subst mtb.typ_delta in 
+  let full_subst = (map_mp mtb.typ_mp mp new_delta) in
+    subst_modtype full_subst
+      (fun resolver subst -> subst_dom_codom_delta_resolver subst resolver) mtb
+
+let rec is_bounded_expr l = function
+  | SEBident mp -> List.mem mp l
+  | SEBapply (fexpr,mexpr,_) ->  
+      is_bounded_expr l mexpr || is_bounded_expr l fexpr
+  | _ -> false
+
+let rec clean_struct l = function
+  | (lab,SFBmodule mb) as field -> 
+      let clean_typ = clean_expr l mb.mod_type in 
+      let clean_impl = 
+	begin try
+	  if (is_bounded_expr l (Option.get mb.mod_expr)) then
+	    Some clean_typ
+	  else  Some (clean_expr l (Option.get mb.mod_expr))
+	with
+	    Option.IsNone -> None 
+	end in
+	  if clean_typ==mb.mod_type && clean_impl==mb.mod_expr then
+	    field 
+	  else 
+	    (lab,SFBmodule {mb with 
+			      mod_type=clean_typ;
+			      mod_expr=clean_impl})
+  | field -> field
+      
+and clean_expr l = function
+ | SEBfunctor (mbid,sigt,str) as s->
+     let str_clean = clean_expr l str in
+     let sig_clean = clean_expr l sigt.typ_expr in 
+       if  str_clean == str && sig_clean = sigt.typ_expr then
+	 s else SEBfunctor (mbid,{sigt with typ_expr=sig_clean},str_clean)
+  | SEBstruct str as s->
+      let str_clean = Util.list_smartmap (clean_struct l) str in 
+	if  str_clean == str then s else SEBstruct(str_clean)
+  |  str -> str 
+
+let rec collect_mbid l = function
+  | SEBfunctor (mbid,sigt,str) as s->
+      let str_clean = collect_mbid ((MPbound mbid)::l) str in 
+	if  str_clean == str then s else 
+      SEBfunctor (mbid,sigt,str_clean)
+  | SEBstruct str as s->
+      let str_clean = Util.list_smartmap (clean_struct l) str in 
+	if  str_clean == str then s else SEBstruct(str_clean)
+  |  _ -> anomaly "Modops:the evaluation of the structure failed "
+       
+       
+let clean_bounded_mod_expr = function
+  | SEBfunctor _ as str -> 
+      let str_clean = collect_mbid [] str in 
+	if  str_clean == str then str else str_clean
+  | str -> str