type expr =
  | Var of string           
  | Lam of string * expr    
  | App of expr * expr      

let rec free_vars = function
  | Var x -> [x]
  | Lam (x, e) -> List.filter (fun y -> y <> x) (free_vars e)
  | App (e1, e2) -> (free_vars e1) @ (free_vars e2)


let rec substitute e x s =
  match e with
  | Var y -> if y = x then s else e
  | Lam (y, body) ->
      if y = x then e 
      else if List.mem y (free_vars s) then
        let y' = y ^ "'" in
        let body' = substitute body y (Var y') in
        Lam (y', substitute body' x s)
      else
        Lam (y, substitute body x s)
  | App (e1, e2) -> App (substitute e1 x s, substitute e2 x s)

let rec beta_reduce = function
  | App (Lam (x, body), arg) -> substitute body x arg
  | App (e1, e2) ->
      let e1' = beta_reduce e1 in
      if e1' <> e1 then App (e1', e2)
      else App (e1, beta_reduce e2)
  | Lam (x, body) -> Lam (x, beta_reduce body)
  | Var x -> Var x

let rec normalize e =
  let e' = beta_reduce e in
  if e' = e then e
  else normalize e'

let rec to_string = function
  | Var x -> x
  | Lam (x, e) -> "λ" ^ x ^ "." ^ to_string e
  | App (e1, e2) ->
      "(" ^ to_string e1 ^ " " ^ to_string e2 ^ ")"

let () =
  let id = Lam ("x", Var "x") in                   (* λx.x *)
  let tru = Lam ("t", Lam ("f", Var "t")) in      (* λt.λf.t *)
  let fls = Lam ("t", Lam ("f", Var "f")) in      (* λt.λf.f *)
  let apply_id = App (id, Var "y") in             (* (λx.x y) *)

  let reduced = normalize apply_id in

  Printf.printf "Original: %s\n" (to_string apply_id);
  Printf.printf "Reduced:  %s\n" (to_string reduced)