| V of int
| A of t * t
| L of t
+ | B
let rec print ?(l=[]) =
function
| L t ->
let name = string_of_var (List.length l) in
"λ" ^ name ^ "." ^ print ~l:(name::l) t
+ | B -> "B"
let lift m =
let rec aux l =
| V n -> V (if n < l then n else n+m)
| A (t1,t2) -> A (aux l t1, aux l t2)
| L t -> L (aux (l+1) t)
+ | B -> B
in
aux 0
(try
lift l (cache_unwind (List.nth e (n - l)))
with Failure _ -> V (n - l))
- | L t -> L (aux (l+1) t) in
+ | L t -> L (aux (l+1) t)
+ | B -> B in
let t = aux 0 t in
List.fold_left (fun f a -> A(f,a)) t s
in
let mwhd m =
let rec aux =
function
- (e,A(t1,t2),s) ->
+ | (e,A(t1,t2),s) ->
let t2' = aux (e,t2,[]) in
- aux (e,t1,t2'::s)
+ let (_,t,_) = t2' in
+ if t = B
+ then t2'
+ else aux (e,t1,t2'::s)
| (e,L t,x::s) -> aux (x::e,t,s)
| (e,V n,s) as m ->
(try
let e,t,s' = List.nth e n in
aux (e,t,s'@s)
with Failure _ -> m)
+ | (e, B, _) -> (e, B, [])
| (_,L _,[]) as m -> m
in
unwind (aux m)