Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 549 insertions, 316 deletions

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 9a76922b..f85cfaaf 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -6,97 +6,299 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: mod_subst.ml 11924 2009-02-13 13:51:54Z soubiran $ *)
+(* $Id$ *)
 
 open Pp
 open Util
 open Names
 open Term
 
-(* WARNING: not every constant in the associative list domain used to exist
-   in the environment. This allows a simple implementation of the join
-   operation. However, iterating over the associative list becomes a non-sense
-*)
-type resolver = (constant * constr option) list
 
-let make_resolver resolve = resolve
+type delta_hint =
+    Inline of constr option
+  | Equiv of kernel_name
+  | Prefix_equiv of module_path
 
-let apply_opt_resolver resolve kn =
- match resolve with
-    None -> None
-  | Some resolve ->
-     try List.assoc kn resolve with Not_found -> None
+type delta_key = 
+    KN of kernel_name
+  | MP of module_path
+
+module Deltamap =  Map.Make(struct 
+			      type t = delta_key
+			      let compare = Pervasives.compare
+			    end)
+
+type delta_resolver = delta_hint Deltamap.t
+
+let empty_delta_resolver = Deltamap.empty
 
 type substitution_domain = 
-    MSI of mod_self_id 
   | MBI of mod_bound_id
   | MPI of module_path
 
 let string_of_subst_domain = function
-   MSI msid -> debug_string_of_msid msid
  | MBI mbid -> debug_string_of_mbid mbid
  | MPI mp -> string_of_mp mp
 
-module Umap = Map.Make(struct 
+module Umap = Map.Make(struct
 			 type t = substitution_domain
 			 let compare = Pervasives.compare
 		       end)
 
-type substitution = (module_path * resolver option) Umap.t
-
+type substitution = (module_path * delta_resolver) Umap.t
+    
 let empty_subst = Umap.empty
 
-let add_msid msid mp =
-  Umap.add (MSI msid) (mp,None)
+
+let string_of_subst_domain = function
+  | MBI mbid -> debug_string_of_mbid mbid
+  | MPI mp -> string_of_mp mp
+      
 let add_mbid mbid mp resolve =
   Umap.add (MBI mbid) (mp,resolve)
-let add_mp mp1 mp2  =
-  Umap.add (MPI mp1) (mp2,None)
+let add_mp mp1 mp2 resolve =
+  Umap.add (MPI mp1) (mp2,resolve)
 
 
-let map_msid msid mp = add_msid msid mp empty_subst
 let map_mbid mbid mp resolve = add_mbid mbid mp resolve empty_subst
-let map_mp mp1 mp2 = add_mp mp1 mp2 empty_subst
+let map_mp mp1 mp2 resolve = add_mp mp1 mp2 resolve empty_subst
 
+let add_inline_delta_resolver con =
+  Deltamap.add (KN(user_con con)) (Inline None)
+    
+let add_inline_constr_delta_resolver con cstr =
+  Deltamap.add (KN(user_con con)) (Inline (Some cstr))
+
+let add_constant_delta_resolver con =
+  Deltamap.add (KN(user_con con)) (Equiv (canonical_con con))
+
+let add_mind_delta_resolver mind =
+  Deltamap.add (KN(user_mind mind)) (Equiv (canonical_mind mind))
+
+let add_mp_delta_resolver mp1 mp2 = 
+  Deltamap.add (MP mp1) (Prefix_equiv mp2)
+
+let mp_in_delta mp = 
+  Deltamap.mem (MP mp) 
+
+let con_in_delta con resolver = 
+try 
+  match Deltamap.find (KN(user_con con)) resolver with
+  | Inline _  | Prefix_equiv _ -> false
+  | Equiv _ -> true
+with
+ Not_found -> false
+
+let mind_in_delta mind resolver = 
+try 
+  match Deltamap.find (KN(user_mind mind)) resolver with
+  | Inline _  | Prefix_equiv _ -> false
+  | Equiv _ -> true
+with
+ Not_found -> false
+
+let delta_of_mp resolve mp =
+  try 
+    match Deltamap.find (MP mp) resolve with
+      | Prefix_equiv mp1 -> mp1
+      | _ -> anomaly "mod_subst: bad association in delta_resolver"
+  with
+      Not_found -> mp
+	
+let delta_of_kn resolve kn =
+  try 
+    match Deltamap.find (KN kn) resolve with
+      | Equiv kn1 -> kn1
+      | Inline _ -> kn
+      | _ -> anomaly 
+	  "mod_subst: bad association in delta_resolver"
+  with
+      Not_found -> kn
+
+let remove_mp_delta_resolver resolver mp =
+    Deltamap.remove (MP mp) resolver
+
+exception Inline_kn
+
+let rec find_prefix resolve mp = 
+  let rec sub_mp = function
+    | MPdot(mp,l) as mp_sup -> 
+	(try 
+	   match Deltamap.find (MP mp_sup) resolve with
+	     | Prefix_equiv mp1 -> mp1
+	     | _ -> anomaly 
+		 "mod_subst: bad association in delta_resolver"
+	 with
+	     Not_found -> MPdot(sub_mp mp,l))
+    | p -> 
+	match Deltamap.find (MP p) resolve with
+	  | Prefix_equiv mp1 -> mp1
+	  | _ -> anomaly 
+		 "mod_subst: bad association in delta_resolver"	
+  in
+    try 
+      sub_mp mp
+    with
+	Not_found -> mp
+
+exception Change_equiv_to_inline of constr
+
+let solve_delta_kn resolve kn =
+  try 
+      match Deltamap.find (KN kn) resolve with
+	| Equiv kn1 -> kn1
+	| Inline (Some c) -> 
+	    raise (Change_equiv_to_inline c)
+	| Inline None -> raise Inline_kn
+	| _ -> anomaly 
+	    "mod_subst: bad association in delta_resolver"
+  with
+      Not_found | Inline_kn -> 
+	let mp,dir,l = repr_kn kn in
+	let new_mp = find_prefix resolve mp in
+	  if mp == new_mp then 
+	    kn
+	  else
+	    make_kn new_mp dir l
+	      
+
+let constant_of_delta resolve con =
+  let kn = user_con con in
+    try 
+      let new_kn = solve_delta_kn resolve kn in
+	if kn == new_kn then
+	  con
+	else
+	  constant_of_kn_equiv kn new_kn
+    with 
+	_ -> con 
+	
+let constant_of_delta2 resolve con =
+  let kn = canonical_con con in
+  let kn1 = user_con con in
+    try 
+      let new_kn = solve_delta_kn resolve kn in
+	if kn == new_kn then
+	  con
+	else
+	  constant_of_kn_equiv kn1 new_kn
+    with 
+	_ -> con
+
+let mind_of_delta resolve mind =
+  let kn = user_mind mind in
+    try
+      let new_kn = solve_delta_kn resolve kn in
+	if kn == new_kn then
+	  mind
+	else
+	  mind_of_kn_equiv kn new_kn
+    with 
+	_ -> mind 
+
+let mind_of_delta2 resolve mind =
+  let kn = canonical_mind mind in
+  let kn1 = user_mind mind in
+    try
+      let new_kn = solve_delta_kn resolve kn in
+	if kn == new_kn then
+	  mind
+	else
+	  mind_of_kn_equiv kn1 new_kn
+    with 
+	_ -> mind
+	  
+
+let inline_of_delta resolver = 
+  let extract key hint l =
+    match key,hint with 
+      |KN kn, Inline _ -> kn::l
+      | _,_ -> l
+  in
+    Deltamap.fold extract resolver []
+
+exception Not_inline
+  
+let constant_of_delta_with_inline resolve con =
+  let kn1,kn2 = canonical_con con,user_con con in
+    try
+      match Deltamap.find (KN kn2) resolve with 
+	| Inline None -> None
+	| Inline (Some const) -> Some const
+	| _ -> raise Not_inline
+    with
+	Not_found | Not_inline -> 
+	  try match Deltamap.find (KN kn1) resolve with 
+	    | Inline None -> None
+	    | Inline (Some const) -> Some const
+	    | _ -> raise Not_inline
+	  with
+	      Not_found | Not_inline -> None
+
+let string_of_key = function
+      | KN kn -> string_of_kn kn
+      | MP mp -> string_of_mp mp
+
+let string_of_hint = function
+      | Inline _ -> "inline"
+      | Equiv kn -> string_of_kn kn
+      | Prefix_equiv mp -> string_of_mp mp
+
+let debug_string_of_delta resolve =
+  let to_string key hint s = 
+    s^", "^(string_of_key key)^"=>"^(string_of_hint hint)
+  in 
+    Deltamap.fold to_string resolve ""  
+      
 let list_contents sub = 
-  let one_pair uid (mp,_) l =
-    (string_of_subst_domain uid, string_of_mp mp)::l
+  let one_pair uid (mp,reso) l =
+    (string_of_subst_domain uid, string_of_mp mp,debug_string_of_delta reso)::l
   in
     Umap.fold one_pair sub []
-
-let debug_string_of_subst sub = 
-  let l = List.map (fun (s1,s2) -> s1^"|->"^s2) (list_contents sub) in
+      
+let debug_string_of_subst sub =
+  let l = List.map (fun (s1,s2,s3) -> s1^"|->"^s2^"["^s3^"]")
+    (list_contents sub) in
     "{" ^ String.concat "; " l ^ "}"
+      
+let debug_pr_delta resolve = 
+  str (debug_string_of_delta resolve)
 
-let debug_pr_subst sub = 
+let debug_pr_subst sub =
   let l = list_contents sub in
-  let f (s1,s2) = hov 2 (str s1 ++ spc () ++ str "|-> " ++ str s2) 
+  let f (s1,s2,s3) = hov 2 (str s1 ++ spc () ++ str "|-> " ++ str s2 ++
+			      spc () ++ str "[" ++ str s3 ++ str "]") 
   in
-    str "{" ++ hov 2 (prlist_with_sep pr_coma f l) ++ str "}" 
-
-
+    str "{" ++ hov 2 (prlist_with_sep pr_comma f l) ++ str "}"
+      
+      
 let subst_mp0 sub mp = (* 's like subst *)
  let rec aux mp =
   match mp with
-    | MPself sid -> 
-        let mp',resolve = Umap.find (MSI sid) sub in
+    | MPfile sid -> 
+        let mp',resolve = Umap.find (MPI (MPfile sid)) sub in
          mp',resolve
     | MPbound bid ->
-        let mp',resolve = Umap.find (MBI bid) sub in
-          mp',resolve
+	begin
+	  try
+            let mp',resolve = Umap.find (MBI bid) sub in
+              mp',resolve
+	  with Not_found ->
+	    let mp',resolve = Umap.find (MPI mp) sub in
+              mp',resolve
+	end
     | MPdot (mp1,l) as mp2 ->
 	begin
-	  try  
+	  try
 	    let mp',resolve = Umap.find (MPI mp2) sub in
               mp',resolve
-	  with Not_found ->    
+	  with Not_found ->
 	    let mp1',resolve = aux mp1 in
 	      MPdot (mp1',l),resolve
 	end
-    | _ -> raise Not_found
  in
   try
-    Some (aux mp) 
+    Some (aux mp)
   with Not_found -> None
 
 let subst_mp sub mp =
@@ -104,39 +306,126 @@ let subst_mp sub mp =
     None -> mp
   | Some (mp',_) -> mp'
 
+let subst_kn_delta sub kn =
+ let mp,dir,l = repr_kn kn in
+  match subst_mp0 sub mp with
+     Some (mp',resolve) ->
+      solve_delta_kn resolve (make_kn mp' dir l)
+   | None -> kn
+
 
-let subst_kn0 sub kn =
+let subst_kn sub kn =
  let mp,dir,l = repr_kn kn in
   match subst_mp0 sub mp with
      Some (mp',_) ->
-      Some (make_kn mp' dir l)
-   | None -> None
+      (make_kn mp' dir l)
+   | None -> kn
 
-let subst_kn sub kn =
- match subst_kn0 sub kn with
-    None -> kn
-  | Some kn' -> kn'
+exception No_subst
+
+type sideconstantsubst =
+  | User
+  | Canonical
+
+let subst_ind sub mind =
+  let kn1,kn2 = user_mind mind,canonical_mind mind in
+  let mp1,dir,l = repr_kn kn1 in
+  let mp2,_,_ = repr_kn kn2 in
+    try 
+      let side,mind',resolve =   
+        match subst_mp0 sub mp1,subst_mp0 sub mp2 with
+	    None,None ->raise No_subst
+	  | Some (mp',resolve),None -> User,(make_mind_equiv mp' mp2 dir l), resolve
+	  | None, Some(mp',resolve)-> Canonical,(make_mind_equiv mp1 mp' dir l), resolve
+	  | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical,
+	      (make_mind_equiv mp1' mp2' dir l), resolve2 
+      in
+	match side with
+	  |User ->
+	     let mind = mind_of_delta resolve mind' in
+	       mind
+	  |Canonical ->
+	     let mind = mind_of_delta2 resolve mind' in
+	       mind
+    with 
+	No_subst -> mind
+
+let subst_mind0 sub mind =
+  let kn1,kn2 = user_mind mind,canonical_mind mind in
+  let mp1,dir,l = repr_kn kn1 in
+  let mp2,_,_ = repr_kn kn2 in
+    try 
+      let side,mind',resolve =   
+        match subst_mp0 sub mp1,subst_mp0 sub mp2 with
+	    None,None ->raise No_subst
+	  | Some (mp',resolve),None -> User,(make_mind_equiv mp' mp2 dir l), resolve
+	  | None, Some(mp',resolve)-> Canonical,(make_mind_equiv mp1 mp' dir l), resolve
+	  | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical,
+	      (make_mind_equiv mp1' mp2' dir l), resolve2
+      in
+	match side with
+	  |User ->
+	     let mind = mind_of_delta resolve mind' in
+	       Some mind
+	  |Canonical ->
+	     let mind = mind_of_delta2 resolve mind' in
+	       Some mind
+    with 
+	No_subst -> Some mind
 
 let subst_con sub con =
- let mp,dir,l = repr_con con in
-  match subst_mp0 sub mp with
-     None -> con,mkConst con
-   | Some (mp',resolve) ->
-      let con' = make_con mp' dir l in
-       match apply_opt_resolver resolve con with
-          None -> con',mkConst con'
-        | Some t -> con',t
+  let kn1,kn2 = user_con con,canonical_con con in
+  let mp1,dir,l = repr_kn kn1 in
+  let mp2,_,_ = repr_kn kn2 in
+    try 
+      let side,con',resolve =   
+        match subst_mp0 sub mp1,subst_mp0 sub mp2 with
+	    None,None ->raise No_subst
+	  | Some (mp',resolve),None -> User,(make_con_equiv mp' mp2 dir l), resolve
+	  | None, Some(mp',resolve)-> Canonical,(make_con_equiv mp1 mp' dir l), resolve
+	  | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical,
+	      (make_con_equiv mp1' mp2' dir l), resolve2 
+      in
+	match constant_of_delta_with_inline resolve con' with
+            None -> begin
+	      match side with
+	      |User ->
+	      let con = constant_of_delta resolve con' in
+		con,mkConst con
+	      |Canonical ->
+		  let con = constant_of_delta2 resolve con' in
+		con,mkConst con
+	    end
+	  | Some t -> con',t
+    with No_subst -> con , mkConst con 
+ 
 
 let subst_con0 sub con =
- let mp,dir,l = repr_con con in
-  match subst_mp0 sub mp with
-      None -> None
-    | Some (mp',resolve) ->
-	let con' = make_con mp' dir l in
-       match apply_opt_resolver resolve con with
-           None -> Some (mkConst con')
-         | Some t -> Some t
-
+  let kn1,kn2 = user_con con,canonical_con con in
+  let mp1,dir,l = repr_kn kn1 in
+  let mp2,_,_ = repr_kn kn2 in
+    try  
+      let side,con',resolve =   
+	match subst_mp0 sub mp1,subst_mp0 sub mp2 with
+	    None,None ->raise No_subst
+	  | Some (mp',resolve),None -> User,(make_con_equiv mp' mp2 dir l), resolve
+	  | None, Some(mp',resolve)-> Canonical,(make_con_equiv mp1 mp' dir l), resolve
+	  | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical,
+	      (make_con_equiv mp1' mp2' dir l), resolve2 
+      in
+	match constant_of_delta_with_inline resolve con' with
+	    None ->begin
+	      match side with
+	      |User ->
+	      let con = constant_of_delta resolve con' in
+		Some (mkConst con)
+	      |Canonical ->
+		  let con = constant_of_delta2 resolve con' in
+		Some (mkConst con)
+	    end
+	  | t ->  t
+    with No_subst -> Some (mkConst con) 
+		
 (* Here the semantics is completely unclear.
    What does "Hint Unfold t" means when "t" is a parameter?
    Does the user mean "Unfold X.t" or does she mean "Unfold y"
@@ -148,352 +437,296 @@ let subst_evaluable_reference subst = function
 
 
 
-let rec map_kn f f' c = 
+let rec map_kn f f' c =
   let func = map_kn f f' in
     match kind_of_term c with
-      | Const kn -> 
+      | Const kn ->
 	  (match f' kn with
 	       None -> c
 	     | Some const ->const)
-      | Ind (kn,i) -> 
+      | Ind (kn,i) ->
          (match f kn with
              None -> c
            | Some kn' ->
 	      mkInd (kn',i))
-      | Construct ((kn,i),j) -> 
+      | Construct ((kn,i),j) ->
          (match f kn with
              None -> c
            | Some kn' ->
 	       mkConstruct ((kn',i),j))
-      | Case (ci,p,ct,l) -> 
+      | Case (ci,p,ct,l) ->
 	  let ci_ind =
             let (kn,i) = ci.ci_ind in
               (match f kn with None -> ci.ci_ind | Some kn' -> kn',i ) in
 	  let p' = func p in
 	  let ct' = func ct in
 	  let l' = array_smartmap func l in
-	    if (ci.ci_ind==ci_ind && p'==p 
+	    if (ci.ci_ind==ci_ind && p'==p
 		&& l'==l && ct'==ct)then c
-	    else 
+	    else
 	      mkCase ({ci with ci_ind = ci_ind},
-		      p',ct', l')  
-      | Cast (ct,k,t) -> 
+		      p',ct', l')
+      | Cast (ct,k,t) ->
 	  let ct' = func ct in
 	  let t'= func t in
-	    if (t'==t && ct'==ct) then c 
+	    if (t'==t && ct'==ct) then c
 	    else mkCast (ct', k, t')
-      | Prod (na,t,ct) -> 
+      | Prod (na,t,ct) ->
 	  let ct' = func ct in
 	  let t'= func t in
-	    if (t'==t && ct'==ct) then c 
+	    if (t'==t && ct'==ct) then c
 	    else mkProd (na, t', ct')
-      | Lambda (na,t,ct) -> 
+      | Lambda (na,t,ct) ->
 	  let ct' = func ct in
 	  let t'= func t in
-	    if (t'==t && ct'==ct) then c 
+	    if (t'==t && ct'==ct) then c
 	    else mkLambda (na, t', ct')
-      | LetIn (na,b,t,ct) -> 
+      | LetIn (na,b,t,ct) ->
 	  let ct' = func ct in
 	  let t'= func t in
 	  let b'= func b in
-	    if (t'==t && ct'==ct && b==b') then c 
+	    if (t'==t && ct'==ct && b==b') then c
 	    else mkLetIn (na, b', t', ct')
-      | App (ct,l) -> 
+      | App (ct,l) ->
 	  let ct' = func ct in
 	  let l' = array_smartmap func l in
 	    if (ct'== ct && l'==l) then c
 	    else mkApp (ct',l')
-      | Evar (e,l) -> 
+      | Evar (e,l) ->
 	  let l' = array_smartmap func l in
 	    if (l'==l) then c
 	    else mkEvar (e,l')
       | Fix (ln,(lna,tl,bl)) ->
 	  let tl' = array_smartmap func tl in
 	  let bl' = array_smartmap func bl in
-	    if (bl == bl'&& tl == tl') then c  
+	    if (bl == bl'&& tl == tl') then c
 	    else mkFix (ln,(lna,tl',bl'))
       | CoFix(ln,(lna,tl,bl)) ->
 	  let tl' = array_smartmap func tl in
 	  let bl' = array_smartmap func bl in
-	    if (bl == bl'&& tl == tl') then c  
+	    if (bl == bl'&& tl == tl') then c
 	    else mkCoFix (ln,(lna,tl',bl'))
       | _ -> c
 
-let subst_mps sub = 
-  map_kn (subst_kn0 sub) (subst_con0 sub)
+let subst_mps sub =
+  map_kn (subst_mind0 sub) (subst_con0 sub)
 
 let rec replace_mp_in_mp mpfrom mpto mp =
   match mp with
     | _ when mp = mpfrom -> mpto
-    | MPdot (mp1,l) -> 
+    | MPdot (mp1,l) ->
 	let mp1' = replace_mp_in_mp mpfrom mpto mp1 in
 	  if mp1==mp1' then mp
 	  else MPdot (mp1',l)
     | _ -> mp
 
-let replace_mp_in_con mpfrom mpto kn =
- let mp,dir,l = repr_con kn in
+let replace_mp_in_kn mpfrom mpto kn =
+ let mp,dir,l = repr_kn kn in
   let mp'' = replace_mp_in_mp mpfrom mpto mp in
     if mp==mp'' then kn
-    else make_con mp'' dir l
+    else make_kn mp'' dir l
 
-exception BothSubstitutionsAreIdentitySubstitutions
-exception ChangeDomain of resolver
+let rec mp_in_mp mp mp1 =
+  match mp1 with
+    | _ when mp1 = mp -> true
+    | MPdot (mp2,l) -> mp_in_mp mp mp2
+    | _ -> false
+	
+let mp_in_key mp key = 
+  match key with
+    | MP mp1 -> 
+	mp_in_mp mp mp1
+    | KN kn -> 
+	let mp1,dir,l = repr_kn kn in
+	  mp_in_mp mp mp1
+	    
+let subset_prefixed_by mp resolver =
+  let prefixmp key hint resolv =
+    match hint with 
+      | Inline _ -> resolv
+      | _ ->
+	  if mp_in_key mp key then
+	    Deltamap.add key hint resolv
+	  else 
+	    resolv
+  in
+    Deltamap.fold prefixmp resolver empty_delta_resolver
 
-let join (subst1 : substitution) (subst2 : substitution) =
-  let apply_subst (sub : substitution) key (mp,resolve) =
-    let mp',resolve' =
-      match subst_mp0 sub mp with
-	  None -> mp, None
-	| Some (mp',resolve') -> mp',resolve' in
-    let resolve'' : resolver option =
-      try
-	let res =
-	  match resolve with
-	    |None -> begin
-		match resolve' with
-		    None -> raise BothSubstitutionsAreIdentitySubstitutions
-		  | Some res -> raise (ChangeDomain res) end
-	    | Some res -> res
-	in
-	  Some
-	    (List.map
-               (fun (kn,topt) ->
-		  kn,
-		  match topt with
-		      None ->
-			(match key with
-			     MSI msid ->
-			       let kn' = replace_mp_in_con (MPself msid) mp kn in
-				 apply_opt_resolver resolve' kn'
-			   | MBI mbid ->
-			       let kn' = replace_mp_in_con (MPbound mbid) mp kn in
-				 apply_opt_resolver resolve' kn'
-			   | MPI mp1 ->
-			       let kn' = replace_mp_in_con mp1 mp kn in
-				 apply_opt_resolver resolve' kn')
-		    | Some t -> Some (subst_mps sub t)) res)
-      with
-	  BothSubstitutionsAreIdentitySubstitutions -> None
-	| ChangeDomain res ->
-	    let rec changeDom = function
-	      | [] -> []
-	      | (kn,topt)::r ->
-		  let key' =
-		    match key with
-			MSI msid -> MPself msid
-                      | MBI mbid -> MPbound mbid 
-		      | MPI mp1 -> mp1 in
-		  let kn' = replace_mp_in_con mp key' kn in
-		    if kn==kn' then
-		      (*the key does not appear in kn, we remove it
-			from the resolver that we are building*)
-		      changeDom r
-		    else
-		      (kn',topt)::(changeDom r)
-	    in
-	      Some (changeDom res)
-    in
-      mp',resolve'' in
-  let subst = Umap.mapi (apply_subst subst2) subst1 in
-    (Umap.fold Umap.add subst2 subst)
-      
-let subst_key subst1 subst2 =
-  let replace_in_key key (mp,resolve) sub=
-    let newkey = 
-      match key with
-	| MPI mp1 -> 
-	    begin
-	      match subst_mp0 subst1 mp1 with
-		| None -> None
-		| Some (mp2,_) -> Some (MPI mp2)
-	    end
-	| _ -> None
-    in
-      match newkey with
-	| None -> Umap.add key (mp,resolve) sub
-	| Some mpi -> Umap.add mpi (mp,resolve) sub
+let subst_dom_delta_resolver subst resolver =
+  let apply_subst key hint resolver =
+    match key with
+	(MP mp) ->
+	  Deltamap.add (MP (subst_mp subst mp)) hint resolver
+      | (KN kn) ->
+	  Deltamap.add (KN (subst_kn subst kn)) hint resolver
   in
-    Umap.fold replace_in_key subst2 empty_subst
-
-let update_subst_alias subst1 subst2 =
- let subst_inv key (mp,resolve) sub =
-    let newmp = 
-      match key with 
-	| MBI msid -> MPbound msid
-	| MSI msid -> MPself msid
-	| MPI mp -> mp
-    in
-   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=
-    let newkey = 
-      match key with
-	| MPI mp1 -> 
-	    begin
-	      match subst_mp0 subst_mbi mp1 with
-		| None -> None
-		| Some (mp2,_) -> Some (MPI mp2)
-	    end
-	| _ -> None
-    in
-      match newkey with
-	| None -> Umap.add key (mp,resolve) sub
-	| Some mpi -> Umap.add mpi (mp,resolve) sub
+    Deltamap.fold apply_subst resolver empty_delta_resolver
+
+let subst_mp_delta sub mp key=
+ match subst_mp0 sub mp with
+    None -> empty_delta_resolver,mp
+  | Some (mp',resolve) -> 
+      let mp1 = find_prefix resolve mp' in
+      let resolve1 = subset_prefixed_by mp1 resolve in
+	match key with
+	    MP mpk ->
+	      (subst_dom_delta_resolver 
+		 (map_mp mp1 mpk empty_delta_resolver) resolve1),mp1
+	  | _ -> anomaly "Mod_subst: Bad association in resolver" 
+
+let subst_codom_delta_resolver subst resolver =
+  let apply_subst key hint resolver =
+    match hint with
+	Prefix_equiv mp ->
+	  let derived_resolve,mpnew = subst_mp_delta subst mp key in
+	    Deltamap.fold Deltamap.add derived_resolve
+	      (Deltamap.add key (Prefix_equiv mpnew) resolver)
+      | (Equiv kn) ->
+	  (try
+	     Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver
+	   with
+	       Change_equiv_to_inline c ->
+		 Deltamap.add key (Inline (Some c)) resolver)
+      | Inline None ->
+	  Deltamap.add key hint resolver
+      | Inline (Some t) ->
+	  Deltamap.add key (Inline (Some (subst_mps subst t))) resolver
   in
-    Umap.fold alias_subst subst1 empty_subst
-
-let update_subst subst1 subst2 =
- let subst_inv key (mp,resolve) l =
-    let newmp = 
-      match key with 
-	| MBI msid -> MPbound msid
-	| MSI msid -> MPself msid
-	| MPI mp -> mp
-    in
-   match mp with 
-     | MPbound mbid ->  ((MBI mbid),newmp,resolve)::l
-     | MPself msid ->  ((MSI msid),newmp,resolve)::l
-     | _ ->   ((MPI mp),newmp,resolve)::l
-  in 
-  let subst_mbi = Umap.fold subst_inv subst2 [] in
-  let alias_subst key (mp,resolve) sub=
-    let newsetkey = 
-      match key with
-	| MPI mp1 -> 
-	    let compute_set_newkey l (k,mp',resolve) = 
-	      let mp_from_key = match k with
-		  	| MBI msid -> MPbound msid
-			| MSI msid -> MPself msid
-			| MPI mp -> mp
-	      in
-	      let new_mp1 = replace_mp_in_mp mp_from_key mp' mp1 in
-		if new_mp1 == mp1 then l else (MPI new_mp1,resolve)::l
-	    in
-	    begin
-	      match List.fold_left compute_set_newkey [] subst_mbi with
-		| [] -> None
-		| l -> Some (l)
-	    end
-	| _ -> None
+    Deltamap.fold apply_subst resolver empty_delta_resolver
+
+let subst_dom_codom_delta_resolver subst resolver =
+  let apply_subst key hint resolver =
+    match key,hint with
+	(MP mp1),Prefix_equiv mp ->
+	  let key = MP (subst_mp subst mp1) in
+	  let derived_resolve,mpnew = subst_mp_delta subst mp key in
+	    Deltamap.fold Deltamap.add derived_resolve
+	      (Deltamap.add key (Prefix_equiv mpnew) resolver)
+      | (KN kn1),(Equiv kn) ->
+	  let key = KN (subst_kn subst kn1) in
+	    (try
+	       Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver
+	     with
+		 Change_equiv_to_inline c ->
+		   Deltamap.add key (Inline (Some c)) resolver)
+      | (KN kn),Inline None ->
+	  let key = KN (subst_kn subst kn) in
+	    Deltamap.add key hint resolver
+      | (KN kn),Inline (Some t) ->
+	  let key = KN (subst_kn subst kn) in
+	  Deltamap.add key (Inline (Some (subst_mps subst t))) resolver
+      | _,_ -> anomaly "Mod_subst: Bad association in resolver" 
+  in
+    Deltamap.fold apply_subst resolver empty_delta_resolver
+
+let update_delta_resolver resolver1 resolver2 =
+ let apply_res key hint res = 
+      try
+	if Deltamap.mem key resolver2 then
+	  res else
+	match hint with
+	    Prefix_equiv mp ->
+	      let new_hint =
+		Prefix_equiv (find_prefix resolver2 mp)
+	      in Deltamap.add key new_hint res
+	  | Equiv kn ->
+	      (try 
+		 let new_hint =
+		   Equiv (solve_delta_kn resolver2 kn)
+		 in Deltamap.add key new_hint res
+	       with
+		   Change_equiv_to_inline c ->
+		     Deltamap.add key (Inline (Some c)) res)
+	  | _ -> Deltamap.add key hint res
+      with not_found -> 
+	Deltamap.add key hint res
     in
-      match newsetkey with
-	| None -> sub
-	| Some l -> 
-	    List.fold_left (fun s (k,r) -> Umap.add k (mp,r) s)
-	      sub l
+      Deltamap.fold apply_res resolver1 empty_delta_resolver
+
+let add_delta_resolver resolver1 resolver2 =
+  if resolver1 == resolver2 then
+    resolver2
+  else if resolver2 = empty_delta_resolver then
+    resolver1
+  else
+    Deltamap.fold Deltamap.add (update_delta_resolver resolver1 resolver2)
+      resolver2
+
+let substition_prefixed_by k mp subst =
+  let prefixmp key (mp_to,reso) sub =
+    match key with 
+      | MPI mpk ->
+	  if mp_in_mp mp mpk && mp <> mpk then
+	    let new_key = replace_mp_in_mp mp k mpk in
+	      Umap.add (MPI new_key) (mp_to,reso) sub
+	  else 
+	    sub
+      |  _ -> sub
   in
-    Umap.fold alias_subst subst1 empty_subst
+    Umap.fold prefixmp subst empty_subst
 
-let join_alias (subst1 : substitution) (subst2 : substitution) =
-  let apply_subst (sub : substitution) key (mp,resolve) =
+let join (subst1 : substitution) (subst2 : substitution) =
+  let apply_subst key (mp,resolve) res =
     let mp',resolve' =
-      match subst_mp0 sub mp with
+      match subst_mp0 subst2 mp with
 	  None -> mp, None
-	| Some (mp',resolve') -> mp',resolve' in
-    let resolve'' : resolver option =
-      try
-	let res =
-	  match resolve with
-              Some res -> res
-	    | None ->
-		match resolve' with
-		    None -> raise BothSubstitutionsAreIdentitySubstitutions
-		  | Some res -> raise (ChangeDomain res)
-	in
-	  Some
-	    (List.map
-               (fun (kn,topt) ->
-		  kn,
-		  match topt with
-		      None ->
-			(match key with
-			     MSI msid ->
-			       let kn' = replace_mp_in_con (MPself msid) mp kn in
-				 apply_opt_resolver resolve' kn'
-			   | MBI mbid ->
-			       let kn' = replace_mp_in_con (MPbound mbid) mp kn in
-				 apply_opt_resolver resolve' kn'
-			   | MPI mp1 ->
-			       let kn' = replace_mp_in_con mp1 mp kn in
-				 apply_opt_resolver resolve' kn')
-		    | Some t -> Some (subst_mps sub t)) res)
-      with
-	  BothSubstitutionsAreIdentitySubstitutions -> None
-	| ChangeDomain res ->
-	    let rec changeDom = function
-	      | [] -> []
-	      | (kn,topt)::r ->
-		  let key' =
-		    match key with
-			MSI msid -> MPself msid
-                      | MBI mbid -> MPbound mbid 
-		      | MPI mp1 -> mp1 in
-		  let kn' = replace_mp_in_con mp key' kn in
-		    if kn==kn' then
-		      (*the key does not appear in kn, we remove it
-			from the resolver that we are building*)
-		      changeDom r
-		    else
-		      (kn',topt)::(changeDom r)
-	    in
-	      Some (changeDom res)
+	| Some (mp',resolve') ->  mp'
+	    ,Some resolve' in
+    let resolve'' : delta_resolver =
+      match resolve' with
+          Some res -> 
+	    add_delta_resolver 
+	      (subst_dom_codom_delta_resolver subst2 resolve) res
+	| None -> 
+	    subst_codom_delta_resolver subst2 resolve
     in
-      mp',resolve'' in
-  Umap.mapi (apply_subst subst2) subst1 
+    let k = match key with MBI mp -> MPbound mp | MPI mp -> mp in
+    let prefixed_subst = substition_prefixed_by k mp subst2 in
+      Umap.fold Umap.add prefixed_subst 
+	(Umap.add key (mp',resolve'') res) in
+  let subst = Umap.fold apply_subst subst1 empty_subst in
+    (Umap.fold Umap.add subst2 subst)   
+
 
-let remove_alias subst =
-  let rec remove key (mp,resolve) sub =
-    match key with
-	MPI _ -> sub
-      | _ -> Umap.add key (mp,resolve) sub
-  in
-    Umap.fold remove subst empty_subst
-      
 
 let rec occur_in_path uid path =
  match uid,path with
-  | MSI sid,MPself sid' -> sid = sid'
   | MBI bid,MPbound bid' -> bid = bid'
   | _,MPdot (mp1,_) -> occur_in_path uid mp1
   | _ -> false
-    
-let occur_uid uid sub = 
+
+let occur_uid uid sub =
   let check_one uid' (mp,_) =
     if uid = uid' || occur_in_path uid mp then raise Exit
   in
-    try 
+    try
       Umap.iter check_one sub;
       false
     with Exit -> true
 
-let occur_msid uid = occur_uid (MSI uid)
+
 let occur_mbid uid = occur_uid (MBI uid)
-    
+
 type 'a lazy_subst =
   | LSval of 'a
-  | LSlazy of substitution * 'a
-	
+  | LSlazy of substitution list * 'a
+
 type 'a substituted = 'a lazy_subst ref
-      
+
 let from_val a = ref (LSval a)
-    
-let force fsubst r = 
+
+let force fsubst r =
   match !r with
   | LSval a -> a
-  | LSlazy(s,a) -> 
-      let a' = fsubst s a in
+  | LSlazy(s,a) ->
+      let subst = List.fold_left join empty_subst (List.rev s) in
+      let a' = fsubst subst a in
       r := LSval a';
-      a' 
+      a'
 
 let subst_substituted s r =
   match !r with
-    | LSval a -> ref (LSlazy(s,a))
+    | LSval a -> ref (LSlazy([s],a))
     | LSlazy(s',a) ->
-	let s'' = join s' s in
-	  ref (LSlazy(s'',a))
-	    
+	  ref (LSlazy(s::s',a))
+