program lazylam; // -*-C-*-ish

/* [Unfinished] evaluator for the untyped lambda calculus with integers,
   lazy version. */

// 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. Difference from eager version is
// that each recursive value is a suspension - Sem() rather than Sem.
// We only evaluate these when we need them
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 force(ctxt.last); // Evaluate it
    } 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 app(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 app(Ctxt ctxt, Sem() f, Sem() a)
{
    case f of { // Evaluate f
	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 { // Evaluate t
	SemConst(x) -> 
	    if (x==0) { 
		return z; // Evaluate z
	    } 
	    else 
	    { 
		dec = SemConst@(x-1);
		rec = primrec@(ctxt,dec,@z,@s);
		return app(ctxt,app@(ctxt,@s,@dec),@rec);
	    }
    }
}

Sem runIf(Ctxt ctxt, Sem() i, Sem() t, Sem() e)
{
    case i of { // Evaluate i, then t or e, but not both.
	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)))))));

    // Wow, this works when we 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))));
    // Wow, it works!
    showSem(eval(Lin,App(add4,Const(3))));
}