open System;;

(* The smallest and purest programming language is the pure lambda
calculus. We can implement this language in abstract syntax in F#
using the lexp (lambda expression) datatype defined below.  A lambda
term can be a variable (represented by a string), a
"lambda-abstraction" lambda x.term, represented by Abs("x",term), or
an "application" (A B), represented in abstract syntax by App(A,B).

An expression of the form (let x=term1 in term2) is equivalent to
((lambda x.term2) term1), which in abstract syntax is represented by
App(Abs("x",term2),term1).

To make lambda terms a little more interesting we've also included integers
Val(3), for example, and closures, which pairs a list of bindings with a term.
For example, Closure([("x",term1);("y",term2)], App(Var("x"),Var("y")))
is actually equivalent to App(term1,term2).  A closure allows us to associate
free variables with terms.
*)

type lexp = Var of string | Abs of (string*lexp) | App of (lexp*lexp) | Let of (string*lexp*lexp) | Closure of ((string*lexp) list)*lexp | Val of int;;

let I = Abs("x",Var("x"));   // lambda x.x
let K = Abs("x",Abs("y",Var("x"))); // lambda x.lambda y.x
let KI = App(K,I);                  // lambda x.lambda y.y
let K12 = App(App(K,Val(1)),Val(2)); // should eval to 1
let KI12 = App(App(KI,Val(1)),Val(2)); // should eval to 2

(* let x=1 in
     let f = (lambda y.x) in
       let x = 2 in
         (f 0)
*)
let WHICHSCOPE = Let("x",Val(1),Let("f",Abs("y",Var("x")),Let("x",Val(2),App(Var("f"),Val(0))))); // what should this eval to?


// The following pretty prints the lambda term 
let rec tostring term =
  match term with
    | Var(x) -> x
    | Val(v) -> string(v)
    | Abs(x,e) -> "(lambda "+x+"."+tostring(e)+")"
    | App(A,B) -> "("+tostring(A)+" "+tostring(B)+")"
    | Let(x,A,B) -> "let "+x+"="+tostring(A)+" in "+tostring(B)
    | Closure([],B) -> tostring(B)
    | Closure((x,e)::cdr,B) -> tostring(Let(x,e,Closure(cdr,B)));;
Console.WriteLine(tostring(K12)); 
Console.WriteLine(tostring(KI12)); //((lambda x.(lambda y.x)) (lambda x.x))
Console.WriteLine(tostring(WHICHSCOPE));

//The following implements "evaluating" a lambda term, i.e., beta-reduction

let rec lookup(var,env) = // lookup var in a list of bindings:
   match env with
     | [] -> Var(var)  // an unbound variable evaluates to itself
     | ((x,term)::cdr) when x=var -> term  // x,var are strings
     | (_::cdr) -> lookup(var,cdr);;
// note: to add a binding ("x",term) to an env, just do ("x",term)::env
// The env list is used like a stack: lookup will return the first binding
// for var it finds from the top of the stack, :: (cons) will add a binding
// to the top of the stack.

// the following evals a term to normal form (lexp -> lexp)
//let rec eval(env:(string*lexp) list, term:lexp) =
let mutable eval = fun (arg:((string*lexp) list)*lexp) -> Val(0); // dummy
eval <- fun (env,term) ->
  match term with
    | Var(x) ->
       let xv = lookup(x,env)
       match xv with
         | Var(y) -> Var(y) // avoids infinite recursion
         | e -> eval(env,e)
    | Closure(cenv,term) -> eval(cenv,term)
    | App(Abs(x,body),arg) ->
      eval(env, Closure((x,arg)::env,body))
    | App(A,B) ->
       let (ea,eb) = (eval(env,A), eval(env,B))
       eval(env,App(ea,eb))
    | Abs(x,term) -> Abs(x,eval((x,Var(x))::env, term))
    | Let(x,term,body) -> eval(env,App(Abs(x,body), term))
    | x -> x;;  // default is that a term evaluates to itself
//eval

let mutable result = eval([],K12)
Console.WriteLine(tostring(result));
result <- eval([],KI12)
Console.WriteLine(tostring(result));
Console.WriteLine(tostring(WHICHSCOPE)+" evaluates to:")
result <- eval([],WHICHSCOPE)
Console.WriteLine(tostring(result));