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);;