(*
Run with SMLNJ
*)

datatype Expr = 
         Name of string |
         Numb of int | 
         Bool of bool |
         Plus of Expr * Expr |
         Minus of Expr * Expr |
         Times of Expr * Expr |
         Fn of string * Expr |
         Apply of Expr * Expr |
         Let of string * Expr * Expr |
         LetRec of string * Expr * Expr |
         IfThenElse of Expr * Expr * Expr |
         EqTest of Expr * Expr |
         Or of Expr * Expr |
         And of Expr * Expr |
         Exp of Expr * Expr;

fun expr2string (Name n) = n
  | expr2string (Numb n) = Int.toString n
  | expr2string (Bool b) = Bool.toString b
  | expr2string (Plus (e1,e2)) = "("^(expr2string e1)^" + "^(expr2string e2)^")"
  | expr2string (Minus (e1,e2)) = "("^(expr2string e1)^" - "^(expr2string e2)^")"
  | expr2string (Times (e1,e2)) = "("^(expr2string e1)^" * "^(expr2string e2)^")"
  | expr2string (Fn (x,e)) = "(fn "^x^" . "^(expr2string e)^")"
  | expr2string (Apply (e1,e2)) = "("^(expr2string e1)^" "^(expr2string e2)^")"
  | expr2string (Let (x,e1,e2)) = "(let "^x^" be "^(expr2string e1)^" in "^(expr2string e2)^")"
  | expr2string (LetRec (x,e1,e2)) = "(letrec "^x^" be "^(expr2string e1)^" in "^(expr2string e2)^")"
  | expr2string (IfThenElse (e0,e1,e2)) = "(if "^(expr2string e0)^" then "^(expr2string e1)^" else "^(expr2string e2)^")"
  | expr2string (EqTest (e1,e2)) = "("^(expr2string e1)^" == "^(expr2string e2)^")"
  | expr2string (Or (e1,e2)) = "("^(expr2string e1)^" || "^(expr2string e2)^")"
  | expr2string (And (e1,e2)) = "("^(expr2string e1)^" && "^(expr2string e2)^")"
  | expr2string (Exp (e1,e2)) = "("^(expr2string e1)^" ^ "^(expr2string e2)^")";

fun appn f 0 = Fn ("x", Name "x")
  | appn f n = Fn ("x", Apply (f, Apply (appn f (n-1), Name "x")));

datatype Val = IntVal of int | BoolVal of bool | FnVal of string * Expr * Env
and Env = Empty | Defn of string * Val * Env;

exception Oddity of string;

fun lookup (n, Defn (s,v,r)) = if n = s then v else lookup (n,r)
  | lookup (n, Empty) = raise Oddity ("unbound name " ^ n);

fun eval (Name(s), r) = lookup(s,r)
  | eval (Numb(n), r) = IntVal(n)
  | eval (Bool(b), r) = BoolVal(b)
  | eval (Plus(e,e'), r) = (case (eval(e,r),eval(e',r)) of
                                (IntVal(i), IntVal(i')) => IntVal (i+i')
                              | _ => raise Oddity("plus of non-number"))
  | eval (Times(e,e'), r) = (case (eval(e,r),eval(e',r)) of
                                 (IntVal(i), IntVal(i')) => IntVal (i*i')
                               | _ => raise Oddity("times of non-number"))
  | eval (Minus(e,e'), r) = (case (eval(e,r),eval(e',r)) of
                                 (IntVal(i), IntVal(i')) => IntVal (i-i')
                               | _ => raise Oddity("plus of non-number"))
  | eval (Fn(s,e), r) = FnVal (s,e,r)
  | eval (Apply(e,e'), r) = (case eval(e,r) of
                                 FnVal(var_name, fun_body, fun_env) => 
                                 let val arg = eval(e',r)
                                 in
                                     eval (fun_body, Defn (var_name, arg, fun_env))
                                 end
                               | _ => raise Oddity("apply of non-function"))
  | eval (Let (v,e,e'), r) = eval(Apply(Fn(v,e'),e),r)
  | eval (LetRec(f,e,e'), r) = eval(Let
                                        ("f",
                                         Fn
                                             ("g",
                                              Let ("f",Fn ("x",Apply (Apply (Name "g",Name "g"),Name "x")),e)),
                                         Apply (Fn ("f",e'),Apply (Name "f",Name "f"))), r)
  | eval (IfThenElse(e1,e2,e3), r) = (case eval(e1,r) of
                                          BoolVal b => if b then eval(e2,r) else eval(e3,r)
                                        | _ => raise Oddity("if of non-bool"))
  | eval (EqTest (e1,e2), r) = (case (eval(e1,r),eval(e2,r)) of
                                    (IntVal n1, IntVal n2) => BoolVal (n1 = n2)
                                  | (BoolVal b1, BoolVal b2) => BoolVal (b1 = b2)
                                  | _ => raise Oddity("eqtest of non-bool/int"))
  | eval (Or (e1,e2), r) = (case (eval(e1,r),eval(e2,r)) of
                                (BoolVal b1, BoolVal b2) => BoolVal (b1 orelse b2)
                              | _ => raise Oddity("or of non-bool"))
  | eval (And (e1,e2), r) = (case (eval(e1,r),eval(e2,r)) of
                                 (BoolVal b1, BoolVal b2) => BoolVal (b1 andalso b2)
                               | _ => raise Oddity("and of non-bool")) 
  | eval (Exp (e,en), r) = case eval(en,r) of
                               IntVal n => (if (n < 0) then raise Oddity("exponent negative") else eval (appn e n, r))
                             | _ => raise Oddity("exponent not an integer");


(*
                       ===========================
                        RECURSIVE DESCENT PARSER
                       ===========================
*)

datatype Token = tPlus | tMinus | tTimes | tVal of int | tLBrak | tRBrak |
                 tString of string | tOr | tEq | tAnd | tLet | tLetRec | tBe | tIn | tEnd |
                 tIf | tThen | tElse | tNone | tFn | tDot | tExp;

type 'a Parser = (Token list -> (Token list * 'a) list);

fun return a = fn tl => [(tl,a)];

infixr >>=;
fun p >>= f = fn tl => List.concat (map (fn (tl',a) => (f a) tl') (p tl));

infixr pThen;
fun p1 pThen p2 = p1 >>= (fn a => (p2 >>= (fn b => return (a,b))));

fun pStar p tl = case (p tl) of
                     [] => [(tl,[])] |
                     (tl',s)::_ => ((pStar p) >>= (fn l' => return (s :: l'))) tl';

fun pPlus p tl = ((p pThen (pStar p)) >>= (fn (s,sl) => return (s::sl))) tl;

infixr pOr;
fun p1 pOr p2 = fn tl => (p1 tl) @ (p2 tl);

datatype ParseT = TTok of Token | TExpr of Expr;

fun parseTok t [] = []
  | parseTok t (t'::tl) = if (t' = t) then [(tl,TTok t)] else [];

fun parseSingle t [] = []
  | parseSingle t (t'::tl) = if (t' = t) then [(tl, t)] else [];

fun parseVal [] = []
  | parseVal (t'::tl) = case t' of tVal n => [(tl, TTok (tVal n))] | _ => [];

fun parseString [] = []
  | parseString (t'::tl) = case t' of tString s => [(tl, TTok (tString s))] | _ => [];

fun substring sv s =
    let val ln = String.size in
        String.substring (s,ln sv,ln s - ln sv)
    end;

fun getPattern (sv,t) s = if String.isPrefix sv s then SOME (substring sv s, t) else NONE;

fun getSomething what s = if what (String.sub (s,0)) then
                              case String.tokens (not o what) s of
                                  [] => NONE |
                                  (c::s') => SOME (substring c s, c)
                          else NONE;

fun getString s = case getSomething Char.isAlpha s of
                      SOME (s',vs) => SOME (s', tString vs) |
                      _ => NONE;

fun getNum s = case getSomething Char.isDigit s of
                   SOME (s',vs) => let val (SOME n) = Int.fromString vs in SOME (s', tVal n) end |
                   _ => NONE;

fun skipWhite s = case getSomething Char.isSpace s of
                      SOME (s',vs) => SOME (s', tNone) |
                      _ => NONE;

fun tokenize s = 
    let fun tokenize' s = 
            if String.size s = 0 then [] else
            let fun tknz [] = raise Oddity("Lexer failed")
                  | tknz (f::l) = case (f s) of
                                      SOME (s',t) => t :: (tokenize s') |
                                      NONE => tknz l in
                tknz 
                    ((map (fn (sv,t) => getPattern (sv, t))
                          [("letrec", tLetRec), ("let", tLet), ("if", tIf), ("then", tThen), ("else", tElse),
                           ("+", tPlus), ("-", tMinus), ("*", tTimes), ("(", tLBrak), 
                           (")", tRBrak), ("fn", tFn), (".", tDot), ("^", tExp),
                           ("or", tOr), ("and", tAnd), ("==", tEq), ("be", tBe), ("in", tIn), ("end", tEnd)]) @
                     [getString, getNum, skipWhite])
            end in
        (List.filter (fn t => not(t = tNone))) (tokenize' s)
    end;

(*
<E> -> ('let' | 'letrec') string 'be' <E> in <E> 'end'
<E> -> 'if' <E> 'then' <E> 'else' <E> 'end'
<E> -> 'fn' string '.' <E>
<E> -> <Z> '==' <E> | <Z>
<Z> -> <T> ('+' | '-' | 'or') <Z> | <T>
<T> -> <F> ('*' | 'and') <T> | <F>+ | <F> '^' <F>
<F> -> '(' <E> ')' | number | string
*)

fun pThenChain [] tl = (return []) tl
  | pThenChain (m::l) tl = ((m pThen (pThenChain l)) >>= (fn (r1,r2) => return (r1::r2))) tl;

fun parseE tl = (parseELet pOr parseEIf pOr parseEFn pOr parseEEq pOr parseZ) tl
and parseELet tl =
    ((pThenChain [(parseTok tLet) pOr (parseTok tLetRec),
                  parseString, parseTok tBe, parseE, parseTok tIn, parseE, parseTok tEnd])
         >>= (fn ((TTok tl)::(TTok (tString vn))::_::(TExpr e1)::_::(TExpr e2)::_) => 
                 return (TExpr ((case tl of tLet => Let | _ => LetRec) (vn,e1,e2))))) tl
and parseEIf tl = ((pThenChain [parseTok tIf, parseE, parseTok tThen, parseE, parseTok tElse, parseE, parseTok tEnd])
                       >>= (fn (_::(TExpr e1)::_::(TExpr e2)::_::(TExpr e3)::_) => 
                               return (TExpr (IfThenElse (e1,e2,e3))))) tl
and parseEFn tl = ((pThenChain [parseTok tFn, parseString, parseTok tDot, parseE])
                       >>= (fn (_::(TTok (tString name))::_::(TExpr e)::_) => 
                               return (TExpr (Fn (name,e))))) tl
and parseEEq tl = ((pThenChain [parseZ, parseTok tEq, parseE])
                       >>= (fn ((TExpr e1)::_::(TExpr e2)::_) => 
                               return (TExpr (EqTest (e1,e2))))) tl
and parseZ tl = (((pThenChain [parseT, (parseTok tPlus) pOr (parseTok tOr) pOr (parseTok tMinus), parseZ])
                     >>= (fn ((TExpr e1)::(TTok t)::(TExpr e2)::_) => 
                             return (TExpr ((case t of tPlus => Plus | tMinus => Minus | tOr => Or) (e1,e2))))) 
                     pOr parseT) tl
and parseT tl = (((pThenChain [parseF, (parseTok tTimes) pOr (parseTok tAnd), parseT])
                      >>= (fn ((TExpr e1)::(TTok t)::(TExpr e2)::_) => 
                              return (TExpr ((case t of tTimes => Times | tAnd => And) (e1,e2)))))
                     pOr parseG pOr ((pThenChain [parseF, (parseTok tExp), parseF]) >>= 
                                    (fn ((TExpr e)::_::(TExpr ee)::_) => return (TExpr (Exp(e, ee)))))) tl
and parseG tl = (let fun appl r [] = r |
                         appl r ((TExpr e)::l) = appl (Apply(r,e)) l in
                     (pPlus parseF) >>= (fn l => case l of 
                                                     [e] => return e | 
                                                     ((TExpr s)::l) => return (TExpr (appl s l)))
                 end) tl
and parseF tl = (((pThenChain [parseTok tLBrak, parseE, parseTok tRBrak])
                      >>= (fn (_::(TExpr e)::_) => return (TExpr e))) 
                     pOr (parseVal >>= (fn (TTok (tVal n)) => return (TExpr (Numb n)))) 
                     pOr (parseString >>= (fn (TTok (tString s)) => return (TExpr (Name s))))) tl;

fun fst (x,_) = x; 
fun snd (_,y) = y;
fun isEmpty [] = true | isEmpty _ = false;
fun parse s = hd (map (fn (_,TExpr e) => e) (List.filter (isEmpty o fst) (parseE (tokenize s))));


(*
                       ===========================
                                 EXAMPLES
                       ===========================
*)

fun Eval e = eval(e, Empty) handle (Oddity s) => (print ("EXCEPTION: "^s^"\n") ; IntVal 0);

(*example of use of closure, and the need for Env in FnVal*)
Eval (parse "let f be (let y be 3 in (fn x . x + y) end) in (let y be 0 in (f y) end) end");

(*example of letrec, calculating 5!*)
Eval (parse "letrec f be fn n . if (n == 0) then 1 else (f (n-1))*n end in (f 5) end");

(*example of letrec in terms of let as on p. 47 of the notes*)
Eval (parse "let f be fn g . fn n . if (n == 0) then 1 else ((g g) (n-1))*n end in ((f f) 5) end");

(*call by value Y*)
val Yv = parse "fn f . (fn g . (f (fn x . g g x))) (fn g . (f (fn x . g g x)))"

(*call by name Y*)
val Yn = parse "fn f . (fn g . (f (g g))) (fn g . (f (g g)))"

(*calculating 5! using call by value Y (since eval is using call by value in its evaluation of Apply, 
using call by name Y here instead does not terminate)*)

val c = "let Y be fn f . (fn g . (f (fn x . g g x))) (fn g . (f (fn x . g g x))) in " ^ 
        "    let f be Y (fn f . fn n . if (n == 0) then 1 else (f (n-1))*n end) in " ^
        "        f 5 " ^
        "    end " ^
        "end";

val ec = Eval (parse c);


(*
                       ===========================
                             CHURCH NUMERALS
                       ===========================
*)

fun nat2church n = parse ("fn f . fn x . (f^"^(Int.toString n)^") x");
fun church2nat e = Eval (Apply (Apply (e, parse ("fn n . n + 1")), Numb 0));

val Aplus = parse "fn x . fn y . fn p . fn q . x p (y p q)";
val Amult = parse "fn x . fn y . fn z . x (y z)";
val Aexp = parse "fn x . fn y . y x";
val Apred = parse "fn x . fn y . fn z . x (fn p . fn q . q (p y)) ((fn x . fn y . x) z) (fn x . x)";

fun tplus n m = church2nat (Apply (Apply (Aplus, nat2church n), nat2church m));
fun tmult n m = church2nat (Apply (Apply (Amult, nat2church n), nat2church m));
fun texp n m = church2nat (Apply (Apply (Aexp, nat2church n), nat2church m));
fun tpred n = church2nat (Apply (Apred, nat2church n));