(***********************************************

  lambda.ml - a fun example of lambda calculus
  This uses de Bruijn indecies for parameters.
  
***********************************************)

open Node

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

let symtbl:(string * exp) list = [
  "ident",Lambda("",NumVar(0));
  "true",Lambda("",Lambda("",NumVar(1)));
  "false",Lambda("",Lambda("",NumVar(0)));
  "if",Lambda("",Lambda("",Lambda("",Apply(Apply(NumVar(2),NumVar(1)),NumVar(0)))));
  ]

(*
let rec print_exp = function
  | StrVar(s) ->
   (* print_string "\""; *)
    print_string s
   (* print_string "\"" *)
  | NumVar(x) ->
    print_char 'V';
    print_int x
  | Lambda("",x) ->
    print_char 'L';
    print_exp x
  | Apply(x,y) ->
    print_char '(';
    print_exp x;
    print_char ' ';
    print_exp y;
    print_char ')'
*)

(*let rec pp_exp ex =
  let open_paren prec op_prec =
    if prec > op_prec then print_string "(" in
  let close_paren prec op_prec =
    if prec > op_prec then print_string ")" in
  let rec print prec ex =
    match ex with
    | StrVar(s) -> print_string s
    | NumVar(v) -> print_int v
    | Lambda(_,e) ->
      open_paren prec 1;
      print_string "\\";
      print 1 e;
      close_paren prec 1
    | Apply(e1,e2) ->
      (*open_paren prec 0;*)
      print_string "(";
      print 0 e1;
      print_string " ";
      print 0 e2;
      (*close_paren prec 0*)
      print_string ")"
  in
  print 0 ex *)


let rec eval = function
  | StrVar(x) ->
    begin
      try
        let ex = List.assoc x symtbl in
        eval ex
      with Not_found -> StrVar(x)
    end
  | NumVar(x) -> NumVar(x)
  | Lambda(_,x) -> Lambda("",x)
  | Apply(x,y) ->
    print_string "Eval: ";
    print_exp (Apply(x,y));
    print_newline();
    eval (breduce x y)

and areduce body param depth =
  print_string "Alpha ";
  print_int depth;
  print_string ": ";
  print_exp param;
  print_string " -> ";
  print_exp body;
  print_newline();
  match body with
  | StrVar(x) ->
    begin
      try
        let ex = List.assoc x symtbl in
        areduce ex param depth
      with Not_found -> StrVar(x)
    end
  | NumVar(x) ->
    if x = depth then param else NumVar(x)
  | Lambda(_,x) -> Lambda("",areduce x param (depth + 1))
  | Apply(x,y) -> Apply(
      areduce x param depth,
      areduce y param depth)

and breduce body param =
  print_string "Beta: ";
  print_exp body;
  print_char ' ';
  print_exp param;
  print_newline(); 
  match body with
  | StrVar(x) ->
    begin
      try
        let ex = List.assoc x symtbl in
        breduce ex param
      with Not_found -> StrVar(x)
    end
  | NumVar(x) -> Apply(body,param)
  | Lambda(_,x) -> areduce x param 0
  | Apply(x,y) -> Apply(eval body,eval param)

  

let exp_ident = Lambda("",NumVar(0))

let exp_true  = Lambda("",Lambda("",NumVar(1)))

let exp_false = Lambda("",Lambda("",NumVar(0)))

let exp_if    = Lambda("",Lambda("",Lambda("",Apply(Apply(NumVar(2),NumVar(1)),NumVar(0)))))

let exp_pair = Lambda("",Lambda("",Lambda("",Apply(Apply(NumVar(0),NumVar(2)),NumVar(1)))))

let exp_fst = Lambda("",Apply(NumVar(0),exp_true))

let exp_snd = Lambda("",Apply(NumVar(0),exp_false))

let exp_zero = Apply(Apply(exp_pair,exp_true),exp_true)

let exp_iszero = Lambda("",Apply(exp_fst,NumVar(0)))

let exp_succ = Lambda("",Apply(Apply(exp_pair,exp_false),NumVar(0)))

let exp_pred = Lambda("",Apply(exp_snd,NumVar(0)))

let exp_one = Apply(exp_succ,exp_zero)

let exp_two = Apply(exp_succ,exp_one)

let exp_fix =
  Lambda("",
    Apply(
      Lambda("",
        Apply(
          NumVar(1),
          Apply(NumVar(0),NumVar(0))
        )
      ),
      Lambda("",
        Apply(
          NumVar(1),
          Apply(NumVar(0),NumVar(0))
        )
      )
    )
  )

let test = Apply(Apply(Apply(StrVar("if"),StrVar("true")),StrVar("Yep")),StrVar("Nope"))

let main () =
  print_string "LAMBDA FUN\n\n";
  print_string "Evaluating: ";
  print_exp test;
  print_newline();
  print_exp (eval(test));
  print_newline()

let _ = main ()


(* End of lambda.ml *)