From 1b728c62ab9568a239f9b5af2a44fb21bce0222b Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Mon, 25 Nov 2024 21:06:20 -0600 Subject: [PATCH] bidir --- bun.lockb | Bin 3504 -> 6484 bytes package.json | 7 +- stlc-bidir/index.ts | 131 ++++++++++++++++++++++++++++++++++++++ stlc-bidir/simple.test.ts | 45 +++++++++++-- 4 files changed, 175 insertions(+), 8 deletions(-) diff --git a/bun.lockb b/bun.lockb index d56199f6be4fabb28f2b4d8f9dbc0232d7ac7b22..52941f5718df24003c3112dc5089a79fe855b2cd 100755 GIT binary patch delta 2644 zcmc&$c~lc;5Z~P-5JG^2Tjf;+1S)0|!XYAtXt71KHnt%37Ggv(5KTbEVuPSOq*}#K zD^iN0_2PN8w9f;NDkv528?Uxn5Ub$z(5e;f%!Z{rpZ|B>+x_j#eBaD`-+bT9?&@(- zy`1fPqDfKmXjN%_+>wQkb~p4p;6EwtLcz7*N2_ud_jwRiHoDfE;z&jn>pY7y#8#cm zCa}F7C@OcRAvHA{*fMzBfhT|{&jXYLS`6v44Q7gp0NxpRMTb6&p(rQd{eYJM{s=tI zdjseQ7%QMCDd4jXxf_g=eFg#;#7$_vmcR8%XxpKc0X`K$ZId^ZR5v899PQU|AdY7a&?KJL$Z1$-XvZ|(H8(&$7&Pbv4Z}np?+Q-`SvlwbUjQUeFhe^v`bnRH=!lK` z{qM|Zcy|8PckVr(r{+v{Jld;8G*p-WO^n~2v6@@u!tz>kqSw_Pm%r|2{HiE*&w(MY zcK%)6ESN_WLT~G)UqdqWs@0@h=*8V0spWsf^^>pnOY`(-lpb3vQffTPdq=-nR$0F} zSoU5*yeXZ!UjXUwnKGpn;w zO!YBNSCs<&cFkpz%ju`uEl(aU+Hh$~Q8)LzlY`vOXT|=|B#*yT*%TO}5ac&{I$YmF zZbEbwK2_sKHW%#*{HLsBN#JPh-2Srk)f0}%EAmGM*Rqw_oBlax4sI_QGj8*dW<$!P zgP}Q}zhtPab|t;=;O1fV^SeYR>Wqz|gcV8O$0SL9T9!9rVBMGn2{TU^gWJQ7Ocq-E z7Uf*gerRH^2oe_sb?-K5SM;1ktZ$;Y>0xBy2`iwcFbbDsy{1ex2;)-P)%Y zJX?L6f*&-5#e23K{5U|`C0sFY6i`^R&(Bh~!LIUI><2C5T=m-y8wIbnNqfghtm;r% z_rLJx%w`(46iJGvwO`KS>!?m*J(Dre4UiUYQ?P}P83=k&K5>gCrNAefE zrDU)uiFP7uL`h@t4)7#Y3y$}{xc)_5$f@i(kq&v;->wXH_9}ca_r#7p9@bmsIR$P0 z_jE7!HQs!ap#SBX>e&s=+1%RJh|Ntu?<|Y{eeaqs%W)x(MS8fvLK$CoW5Es9Nhk`@ zoPsa7IWP?iERox<;}l2XV8LC?y$I+9Sas5_jIQcsA4e0NomNtU_Y-KFjF`nEo$=N- zbco#L}3M(9*bF2q= zqRD;Tz_L6D8Se)6P$4=r1E-MIkEc4MU_7Zy&z1I+&u5-5XU}4Fkei zbp#uR1GExv%{$%V8s5E+p{QwagLr|w-ARgM2-zZ0b?*mB#*?`)GW;Yx*ZFlE{2n0f z_a;vyQPD=jJcC)8YRE8{lQT_bZD#gNgGHH=m7%q1jAo;0O0s1dJKbWKm6dEvnVzBK za>AxrNSU<9P>xY5Y(fQOlU1>qsq?g)Jk6q4T|*S znTk%gXi51l1sHypSOHlh3mkiQ@3aa7JHHi}Y*72E-wpys@$o3Q!-ApWl5E-USd)j1 zL*LwQlY%=5q(s`2OmrOT&ut)@G^h_$HZ{? zs07_s#B>o9Va|3B}Mg|5RApH_54wM6{dw#2V<#ppP z`!gz;>~~(3a6QDbriV*ryj!(=XIJEnYw$)|wSIv|h5j_EJMWG^7)%s9CVNVPCd zJ_V$XFi!SjwW?HjymnJsJbQV#FQ z7VNx}*K&F@GEe@=89w<1kQdA4&B!`=C0F?5863QmdAYqA*(Y!0PM$o0r(&}X?;J+1 z4N!L+;g}pH;Kv7Y-3O=;59ee#L8Zwz1SI%Cp0EIg8xTZ*g|$E`LH+~z1>}B^5|E!+ zp>zjKIoIS#f-aLk2#N*3A_^AZOd$PW0E@EfH|b|PgkCE#F&gR_>KU6bFu)>h@#z_r z^Rq5xGBMU!=$Yyn8Zdlfn9L(AAp?tD&U~9=uL5W71}ZSsGcwaN0V!}0mf%_eOcNmR zf@|_LVJD!KldlOIN$r3piWUpgGmI5{|0IAZ1q38`Co73qiI-Fsq!#NZmFDH-rz93< e=w%kC7M3RFOui^8Jy}7_b@Kx;UB<~J5)S~@s*OGX diff --git a/package.json b/package.json index fc46a80..4f4572e 100644 --- a/package.json +++ b/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" } -} \ No newline at end of file +} diff --git a/stlc-bidir/index.ts b/stlc-bidir/index.ts index 868ef8b..6bade39 100644 --- a/stlc-bidir/index.ts +++ b/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" }); diff --git a/stlc-bidir/simple.test.ts b/stlc-bidir/simple.test.ts index b36ad3c..0981320 100644 --- a/stlc-bidir/simple.test.ts +++ b/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", () => { - const expr = abs1("x", unitTy(), abs1("y", unitTy(), var1("x"))); + test("K combinator negative", () => { + 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); });