From 7d147032428e6787298ddf5a269b96b2ed584c83 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Thu, 12 Sep 2024 18:38:07 -0500 Subject: [PATCH] initial --- .gitignore | 178 +++++++++++++++++++++++++++++++++++++++++++ README.md | 9 +++ biome.json | 32 ++++++++ bun.lockb | Bin 0 -> 36772 bytes package.json | 22 ++++++ remark-agda.agda-lib | 2 + src/index.ts | 168 ++++++++++++++++++++++++++++++++++++++++ test/.gitignore | 1 + test/Simple.lagda.md | 27 +++++++ test/index.test.ts | 38 +++++++++ tsconfig.json | 27 +++++++ 11 files changed, 504 insertions(+) create mode 100644 .gitignore create mode 100644 README.md create mode 100644 biome.json create mode 100755 bun.lockb create mode 100644 package.json create mode 100644 remark-agda.agda-lib create mode 100644 src/index.ts create mode 100644 test/.gitignore create mode 100644 test/Simple.lagda.md create mode 100644 test/index.test.ts create mode 100644 tsconfig.json diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..509c6d3 --- /dev/null +++ b/.gitignore @@ -0,0 +1,178 @@ +# 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 + +# Agda build directory +_build \ No newline at end of file diff --git a/README.md b/README.md new file mode 100644 index 0000000..63d4c5f --- /dev/null +++ b/README.md @@ -0,0 +1,9 @@ +# remark-agda + +## Contact + +Author: Michael Zhang + +License: GPL-3.0 + +Send questions to ~mzhang/public-inbox@lists.sr.ht \ No newline at end of file diff --git a/biome.json b/biome.json new file mode 100644 index 0000000..72ea95b --- /dev/null +++ b/biome.json @@ -0,0 +1,32 @@ +{ + "$schema": "https://biomejs.dev/schemas/1.9.0/schema.json", + "vcs": { + "enabled": false, + "clientKind": "git", + "useIgnoreFile": false + }, + "files": { + "ignoreUnknown": false, + "ignore": [] + }, + "formatter": { + "enabled": true, + "indentStyle": "space", + "indentWidth": 2, + "lineWidth": 80 + }, + "organizeImports": { + "enabled": true + }, + "linter": { + "enabled": true, + "rules": { + "recommended": true + } + }, + "javascript": { + "formatter": { + "quoteStyle": "double" + } + } +} diff --git a/bun.lockb b/bun.lockb new file mode 100755 index 0000000000000000000000000000000000000000..23e0969a07c13ed4e0779eacd541ae6e06e3158b GIT binary patch literal 36772 zcmeHwc|4R~^#5Q&%O{eQO4i6ScA})RMT(RZrEG(-jm%ivRFt$xMbd(#gcgM)6&0;2 zZCaF667Bn*-?`7sHIEon-#@ z6c2X>{H0Kk0sTQQ*gb?rH=t1HL2L$_L1$%9DU<;apWcH)=?i>4moEY?iShy73;1hc z3PlR|E#S!BWY9z9ILVE-0eocNYH)!BaFw2%{A7S5eL>(ufZM|j%5M~xD*#7$ZUBbz zdj|Rgfky*Jei#F|h_8V^DBTLkL=m_@@S(teK)f9A2VgwPcNE0y0M`KySw<&-lLrGg z1&-_w<=#62mxp^5;3&Voz@>rD04E__L*Ph0n0qe-9Hn~>nIL`{II0IPx<{xF*cixy zKM(`~2ia>5nW6k;zz$R{8puEtEe*>3fJcQh*q%^-sc?_%wt&K+{5621a>jAv*}##$ zrzbNsh)tB8@TVjc3gNp0NA<7^ILdb>Hy(UU)Taa#2HE)uoR9op2Y(R$IpD}22Y{n| zHv@;PqL*;x{#-d=6ZvKT80hN!UO!Vwc5we6hk8jLQXV*9^%l=OpV6ZG7cgUumFvHY z{ZM-t-DDy9aZW|w`Fqr#SPz)C>Ql`01m6!LswefAu9F{qxm;Q6+4OG@trR8>8fG?2 zVTo$t7|E%V3}g4EyD{ywPO8*1?z`zbuF!uJcc-Zj`$_S2X2PYf2`aBO?T4St&61N3 z4e0IrnW3L^Wyj4iQ-)6Ta4;HRCUr)0+6v7<&kpvr54N9We`I^X;2VyNylYcLug`9F zaCLlQxbw_~r|Nq=8$O0+W=?JRn6a(qgnoGV0_V^*A4M{Lv<5&AEpOP_32H@7M`k9ir&s#w~1 zaQ{T=?s>`UXjhF^(}u>*Nl7T1a9*MI?%ALR+VULd&FmE}mDJJ6J%{EkbXe!{sMy zS9_(JMN!X0=iW%k&(d=77f{mGUFz2R+1zRK$MmVsSX8SpVG&ha)h_nO#+_D|&kL&_ zv(;Yme*SZxsyK;f3W-`SYm^Je824nFR5m-L9?iUv5}D?Am9b-MK=!;-%KN4#j9a>I z;zPxfRQjL^8~sj=rR@>*yEE)n!xugO$BIIN$MUSl4xM3?CiZSqvaIRl^lHOHW+yJa zos)M*%AowCU3J>;^9R60o`fovNCg{U(Nrdj&h4m+b zf*DDl3)3aT`l~_T81#j>8klzlfb}ateKx+3oblJ`g|3B5nz2$Fjyb-(LIj)C25DZIIRijkK^Xw-MUABSbqUGf9y9L z-(jYtNSy8fS0Cm5C;30->SH`?2Pvx#FLC-oP;uH^|Dl99zC$HaBu-}y`gVVzUj+K7 z{zL#9l^^4hvg+^>r)vg%BX0e5x9uZ9tgiq{Q$Zi5HALuc9bo-^pl?Ac|L^L*|${4Ia1{#hzVNni%e&$@ebHa) zi$cYr_J{DgTXtj{&YunXsQ=;nuI$Egoc=WE+k-yJ8^_@^opGGDKfGL^`2%kEn0Ka& zWLSR^=#K||)P8>_VEru6$Noe5-Sr{X&w+*?1o`9p?%IIU4}$kgx4+Pj0DWK3$97}f zuI#|+-h%!lQvNu;yZWYL6iPfvAKTGg{j;Dy3iP{M?-&=`xd&c;Xa7b1J>aF8JpN<+ zt~k!$8T85dccq8rSicbT{Yds>c~>0k%SsSyFn`?sLP6h!l>hJ69}Ctm+(`Oe*^TAc z{%fHBH{~BA`FHtm1AV8zu>aj(>f6AAipO8%p9}iBppW_wdIrLDpj!d^{~qXTaPvoX zkDsGmfnfcfu-Jq9FVctMv|9n|PXc{?$R8;o+ZE77Hv-m=27UDW`qS~_3h3K_K0Jnh zE8zUqU~y|A=)*LE2spkgFq|$A^ilcoeRs=&(?0-xG=5_}%)6Vv>mW}5?{2+gT%7-5 z(8tfu?v5P@1M7>yA|bN>PxGGz`l$Z@R6iH=$^P$d8L<6zpl<;ABRxd89iTFH7O=hy ztgDVD>BI79w*uA=0DaW|U>G9$9z4#w6|nw6&>s)_X#NeC-F^qd`tLvq`47E+B8=bd z|JqPsT>kF*4zg)&KUza66lbpg{zN|x^r!!Y{yosg^WQ(oUjr7=ZT}+waL{-73;na8 zkKW&Yr|pvcKVaD3mEQ~W|EBy$LEi-IM{N(SA>ek2Z0staF&_~cJMjA}Oh<`+4AV*? zAda3(Fw7Fz(A^1+`YG}mR6h|q;z$neB?6fvI~9SDT#1l!IO;~Q-hOWt!b@i;!m3ft?iS;zf(ewc-_rk>U6ImXXC>YS})dZ zl1{(&&YoK6`Ed0PW81!i`(GmAqP~p-RqI{ztdZBo-ez62DiO`q-@quFAbF2|_duOV z#+!R<9HpP1fAh#@QGb^+hu>AI?-krqnxK7mLgi|P`;xIyvjh)rAmO4h2nXt&^bNyQ z4}?q9U4Ej+_IaFrd&1SL4?hjMwl&<<)FZfH$uVtznV@HLCtni#DwQC1WPUG`xj(!; zzlj{#^TGc3_qm=VTr@`FKwY2kKyIqTi8XNRH?XU*$H8P{j19^ z#}6gpqGurvRCV1UvMqtGxnV~aDlUGetS4Z0Fv_Sb)YUMc;_QhH-;Z4%oU`-k`ZTA^ zSmQ)hx_numgY7@7*H7yn2^T%HaiFddzkPjK@1p9=M^m?YfAMz{j;mE^ z-dQp?t7Y|~5eD}^Z+Loj{{(~0U#GvTUTgkr(x~F~0+jlkk6tSlTPqc~${Z!(qOlwY z>J@6zwRB2)`m#jY@iToLW^X;P?^$lvf#TsCcfE}Iru{5*hqm4cjnvT%I`kh463Wd6 z?oqy|JTX}GzZUhPrGcB4kZ{R!M{1F$s`_MsH7Og<&EB6Uaddrnu3^vgV-<@>6o!;| zpRm^2Fz#N|bH9t0XQK^F-hXNuS;g%A_I|+{&%(i*9@B4K^C#h=X9W(_&z}{(zSEp? zyXVtm78l2QXn}bEpgL`IQPZ$7&-dAgwDt=^nvC+Kv?M?Ot3iN_J z5-ytG;Xu7Q@_6>!72@aRkG-EJI&oyLLzPWsdIE9E7xVJ1lqIZ^-&?mw2+osfh&vywW$4;*tC`!U5zi&~m^)K1HV!o10O4LPjwaqRI2M5GGzkK)x z`*w}JXwj`2DPfa_j}NZD9l1?y+ax#9PZAl+PVkZq(ZxNpFuw$j+#VvJS_AeV>tG?KAd4AxQzPoon&l6tPy!L|bmy7Z7 zCzS_&fBd5Vc&DYuH_ayD;(0BCr}j4b;Jh;_D@XB~aJ`=HlbNQ+{G!5UE~=PawlK}{ z;Jc5O18+S|QW~K9!a5--?kr=gu&>v1^W9+^ic{h}VqK!=l5o)+4+rWDYfsq~R;IG! zGE>>QF*BbI@HvclK1J z;i@<9-mDCAzJeJCqW$e&j|UH(jm(tLmZ`4GMH3Q}H4W~)96 zj8-`sy>qQn`HQ^mCyz(0-Do$~Vi*Z`00sq4HKjf{^qO9}!0za2P4WA$SFO_@MZeRd zyeUO#L)1WxCfj}QR|?5ZG^ky0H0|;Ni|}XW3Cs~{!jaxneFY0{E*KC`!j&T9vQO>3 zC@)h>ag0SUcKHX%qDph~O-MP~oYuCTcKfNk}BCc0? zQ+JSca&XSJA*bv~xafTe2dc^VETLYN?}k^p4!T+AQyJ8^M5(8pknp9T=A`sg=1(uT z47V$b1U{7My*g}g&_QwB?0)MvoSom8EEIT{dV#&-HVGG&n_2_)q=jIj@(3fh#1R&j z&KD;+p4#d*IsUrv8k)V3tCq`t=?li=r2-nx&rxt3siV4Q+c~2gpV+;R*15b)vA&Tk zcmFvF7rocvK%M!`G_XLsAwBckuq@x|WQ~QdkITPES8o}+IJ;obtWgqfL(cEby3!{} zJ74o||CxO+$WF`nk#9Dv%%@uK>XX3t{Ybd5JklDdQZMC)-+eb<)oh_q(+BzFm3LTq z7e*J3YB-uT>&?7W3m>I7)HPn~8I6mj_8u>wsA>E?hw6@!y4u$veDJuS!`|S+Of-9k}F<(kr=v4wK7v{;ln95pKLA$ zO08bF&9?f;`^DaeOU>;?$m1`5k44zjao)Wo8Z_L;hOA3B)2i-y0axyc#!a&&n245 zK62u>Qkjke7dK5#NsjKnDBZn>{_5CKZq)gXSI&I0BH_xmqJke>q_i5w5A`l8E1IQZ z`XEDQoW{}5OH3ME`pr@)IA9%?vSsuH*9)f(`F&*FSNK>ltK6&EH~Hz+WW}$Ka|&7x z#*yb|a%9}s$${@}oS#hEu=Q0$>Z3PuUZt7x!!43`D7~Uq&Dm@#zwY`flQTUd%-8x& zOX|DqNu_MGLSn$f%hqcimfN~q78^pcSDuWUrIl#>dK1Otrf8!{l!(BwF-nVrDlUK|hN3-T=TD-_+X$ve!U$v)?Zd9tue#MMM8!7!0 z3&fK|^M}9x#311+l5x{-McL9<%Xm5O^WU2_p z9Ztqw=e;K2bLfTxJudYM3jf?E?5%R+keJ@8{U$v0nYmLX^Lm-9Q_0L&Gikk7ZazEZ zbUz=ZY#y&XWLp36Hpg71uKkft!c`{YN@~zY9I{%^J`%Y9L$cq@cszgQf!7$3+ zIAE^7vBpiaWn?K`PpQTgQi79W8>OJhK>fX&)Lm%7tOqVuWHmhmm@W8;P zf-wONhANxM?O_BN_wJyX_O`N_mn?M)#R|g3GX0+Ib`B2EpA-2E|In`dlyF#a?)Tj{PaSgbIiT7_ItPqKfR?jKzDdT?B2ZI+cY(g?1>*NedCtX@LQ++yiylk*}BAqY_A#_ zcl5>3+e4pCnX7Yd#-J-Ze9QfneYZ{t3Mlw)>tk45z3bFg`@@zSl8$^jGh$f!^j-Aq zn=#^x%5oN{?)18Eu3R)djAXAm8Ta7O`5FIF%9~nxNXV==*1Ei1Z0mT@@7Awp>&JPg zjrzW0Tj1_9E2h-_kP;S_{v3O_=Wck-DT0v zrH0;)tWEdSvr$fSZZE9ER47RyR&C^{r8=8TOh!sx{bW$8 z_V|Qc|Hozlej83DSgLQ-Jx;>aCgVQM8kPO>lu!Q3#PsyC{(-xupDbncgr@pTxm;j^ z%kj?|z2r-il=gcL{-HZm+5FkI-6jWyor|zaT$vxc{N}n#!6aNAGVZZtkIV$6=a1M6 z9S`@k?%{W1Mf$G0G~E+>O`9&Qj}RUescbAAncHts!LgHNu6@=Q1+PD&b8aBL_OgxI z2a(F+3=%GU+ieZhNjX0?qHFGK78pLy_R`jb^E2PM?Y&sUpzE0T{ZGHA{Df13!>Kko zOFm7Q^*&mXWlHf9v<$72{G_+%V{PH1H1$dnE?Pgvf!fnTSMAuGmX_N_Cd+P2eiMKH z(A++S{^yJQ9Seu%S||Hzm6V*$${XuhTcWBkWZB*yHXXvd`8SaR~axZ;`gnDTxzwqL(v+481lS5D%->?1CkMa*?! zW)gOe-{uEge_ldopqSR0h^__E0N zyt`4ds6>ZYt{@!pE4EA^_3MT%e?1rSgIO)K#_!Nh>bs{tl}tf^PIzzF8d_=+)0mLbYU)>go-XH@|&* z^0w5&>lp$|d-+zsFWF>KxIJvoNe_j(;U_+OuJqeBabI8UD-kAFqjSjXC8IGYaOzWM z){%k>UV-Os@2_%{8y;cpd1;?-rNCR?;bYFlz6w67mEp8PdH?gq0cW3ms2Q8fdLcWH z@@&F3#S?||E$?|v+eot4gp6Ano#A}Lsy4sS`l3Z?LYaEKlkzS4zCF{99=^M8_5nMa z!A7-8KgJ0&%xbJ=d_O*^f?DW(&A1O+ZC}iBmr+JD#*lEwka4#%qlSd;Y1*wTDCj4h zt7v5SlX3p+^F4v4O7kwVYPSBUie6J1v{A_FXZQ}MX6dlH5P?X)5i3$&yxA?FYPLsBOKdw-;%(mJm%&)(a8C-p2ms#_q zmD?rfojfIS>pls0JQ+7|p3ywn$J0|L(ic~+ej~dvEZ%9rfK8WtGA6%jIx#rwJ(V>( zLg;yUrD4Rzy58A7QO?`$ZK_lCj2~T7XqmdKiQM1J$he9k<-2a~-S}#qXwrz9D{99N zRpm^dl*ODWer%Pzld08~k2z;g4v|`>aosJ#UwmfDT!oq~#VG;O3XgoHs%*q|M3L+@ zC*xXeXsXWb-;$eV#cZJ@1!v9N9N;-t*ZRspiP`h06H;PgTLRYz-xbO3u}kY!Q>yvR z^w^%E0o$EsY}hngmmS=HItkZ;jC=EE-4d#2v-H(67r*Pa1?Qt$M0K>U7CyZ-tZ+}% z1%v9_DR0x6hnsDkic|#Hc`?}^_kCNfYvNcglHSYbZTeF$60Ri~H(+A+v&?>TDugTC zZ#-W1evEbWtX|YLMa7O953UqfC=H$+^Krvsm6NJEC4rYL-!}G&tZHu5%rUM$=&rv+ z;H{Xq~co5E|cRu@8?@t z9ymJe)QDHb`Ad5j9B`1!)(G2Jv_xcdE(sTZ*F^Bt`DztcjbgJB4u=(dt*ffLne7$e z-+Q7;m7w;h>#>U7#;bbzo-JIvN~Gq+hdAH9ePlPE8-Ld*sBvoTt5=cCQx1Y8Tx+tu zHX#mC22Cjt)@q(4>>`SKRUmrU%p6=_uS~9hkz4N5u71mh1ou>h(V?ipDivnyIUPW_T2Kj@giC8euPuS&ku#vb1^C;RA-@yVkl&hFgk^kY`i z^GDN-N^Me}3%RlHEXtVjFdEv)#eZ=CH-Y!mO ztG3!qsGTJJRa(6!^>ik+T1HxBQoT>({Nvw@U;Qw;x$L_4k$aO@tS>*KMY7j{jQdtw zZ*9prJJZmsTh;2b0$!}&IqHq>^|8Az%{5p1dU-|6rE`;vGT!iUUb*A9e;kmYjP)nU$!5fS4b&AnO|c|CGu)BzvUiHiyxx2l9Knlo#2NMUawwGq-I z2IifPBkbjTH+3T88ZZUUuQ0Q|a)AC+e)YYlpOd~AIlLcbG%A0$r}!?TU^ z*Qf8=MfPF~k~B(cZ!%Y{{5jv$`_4<(2VbNw0Per=&jbHF@XrJPJn;Xo2heY3JQ&PC zI&c;EPzAqji2mR14Kyb}0dvmX@BRJv`1?J7{Y(AN1OGhm&jbHF@XrJPJn+v0|2*)| z1OGhm&jbHF@XrJPJkV_qlyTSauXA}X6IO_)CL@T&b`J>9#5>SxI)>2crgFO4ax6v^ zo$0M1r!VIo!0-uTdgK2Q`Psq=C}#p|2FHe(@DKhd^fC$6(=`P>J_u<21Fij_|7}9+ zDCmEN(Es;{0HObzLI2}&7^oQN2v7;oQJ_+wV?f7&(EnFv0PO%m-!9R2M)XY({hnqZ z5c>T$`pqx;eXbl3`o9D8TYmJrd-NN5^nWRRfDQo_0POJ#z* zfY5K}QF;j=aUhfyr9*XtWGEeyO97!eLUL4JsNRqa-J^8qxALfdQ5sa&SQqi(K*;yV zew-e~DFGpDSs>Id(C^Gq`A`~!tpFqsB*!IGUnm~wqIyL42ov3-cvP)8yh#{*danFApm8=y%*6M<~Gd^&K{ zM^Rs$3giGZ1;`%A4yc&hM}{%s20|~BS-OUJ!E-=SH zQ(F_N1X%|?AsX)-D=IKYN7EQdkgs}y1n)g7Dj49-rnA_b79$Q4yt^&Z0WeTPz5)M5 z*ee8+42~-og96<9)P2GLj?V?;ZX=z`Mue-M9fwUlZzqLg8;Uf4_BD9-@Wd-RJRc z-n{bQ{ps<3-yq@EDgW}|z3uT{;h@9qS?MqYqA>*TCJqvA8|7~`|9trS0PmKMcOU2F zgZI_P`;>!(+phVS6z|E8_c-UF@wcFTdC-#y1^znG@E}Fw4&K|GXB*z_AMc(H5* zL=xTJqXA$7N-9d+2+xWBsy!$&yxP1mkJtQLNc&pA`6$2x3ys%!e|es5_{0Rf13gcI&s4yB)OSbX1`kx2+ePF3>v=lu zZNn{ue>=dZGvM9sd1(Ce;om~|=hNOc>^FQ41m0I4Ea2n!>1Z_r=)_=dC=&BPapstZY|)mHSk#lJPCgb_&-bV2_N{x1fFg93=n*#0#Cx< zZ}>bBd_DtD2cIm0Pio*v__rPYeVc#V!6%vElOcHd@E_k2z}GOlkH)7<@O1dsHvg8$ z-`D)T^C$WIi4K1Y_?L%&ZS&Xpla`3jj=^Vf@M-~{E`v|&;7RzmQG7BDKIwy}gU_zP zXMyk}{7cH;Z}>zUe8LD14WF5V&miGR{-pK(&$dziCH<3D#lIH*Z|1|l2mjBO=YJLr zpS6U~t|8i+jwUSM;8U0IDK>%vUC&+k&pPp0P5A5^$OqOH&|41wxeI?Z{&N?6wi7-p zhu44jzc1i(q3}67pu?T1;*+EBNjy9W|JnMVykp>#tMExckPr8{jnB3c;GPx4Ee|Yh z;nS_~X+c~Gcod(1h0hb>SH3_(-MxF3kh-$n8pra1o@cC>F^fqj9M4%*ep-tt+MQ!WLC(=b&}}7 zJrpN)Khxx;%)Amdi$xCsG}mi#OQw3;e%=p@!e|y4V`OkqAfoTjTU-k+uO(p6dOEBR z>hN10q=e7|-9!9o?mk}b?8sm`%QJ)#%pOPly48;b$Nj;tT*natEjaEkgzgJzXe^=t z4DU#;GO2;w9UO?v|a&*uYjk8>e)FAKR0Cz?Zjp^an ziS@+mH~ zwYrLEi|uiV?7Q+kXMq%;I2SZsFt{rnvTH$;d<%J^H|)+^3}+!1G&vVERMmu=I`IT& zQUW@h3mO{KyUK^Nj7sRBb1$K6T{kJTFbx`r5$U_KtAoJ+)H{gfp>dl#O7lxP&U$Po zUf?8v3^*6Gk?7IZmAAQvdV&^Sp@mvPLrmwj)S+$d%f__?ttfLw3Mdw5pbZXT2Gc{> zku*jS=Kxh`>zsZCpS9gl%MYh}(1P5dw*ApxjUWcy zt_GZriUdd(Oz5gdcTzayF8)O)Dw!Dneo5r%3;oO!X0pG;(}O&j zUhSM28R)?b=%j4FfUt=49au)h^K9xqBFC)uh@AL8L2PwEd(c)9;BwpdF9jr~(%rY7 zGxKg&QABjNZ0FPF!Sr9d0ZbRVp4O0iD=I$fwZzEO)eu8|QvgNsEoVZ?X=(%>@4W%_ zN-t)3XVX7Yk0)L=uu7|S?a>Iw5go^ij@m5oe1*XPH*8u6-J1@t3Z8TlI1EUf>0@h! zwq9_?4U82UNDpCnc8J!tw{aDILFIr2q0`g@&?v<4LNgMWxQBGV)pVqd{Lwc5j#722 zP5pw?rX20FX(R3yKK3NcdOEBX$fK(y(3rXNWnQh~nO!G-Y@ZnNY9C3IqN_P&$6gBJ z-#qxbt`i+zQ|_cxt(LUOfmm}w69aCaCO#UqCZ%~YL+J1)FpwF9x)e{~4TC>3B$7r< ze|XVEH}muj4f3aZ{Tj;*gjEbWjd+z|!JL-$OM(zOiy06`r@_xTf03|4J&5TX^n~sd zkoyGZDYYpv=kd-H{+{zV*xVAf$K?vT)xdu#B&qoAaY@2I!G;?A#rN&AXrJacb86Eh z+Tgd5{3hxzEwBylFERp|7}0sI#aVm757!t$#Jf~`VSu{_oz&*A4x7OaAWda(bhs}A zeg=nL#CS-Yb|2u*V!?VCZ`A)K0a^f~vE6-$M@{!zavQZa4j{5^BmPbA^0B*pCZ6re z_M17i_gQa z^97=H$UqjL!v~-)(vqJLq)gx)j(7;-NnvNJ6Rl}DxoU%bdR@&KJDPnVb>1YgbyC)? zx8q+|uL0}VC>rP2tb{+%)RyQa=v@^0ZztWB_dd@}3()Q2Xy_XlXV%aP%^OjOz8uD6 zc+p^?A`q=pb0&spRO!adh4bkMvgKS5jixLAw$A|c+eh-|_Z`fHklFej#0SuQ+&v>Z zaT#A7uz|0Pc;)SCQLY1R!pe?;2@%l?y25Q=Lx9*mvRgLt8V9chAhZq|Mz`=dUqVp{ zJ(;0FY@+(RS{mSXN%*V-dhnN6FE&O^AKi5IqS~5sfYr3Jo88gy@@3rB-vI1APo;oB$CWzlCi z;$v86WoYx&4EY6pJp;F*j*nb|<(>fyS~w#}PnQ;9sNX@Xdr06f@m}sBpwKQkH@ba# zShEU^XqTK5+evC#U??k~jX@+8LfD<+qvHLl2j1u?n&+I~0|vhl=Cpyuk$(zGIHnCE z5%Z^TU``t_WL|4q=x%YzHOxgLNBuD%&p2Mw`h74?BPRQe6!WKWJkwhH2oH+$Ih^we zyb~W1qY?2b8=S_wfkD8K^9bgA9H&s&Q$we*EiJsn6F4!FT;A2cp;6F(&0vuKE&Trh DD?Jvp literal 0 HcmV?d00001 diff --git a/package.json b/package.json new file mode 100644 index 0000000..37fbb11 --- /dev/null +++ b/package.json @@ -0,0 +1,22 @@ +{ + "name": "remark-agda", + "module": "src/index.ts", + "type": "module", + "devDependencies": { + "@biomejs/biome": "^1.9.0", + "@types/bun": "latest", + "rehype-stringify": "^10.0.0", + "remark-parse": "^11.0.0", + "remark-rehype": "^11.1.0", + "vfile": "^6.0.3" + }, + "peerDependencies": { + "typescript": "^5.0.0" + }, + "dependencies": { + "hast-util-from-html": "^2.0.2", + "unified": "^11.0.5", + "unist-util-visit": "^5.0.0" + }, + "trustedDependencies": ["@biomejs/biome"] +} diff --git a/remark-agda.agda-lib b/remark-agda.agda-lib new file mode 100644 index 0000000..cd69214 --- /dev/null +++ b/remark-agda.agda-lib @@ -0,0 +1,2 @@ +include: test +depend: standard-library \ No newline at end of file diff --git a/src/index.ts b/src/index.ts new file mode 100644 index 0000000..f792e9c --- /dev/null +++ b/src/index.ts @@ -0,0 +1,168 @@ +import { join, parse } from "node:path"; +import { tmpdir } from "node:os"; +import { spawnSync, spawn } from "node:child_process"; +import { + readdir, + mkdtemp, + exists, + copyFile, + readFile, + writeFile, +} from "node:fs/promises"; +import { mkdirSync } from "node:fs"; + +import type { Plugin } from "unified"; +import { visit } from "unist-util-visit"; +import { fromMarkdown } from "mdast-util-from-markdown"; +import { fromHtml } from "hast-util-from-html"; +import { toHtml } from "hast-util-to-html"; + +export interface RemarkAgdaOptions { + /** Place to output the HTML files */ + destDir: string; + + /** Function to transform HTML files */ + transformHtml?: (_: string) => string; + + /** Path to Agda */ + agdaBin?: string; + + /** Extra agda options */ + extraAgdaFlags?: string[]; +} + +const remarkAgda: Plugin<[RemarkAgdaOptions]> = ({ + agdaBin, + extraAgdaFlags, + destDir, + transformHtml, +}) => { + // const destDir = join(publicDir, "generated", "agda"); + mkdirSync(destDir, { recursive: true }); + + return async (tree, { history }) => { + if (history.length === 0) { + throw new Error( + "No history attribute found. Did you parse the VFile from a file?", + ); + } + + const path = history[history.length - 1]; + // console.log("path", path); + // if (!(path.endsWith(".lagda.md") || path.endsWith(".agda"))) return; + + // console.log("AGDA:processing path", path); + + const agdaOutDir = await mkdtemp(join(tmpdir(), "agdaRender.")); + // const agdaOutDir = join(tempDir, "output"); + const agdaOutFilename = parse(path).base.replace(/\.lagda.md$/, ".md"); + const agdaOutFile = join(agdaOutDir, agdaOutFilename); + console.log("looking for file", agdaOutFile); + // mkdirSync(agdaOutDir, { recursive: true }); + + const childOutput = await spawnSync( + agdaBin ?? "agda", + [ + "--html", + `--html-dir=${agdaOutDir}`, + "--highlight-occurrences", + "--html-highlight=code", + ...(extraAgdaFlags ?? []), + path, + ], + {}, + ); + + if (childOutput.error || !(await exists(agdaOutFile))) { + throw new Error( + `Agda error: + + Stdout: + ${childOutput.stdout} + + Stderr: + ${childOutput.stderr}`, + { + cause: childOutput.error, + }, + ); + } + + // // TODO: Handle child output + // console.error("--AGDA OUTPUT--"); + // console.error(childOutput); + // console.error(childOutput.stdout?.toString()); + // console.error(childOutput.stderr?.toString()); + // console.error("--AGDA OUTPUT--"); + + const referencedFiles = new Set(); + + const writtenFiles = await readdir(agdaOutDir); + const promises = writtenFiles.map(async (file) => { + referencedFiles.add(file); + + const fullPath = join(agdaOutDir, file); + const fullDestPath = join(destDir, file); + + if (file.endsWith(".html")) { + // Transform the HTML optionally + const src = await readFile(fullPath, { encoding: "utf-8" }); + const transformedHtml = (transformHtml ?? ((html) => html))(src); + await writeFile(fullDestPath, transformedHtml); + } else { + // Copy the CSS file over + await copyFile(fullPath, fullDestPath); + } + }); + await Promise.all(promises); + + const htmlname = parse(path).base.replace(/\.lagda.md/, ".html"); + + const doc = await readFile(agdaOutFile); + + // This is the post-processed markdown with HTML code blocks replacing the Agda code blocks + const tree2 = fromMarkdown(doc); + + const collectedCodeBlocks: RootContent[] = []; + visit(tree2, "html", (node) => { + const html = fromHtml(node.value, { fragment: true }); + + const firstChild: RootContent = html.children[0]!; + + visit(html, "element", (node) => { + if (node.tagName !== "a") return; + + if (node.properties.href) { + // Trim off end + const [href, hash, ...rest] = node.properties.href.split("#"); + if (rest.length > 0) throw new Error("come look at this"); + + if (href === htmlname) node.properties.href = `#${hash}`; + + if (referencedFiles.has(href)) { + node.properties.href = `${base}generated/agda/${href}${hash ? `#${hash}` : ""}`; + node.properties.target = "_blank"; + } + } + }); + + if (!firstChild?.properties?.className?.includes("Agda")) return; + + const stringContents = toHtml(firstChild); + collectedCodeBlocks.push({ + contents: stringContents, + }); + }); + + let idx = 0; + visit(tree, "code", (node) => { + if (!(node.lang === null || node.lang === "agda")) return; + + node.type = "html"; + node.value = collectedCodeBlocks[idx].contents; + idx += 1; + }); + }; +}; + +export default remarkAgda; diff --git a/test/.gitignore b/test/.gitignore new file mode 100644 index 0000000..872aa27 --- /dev/null +++ b/test/.gitignore @@ -0,0 +1 @@ +results \ No newline at end of file diff --git a/test/Simple.lagda.md b/test/Simple.lagda.md new file mode 100644 index 0000000..68d0de7 --- /dev/null +++ b/test/Simple.lagda.md @@ -0,0 +1,27 @@ +``` +module Simple where + +open import Agda.Primitive +open import Relation.Binary.PropositionalEquality.Core + +variable + l : Level + +data ℕ : Set where + zero : ℕ + suc : ℕ → ℕ + +_+_ : ℕ → ℕ → ℕ +zero + b = b +suc a + b = suc (a + b) + ++-comm : (m n : ℕ) → m + n ≡ n + m ++-comm zero n = lemma n where + lemma : (n : ℕ) → n ≡ n + zero + lemma zero = refl + lemma (suc n) = cong suc (lemma n) ++-comm (suc m) n = trans (cong suc (+-comm m n)) (sym (lemma n m)) where + lemma : (m n : ℕ) → m + suc n ≡ suc (m + n) + lemma zero n = refl + lemma (suc m) n = cong suc (lemma m n) +``` \ No newline at end of file diff --git a/test/index.test.ts b/test/index.test.ts new file mode 100644 index 0000000..519556c --- /dev/null +++ b/test/index.test.ts @@ -0,0 +1,38 @@ +import { test } from "bun:test"; +import { resolve, dirname, join } from "node:path"; +import { unified } from "unified"; +import remarkAgda from "../src"; +import remarkParse from "remark-parse"; +import remarkRehype from "remark-rehype"; +import rehypeStringify from "rehype-stringify"; +import { VFile } from "vfile"; + +test("simple case", async () => { + const file = join(dirname(import.meta.path), "Simple.lagda.md"); + const vfile = new VFile({ path: file }); + + const result = await unified() + .use(remarkParse) + .use(remarkAgda, { + destDir: join(dirname(import.meta.path), "results"), + transformHtml: (src) => { + return ` + + + + + + + 
+          ${src}
+
+ + + `; + }, + }) + .use(remarkRehype) + .use(rehypeStringify) + .process(vfile); + console.log("result", result); +}); 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 + } +}