(* node.ml *)


type exp =
(*  | Num of int *)
  | StrVar of string
  | NumVar of int
  | Lambda of string * exp
  | Apply of exp * exp

exception NoEval of exp

let global_env : (string * exp) list ref = ref []

let debug = true

let rec print_exp = function
(*  | Num(n) ->
    print_int n *)
  | StrVar(s) ->
    print_string s
  | NumVar(n) ->
    print_int n
  | Lambda(s,v) ->
    print_string "\\";
    if not (s = "") then begin
      print_string s;
      print_string "."
    end;
    print_exp v
  | Apply(e1,e2) ->
    print_string "(";
    print_exp e1;
    print_string " ";
    print_exp e2;
    print_string ")"

(* Changes an expression to De Bruijn notation *)
let rec bruijnize = function
  | StrVar(x) -> StrVar(x)
  | NumVar(x) -> NumVar(x)
  | Lambda(v,x) ->
    Lambda("",bruijnize (replace v x 0))
  | Apply(x,y) ->
    Apply(bruijnize x, bruijnize y)

(* Does a recursive replacement in a bruijn re-write *)
and replace var body depth =
  match body with
  | StrVar(x) ->
    if x = var then NumVar(depth)
    else StrVar(x)
  | NumVar(x) -> NumVar(x)
  | Lambda(s,x) -> Lambda(s,replace var x (depth + 1))
  | Apply(x,y) -> Apply(
      replace var x depth,
      replace var y depth)

let rec expand = function
  | StrVar(x) ->
    begin
      try
        let ex = List.assoc x !global_env in
        expand ex
      with Not_found ->
        if debug then (print_string "NotFound(e)\n");
        StrVar(x)
    end
  | NumVar(x) -> NumVar(x)
  | Lambda(s,x) -> Lambda(s,expand x)
  | Apply(x,y) -> Apply(expand x, expand y)

(* Evaluate a lambda expression *)
let rec eval = function
  | StrVar(x) -> expand (StrVar x)
  | NumVar(x) -> NumVar(x)
  | Lambda(s,x) -> Lambda(s,x)
  | Apply(x,y) ->
    if debug then begin
      print_string "Eval: ";
      print_exp (Apply(x,y));
      print_newline()
    end;
    (* If evaling the first element changes nothing, just
     * breduce. Otherwise breduce and eval *)
    let n = eval x in
    if n = x then breduce n y
    else eval (breduce n y)

(* Alpha reduce body with param at the given depth *)
and areduce body param depth =
  if debug then begin
    print_string "Alpha ";
    print_int depth;
    print_string ": ";
    print_exp param;
    print_string " -> ";
    print_exp body;
    print_newline()
  end;
  match body with
  | StrVar(x) -> body
  | NumVar(x) ->
    if x = depth then param else NumVar(x)
  | Lambda(s,x) -> Lambda(s,areduce x param (depth + 1))
  | Apply(x,y) -> Apply(
      areduce x param depth,
      areduce y param depth)


and breduce body param =
  if debug then begin
    print_string "Beta: ";
    print_exp body;
    print_char ' ';
    print_exp param;
    print_newline()
  end;
  match body with
  | StrVar(x) -> breduce (expand body) param
  | NumVar(x) -> Apply(body,param)
  | Lambda(_,x) -> areduce x param 0
  | Apply(x,y) -> Apply(eval body,eval param)

let rec print_env = function
  | [] -> ()
  | (s,v)::e ->
    print_string "let ";
    print_string s;
    print_string " = ";
    print_exp v;
    print_newline();
    print_env e