12 let rec print ?(l=[]) =
15 | A(t1,t2) -> "(" ^ print ~l t1 ^ " " ^ print ~l t2 ^ ")"
17 let name = string_of_var (List.length l) in
18 "λ" ^ name ^ "." ^ print ~l:(name::l) t
24 | V n -> V (if n >= l then n+m else n)
25 | A (t1,t2) -> A (aux l t1, aux l t2)
26 | L t -> L (aux (l+1) t)
31 (* Reference implementation.
32 Reduction machine used below *)
33 let subst delift_by_one what with_what =
36 | A(t1,t2) -> A(aux l t1, aux l t2)
38 if (if what < 0 then n = what else n = what + l) then
41 V (if delift_by_one && n >= l then n-1 else n)
42 | L t -> L (aux (l+1) t)
53 | L f -> whd (subst true 0 t2 f)
60 let unwind ?(tbl = Hashtbl.create 317) m =
61 let rec unwind (e,t,s) =
70 let s = List.map cache_unwind s in
73 | A(t1,t2) -> A(aux l t1, aux l t2)
74 | V n as x when n < l -> x
77 lift l (cache_unwind (List.nth e (n - l)))
78 with Failure _ -> V n)
79 | L t -> L (aux (l+1) t)
82 List.fold_left (fun f a -> A(f,a)) t s
87 (* let rec print_machine (e,t,s) =
88 "[" ^ String.concat "," (List.map print_machine e) ^
90 String.concat "," (List.map print_machine s) ^ "]"
93 let omega = let delta = L(A(V 0, V 0)) in A(delta,delta)
95 let rec is_divergent =
97 t when t = omega -> true
98 | A(t,_) -> is_divergent t
99 | L(t) -> is_divergent t
105 (* mmm -> print_endline (print_machine mmm); match mmm with *)
106 m when is_divergent (unwind m) -> [], B, []
108 let t2' = aux g (e,t2,[]) in
112 else aux g (e,t1,t2'::s)
113 | (e,L t,x::s) -> aux g (x::e,t,s)
116 let e,t,s' = List.nth e n in
118 with Invalid_argument _ | Failure _ -> m
120 | (e, B, _) -> (e, B, [])
122 let t = subst true 0 (V g) t in
123 (* print_endline ("." ^ string_of_int g ^ " " ^ print_machine ((e,t,[]))); *)
124 let m' = aux (g-1) (e, t, []) in
125 let t' = unwind m' in
126 (* print_endline ("=" ^ print t');
127 print_endline ("==" ^ print (lift 1 t')); *)
128 let t' = subst false g (V 0) (lift 1 t') in
129 (* print_endline ("===" ^ print t'); *)
130 [], (if t' = B then t' else L t'), []
136 let omega should_explode =
138 then let f t = A(t,t) in f (L (f (V 0)))
142 let diverged = (=) B;;
144 (* Note: maps only variables <= freshno *)
145 let env_of_sigma freshno sigma =
152 e, lift (-n-1) (snd (List.find (fun (i,_) -> i = n) sigma)),[]
154 Not_found -> ([], V n, []) ) :: e
165 if n = 0 then L (L (A (V 1, L (V 0)))) else L (L (A (V 0, mk_n (n-1))))
167 let dummy = V (max_int / 2)
170 let bs = List.sort (fun (n1,_) (n2,_) -> compare n1 n2) bs in
176 A (A (t, L (lift (m+1) p)), L (aux (m+1) (V 0) tl))
178 A (A (t, dummy), L (aux (m+1) (V 0) l))