(**

This file contains a simple lambda calculus interpreter following the
definitions we used in class, on the first lambda calculus
lecture. You can uncomment the TESTS portions to see it run on some
examples. You can do `#use` on this file in the OCaml top-level to
call its functions directly, or just run `ocaml interp.ml` on the
command line (though doing so will not print anything except for tests
that explcitly call print).

**)

type id = string

type exp =
    Var of id
  | Lam of id * exp
  | App of exp * exp

(* generates a fresh variable name *)
let newvar =
  let x = ref 0 in
  fun () -> 
    let c = !x in
    incr x;
    "v"^(string_of_int c)

(* computes the free (non-bound) variables in e *)
let rec fvs e =
  match e with
      Var x -> [x]
    | Lam (x,e) -> List.filter (fun y -> x <> y) (fvs e)
    | App (e1,e2) -> (fvs e1) @ (fvs e2)
;;

(*
(* TESTS *)
fvs (Var "x") = ["x"];;
fvs (Lam ("x",Var "y")) = ["y"];;
fvs (Lam ("x",Var "x")) = [];;
fvs (App (Lam ("x", Var "z"), Var "y")) = ["z"; "y"];;
*)

(* substitution: subst e y m means 
  "substitute occurrences of variable y with m in the expression e" *)
let rec subst e y m =
  match e with
      Var x -> 
	if y = x then m (* replace x with m *)
	else e (* variables don't match: leave x alone *)
    | App (e1,e2) -> App (subst e1 y m, subst e2 y m)
    | Lam (x,e) ->
      if y = x then (* don't substitute under the variable binder *)
	Lam(x,e)
      else if not (List.mem x (fvs m)) then (* no need to alpha convert *)
	Lam (x, subst e y m)
      else (* need to alpha convert *)
	let z = newvar() in (* assumed to be "fresh" *)
	let e' = subst e x (Var z) in (* replace x with z in e *)
	Lam (z,subst e' y m) (* substitute for y in the adjusted term, e' *)

(*
(* TESTS *)
let m1 =  (App (Var "x", Var "y"));;
let m2 = (App (Lam ("z",Var "z"), Var "w"));;
let m3 = (App (Lam ("z",Var "x"), Var "w"));;
let m4 = (App (App (Lam ("z",Var "z"), Lam ("x", Var "x")), Var "w"))

let m1_zforx = subst m1 "x" (Var "z");;
let m1_m2fory = subst m1 "y" m2
let m2_ughforz = subst m2 "z" (Var "ugh")
let m3_zforx = subst m3 "x" (Var "z")
let m1_m3fory = subst m1 "y" m3
*)

(* beta reduction. *)
let rec reduce e =
  match e with
      App (Lam (x,e), e2) -> subst e x e2 (* direct beta rule *)
    | App (e1,e2) -> 
      let e1' = reduce e1 in (* try to reduce a term in the lhs *)
      if e1' != e1 then App(e1',e2)
      else App (e1,reduce e2) (* didn't work; try rhs *)
    | Lam (x,e) -> Lam (x, reduce e) (* reduce under the lambda (!) *)
    | _ -> e (* no opportunity to reduce *)

(*
(* TESTS *)
let m2red = reduce m2
let m3red = reduce m3
let m4red1 = reduce m4
let m4red2 = reduce m4red1
let m13sred = reduce m1_m3fory
*)

(* pretty printing *)

open Format;;

let ident = print_string;;
let kwd = print_string;;

let rec print_exp0 = function
  | Var s ->  ident s
  | lam -> open_hovbox 1; kwd "("; print_lambda lam; kwd ")"; close_box ()

and print_app = function
  | e -> open_hovbox 2; print_other_applications e; close_box ()

and print_other_applications f =
  match f with
  | App (f, arg) -> print_app f; print_space (); print_exp0 arg
  | f -> print_exp0 f

and print_lambda = function
  | Lam (s, lam) ->
      open_hovbox 1;
      kwd "\\"; ident s; kwd "."; print_space(); print_lambda lam;
      close_box()
  | e -> print_app e;;

(*
(* TESTS *)
print_lambda m1; print_newline ();;
print_lambda m2; print_newline ();;
*)