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)))); }