program lam; // -*-C-*-ish

/* [Unfinished] evaluator for the untyped lambda calculus with integers */

// Raw values
data Expr = Var(Int x) // de Bruijn indexed variable
     | Lam(Expr scope) // Binding
     | App(Expr f, Expr s) // Function application
     | Const(Int val)
     | Inc(Expr ni)
     | Dec(Expr nd)
     | PrimRec(Expr target,Expr mzero,Expr msuc)
     | If(Expr i, Expr t, Expr e);

// Semantic representation of values
data Sem = SemLam(Sem(Sem) scope)
     | SemConst(Int val)
     | SemPrimRec(Sem target, Sem mzero, Sem msuc)
     | SemInc(Sem ni)
     | SemDec(Sem nd)
     | Blocked(Blocked f, [Sem] args);

// Irreducible terms
data Blocked = BVar(Int x);

data Spine<a> = Lin | Snoc(Spine<a> init, a last);

type Ctxt = Spine<Sem>;

Exception FellOffEndOfContext;

Sem lookup(Int v, Ctxt ctxt)
{
    if (v==0) {
	return ctxt.last;
    } else if (v>0) {
	return lookup(v-1,ctxt.init);
    } else {
        throw(FellOffEndOfContext);
    }
}

Sem eval(Ctxt ctxt, Expr e)
{
    case e of {
	Var(v) -> return lookup(v,ctxt);
	| Lam(sc) -> return SemLam(lambda(arg) -> { eval(Snoc(ctxt,arg),sc) });
	| App(f,a) -> return lam::apply(ctxt,eval(ctxt,f),eval(ctxt,a));
	| Const(c) -> return SemConst(c);
	| Inc(n) -> return increment(eval(ctxt,n));
	| Dec(n) -> return decrement(eval(ctxt,n));
	| PrimRec(t,z,s) -> 
	      return primrec(ctxt, eval(ctxt,t),eval(ctxt,z),eval(ctxt,s));
	| If(i,t,e) -> 
	      return runIf(ctxt, eval(ctxt,i),eval(ctxt,t),eval(ctxt,e));
    }
}

Sem apply(Ctxt ctxt, Sem f, Sem a)
{
    case f of {
	SemLam(scfun) -> return scfun(a);
    }
}

Sem increment(Sem n)
{
    case n of {
	SemConst(c) -> return (SemConst(c+1));
    }
}

Sem decrement(Sem n)
{
    case n of {
	SemConst(c) -> return (SemConst(c-1));
    }
}

Sem primrec(Ctxt ctxt, Sem t, Sem z, Sem s)
{
    case t of {
	SemConst(x) -> 
	    if (x==0) { 
		return z; 
	    } 
	    else 
	    { 
		dec = SemConst(x-1);
		rec = primrec(ctxt,dec,z,s);
		return lam::apply(ctxt,lam::apply(ctxt,s,dec),rec);
	    }
    }
}

Sem runIf(Ctxt ctxt, Sem i, Sem t, Sem e)
{
    case i of {
	SemConst(x) -> if (x!=0) { return t; } else { return e; }
    }
}

Void showSem(Sem v)
{
    case v of {
	SemConst(x) -> putStrLn(String(x));
    }
}

Void main()
{
    // plus = \m n. primrec n m (\k ih. inc(ih))
    plus = Lam(Lam(PrimRec(Var(0),Var(1),
			   Lam(Lam(Inc(Var(0)))))));
    // mult = \m n. primrec n 0 (\k ih. plus m ih)
    mult = Lam(Lam(PrimRec(Var(0),Const(0),
			   Lam(Lam(App(App(plus,Var(3)),Var(0)))))));

    // This'll never work because we don't evaluate lazily...
    // y = \f . (\x. f (x x)) (\x. f (x x))

    y = Lam(App(Lam(App(Var(1),App(Var(0),Var(0)))),
		Lam(App(Var(1),App(Var(0),Var(0))))));

    // add4 = \x. y (\add4 x. if x==0 then 4 else 1+(add4 (x-1))) x

    addbody = Lam(Lam(If(Var(0),Inc(App(Var(1),(Dec(Var(0))))),Const(4))));
    add4 = Lam(App(App(y,addbody),Var(0)));

    showSem(eval(Lin,App(App(mult, Const(6)),Const(7))));
    //showSem(eval(Lin,App(add4,Const(3))));
}