open List;;
type lambda = Var of string
| App of (lambda * lambda)
| Abs of (string * lambda);;
let a = App (Abs ("x", App (Var "x", Var "x")),
App (Abs ("x", App (Var "x", Var "x")), Var "x"));;
let y = Abs ("f", App (Abs ("x", App (Var ("f"), (App (Var ("x"), Var ("x"))))),
Abs ("x", App (Var ("f"), (App (Var ("x"), Var ("x")))))));;
let b = Abs ("w", App (App (Var "x", Abs ("y", App (App (Var "x", Abs ("x", Var "x")), Var "y"))), Abs ("t", Var "y")));;
let print_list = iter (print_string);;
let rec print_term t =
match t with
Var a -> a
|App (a, b) -> "(" ^ (print_term a) ^ " " ^ (print_term b) ^ ")"
|Abs (a, b) -> "\\" ^ a ^ "." ^ (print_term b);;
let isin l a = fold_left (fun x y -> (y = a) or x) false l;;
let unique z =
let rec unique' l acc =
match l with
[] -> acc
|l1::ls -> if isin acc l1 then (unique' ls acc) else (unique' ls (l1::acc))
in unique' z [];;
let fv z =
let rec fv' exp =
match exp with
Var a -> [a]
|App (a, b) -> (fv' a) @ (fv' b)
|Abs (a, b) -> filter (fun z -> (z <> a)) (fv' b)
in unique (fv' z);;
let cx y z =
let rec cx' a x =
if (not (isin (fv a) x)) then [] else (
match a with
Var b -> []
|App (b, c) -> (cx' b x) @ (cx' c x)
|Abs (b, c) -> (cx' c x) @ [b] )
in unique (cx' y z);;
print_list (cx y "x");;
print_string (print_term a);;