diff --git a/stlc-bidir/index.ts b/stlc-bidir/index.ts index 10428b7..13b212d 100644 --- a/stlc-bidir/index.ts +++ b/stlc-bidir/index.ts @@ -200,7 +200,7 @@ const buildTy = (s: string, c: TreeCursor): ty => { }; const buildExpr = (s: string, c: TreeCursor): term => { - let result; + let result: term; c.firstChild(); switch (c.name) { case "App": @@ -215,6 +215,9 @@ const buildExpr = (s: string, c: TreeCursor): term => { case "Expr": result = buildExpr(s, c); break; + case "EUnit": + result = { kind: "unit" }; + break; default: throw new Error( `unknown ${c.name} (${c.from}:${c.to} = "${s.slice(c.from, c.to)}")`, @@ -245,5 +248,21 @@ export const parseTy = (s: string) => { cursor.next(); return buildTy(s, cursor); }; -// export const parseExpr = (s: string) => parser.parse(s, { startRule: "expr" }); -// export const parseTy = (s: string) => parser.parse(s, { startRule: "ty" }); + +export function evaluate(t: term2) { + function helper(t: term2, ctx: term2[]): term2 { + switch (t.kind) { + case "var": + return ctx[t.idx]; + case "app": + const func = helper(t.left, ctx); + if (func.kind !== "abs") throw new Error("not a function"); + return helper(func.body, [...ctx, t.right]); + case "unit": + case "abs": + return t; + } + } + + return helper(t, []); +} diff --git a/stlc-bidir/simple.test.ts b/stlc-bidir/simple.test.ts index 0981320..995ff43 100644 --- a/stlc-bidir/simple.test.ts +++ b/stlc-bidir/simple.test.ts @@ -6,6 +6,7 @@ import { app2, arr, convertToDebruijn, + evaluate, infer, parseExpr, parseTy, @@ -96,3 +97,12 @@ describe("infer", () => { expect(infer(expr2)).not.toEqual(ty); }); }); + +describe("evaluate", () => { + test("simple", () => { + const expr = parseExpr(`(lam (x : ()) . x) ()`); + const expr2 = parseExpr(`()`); + + expect(evaluate(convertToDebruijn(expr))).toEqual(convertToDebruijn(expr2)); + }); +});