type ('a,'b) sum = Inl of 'a | Inr of 'b;; type elift = Lid | Llift of int * elift | Lshift of elift * int ;; let lid = Lid;; let lliftn n el = match el with Lid -> Lid | Llift (k,e) -> Llift(k+n, e) | _ -> Llift(n,el) ;; let rec lshift_rec k el = match el with Lshift(e,n) -> Lshift(e,n+k) | _ -> Lshift(el,k) ;; let llift el = lliftn 1 el;; let lshift k el = if k=0 then el else lshift_rec k el;; let rec reloc_db acc el n = match el with Lid -> n+acc | Llift(k,e) -> if n >= k then reloc_db (acc+k) e (n-k) else n | Lshift(e,k) -> reloc_db acc e (n+k) ;; let reloc_rel el n = reloc_db 0 el n;; type 'a subs = Sid | Slift of int * 'a subs | Sshift of int * 'a subs | Scons of 'a subs * 'a ;; let subs_id = Sid;; let subs_lift = function Sid -> Sid | Slift(n,s) -> Slift(n+1,s) | s -> Slift(1,s) ;; let subs_shift_cons = function (0, s, t) -> Scons(s,t) | (k, Sshift(n,s1), t) -> Scons(Sshift(k+n, s1), t) | (k, s, t) -> Scons(Sshift(k, s), t);; let rec exp_rel lams s n = match s with Sid -> Inr (lams+n) | Scons(st,t) -> if n=0 then Inl (lams,t) else exp_rel lams st (n-1) | Slift(k,e) -> if n >= k then exp_rel (lams+k) e (n-k) else Inr (lams+n) | Sshift(k,e) -> exp_rel (lams+k) e n;; let expand_rel s n = exp_rel 0 s n;;