1 files changed, 30 insertions, 5 deletions
diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index a11a0dc0..9fc3b11d 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -19,6 +19,8 @@ open Util
 (*********************)
 
 (* Explicit lifts and basic operations *)
+(* Invariant to preserve in this module: no lift contains two consecutive
+    [ELSHFT] nor two consecutive [ELLFT]. *)
 type lift =
   | ELID
   | ELSHFT of lift * int (* ELSHFT(l,n) == lift of n, then apply lift l *)
@@ -28,15 +30,15 @@ type lift =
 let el_id = ELID
 
 (* compose a relocation of magnitude n *)
-let rec el_shft_rec n = function
-  | ELSHFT(el,k) -> el_shft_rec (k+n) el
+let el_shft_rec n = function
+  | ELSHFT(el,k) -> ELSHFT(el,k+n)
   | el           -> ELSHFT(el,n)
 let el_shft n el = if Int.equal n 0 then el else el_shft_rec n el
 
 (* cross n binders *)
-let rec el_liftn_rec n = function
+let el_liftn_rec n = function
   | ELID        -> ELID
-  | ELLFT(k,el) -> el_liftn_rec (n+k) el
+  | ELLFT(k,el) -> ELLFT(n+k, el)
   | el          -> ELLFT(n, el)
 let el_liftn n el = if Int.equal n 0 then el else el_liftn_rec n el
 
@@ -132,13 +134,36 @@ let rec exp_rel lams k subs =
 
 let expand_rel k subs = exp_rel 0 k subs
 
+let rec subs_map f = function
+| ESID _ as s -> s
+| CONS (x, s) -> CONS (Array.map f x, subs_map f s)
+| SHIFT (n, s) -> SHIFT (n, subs_map f s)
+| LIFT (n, s) -> LIFT (n, subs_map f s)
+
+let rec lift_subst mk_cl s1 s2 = match s1 with
+| ELID -> subs_map (fun c -> mk_cl ELID c) s2
+| ELSHFT(s, k) -> subs_shft(k, lift_subst mk_cl s s2)
+| ELLFT (k, s) ->
+  match s2 with
+  | CONS(x,s') ->
+      CONS(CArray.Fun1.map mk_cl s1 x, lift_subst mk_cl s1 s')
+  | ESID n -> lift_subst mk_cl s (ESID (n + k))
+  | SHIFT(k',s') ->
+      if k<k'
+      then subs_shft(k, lift_subst mk_cl s (subs_shft(k'-k, s')))
+      else subs_shft(k', lift_subst mk_cl (el_liftn (k-k') s) s')
+  | LIFT(k',s') ->
+      if k<k'
+      then subs_liftn k (lift_subst mk_cl s (subs_liftn (k'-k) s'))
+      else subs_liftn k' (lift_subst mk_cl (el_liftn (k-k') s) s')
+
 let rec comp mk_cl s1 s2 =
   match (s1, s2) with
     | _, ESID _ -> s1
     | ESID _, _ -> s2
     | SHIFT(k,s), _ -> subs_shft(k, comp mk_cl s s2)
     | _, CONS(x,s') ->
-        CONS(CArray.Fun1.map (fun s t -> mk_cl(s,t)) s1 x, comp mk_cl s1 s')
+        CONS(Array.Fun1.map (fun s t -> mk_cl(s,t)) s1 x, comp mk_cl s1 s')
     | CONS(x,s), SHIFT(k,s') ->
         let lg = Array.length x in
         if k == lg then comp mk_cl s s'