11 let rec print ?(l=[]) =
14 | A(t1,t2) -> "(" ^ print ~l t1 ^ " " ^ print ~l t2 ^ ")"
16 let name = string_of_var (List.length l) in
17 "λ" ^ name ^ "." ^ print ~l:(name::l) t
22 | V n -> V (if n < l then n else n+m)
23 | A (t1,t2) -> A (aux l t1, aux l t2)
24 | L t -> L (aux (l+1) t)
28 (* Reference implementation.
29 Reduction machine used below
30 let subst delift_by_one what with_what =
33 | A(t1,t2) -> A(aux l t1, aux l t2)
38 V (if delift_by_one && n >= l then n-1 else n)
39 | L t -> L (aux (l+1) t)
49 | L f -> whd (subst true 0 t2 f)
56 let unwind ?(tbl = Hashtbl.create 317) m =
57 let rec unwind (e,t,s) =
66 let s = List.map cache_unwind s in
69 | A(t1,t2) -> A(aux l t1, aux l t2)
70 | V n as x when n < l -> x
73 lift l (cache_unwind (List.nth e (n - l)))
74 with Failure _ -> V (n - l))
75 | L t -> L (aux (l+1) t) in
77 List.fold_left (fun f a -> A(f,a)) t s
85 let t2' = aux (e,t2,[]) in
87 | (e,L t,x::s) -> aux (x::e,t,s)
90 let e,t,s' = List.nth e n in
93 | (_,L _,[]) as m -> m
105 if n = 0 then L (L (A (V 1, L (V 0)))) else L (L (A (V 0, mk_n (n-1))))
107 let dummy = V (max_int / 2)
110 let bs = List.sort (fun (n1,_) (n2,_) -> compare n1 n2) bs in
116 A (A (t, L (lift (m+1) p)), L (aux (m+1) (V 0) tl))
118 A (A (t, dummy), L (aux (m+1) (V 0) l))