let a_term = App (Abs ("x", App (Var "x", Var "x")),
App (Abs ("x", App (Var "x", Var "x")), Var "x"));;

let y_term = 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_term = Abs ("w", App (App (Var "x", Abs ("y", App (App (Var "x", Abs ("x", Var "x")), Var "y"))), Abs ("t", Var "y")));;

let redex_term = App (Abs ("x", Var "x"), Var "y");;

let print_list = iter (print_string);;

let fst (x, y) = x;;

let scd (x, y) = y;;

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) ^ ""
|Nil -> "NIL";;

let rec isin l a =
match l with
[] -> false
|l1::ls -> if l1 = a then true else isin ls a;;

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 intersect c d =
fold_left (fun x y -> if isin d y then y::x else x) [] c;;

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)
|Nil -> []
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]
|Nil -> [] )
in unique (cx' y z);;

let replace c d f =
let rec rep' a x b =
if (not (isin (fv a) x)) then a else (
match a with
Var z -> b
|App (p, q) -> App (rep' p x b, rep' q x b)
|Abs (y, r) -> Abs (y, rep' r x b)
|Nil -> Nil )
in rep' c d f;;

let redex_reduction c =
match c with
App (Abs (x, a), b) -> if ((intersect (cx a x) (fv b)) = []) then (replace a x b) else Nil
|_ -> Nil;;

let reduct_once z =
let rec red' t =
match t with
Var a -> (false, Var a)
|Nil -> (false, Nil)
|(App (Abs (x, a), b)) as c -> let (p, q) = (red' a, red' b) in
if (not (fst p)) && (not (fst q)) then (true, redex_reduction c) else
(if (fst p) then (true, App (Abs (x, scd p), b)) else (true, App (Abs (x, a), scd q)))
|(App (a, b)) as c -> let (p, q) = (red' a, red' b) in
if (not (fst p)) && (not (fst q)) then
(false, c) else (if (fst p) then (true, App (scd p, b)) else (true, App (a, scd q)))
|(Abs (x, b)) as c -> let q = red' b in if not (fst q) then (false, c) else (true, Abs (x, scd q))
in scd (red' z);;

print_string ("Original: " ^ (print_term (App (y_term, Var "g"))) ^ "\nReducted: ");;
print_string (print_term (reduct_once (App (y_term, Var "g"))));;