From 0675cbef16bebe85197730564d5c31a9d9ae8ed3 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Sat, 19 Oct 2024 20:11:15 -0500 Subject: [PATCH] wip --- .gitignore | 175 +++++++++++++++ README.md | 15 ++ biome.json | 31 +++ bun.lockb | Bin 0 -> 62452 bytes index.html | 3 + package.json | 26 +++ src/App.tsx | 47 ++++ src/global.scss | 20 ++ src/index.tsx | 5 + src/lib/core.ts | 30 +++ src/lib/defaultJudgements.ts | 15 ++ src/lib/defaultRules.ts | 58 +++++ src/lib/index.ts | 20 ++ src/lib/judgements.ts | 8 + src/lib/pi.ts | 400 +++++++++++++++++++++++++++++++++++ tsconfig.json | 27 +++ vite.config.ts | 6 + 17 files changed, 886 insertions(+) create mode 100644 .gitignore create mode 100644 README.md create mode 100644 biome.json create mode 100644 bun.lockb create mode 100644 index.html create mode 100644 package.json create mode 100644 src/App.tsx create mode 100644 src/global.scss create mode 100644 src/index.tsx create mode 100644 src/lib/core.ts create mode 100644 src/lib/defaultJudgements.ts create mode 100644 src/lib/defaultRules.ts create mode 100644 src/lib/index.ts create mode 100644 src/lib/judgements.ts create mode 100644 src/lib/pi.ts create mode 100644 tsconfig.json create mode 100644 vite.config.ts diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..9b1ee42 --- /dev/null +++ b/.gitignore @@ -0,0 +1,175 @@ +# Based on https://raw.githubusercontent.com/github/gitignore/main/Node.gitignore + +# Logs + +logs +_.log +npm-debug.log_ +yarn-debug.log* +yarn-error.log* +lerna-debug.log* +.pnpm-debug.log* + +# Caches + +.cache + +# Diagnostic reports (https://nodejs.org/api/report.html) + +report.[0-9]_.[0-9]_.[0-9]_.[0-9]_.json + +# Runtime data + +pids +_.pid +_.seed +*.pid.lock + +# Directory for instrumented libs generated by jscoverage/JSCover + +lib-cov + +# Coverage directory used by tools like istanbul + +coverage +*.lcov + +# nyc test coverage + +.nyc_output + +# Grunt intermediate storage (https://gruntjs.com/creating-plugins#storing-task-files) + +.grunt + +# Bower dependency directory (https://bower.io/) + +bower_components + +# node-waf configuration + +.lock-wscript + +# Compiled binary addons (https://nodejs.org/api/addons.html) + +build/Release + +# Dependency directories + +node_modules/ +jspm_packages/ + +# Snowpack dependency directory (https://snowpack.dev/) + +web_modules/ + +# TypeScript cache + +*.tsbuildinfo + +# Optional npm cache directory + +.npm + +# Optional eslint cache + +.eslintcache + +# Optional stylelint cache + +.stylelintcache + +# Microbundle cache + +.rpt2_cache/ +.rts2_cache_cjs/ +.rts2_cache_es/ +.rts2_cache_umd/ + +# Optional REPL history + +.node_repl_history + +# Output of 'npm pack' + +*.tgz + +# Yarn Integrity file + +.yarn-integrity + +# dotenv environment variable files + +.env +.env.development.local +.env.test.local +.env.production.local +.env.local + +# parcel-bundler cache (https://parceljs.org/) + +.parcel-cache + +# Next.js build output + +.next +out + +# Nuxt.js build / generate output + +.nuxt +dist + +# Gatsby files + +# Comment in the public line in if your project uses Gatsby and not Next.js + +# https://nextjs.org/blog/next-9-1#public-directory-support + +# public + +# vuepress build output + +.vuepress/dist + +# vuepress v2.x temp and cache directory + +.temp + +# Docusaurus cache and generated files + +.docusaurus + +# Serverless directories + +.serverless/ + +# FuseBox cache + +.fusebox/ + +# DynamoDB Local files + +.dynamodb/ + +# TernJS port file + +.tern-port + +# Stores VSCode versions used for testing VSCode extensions + +.vscode-test + +# yarn v2 + +.yarn/cache +.yarn/unplugged +.yarn/build-state.yml +.yarn/install-state.gz +.pnp.* + +# IntelliJ based IDEs +.idea + +# Finder (MacOS) folder config +.DS_Store diff --git a/README.md b/README.md new file mode 100644 index 0000000..0188b2a --- /dev/null +++ b/README.md @@ -0,0 +1,15 @@ +# inference + +To install dependencies: + +```bash +bun install +``` + +To run: + +```bash +bun run src/index.ts +``` + +This project was created using `bun init` in bun v1.1.29. [Bun](https://bun.sh) is a fast all-in-one JavaScript runtime. diff --git a/biome.json b/biome.json new file mode 100644 index 0000000..f85e6eb --- /dev/null +++ b/biome.json @@ -0,0 +1,31 @@ +{ + "$schema": "https://biomejs.dev/schemas/1.9.4/schema.json", + "vcs": { + "enabled": false, + "clientKind": "git", + "useIgnoreFile": false + }, + "files": { + "ignoreUnknown": false, + "ignore": [] + }, + "formatter": { + "enabled": true, + "indentStyle": "space", + "indentWidth": 2 + }, + "organizeImports": { + "enabled": true + }, + "linter": { + "enabled": true, + "rules": { + "recommended": true + } + }, + "javascript": { + "formatter": { + "quoteStyle": "double" + } + } +} diff --git a/bun.lockb b/bun.lockb new file mode 100644 index 0000000000000000000000000000000000000000..63ab9783e12bae9a2544d7b6640672700d89336a GIT binary patch literal 62452 zcmeFa2|QI@`!{}Y63Q5oh>&ESMdo=XB#C4y^DJXRWGF>4rlOHl$`Fx^DT+|Z5QQXZ zFqEXy|60yDxBWi9=YF5My}$qG9a^8hUG~2A_q*1**09$;d+&32*NX-E`-wTYdWkuE z?c;U`^r8WXcz8Ry?{W2T7TM$N=V>1xvQM0b9EZcvdtJJs?DAlhuU@uXPr?rliU^Kb zkIFsnn|5~Imbqv<;WP~gK{`V)II4fKk;LtDr-*+n7-}3YG6McW*3a4AF#!I409Xmz z)?|eJ^+dl9SUT9h&o#gq{>1I^ci!jh72xmV?H}Oi?~hwffy2>){|6M82CSF8m$$1E z4(IIe5a{aRglk@g!>xw>C16>>o+8>fqV*+O8?Y?k*9FTAR+?zJiFPH?&f*FFS47)R zw6}@20PHH@rxWc#qV*x#U0|8OZ%DKXL@PkFtVHYQ?cos!mG^?mbHedvU^&3b5VtwN zu7T}&sQfyxy7auZOn-ZVa}O-v;W0+It8Jh3eT37PU_+6dLuLc(4$H z$jeX}v_Bp!ilZl3RNiv%L(wAhi1q|nq>~Ri0$_u{qH_8>d+u}g!{OZgy}e{0&%MrG z{vlqDI45U^z`d~Txe#3(jtv?SyJ@~<*`nuTri|p~R-@6vJQT}F77*wu2u&CZSpo92s{?7i6z*pTwi0>R&RIg#M zsQ#OX_M0GKe7pl5(r*O|RgGj2CLI4sh|rE#U_WaA{UU^ThuC{~xcUd+d|?~K(N~lZ zFUZy2!`{i+3ARzWOu?dd&;*N)Gl%0LbdhRcQ9Sm6E;Mx{A6V2cqQMCvh%|(Z$_L7}Q2!7qLiyZa-azreNfY?h#Qm$_I6Bzx0gZ+F z=~l2PF7ja6!197c?M?$0^~-7Cqj>d!MgF^Bk)N8F-y79x*?@{CK4ENI=3L_}_9TyX z53EUUJVE}2)Hdd{!Iz1YS-L3h6N0$;eD2^Swveb-?IUL}p7<1+G$nJKpmad0wTI=xoB^6{9X_5GPhuJH5QQd76Q z<8@2Qj(1@FPEF6nJR`^?AVqd~IIr*E9&L&A-nx3+2Oa(~a#gmuISI2CS?Bx9O*6FL zc-B)fDhpMRop>0Jzv5!Ys1SU%Aj0hf)rL-S^=!LxN_uix!-qHXj+chkjiltSTCMYC zG(BJ{Pi3ac^_F73G^OY3fq|M+g_70srXGE|^cU1p;{8r;?2p%@r61~$5dQw)J7=f~ z*+}@)NR{PV_xQy(J6R0WH|y-4a?` z+1|{H8XOC3a`_q_iB~Dp8TV{FX*Ig_!M5G+e$FM^&(tz^Q&u*Naw$#M-e_Tvalurj<61YoQWKScIn}+g zmB+O#7-PD1=ry$a=#}1Y=I3UW;|kx_U;1@jZ*t`63KqQ)OWNan!wP;5yOh`pgLbo< z$mLkBXgzumCq2mC(saJG@oCw!W4hySva`*_8VuQIJ>M4?@Fa@fsSs6{6zEhp*=Ayt zlzKad^h&JJD|_}XgEsTkkzL9XkPKQANwC|(`s;ZY~48Rm-^hLlGduP z#aOKV?3$JaW(QwBCDj%5n>(y7x9fd6GcxWLc8FR*_RP4MzVi4hv+>}~hK`POR!(zKa6Lmpa!b>+8qgr2Yd%rbDzJ0ex9 z=aOLSuAT`|<6QOx>F}h?sqo@~iN^gtInN$Gp31o1#U8$X$~*HBeMG!rhUv$=OV;

urfo32_lCb}YJUsmrfLK6s83<<_O`||jq{|4Sts$ADaliND>l8| znq777L1xGqw@%lyIUf1G4gA-(9aD|Ira#16neEJ`bHc4bMWlert#{qWk*`wjuXriQ ztFP#)aBSavhJHFDolE&qZij4%dQIEZt}DH)GIcY?9cMN~3Jb+LJCMQrx0D3a^FoS) z|F^(=3g-eG1>je8N&IKPfvNo;^JySMRp6t1@qk}Vr2HL$r~v%m;i5c9{8PY3^+)^Q zJoDFnwEaIzBz`yWHHrDdQudbsNM+6esun|HE)GyK@Qr*TCPg1ilJ< zc(IiHvw?5Eg#6zF-*yRnefW^UbqV|u;M*^O&kP^>ET#Ouz~8%s{JVkgyac`yEZpsu zz|UDC{~Pd^5ITYvvQDS!8W;gk0NJ(J)e9d{1+%8)r$X8m6!mRs`Sr|LNJAOuikH#N~_q+4Y2Dl%D zuHQ-X2V9Q)QX-9iH{dG(A8n(&N#*!YA|(EK;7bFaRBn>}RsImM{Qoq5!f+D<#h>)K z!S9wo1o)`_DF5F{r23ZtUl#bJ`2TMGr-6^!59y(@|8Duk;C>Ohenk1Byni?UpTO4u zK2XtpAsne*X#0PbNXMze%`$ZThT;dO!r%V<<`wWwh|n7>fm(AfFi@fQtzNhm*x z2g2`;zf#~U0smj~b#M-_7X{&jQ|l++eAZJ1>Hi_2yil4X=8uQJQQp5BKi&;EoG`Kc zs0_bbeiPs?W&E53zUmU%zYqAEfe#;Jp!?*%oJjFo#lN)t&4I7Egz{ekzWNgQW56f% zKhy_E_4-eNARVW>5r>28p1=Cvvj0RR`bqpu;G_B@-mh|z1d0C~_^ADUwcio5|BKHo zKv+K^KGOWxaYQ=)Uo9zrJK(Dm>kl7g{&xQ_1U{PoP`>|U{EQOwN8|RN%>NFX2<=ab zAE{pdTHk-&CLMPI_~`tL{73_p;a3ug&mu@zKcl+;llI>We0^g3BMp-7e<}m%xEn-1 zIv$n(SIa=+GYApZFQmMY{gp)GTLK@g-~Va*odEvsCGdq{@?OgN;UMs>mymxy@ST>x zKLpP~q4hUvHx&Edjejlh(fS*;{XgN)0ACIGXzpYK{Awb#f1D`c`jwRT@0R}+@JaI@ zN%L3AKsuH~jIe$uZ8QA}8IBe_H+y;BQ?5p9dbkFzdC=QK8E@#0^*?g3$+0Q(W1EkC1lZlG(Vz*EaH&HDYA&a9)Qxn zvv7+8o#PkM|A`jW8P@0v>3;`{<_KeAd5}fz1ATBIA&c4&?rAQh|3597lkAE4B8$r9 zK(vlT>jV}hWRc$)Z9qa6^@6y#J#`=k*lgeq>QOP5@9o=>XIo*#NZv6aXb;k=|*v0SQ^OeTHar z!J?E4K>YInl#oTb7tsbJtVQ|-3wsF`9ajiIak>sb+r>m%3Ks3Z1wi>$0#HI0<#z{w z^y&a8{fNVHC1Q9>5^ozVs)WdF>2f9Ada z{&{bnejata|CI^!$Z!N*tTg_$*GARL5m!&_eB9Z}bw*n%($|=4->BVGT5-HrMwM~O zjqo$o$LFI&)$45Hhl|r+dijyb7U=ecZ9OHE+S&Ys7o&^D7AfKD#PZ0=&0;xeVhkSf z(Y&bmZ1ik!x~reJ*Nd;I8~{Y(RQ zY-H9^NE*<+7`L@pe^h$Hz*kF@KjoMR!WLLCf$$ z;f3w0>Rpn{6RzRz=09WzPNeTI+s%Ldp#j4&@hX*r_848XW+EkgpGMmGl)?6im7Ot1 z8E)QMbJ1wW%VD1t?MIxadJGG{Dnxu&s^NS-Ctb0LuZsQ3r`jI!(3<9q?jJk$S1}2G zF+5JxMX^O|0aC(`vQz9oa7L`WmrTAl+WFXp8=m!C9UsdsinmZ_BbC1Tg$8skQvanUiGszCUY?}6*7PH&?xo)9!Vc~; zDbbhTu-=w%be(83X5tiIOZ6=Cvhw+mqFv_u1wZeeS;vsH-~M%mIDhxskBW|W4vApm zK!erY8hAvIsjbfJM4`cMr;5>Cfz`cxFRr(Fu?^ za@UrbU)UJ=b2ZDu?-I)nsr3a)h?~Caip>7p5HaoR^*QYYXYrejnp^Kj>(}0+rQ8{N zC~A^SpckV{OA-Z(&!%ltyc--Fe!V`MqUn8m;5A>W^E`7Cse6i;KAma2sH@f;-m>c& zleDGgi(&mQepYuMu}Ewzm@_}2E7oCgF{*H(-3Zq?*w1_L>+{<(KPK{BE%#F17hsV@ z^+4(=#b>&63jX9zY68nNR^CYEVGX(08{sEEn(UMrz7f= z^q_z}*%$MyIECh+vs6tcos=F2S7LP0wHYblD}p{#I#N#MiM94lljqCoM%6s_uJ|rd zH&&$Y&0lJ>Wn!gzbgtMMEeCnNldXZe@BO&7S?EkE*0?f^v>zKX)nCxXFN_IvolZ*l zR~d}=m^Dm~KbuG!`?;KKg~%8~Pkkiwevg5K8%OD~S3fC@8t6|e&ANj7_)3GUVa1jD zHLgG8WG#5?+MDiktsf%lqJ;`t1CkQn-yq|&Df2SAenatdh3`1;JG`mA=czN9zrtC5 zeS*q6C7mbfh9I0GaC46`T1?jwb5d`phuK>zS73gg&)Y8D9mb#6n=`X zTV=LsRk8U%+3^+X^xLanB_7+vN5fU6X575jAWU^)K^I5G4Vo-iU5*l?h8MoY-vfKM zs+rTQn$S|eA=Du)<13rl^S)&C%hA3ma+B7ehk~4S5#k%hRJF~*G1D!P?y)tGhZ=z<-L-us-)GEe9oZ92R}@V zFDfq^NfazTp}6QIzm#C@F1vf-yd}$jNO4)o)U6KMIdo2;M6BxSdp0}%J3`ynoebUh zIhfPLo`LN_MeNF~*n)3HuM~Hw6$}#Ni{^CfeOLU(0Vip;&u!WdcXd4F^4>{Vk=#PD z`f{wPJSA>6=E~zA7y4BW99Nb-M|<(&r9w>(4gQexrsCOZD*fS4yX!bCTQR z=N{*-w41w+Ez5M_KX168OPGA%vBkd<{xbe`tK@cCRiyloGikli92=o3`^l zRp%8wyN=BXT|c>Yli~oHoLF7!_?r^p&yL((;ae{*>G%9Fzs`_PykuH3dF$p+dFv#n zbEI)ko06FEG4%U4-B|9EzG-xCG~K%$83wn@r7pY|5ha!v^#}C%A1UD-W}nfW?Z}@P z>FMj(EX$wGF?;1p+NQ%}7bY_|@oES0J5d+~3|}_b$)_)n)O+tG@WXT z9_~mAHzt-B%@6Qc++PWQ<74v?JKA)Iw6zJeJnzya>}Gn>Pha7>>?&|eqW4+ZK+5B0 zu@bjvxyaHPmunXdG!pv;r=+zaY$%zTIqsft^d{;?f+F`{su16@VTG+Z@9LM|7;v)_ zgmo&8N)OuywT6&O*Jg#kJ~^fqKvxrV-Yc=cKK!wT z_UvUpF}0@Eh51sce4}}1Y@NIh4p9~g63dI?%Y)VJy2)vrQ}j5v*vB@4l4HD;Ts>es zQlaZIr%Zy=hN48tgWUt$t2EzRh^c(r-fMk{eui7!YV2G#`|>YwI@7y-l@@f#7v=|E ztggq*SKK~N&tdH&JZXEMQs#RIOlXM?*1sLEQ+h=gBxs|mwB|(f;Tih8fLrPcBf(eL zhCauv`kJNi=2V5iH|@JV3%ZdDpX2ahb)Ry-QOoJc+E?OxyAIK&jW+H=|dz*a-+82j)98J9qI{#}6!x`gYC4OrckV}&Q2 zGGvW3r1TsUaLR|@N?+v}yeUwY^uZ_Exb)aD+b)U6BZovv*M3fLykyVU^c7AZ8|ZYq zBQqYEtsjp-?|j2QDimLStZswV9kE+D+f-WzyCT-_oqNUDo?h+I|Fu5Cs~n~izE?ODjs zcGa-8kG=*rD)A|Vrwo}zR5#^iWH23Et};1t=e#k6{}GRSc13o&M>Zyr`#)LR-}i>7 z8wr{MSl#_4e7IdNZhaMP??1KbM4fGe^Fe*jj(V@KBWjvP$^L0>iH7cjrn!PDgXQOs z1Z<~sy{kG?8T(O{eq*E2&%+Nl5_Qpd+l1A%D;nKGvrMkky!Sz)nzQiEdG#MNE0=xX z$|8v?ro|BHBwnvL+mz-#%Jeq3a*y*D#+ICCC`ks_-s@_Ap{LX`- zSz8%;`e+$;=6-#j%40sSUnq8{YGcofsBnjMXbJ@sWx8% zF0XuX-naoZC7>gSkNVmV^OSbVt>@m0vZ;p@FtVGoS@!hoqXYM z-}NM^^u{*j+Fhbtc4TlMg!*{Sdu57y)|#I3-6y|m3fz}`(%|Xv7B|VLONawOR}8D$ ze&HkciItlZ4pW{|=hp8x&xaMy6|SCpqsJF=QQ>g!>Xn!D z9D`jghKgL~OWDb2YYFEe!g*61tE-XM9CTCRZhP=F*BTkqw#!X}y)XSJ*=QzalOtz+ zl8>lxh;`eg&(kt?@+*8Ne~^124)}$3lfdeJGCs0N-Jb5{ z;J7h^-%&r6A8*fuSLv2@S8|tXXMg{Ej>%W#1i3?5t^bU7aisf>&Ljt$A3q=XYh8G9 zXUpZy#Tpo0Nv!T+LvxYfw{E9SYkj-GvcoK=&6ctB>E+Ry=d%?DJ*xcK-+g>tP5VLi zQS79^P3n)sd8_=mo4&M5Rkiyk_0?^ruO;e6f+pOy{wv|P`MBqN&ZSJ#pte-7v3)ouMN3xz(XO^#3&w0Pg)6-47{A!*?!5d*NyXC6WY^4jjgn3=| zFI6ZnSwde|fTZIw&#;lLWLEsGU$~QEs=M~ct7x{EiXUcplq>6_+^<|{74uBc}ffzGP3K^X6kk76yuSqH7+$F}R7FA|HIvm~I=RO7VFjTx~2O>3PF( z?ZlY!p05veFuL-8l@@f*+`F{ZG=_dEO^e#v+sggLm_P;7nst-FE$Ax2jLt9xHcYKA_|HA`?=OwBn3vW=8c zv9dkq0%`5ZT6JhO`qfOAw=7?N`1pJ~-O7(yq7vy@+ATQ=##SG*UE(8~%2+uty70`x zUkT6A{W`o9zm0VdC*!IY5oh|;eokrRx2j!Fy`6pZo4{!)UoWNW%OuOJ8%5Wter=B5 zufwP7r*W46BODcspzv(D;l`)gQltg+Zf)6-ZW^+KkLFz*m_;Te~|68=(b z-@BB{&+A{3&8#opCabT&^2w8rS8M!%p6K1dn&E9+7bTh$)_yaKrJzt5_TG6j)N;^W zvEnL&!Niwb#T2!eg*Xt_56XY3Lc5hbE)VC(`swDkTk4H)TS<9;an-rmRR^pehkx9n zAI7xsoxi zcQm3-D_n0xEjaM8&*|!#Cm&XFw3!?^W>al@xy603?nG=<=t+Yn0b^r_?+^1M z-hV>5bFbTZ`T#zc5(T!`<#fjqR~q+*>|ZD^%no4Hu)4x;YIex>#qCQy<75@s+cuTe zdr?@mZN2jtuLMV1by1ji;HK)AC)GpuB}N-*Ytw0M%-JL^s1xE{)pBm6`s6pl=Y9Bv z`;_Wf-Sh~VP=P%ovG*N~b?QNv#2*GnQU}%4o!xP5|Ed?)R<=#;Jv&*a&ZWH&2OJf;j@88K z8m5;ky*m)KzuxM|0h(ic-!{<(h#$W9>cbwT7X#}C6gF=PIHxQbeB(u_)s5KA!od!^ zbH1#+wwIZ^(7o05Ev@|H1zp1WK?|#!b#80ofT^18`AA#8IJnT^p<0a$E5U zv%%3VI`_9!ZM^ED{3<^rHf6xHF|DC#BX80Ako=>Ir^DC^{>4cs?x)UR_N z{gC>|ee5Ca+Ol(&-Hs|FuOj!!Y)#tW68C{qbF_XL`i>*g=d`+5-PfLdC4$2&_A+

9WWreFVNHGT8;he#@7YCF?UYV=*-+N3{DOCV3;dnlK6$&n_7nRl3)GGz>|>= zGw-QkboH>h=UpZaHD9@uu%d@~`td^!g{?``p(5#d1N1W?CUqH3Ts8JBra!s`<}9B~ zo}|2MyPRk4a?>&A4{n(a{443ZTIevk`dD41a4t$#(M|?+6?%#@YRXo!Yu{h`63Fw^ zD!-h={rk%}twF`uToK6-W=D#Ne;L1?XdmB?;Bdo4NT|ro2oN&<^2T>8L&9WOs20S@t zu7--!uNetC^h%Xe+V|1tz4WTqKBb4Bzh9YoHSwEi^;xA&XQu?qm19^+TQIul`4>{c zkEeb+tei2rUg+sVj_6Mkp2gzt_2eSo-3o~F+?&`?J@ocaxt_|<(D(4ra-LFY?fLHA z#iw2#;a`9G3a(zaNAU(m7d=NqO88;Zvk|%qVU1I1g0^J}yF|xyJgCpqu2ptNkVJ>q*BqiaeM1&hBsX6C;B-iwR7 zSKYKcWL0&+b2g@{HKXBN&GEEsb&VkgTlz5jNx4@uGwjz(l(Pbl?qPI_%9xBPy;OvE z9~?8&$LMaw>gpAr#P!gQ8$CT7-?(R9Nn}J%GD33ginXmd0$21UnS`!h?;qU|w{uHG zNd#lU7#YR+*Sf5#?@wRT(^*rL5&SL>qicrMl})4w>nPxGOFG@^FzM5%P0LbDXQmfp zufySI=*GRZhf{W7OHx6^{;JHwuek~@`)l%Kv>beHEyUGmoWkAOB!JO1$LbytdR<&o zwqEmyxo}&`YOzz6&-&BJ-_o1YUGHNZ+@q;brKl|Fvgd)olNE1`&gIZNonq^5S~qCP zux5Fo5{EY>I?9b8dA(Q-0mvND=Qv=U(%kT<{$0|JI^TV#A;2Fuk5}r(mcdl2Hu8xPb+WM;7 zh}?ystY^cTO`dP6^nX|%I9?tr8v0c=B7$yh!)rfU`?TrWlh1rjWKnO};QD;qqv=^Li6?B_;uqg$`?-ln`Fe~5Px6pola+sPR#WPh z)rj$w)MnX(*_n?Aj@Ya?Ce~u2iN0f*G*52F>VAKnC}e1Lt+nAKvsHf06z!wf#%(MP z3?nx8w`TvC{<6!b+c)s0f8g2OL8I~Cx2YYSXYF{zJ?9vP`!L^R@MYaujII?{7uS~h zh*FSEz<4;Dr(*89nESrRll|f%?uHZViha~0CyuYS3Cew8xXqAZyG!w-BW~8^BDL4H zN{g-7?s?u7m*jxa-GSAmzQt?bM=kB^H1)QCNngEst(-mk{<5R7nU-5>OPCx6Gmn>B z9Il*6Yg4H&6gv^RvMun7)frut`#fxOm6IyngwF{G{lOZmTVy#MajW!Z!cpG)G6q}f zUCG|ODHj{xQp!M|-m5lVe$VepfW%sHHL(QFR7s{eal`F{Y(BMk@(XY6&o&okx9!1{ zcPCaiZrZ|C_|PlE8~DUw2VISWn{$u0Bn6)z?3HOxV9Lt=H#Cl^d266rK^g zVe+l$3nmV`u(}Gud%a&yXEA^2EUXR+)6=7ts1jg3x&PqmO{)e=UF28w&afU3i_Wv) zdX})JQoy?~H)`cOanp1c*$;-YoLQXM_>!JmMDqA$>z>{gPviJ_xsO59x>>>?w|SLy z%BedI_hf|5Qhs}~AzyDcXF02IJlUz)f`Dwd8p-UYFWf@fhJ_l;ZDYX?vEz6*w!FI> z)5FS(Iio%g*7sY?NgfEk7K{OvYOd>yd5Ox2hCC%6QmT~+=??zefkAHrq zQt1Dl%NIAUbBed7EKIB4$@~OH*NG$w7B4s#JlZk7-ClE}X=Jg8e$_DBfc6zGJ9Fp{ zk31|h?_D0dB`ag}Y}c3OuXJT64V}t7M80k9wExk(r}1^kz7&3pE_zOil<-M~dP+(= zjusC7-0H{Qb{Xe4PcQrJhU|RPo%T5j8SnQllnugabjwoAPL6dr^G}UfJ`hadc>4Ib ze`wYFF9Lh9@!dlb1&gH1xb(u_xVgJ4+QgP#x1(amk!ZBDMS30t(_)yf38QKu3fO)kGI;@*ZuWsmlfC`J-KjO_PRcep*RioZ+w$?VG<~v3$q6yxI5I^P3A+ z_c5y;bBDZ5i>B;-F3y;V3Cm|g244s44bHff+sp}$cTUB|MB`67l;ur+rhd0g;oVvC z&3g~TmFo2LO~xvY+r7rb*A=Uqa3qo@tvtbd8Jxd7$?xnd6$%@BH{V%cTcW8qHz@1> zfJe{3GxVE8bZF!xXXpA=Y$b_bg$l~rrx>!-;)lyUqP zM%NvyTV3jMWu4a6WkqRML(LlxT&9fW<-eKlF+o?dhx%lu;LUzL4azr3JE)u(L%uRv zu05I@m3HbwokoO)-ki+kDK}P(t_N0EUBHYE~Me+E^{0*~t>Q|zSV)DsKN*u?I zd$Fq>8b0}2(@KYRaN}JWh1rUR9a&e`J&607PClN@$!@2)l5n4wFt2-Jb+4bbdp5dG zm3>yXSxntWLwbwdpv;&hi?-XdYn?9wCvOF{@910QT5-Gc+1G8SfAl)0)x=ejWwv^K zQ1ksU;osc0PDR~ z1&UYpvv6uq zX8BZ!J&gy)#p@>epI@vaBmd-k>3JJF-Ju`r?`?=&HT|gf(Uj=Q-7Bs?-N}y8^}*_X z+}jx%Y}jDmBO#*`%&jD_ses|ov^Agbkrz>%wL1;^#=G1-=cXK$dW5-GS!Cw2PD)s; zoYEiJz}!!z`KeH6PA~bU>y!gD zIeGWi&%0<$+;HbARkGKfmC%UvSKTL;YNHyt@>q()dJ9R9@Q?jBt~d2X1<$Uaenfb# zg3urQvAVZ=6kH4?J>0G9T#LVdpUBzWc4X6v9o#eZg~M#Sxi_yQU*mDyKB)WL+JN?G zCquj2B6q^*DNa78EIrpAdEu>tJ*KO4#&0z6q$Er1=^gViFBUE?QuhyBVPA@AnzWMpc0~yV2Z=P_Q%bfXo zD7jkwYvPXHO+pymeI!w^cwWixd!i_~nJrhztNXGUy9gCH@`glp(tM>mAUq~=)Hh)47s9+yMxZgW9rvcHf6WQ1#};g!03izb(tq4 zle3C*1x$k<6;?3D(+fWC?L6a@dRyk9?TVM_(wS9qkH+_$xFK}A2!Gmm-ZwDn+btof zFpIo$dyB&?pUm!Jbi=T^=M2@OQ}<}c?>QZtsG-g~5ofzkF^buERj+og*!NJW0~M{h z9N!XC}(&Fk_;K zjYA|>SLd!2^~GummGVhO`uJ0xyUh3v(?+(}7^T|bTW{|~q#t$vlCbX+CcaTv-5t6!mu;-oA6Fba_jaVUdW{?_o8qY{A%kh@ zk;F{=3Z>@ITAui!{IVC+=9fj5``6NtRW_+xG+XV=ZM@?pS91iT8;#Wsdb-P2nQ7zA zT?%;_W9u}fjBeH+pAT_-lUuAjqHlS|rQXCc|Ar<$mSX1Fk)VE8@q2!zl2iP1odOo4 zE&&!5ofzGNSlz%c-akEzlJ?V2+Pn^n<9Zl+N!iQyM%qMig1JNWx@OPt^?FJ7Jr!@) zoVnRIbV_b;(-ci0yI`^;`R9)gJ8((Z`8NiuOSi3rS<Ky*4bLD1csHpe^6Hcs{?1vgf)gz^#2ZPj7wS>=q3G+@YR=1_= zk!bTBc5xxv*yhPN_ot6q_{Xmvu{{~u(CTq$@7{AX=4>^$#ASQ?i?ercwzBGB%^bot zls1hgD4)G~dg3YJb9;jBA*}A6hgbG)=pK~!{Yn>P+tbGCc0HWSlvbkq?nNs%nUq|n z55lVAyv|f!&yAB@4)|DRe~LblRvWQ$OMbEX2f+`ae3>OS>4(D>GF08qy8?M$5k74=V%R7 zgsCxHZQ_m(KFOHX#@?7Yh|hJ$ls5sZ%co*!=GUiK%^GNSn{0R0>MHZKj>q4AtQ9DD zCp2uU&BC*-XS$iwY(PDk`n-Vx{|V90Jo(qMUY@{@M{J93j}67>CSr99JPjj$int`C z-dtND82gfT>O<k6fzKK-vJ&)>s?NxE?@hiLHG}G?N zv*f~_HOIRr?-|Uof8JZV{JZg_R0#R=?K&^C1)o)5;&2SBTReLrbG;&2ob~Fdc#iAM z%c#~lO4aciy!g4R)io{;pV3WkHTS(HMBgglU5}rTOVa&S)=b)8nD(F3evv&bGU<%b zO~&fB4>Wu~@cl;l558vhwJAZf$DS{b8HqXnYD1(O8T@0KG7n5E}RhBIu$k{i0;n1h~`#ya=n}42_ZN}&x$Lii_ZWw*yx?3f% zDOgC2yeZkF((J|)6}d!b7yBd3+0O&c*UPs1A5bm~a9O`q{4QBagTL~zOjl_N<@9Ai zzSct77~NE?F2CuKEu(n>>NJmT5@}G!u1>BK5qtAH&WMOUOFoF z)WvbCr=$DX9y~fDn|E80>XK9_%RAwt-!92f=?1>hEjj7w#ko_`f{|>DY2`%9{fu17 z-9mF3=amT0WfIDpiPa51&iZ($yHd{4j9jm3`4yEYUhXvqKCLb9h-;-86=Tn$HgXJAAUrLxtWl zwC5Xe)Jk4|v0+za{QID|4A$(UMhaCo?wHk?Z80(;Z*y=MNzAfz%;qiGsF9HAzOsHn zmvH|$8>{PK>Y?P;dPhh9N_%E7O+-^tTu8$q#g)}NdHt5pwww++bx=NdXH?(kRH@xv zFD4(8vpaL@6^`rZoe)Zd*AdVR`)a|S=`T)jH7NT8;g{z3{+ycEG7!PKaeeZ zU+_LmuBUx>N#)?oK3Uu$X0hDeVzheO0>jy@^|NXQWrgDJPQM_0?n$^WorBfAX*nor zl5U%oTOUnR>$jYN)uLg|h4-a;(MGF#8>VD9JHG^RYG2E!G+m=b9{A3Za;?mzFrAlI zee^Hx8hQC>%Q|9wBSG^NR(JBKk0gt((uLD+6=k`GE--nCt9<#!==uGbwn3)6JA>gZ z!3huV4synCHOY4m4!7|neNvqBozQ5m@m495*5Zw459X(t{-LMzg|3Db&k$#_&12$IRaFPE&=6^~-d60hF@;C+Ix9QM6((hb8 zfqnlS`TkD}^~d?&8UfV4q~8IxSV{Q($N$z0{~r}caVGt~DY8qR5dI&H$c^!vf2_1eNdc&ULE;z8Q?e`EXqpIj%@Mh>ptp6H%@ z6ufZoe?s5I69Z1N|0MoPygd0QS^nYtiNK!-{E5Jy2>gk_p9uVkz@G^GiNK!-{E5Jy z2>gk_p9uVkz@G^GiNK!-{E5Jy2>gk_p9uVkz@G^GiNK!-{E5Jy2>kCCfj7iwaK95R zjiSGwqo}Kwe}KJ*hp30Qqx&9L4`)#eKWArUZb@-&f7eiF?>)lY(%kkQu6w<__rS9_ z3u*o*A)yWQ{H*}-A>7s4J$JhB`#X=owgWlqj%L^0r~&~0Qznr z^gTdKfK>oy01JQ~0FOZ~{1(syu;`sd^nM|F7ZAO-hu*P6@54m`q5#nV^!`>1AQph$ zVM6a4p?8BC0O(z7^jV_!7Jwo^37`x>-_fQDPy?s~Gys|aEr2#a2cQek1FQ$|0C)j>fDHhC zz(#-oU=u(PAOsKwhydU*7@QbD93TOZ1V{nkk&A`zW0VCe2UrK-0x$p`0_p(ufD?do zfKosi;3l9PPzbmJxC%%H_yYU^2>>U69bh-$A|M}d9)R8_s0362ZUd?Tw*dBlY`{rC z4&V;J0dN{{3g8Gh18C2M{~!q^K1F#mr4p;+V1FQzX zvr7y8ni(wW=cvCk0#N&)zD@@~ZHLMu13>MG+7-1gYG-i(YIoHBs2`yIfcgdMAE=+8 z{(|}q>OZJY$^%dzMP)|))D)l(&;#fKP(RcLpnj4FLuK zBY-ggjiIf8T>#WaYylPka{y`wOMnevC%_u84S@EcF@?s~cH%baIAr4iNG}fH0ziE* z91sEs1|Yq?0A~O?-U;9Uum|i0pg!sdAaO~@qhrx=dx$=?AMJAmpms&&aRZ?KfwsK> z9sqZMC%_xv13;X805mTA0D*u2Ko9`!Lw}?4q2s~;p#Y?f%8TknDmTd|2Ajsa2tCjiF*sYH7UY!2WgARCYc$OL2n z(g9ZI;Xg>sl>|$pxKmQrHgGeXab*8GUq~#Taj4-i=vR?vHbe>w#X37MknNHY6&Hmr zx(YndlOxaOc;x#w@L!`M+a)0?FDgwKD~QuVxvAPfJn9n_xrcp#vp?|7?qj=39BDKw;Qlb(Ps5dfzC%)=pCtFa5@L!&VKEezh znsk}?a1ke?1vM#Asl}(h%|_J|8B<(>smMWOA(7ta5Wu@K=upoE14l+wS`>y5YIRf} zmk@H5TOEV8{;~G!|}*t zHhj_jghP=fc*I2|r9>tFdP9Z$nQvrZ0nUE@&M*`wqpg2l;w4jK zCbS&H%|CFjy&q(CtJU#I&9eK~7CCOv?kgY`DPq=1{AEh=%w*eP&nnmx2o^;&q9V}$ z{^qBWpe7+IiJBn_Jhb3hoh}^GfAz=PMK#iUI(8;pd_47Cham<~Pf?gwyCkM~c| zoiDw>7Y-g`n=Ypys0lqi=hxw0Y_s5z6oqM?6{a92;0z4ZoGO&8mdBGp2aynk6M_KI z<9bUmUz*bM^`b|C=ow89n95U`sao_H5wH=C>>_$(4IkdjJ6;;P=PkH6w#$EXmz=qVt2s2G)nD#%VeT=d)q z4;rWUmz!p2zwxYJ^t2N_Y;$uGW-YSLi=J0RPd)B~4*wXr>Y`_s=;=GSM_VGjw{Fq1 zav32XK_&qyvcto9iym&G$AR@bH9Z&e%%Vq{=tiis&iScD40W z*_gBFDIt11cAx#(m2yjM(bEi`)sRm|9s_5iz?jLRClfj~>b=Ul$ZtRSNcDo84EnUF zER4Co8K;ss+y&sQ1x^(+E0gW9tY|zLOb60vMydr52YAYUzMG<9Z`rWuc@7>f@NCWg z@If`VV}8-|4Ls|>LmANNcofHuh<%?07CrMsHH(3oytq$M?28@_I9;p(j>___d;H>?ofbVZ z;Nb)hXQ&C;NchvpMUNSHP(aLk}G9i6BkZ zL<3!25#?^2 zpy-y++KMM5Rusnx9(M2u8I27^Tz}HM=#e9OqUomd`-eI!7d>0SgZj0WFpfXBr)T$~ z$Ajoezn0dzZ@eRB(Gv%rg&sfh#%g%J5c)N#1n0nm+H_dsXu{n#qqId&EqG9WyU#a} zUvaS|V$m}I9@OK*&Ysc_-rfTvn56cD=y{=FENd~T;l1eLfPszr=#JvI33l{Vv5Ou> z@T>=qm_@&QN1r-I&B4#!(b*ryD|0txWy2^JL{y3pYkQ~+>Id6)zxz3tY(E1YbasX| z?FJ8OIi=~^8!ZenE(@&yXDz4;R1>ui-b&JDP6=$&sfk7C4eJuo8*}4_w1UJ}BYRS8>xj zNbpF*2{j))0^s52W|iX#-`2nAX$KEFYaY^5HaPbw{s+M$4yVl_@W4=wyqLmJ7mW)? z=U^x^%sqd-!%JH8F_3+PW6>HZ9vTOxt4P*WuMGv_b?ZoKa<~)VL2C3G+I{p&?>8@c z^1uU)7rFAdmIY%>H}q>km|amSCwi2cs07TZ?v*WiTETf#}482hEAEO+zV+wq>DJnw%&^R1S9;JSaM9%!RJ(MV4XU zktB?)f13}i`9KZI_FrPKP=bFOgN2pqzvVy)HsknUN=D;!|84WgEp>6kmP2Lx*M0!2 z+l5gtBEAne=zNOXbEolrvhVYSQbW1nsvkUz;L$Jp`EtPK<+jC|=70ya;J91ZA!-HL zGmD-p;6bBAIy@`3Ze;b2^ zn$7_S&C2Q~+f0m-QtvEssNqC{JnXZc?+Xlg5*IyxA2&AOpq3kdlbvlY)?f%6V#_%> zI|QOD&7%i#(u3?RXtsp8A4O-cvzLE}mm_XByNO(m<%(A5RiJ`;E$IzD1wV&fN^FJD z-#`t0XF6nyPUB^?HtUM*sVK)@~%su*PEb zXVR)eEs>&9t6@W?=G|9{P0eT*bU72nf;JP{8S&4r*Yphnc5 z{k*+B<&M>W3MzpkM4}Pso$1}}y`Jg0?w;FSyt}B;1QMf0h#-o0gb<<-Ag(D^^B+3~iz1~t5>gH*T)`gXBrfW$-j2f zk1u)kz{51NXm!TAz2v9fLgX)A^W@T#dC%`5M{@$iAyY}$?z zvh)k_OS9zIhkXCnlNW3T55CYFld~f&S>uka_dj{$$nmE@A%8tFJF*uPiVrS)_NH4u z^Q-;hi=QnKw(CcJEBJ48->aYc?CRw#0k3nVbDMdJIyh<5QQ%YGho3*wwN~dj_$i7H z@|`&yyI?;kTk8fRJ6_7(aKhR(w2ve;dOEa9>-Ifgeet6wKf8uCE02+028A^H?hAkU zxA)xjJanB?*09o0zdrwu#fPqX^Rd&V4}o{NM^bM7?e%MimLCmYv+3Y0Mqy%nq`1EW z3SydxNdzL(Lh8-&Sr0sO(G7Qjf^nO{_GCX#F2Viap^>}oiMMUL_oWN)6)HD0M~;HB z6_iJ2e)5r@|L*zAH01?QD6-q~!gb$z=dOnjYs%~4$;gY{bKA$yKK0YHhcx93P^g`! zU!L0Y)ETeE7joXt4p69_v%T-XZuyCKJgX@efkIyF&KrWQAG>z>K23>0q3@DQzCQP* z+t2^Y8Jcp1+~Ym0_Ik|&M=?_x=dNO7t>Z@*XGz#u+%-C(w}EH%Ht*xkA`k2$G=F49LRLW)gO@Iev4zoR0DD923UodmWjI;+CH- zHNrI5+w&t?$Xlvr+H1w_IobpUPB-c;h8>UV*xX!1RhP1?n|^R?ED09jJCe0Vr`ujm z8*#FTBJ2uNoiR_RJ+Wci$QG|mn@d5f7X?Wa$7$dNoqgfLS{0tc(l`zl6B(Rl)}u9U zoaEp+IX=37|EP#0mQyc__aJn10INDcRcVj676{V8sd^1gmG;EecLl3G1l%8UMA1Bb zg`#<~JsLv%Jr{>0R0AON1!8Cwpqb+JL zXwL_&R?u=ZlW(h`sXXcN{&z)h<%T-gWXj|H^zFpf4V!T@j$&+T$GxN(cx}JyIXi3B z1E!USEg-6?l1H^kBB=~`=|8D;u>;;{I%N@+fFcqe?~&&S@`S;mP+0@~GDX%yt1e`i z%ZYxt>UF!#nQ2uLg`M82=O^t#$*NH&?RDbRGfP&&&eWt;g55L}T15gn^rt2jb|=W@ z)0S0BKv}i?PAiGSmL*kQW=gSuD<4HT)gMECQC8OPbZW==s**152Av|F5D)q>@MK@@ z!dyVRG#Ak>6#~KUbQTR*QJRElb6;O+JM5-2(?R4g0M!kFlXJiz>;l6s){iEoQeZM) z3rqG}VafcESe9miW#xy&vc?WrR(?n<(>MTSW`{&FObpMMG2oj7T8#r1MaYK*VPUZnI#`o|E-tEz?C7NQUua zNwnF-(4o6C(_TB>*DR2gHb7qN^c>W7FO3Rhqg^lX=feV7VG}aZmlg)rAoS8I#*7>& ze!k2O>OePM2@;CuqF`Vr*l>%34vxT8$L_qi&%{sRgf;L9QLHM8g*;8-_1&3t~yx zm}Ah(l9pW$1^hJ6=FrWqA!mgyFWV!l(jL4Kf|N-lMg z)KE_5SY=bu(9%{1vc{hG*@E5}DEXJwjVz63?WLE^5U4Vlz83f>lZ>NXTuEZghsskLAhEQ~j<_?JD{b9jJSGIT@ zcnm=bRx>Jdw=63O2${i9$ipcIZ`o-tP|U+$NJEEI6r;`i^9a$JaT3U+te0WT(uEi+ zv^e)&PFKA&h!)mSi;wW+DI>#QemUU_oFss!Ntftii#V3#tG45g{#bnIh?U1~7hQR+ z7><5nfMbY;F~!-aIB^pS;aE8DD<0bfiH(s3?Jhm?DwHNZt^}loQe0aM5(oure@WVhm)I>5 z-3wcI^As+GL4p~z;HR0_O>iQSWFba#@TGzN%IH#mAq=~EQdNrvY=_`N0ac$4b}N={ zG`v;3PFyh<(&{k1*i!TW=Ou(z{l#V5OKyz@nzT=#;n5n6xmb<3c{$YX?8Ae z;MPGGGeL3S+iW56+qq{{Q_waMEUVoRz97U$T!yD9L6+JT+A&>=@l+RWa-Pe_Q1a&H z(2P4Ul+4o?9QfYqxHlhUeq)k$_vOVV=N$!62MQ1gkMBT}PVsp(CjQ+C$1LXS)nMjd z%vFjA+zTLdMOU@KBU2p29$n@pXXsXMZX|M+Q@eV?({1DR@i%GvflZuMkY^0pb4$iWA-*i+ zFp^?bKrZEM2BHIjZ;6v6bXy$ymkT=rkr0d28a=P=b-Qtrr5@iFqWh)YAYZ>YKngmHA)7HoKr(Wym_EIvL5AC7iSN2N zY6`0AQ>SxYbhrBcU+%6r2BzghM2<2{UZ(?<(PrNYui(5sl4;6TtSxJXZT4`McwUN9 zgb;ocuO8PC>`1XJE-jK(Y>4BSAhtBNq#D>RuY+6?OKJELqS1yFkt+GPrtD|FEwuiW ziMtf5%_s2+zIRf3BM~J%uj%8E!l43H2Lh=ye0=o>xqOHLKAGZ4RK263OE72qI3Oq)8g=4hXFul764ce#BlAXkjrhp0Pg$L6^3oh35UY_rwfUyCyzj>(p~BI6M)pW z6o!Dd0^K8E_tgBZ)4eoHhw7p00~7mMXrZFUI$IN;_hNHu@FNM=h!_a0LV9i?o<*?5 z$xnXTcJa7sHI}YR-BgU;1brb)R0U-6xf57riv3mE}a zT;T+|QW=qmM(}tBocOHx5us%JbvH5)wDSN7d`;K6S)sD!=Md zR;-mX9B?ixl&oR%!n&Z`OAAr-TMgjQGFo6H-q29yDXBy=i)sTx7#psZbmC~x)SFQ< zylm>EQHrMW8j9v&{ + + \ No newline at end of file diff --git a/package.json b/package.json new file mode 100644 index 0000000..3a39411 --- /dev/null +++ b/package.json @@ -0,0 +1,26 @@ +{ + "name": "inference", + "module": "src/index.ts", + "type": "module", + "devDependencies": { + "@biomejs/biome": "^1.9.4", + "@types/bun": "latest", + "@types/lodash.isequal": "^4.5.8", + "@types/react": "^18.3.11", + "@types/react-dom": "^18.3.1", + "@vitejs/plugin-react": "^4.3.3", + "sass": "^1.80.3", + "vite": "^5.4.9" + }, + "peerDependencies": { + "typescript": "^5.0.0" + }, + "dependencies": { + "lodash.isequal": "^4.5.0", + "react": "^18.3.1", + "react-dom": "^18.3.1" + }, + "trustedDependencies": [ + "@biomejs/biome" + ] +} \ No newline at end of file diff --git a/src/App.tsx b/src/App.tsx new file mode 100644 index 0000000..a765434 --- /dev/null +++ b/src/App.tsx @@ -0,0 +1,47 @@ +import { ppJudgement, type rule } from "./lib"; +import { + contextVar, + ppAnyExpr, + type AnyContextEntry, + type anyExpr, +} from "./lib/core"; +import defaultRules from "./lib/defaultRules"; +import type { ContextEntry } from "./lib/pi"; + +import "./global.scss"; + +const globalContext: ContextEntry[] = [ + { + x: { kind: "string", name: "Type₀" }, + type: { kind: "var", x: { kind: "string", name: "Type₁" } }, + }, +]; +const database: rule[] = [...defaultRules]; + +interface InferenceRuleProps { + rule: rule; +} + +export function InferenceRule({ rule }: InferenceRuleProps) { + return ( + <> +

+ + ); +} + +export default function App() { + return ( +
+ {database.map((rule) => ( + + ))} +
+ ); +} diff --git a/src/global.scss b/src/global.scss new file mode 100644 index 0000000..f8c83ce --- /dev/null +++ b/src/global.scss @@ -0,0 +1,20 @@ +.container { + display: flex; + flex-direction: row; + align-items: center; + gap: 8px; +} + +.inferenceRule { + border: 1px solid gray; + border-radius: 8px; + padding: 8px; + box-sizing: border-box; + text-align: center; + box-shadow: 0px 1px 8px lightgray; + + hr { + border: none; + border-top: 1px solid gray; + } +} \ No newline at end of file diff --git a/src/index.tsx b/src/index.tsx new file mode 100644 index 0000000..7141563 --- /dev/null +++ b/src/index.tsx @@ -0,0 +1,5 @@ +import {createRoot} from "react-dom/client" +import App from "./App"; + +const root = createRoot(document.getElementById("root")!); +root.render() \ No newline at end of file diff --git a/src/lib/core.ts b/src/lib/core.ts new file mode 100644 index 0000000..c1b426e --- /dev/null +++ b/src/lib/core.ts @@ -0,0 +1,30 @@ +import { + ppContext, + ppContextEntry, + ppExpr, + type context, + type ContextEntry, + type expr, +} from "./pi"; + +const _contextVar = Symbol("contextvar"); +type ContextVar = { [_contextVar]: true; name: string }; +export function contextVar(name: string): AnyContextEntry { + return { kind: "contextvar", name }; +} + +export type AnyContextEntry = + | { kind: "contextentry"; entry: ContextEntry } + | { kind: "contextvar"; name: string }; + +export type anyExpr = expr | { kind: "context"; context: AnyContextEntry[] }; + +export function ppAnyExpr(e: anyExpr): string { + if (e.kind === "context") { + return e.context + .map((ce) => + ce.kind === "contextvar" ? ce.name : ppContextEntry(ce.entry) + ) + .join(","); + } else return ppExpr(e); +} diff --git a/src/lib/defaultJudgements.ts b/src/lib/defaultJudgements.ts new file mode 100644 index 0000000..69d9473 --- /dev/null +++ b/src/lib/defaultJudgements.ts @@ -0,0 +1,15 @@ +import { ppAnyExpr } from "./core"; +import type { judgementKind } from "./judgements"; + +const defaultJudgements: [string, judgementKind][] = [ + [ + "contextHas", + { + arity: 3, + pp: ([ctx, term, type]) => + `${ppAnyExpr(ctx)} ⊢ ${ppAnyExpr(term)} : ${ppAnyExpr(type)}`, + }, + ], +]; + +export default defaultJudgements; diff --git a/src/lib/defaultRules.ts b/src/lib/defaultRules.ts new file mode 100644 index 0000000..6c7b9da --- /dev/null +++ b/src/lib/defaultRules.ts @@ -0,0 +1,58 @@ +import type { rule } from "."; +import { contextVar, ppAnyExpr } from "./core"; + +const defaultRules: rule[] = [ + { + premises: [], + conclusion: { + kind: "contextHas", + args: [ + { kind: "context", context: [contextVar("Γ")] }, + { kind: "var", x: { kind: "string", name: "ℕ" } }, + { kind: "var", x: { kind: "string", name: "Type₀" } }, + ], + }, + vars: ["Γ"], + }, + + { + premises: [], + conclusion: { + kind: "contextHas", + args: [ + { kind: "context", context: [contextVar("Γ")] }, + { kind: "var", x: { kind: "string", name: "zero" } }, + { kind: "var", x: { kind: "string", name: "ℕ" } }, + ], + }, + vars: ["Γ"], + }, + + { + premises: [ + { + kind: "contextHas", + args: [ + { kind: "context", context: [contextVar("Γ")] }, + { kind: "var", x: { kind: "string", name: "n" } }, + { kind: "var", x: { kind: "string", name: "ℕ" } }, + ], + }, + ], + conclusion: { + kind: "contextHas", + args: [ + { kind: "context", context: [contextVar("Γ")] }, + { + kind: "app", + left: { kind: "var", x: { kind: "string", name: "suc" } }, + right: { kind: "var", x: { kind: "string", name: "n" } }, + }, + { kind: "var", x: { kind: "string", name: "ℕ" } }, + ], + }, + vars: ["Γ", "n"], + }, +]; + +export default defaultRules; diff --git a/src/lib/index.ts b/src/lib/index.ts new file mode 100644 index 0000000..5551d7f --- /dev/null +++ b/src/lib/index.ts @@ -0,0 +1,20 @@ +import { ppAnyExpr, type anyExpr } from "./core"; +import defaultJudgements from "./defaultJudgements"; +import type { judgement, judgementKind } from "./judgements"; + +export const judgementKinds = new Map(); +for (const [name, kind] of defaultJudgements) { + judgementKinds.set(name, kind); +} + +export function ppJudgement(j: judgement): string { + const kind = judgementKinds.get(j.kind); + if (!kind) throw new Error(`could not find judgement kind ${j.kind}`); + return kind.pp(j.args); +} + +export type rule = { + premises: judgement[]; + conclusion: judgement; + vars: string[]; +}; diff --git a/src/lib/judgements.ts b/src/lib/judgements.ts new file mode 100644 index 0000000..9bb16fc --- /dev/null +++ b/src/lib/judgements.ts @@ -0,0 +1,8 @@ +import type { anyExpr } from "./core"; + +export type judgementKind = { arity: number; pp: (args: anyExpr[]) => string }; + +export type judgement = { + kind: string; + args: anyExpr[]; +}; diff --git a/src/lib/pi.ts b/src/lib/pi.ts new file mode 100644 index 0000000..2a8098b --- /dev/null +++ b/src/lib/pi.ts @@ -0,0 +1,400 @@ +import isEqual from "lodash.isequal"; + +export type expr = + | { kind: "var"; x: variable } + | { kind: "universe"; level: number } + | { kind: "pi"; abs: abstraction } + | { kind: "lambda"; abs: abstraction } + | { kind: "app"; left: expr; right: expr }; + +export interface abstraction { + x: variable; + type: expr; + body: expr; +} + +// ============================================================================= +// Substitution + +export type variable = + | { kind: "string"; name: string } + | { kind: "gensym"; name: string; n: number } + | { kind: "dummy" }; + +export interface Substitution { + x: variable; + repl: expr; +} + +let ctr = 0; +export function refresh(v: variable): variable { + const n = ctr + 1; + ctr += 1; + switch (v.kind) { + case "gensym": + case "string": { + return { kind: "gensym", name: v.name, n }; + } + case "dummy": + return { kind: "gensym", name: "_", n }; + } +} + +export function subst(s: Substitution[], e: expr): expr { + switch (e.kind) { + case "var": + return s.find((sub) => isEqual(sub.x, e.x))?.repl ?? e; + case "universe": + return e; + case "pi": + return { kind: "pi", abs: substAbstraction(s, e.abs) }; + case "lambda": + return { kind: "lambda", abs: substAbstraction(s, e.abs) }; + case "app": + return { kind: "app", left: subst(s, e.left), right: subst(s, e.right) }; + } +} + +export function substAbstraction( + s: Substitution[], + { x, type, body }: abstraction +): abstraction { + const x2 = refresh(x); + return { + x: x2, + type: subst(s, type), + body: subst([{ x, repl: { kind: "var", x: x2 } }, ...s], body), + }; +} + +// ============================================================================= +// Type inference + +export type context = ContextEntry[]; + +export interface ContextEntry { + x: variable; + type: expr; + value?: expr | undefined; +} + +/** Returns the type of the definition associated with `x` inside the context `ctx` */ +export function lookupTy(x: variable, ctx: context): expr { + const res = ctx.find((entry) => isEqual(entry.x, x)); + if (res === undefined) + throw new Error( + `unknown identifier ${ppVariable(x)} (ctx: ${ppContext(ctx)})` + ); + return res.type; +} + +/** Returns the value of the definition associated with `x` inside the context `ctx` */ +export function lookupValue(x: variable, ctx: context): expr | null { + const res = ctx.find((entry) => isEqual(entry.x, x)); + if (res === undefined) + throw new Error( + `unknown identifier ${ppVariable(x)} (ctx: ${ppContext(ctx)})` + ); + return res.value ?? null; +} + +export function extend( + x: variable, + t: expr, + value: expr | undefined, + ctx: context +): context { + return [...ctx, { x: x, type: t, value }]; +} + +/** Infer the type of the expression `e` in context `ctx` */ +export function inferType(ctx: context, e: expr): expr { + function inferType(ctx: context, e: expr): expr { + switch (e.kind) { + case "var": { + const ty = lookupTy(e.x, ctx); + return ty; + } + case "universe": + return { kind: "universe", level: e.level + 1 }; + case "pi": { + const { x, type, body } = e.abs; + const k1 = inferUniverse(ctx, type); + const k2 = inferUniverse(extend(x, type, undefined, ctx), body); + return { kind: "universe", level: Math.max(k1, k2) }; + } + case "lambda": { + const { x, type, body } = e.abs; + inferUniverse(ctx, type); + const te = inferType(extend(x, type, undefined, ctx), body); + return { kind: "pi", abs: { x, type, body: te } }; + } + case "app": { + const { x, type, body } = inferPi(ctx, e.left); + const te = inferType(ctx, e.right); + checkEqual(ctx, type, te); + return subst([{ x, repl: e.right }], body); + } + } + } + + const result = inferType(ctx, e); + return result; +} + +export function inferUniverse(ctx: context, t: expr): number { + const u = inferType(ctx, t); + const n = normalize(ctx, u); + switch (n.kind) { + case "universe": + return n.level; + default: + throw new Error("type expected."); + } +} + +export function inferPi(ctx: context, e: expr): abstraction { + const t = inferType(ctx, e); + const n = normalize(ctx, t); + switch (n.kind) { + case "pi": + return n.abs; + default: + throw new Error("function expected"); + } +} + +export function checkEqual(ctx: context, e1: expr, e2: expr) { + if (!equal(ctx, e1, e2)) + throw new Error(`expressions ${e1} and ${e2} not equal`); +} + +// ============================================================================= +// Normalization and equality + +export function normalize(ctx: context, e: expr): expr { + function normalize(ctx: context, e: expr): expr { + switch (e.kind) { + case "var": { + const n = lookupValue(e.x, ctx); + return n ? normalize(ctx, n) : e; + } + case "app": { + const e1 = normalize(ctx, e.left); + const e2 = normalize(ctx, e.right); + switch (e1.kind) { + case "lambda": { + const { x, body } = e1.abs; + return normalize(ctx, subst([{ x, repl: e2 }], body)); + } + default: + return { kind: "app", left: e1, right: e2 }; + } + } + case "universe": + return { kind: "universe", level: e.level }; + case "pi": + return { kind: "pi", abs: normalizeAbstraction(ctx, e.abs) }; + case "lambda": + return { kind: "lambda", abs: normalizeAbstraction(ctx, e.abs) }; + } + } + + const result = normalize(ctx, e); + return result; +} + +export function normalizeAbstraction( + ctx: context, + { x, type, body }: abstraction +): abstraction { + const t = normalize(ctx, type); + return { x, type: t, body: normalize(extend(x, t, undefined, ctx), body) }; +} + +export function equal(ctx: context, e1: expr, e2: expr): boolean { + function equalHelper(e1: expr, e2: expr): boolean { + if (e1.kind === "var" && e2.kind === "var") return isEqual(e1.x, e2.x); + if (e1.kind === "app" && e2.kind === "app") + return equalHelper(e1.left, e2.left) && equalHelper(e1.right, e2.right); + if (e1.kind === "universe" && e2.kind === "universe") + return e1.level === e2.level; + if (e1.kind === "pi" && e2.kind === "pi") + return equalAbstraction(e1.abs, e2.abs); + if (e1.kind === "lambda" && e2.kind === "lambda") + return equalAbstraction(e1.abs, e2.abs); + return false; + } + + function equalAbstraction( + { x, type: type1, body: body1 }: abstraction, + { x: y, type: type2, body: body2 }: abstraction + ): boolean { + return ( + equalHelper(type1, type2) && + equalHelper(body1, subst([{ x: y, repl: { kind: "var", x } }], body2)) + ); + } + + return equalHelper(normalize(ctx, e1), normalize(ctx, e2)); +} + +// ============================================================================= +// Pretty printing + +export function ppVariable(v: variable): string { + switch (v.kind) { + case "string": + return `${v.name}`; + case "gensym": + return `?${v.name}$${v.n}`; + case "dummy": + return "_"; + } +} + +function occursIn(x: variable, e: expr): boolean { + switch (e.kind) { + case "var": + return isEqual(e.x, x); + case "universe": + return false; + case "pi": + case "lambda": + if (occursIn(x, e.abs.type)) return true; + if (!isEqual(e.abs.x, x)) return occursIn(x, e.abs.body); + return false; + case "app": + return occursIn(x, e.left) || occursIn(x, e.right); + } +} + +export function ppExpr(e: expr): string { + switch (e.kind) { + case "var": + return ppVariable(e.x); + case "universe": + if (e.level === 0) return "U"; + return `U(${e.level})`; + case "pi": + if (occursIn(e.abs.x, e.abs.body)) { + return `(∏ (${ppVariable(e.abs.x)} : ${ppExpr(e.abs.type)}), ${ppExpr( + e.abs.type + )})`; + } + return `(${ppExpr(e.abs.type)} → ${ppExpr(e.abs.body)})`; + case "lambda": + return `(λ (${ppVariable(e.abs.x)} : ${ppExpr(e.abs.type)}), ${ppExpr( + e.abs.body + )})`; + case "app": + return `(${ppExpr(e.left)} ${ppExpr(e.right)})`; + } +} + +export function ppContextEntry({ x, type, value }: ContextEntry): string { + return `${ppVariable(x)} : ${ppExpr(type)}${ + value ? ` = ${ppExpr(value)}` : "" + }`; +} +export function ppContext(ctx: context): string { + const ss = ctx.map(ppContextEntry); + + return `[${ss.join(", ")}]`; +} + +// ============================================================================= +// Testing + +function test() { + const ctx: context = []; + + const dummy: variable = { kind: "dummy" }; + const varify = (name: string): expr => ({ + kind: "var", + x: { kind: "string", name }, + }); + const define = (name: string, e: expr) => { + const type = inferType(ctx, e); + ctx.push({ x: { kind: "string", name }, type, value: e }); + }; + + // N : Set lzero + ctx.push({ + x: { kind: "string", name: "N" }, + type: { kind: "universe", level: 0 }, + }); + const N = varify("N"); + + // z : N + ctx.push({ x: { kind: "string", name: "z" }, type: N }); + const z = varify("z"); + + // s : N -> N + const NtoN: expr = { kind: "pi", abs: { x: dummy, type: N, body: N } }; + ctx.push({ + x: { kind: "string", name: "s" }, + type: NtoN, + }); + const s = varify("s"); + + const f = varify("f"); + const x = varify("x"); + const threeExpr: expr = { + kind: "lambda", + abs: { + x: { kind: "string", name: "f" }, + type: NtoN, + body: { + kind: "lambda", + abs: { + x: { kind: "string", name: "x" }, + type: N, + body: { + kind: "app", + left: f, + right: { + kind: "app", + left: f, + right: { kind: "app", left: f, right: x }, + }, + }, + }, + }, + }, + }; + const three = varify("three"); + define("three", threeExpr); + + const nineExpr: expr = { + kind: "app", + left: three, + right: { + kind: "app", + left: three, + right: s, + }, + }; + const nine = varify("nine"); + define("nine", nineExpr); + + const evaled: expr = { + kind: "app", + left: nine, + right: z, + }; + define("result", normalize(ctx, evaled)); + + console.log("ctx ="); + // biome-ignore lint/complexity/noForEach: + ctx.forEach(({ x, type, value }, idx) => { + console.log( + ` ${idx === 0 ? "[" : ","} ${ppVariable(x)} : ${ppExpr(type)}${ + value ? ` = ${ppExpr(value)}` : "" + }` + ); + }); + console.log(" ]"); +} + +// test(); diff --git a/tsconfig.json b/tsconfig.json new file mode 100644 index 0000000..238655f --- /dev/null +++ b/tsconfig.json @@ -0,0 +1,27 @@ +{ + "compilerOptions": { + // Enable latest features + "lib": ["ESNext", "DOM"], + "target": "ESNext", + "module": "ESNext", + "moduleDetection": "force", + "jsx": "react-jsx", + "allowJs": true, + + // Bundler mode + "moduleResolution": "bundler", + "allowImportingTsExtensions": true, + "verbatimModuleSyntax": true, + "noEmit": true, + + // Best practices + "strict": true, + "skipLibCheck": true, + "noFallthroughCasesInSwitch": true, + + // Some stricter flags (disabled by default) + "noUnusedLocals": false, + "noUnusedParameters": false, + "noPropertyAccessFromIndexSignature": false + } +} diff --git a/vite.config.ts b/vite.config.ts new file mode 100644 index 0000000..081c8d9 --- /dev/null +++ b/vite.config.ts @@ -0,0 +1,6 @@ +import { defineConfig } from "vite"; +import react from "@vitejs/plugin-react"; + +export default defineConfig({ + plugins: [react()], +});