evaluate

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, []);
+}

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