bidir

package.json

@@ -9,6 +9,9 @@
     "typescript": "^5.0.0"
   },
   "dependencies": {
-    "lodash.isequal": "^4.5.0"
+    "@lezer/generator": "^1.7.1",
+    "@lezer/lr": "^1.4.2",
+    "lodash.isequal": "^4.5.0",
+    "peggy": "^4.2.0"
   }
-}
+}

stlc-bidir/index.ts

@@ -1,4 +1,7 @@
 import { isEqual } from "lodash";
+import { generate } from "peggy";
+import { buildParser, buildParserFile } from "@lezer/generator";
+import { Tree, TreeCursor } from "@lezer/common";
 
 export type ty = { kind: "arr"; left: ty; right: ty } | { kind: "unit" };
 
@@ -116,3 +119,131 @@ export function infer(t: term2): ty {
 
   return infer(t, []);
 }
+
+const parserSource = (top: string) => `
+  @top result { ${top} }
+
+  @precedence {
+    arrow @right,
+    app @left
+  }
+
+  Expr {
+      EUnit { "()" }
+    | Var { Ident }
+    | Lam { lam "(" Ident ":" Ty ")" "." Expr }
+    | App { Expr !app Expr }
+    | paren { "(" Expr ")" }
+  }
+
+  Ty {
+      TUnit { "()" }
+    | Arrow { Ty !arrow "->" Ty }
+    | paren { "(" Ty ")" }
+  }
+
+  @skip { space }
+
+  @tokens {
+    space { @whitespace+ }
+    lam { "lam" }
+    Ident { $[A-Za-z_]+ }
+    @precedence { lam, Ident }
+  }
+`;
+
+const buildApp = (s: string, c: TreeCursor): term => {
+  c.firstChild();
+  const left = buildExpr(s, c);
+  c.nextSibling();
+  const right = buildExpr(s, c);
+  c.parent();
+  return { kind: "app", left, right };
+};
+
+const buildLam = (s: string, c: TreeCursor): term => {
+  c.firstChild();
+  const name = s.slice(c.from, c.to);
+  c.nextSibling();
+  const ty = buildTy(s, c);
+  c.nextSibling();
+  const body = buildExpr(s, c);
+  c.parent();
+  return { kind: "abs", arg: name, ty, body };
+};
+
+const buildVar = (s: string, c: TreeCursor): term => {
+  c.firstChild();
+  const name = s.slice(c.from, c.to);
+  c.parent();
+  return { kind: "var", name };
+};
+
+const buildArrow = (s: string, c: TreeCursor): ty => {
+  c.firstChild();
+  const left = buildTy(s, c);
+  c.nextSibling();
+  const right = buildTy(s, c);
+  c.parent();
+  return { kind: "arr", left, right };
+};
+
+const buildTy = (s: string, c: TreeCursor): ty => {
+  let result: ty;
+  c.firstChild();
+  if (c.name === "TUnit") result = { kind: "unit" };
+  else if (c.name === "Arrow") result = buildArrow(s, c);
+  else if (c.name === "Ty") result = buildTy(s, c);
+  else throw new Error("unknown ty " + c.name);
+  c.parent();
+  return result;
+};
+
+const buildExpr = (s: string, c: TreeCursor): term => {
+  let result;
+  c.firstChild();
+  switch (c.name) {
+    case "App":
+      result = buildApp(s, c);
+      break;
+    case "Lam":
+      result = buildLam(s, c);
+      break;
+    case "Var":
+      result = buildVar(s, c);
+      break;
+    case "Expr":
+      result = buildExpr(s, c);
+      break;
+    default:
+      throw new Error(
+        `unknown ${c.name} (${c.from}:${c.to} = "${s.slice(c.from, c.to)}")`,
+      );
+  }
+  c.parent();
+  return result;
+};
+
+export const parseExpr = (s: string) => {
+  const tree = buildParser(parserSource("Expr"), {
+    typeScript: true,
+    warn: false,
+  }).parse(s);
+
+  const cursor = tree.cursor();
+  cursor.next();
+  return buildExpr(s, cursor);
+};
+
+export const parseTy = (s: string) => {
+  const tree = buildParser(parserSource("Ty"), {
+    typeScript: true,
+    warn: false,
+  }).parse(s);
+
+  const cursor = tree.cursor();
+  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" });

stlc-bidir/simple.test.ts

@@ -7,14 +7,47 @@ import {
   arr,
   convertToDebruijn,
   infer,
+  parseExpr,
+  parseTy,
   unitTy,
   var1,
   var2,
 } from ".";
 
+const kCombinator = `lam (x : ()) . lam (y : ()) . x`;
+const kCombinatorTy = `() -> (() -> ())`;
+
+const sCombinator = `lam (x : () -> (() -> ())) . lam (y : () -> ()) . lam (z : ()) . (x z) (y z)`;
+
+describe("parser", () => {
+  test("K combinator", () => {
+    const parsed = parseExpr(kCombinator);
+    const expr = abs1("x", unitTy(), abs1("y", unitTy(), var1("x")));
+    expect(parsed).toEqual(expr);
+  });
+
+  test("S combinator", () => {
+    const parsed = parseExpr(sCombinator);
+    const expr = abs1(
+      "x",
+      arr(unitTy(), arr(unitTy(), unitTy())),
+      abs1(
+        "y",
+        arr(unitTy(), unitTy()),
+        abs1(
+          "z",
+          unitTy(),
+          app1(app1(var1("x"), var1("z")), app1(var1("y"), var1("z"))),
+        ),
+      ),
+    );
+    expect(parsed).toEqual(expr);
+  });
+});
+
 describe("convertToDeBruijn", () => {
   test("K combinator", () => {
-    const expr = abs1("x", unitTy(), abs1("y", unitTy(), var1("x")));
+    const expr = parseExpr(kCombinator);
     const expr2 = abs2(unitTy(), abs2(unitTy(), var2(1)));
 
     expect(convertToDebruijn(expr)).toEqual(expr2);
@@ -48,17 +81,17 @@ describe("convertToDeBruijn", () => {
 
 describe("infer", () => {
   test("K combinator", () => {
-    const expr = abs1("x", unitTy(), abs1("y", unitTy(), var1("x")));
+    const expr = parseExpr(kCombinator);
     const expr2 = convertToDebruijn(expr);
-    const ty = arr(unitTy(), arr(unitTy(), unitTy()));
+    const ty = parseTy(kCombinatorTy);
 
     expect(infer(expr2)).toEqual(ty);
   });
 
-  test("K combinator", () => {
+  test("K combinator negative", () => {
-    const expr = abs1("x", unitTy(), abs1("y", unitTy(), var1("x")));
+    const expr = parseExpr(kCombinator);
     const expr2 = convertToDebruijn(expr);
-    const ty = arr(unitTy(), arr(unitTy(), arr(unitTy(), unitTy())));
+    const ty = parseTy(`() -> (() -> (() -> ()))`);
 
     expect(infer(expr2)).not.toEqual(ty);
   });