From 4d8e83a74a39525f81f29d3a7a34fda9dd2ab5cd Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Thu, 12 Sep 2024 19:43:27 -0500 Subject: [PATCH] works --- bun.lockb | Bin 36772 -> 43420 bytes package.json | 14 ++++++-- scripts/prepare-release.sh | 5 +++ src/index.ts | 69 +++++++++++++++++++++++-------------- test/Simple.lagda.md | 43 +++++++++++++++++------ test/index.test.ts | 30 +++++++++------- tsconfig.json | 10 ++++-- 7 files changed, 117 insertions(+), 54 deletions(-) create mode 100755 scripts/prepare-release.sh diff --git a/bun.lockb b/bun.lockb index 23e0969a07c13ed4e0779eacd541ae6e06e3158b..da1d5c90eb3eabb31e644b79bea4e901e861be96 100755 GIT binary patch delta 10333 zcmeHNd3;UR+TQzQJmf@3a83r9L`a;Id5#R`I0Ok!OqovxGD(7<;YN%N+t@y544Mhz_zvtaUPIABA+xz={_mA(7Z}aSTJ!`$|UGI9=u=hSI zpMI=Zby~4V*RA`W-8n}N#~tdPUo+k+DQ#2Zw)(>x7tc*pw5cC(X6GF@yBbco@)sN2 ztMz#z5$~-z&NLHA2gsix)sWX9Rgf1U?I0(X6joFs4VhPH%;hHK6&4x6XDdX#(~xe^ zt1K^_m|wtgeZi@ov8vKolFM*^9zc7#G%R(XXnjN^NCx2-tN9`ceT8z7y)_dvFSjJDyp4v=1uW; zv4eh)s9$YzMS=<(Aj#7#tY7^VpIMdfyojgZu# z^N^%p59tD_gi-3yVz0+j5*Yqz|Mk z2=7Dd%^9tVD`!n~{CrMsM_V<~WaJR;#aOsYv$F$dXB&BcYb1*08 znD3+VS4I4nWnR6%A9*M|<@SK*ckkwo8h$x;UvD?BM(=$}uewqEs=xJp`f*vOo7F|p zJ5qdyUij+GkR5;NQ|n+^z^il0tEY@A?X+j@w9uF1yRS;LS$QmY-Mr!{tjcPiaxuqo z{o$q++ixAAXvMRs)^U6`tFw;hKV{FYKY~)#zB|e2k*~as8*%aG&3q^?q+iw%0d?7KO&9seB>agahOhJ~E z*oFdeUMYoDm7GVvipv;!sQa%IgEoc&pwHBF`VABLP1ZCDN zu~mffBv`Ca4_+#VV5JWe>QQ^2f~A3pJ$T8Y?BbOnShAu9`8N-Y{NvgF4v}^s)F=c; zo$+U7*0##tm__}Oi_Tg{+JaDPf<;vW7*&AaEZIXVv4S0@Wdd@og?N;Lkq*ZaZ6j2* zVDVrOO*NFZU}V%rs1S+0g&3;a$5`o+vSs_7B9wcPA1N|)^eI>`u+~DIG|cQlU@B@v z`527CEKC7qPpl5IXCVZ323R_nf(BLD3HuNQU1Vh~*a0vKoRpK(Pp; z^bBl)z-Tti!qyTECX9hH$BE;{G?ncIlg1yKj#%Vk8FjW4Y@BEl>>}8RCKiB|KB~!z z7VF&X*gIh6dQV%F8Pv_KY-+(Quxrrz5kjUgYS>h#IK?sz+XZn@!(KpGJG1Eaamr|H zh7??}M+?A`z*-3b{5#kHFr~28@~{hr3N|U!E5Im9V&FTvihZDo8ljv3W*)x7V5BLQ zwa1=G?TO3?CfcOveh3zeG8@6lRj{65N?~Xtuy-bdVM1c-nA3^9=!mX#V$te2MLTyk z6(Y@@?SlBwoxOlK=gy)vaaLzNIBq2Cp^355;aM_VNWF>FU?Fu1DZP+#^WwOnLaGF* zL9B;MtR)hnS}Si!O_Alzrn*E|W7cs53jh;@Qvgl?576#TS96KYfF5Cj9y%gO4@lC7 z3&Qn#lFH$Qa5a zDdJ?WCqQN3{=J2ei$*Cl|M`^wqqzQmAqeyT|NcTq7FNc8Y$4QYJkRh6C2!p8 zc<9CCchA**899E{+Z#sQ%a6bR^31L&u1=n(SJ;pDJ7Ib4$Zx^=w1|+c?IxWZvbk%U zHd7b)A3yMQePi1Pb1pHhx0?OrrRQx}l(&K1^j5Le-g;iiZh-pB~!_EfQ z-$%t>fvH%MkAXb{+vKC?+pya?F1|Cs^>ehIb^UO^rR}G*zB?{{ z&j$xKz5nN9ofmv~{quHtcW>MuJ~i>j#f8sCJ`2j&aD4ClyglPOyj*exB?E|-c9&bNW6V!Eg&S>AUyTe`4t<`QcXPGJr&}J>rAF263?KBQpw{~QJ0IEXd`lnF zd3M9XsJHhXeALW4_a@)4oiBZQ!aHSrQQ7I_S!Ly${FnV{|BC)6mmgiW$gU{&amwSc zzZEPAsMs8?sp=Z-P&6i^V0*xgKbPDb_iN$wZ5reC-?%Bvt-HE<*xvQwTe^C_5qS1U z>)2bLw9DRmYX2v*21ME3?SJ}It=qAsKIKKdW}GQ(Q~#$sTNXx`?qB`9d+xb@-pl%L z{qADkv-g^L=h@slHmGQySHeu?W-hQYb6(s}F)Ow|DjnE9dF}cRT|)Oi>D1mgbV~i% zT21xJstdiB=BA!{XGj3kl)glN2tf&*t&6^^F6QIY0bRz zZtk5!z_zu$)MuSPyK?Vs-A?cAru!2{I3C^MXu4ZBnPE!S?l>38v?)qZ<-=1yqlolkS`?p7{q zv~;=R->uy1*03?beeS)Ad85d4(ZTM$C!I@d+iQ10!3(#J4M#QiOA<`Xil2LP&4LX} zRillFu!?{PmCz)T*~1O-j#e=ACbI?>rCBJMS>%#-4>f zC&o>9sCZp^Bf+!y^2=}CyG^c?49m`8%oK88I9YXBP?r009EnjizK3df!ltmos|$Y2BO8i73tERiWg4D13}afqJp z#p=M`io~82s^|N#!cYT?jKZD-){kkzus?!L57YBW>@e8!X!I{!&+FNgaP%(*{R11s zx_gl~vxm5kVM#Ftek@yydpdiLdj=aCYv40k4enWt?_t2tIwNt< zVOwy|Wy&}MZ)91x=hfE5rCQf|#3%6h3B!^(^s%))hMg5(04CNpeogJZK3_Ya*ukRJ zqCBxIeY6SxK32JQg# zI!v$3hk>0yCXfYW1A_p1`K0F%eci+W_~7Jv00}@MKs#Ay0DDF?{Rl@t$kC5*^c$w| zIY6HfSAa&~7;pkO37iJb0q22wU^lP_*bf{44g%D@0-z8W2aE@bfMQ@6K=ZIK&=2U3 z_Jxnb?jQj`SKul@9}b5A`p%(mnkrx#@CGm)m;sK!Dz($s5|aYydaF6`-#rYqmbkSNK4t5winm z1ZgBm(-N?iq*9VJsuWz(cLXTFq)U4AaZP1ZkIFj&G$>Tw9&iGvj5z7xON<7~JaTg7 zE-3H>JOFA~ZU9r0qc3uq%aW!5O$9FiQ=zGWV5GYN*8h+f1WpdpVEI${{gB`RGDsfM z2gg{8jCxf8?aWYDr@*@B;s0X3}`brN6!T_>C`qU9hlWi)eG}Viw;U|&=^aEsL z2}s8SR3R3K1E?Z7MuvL;)B{==aw96FNmu5wq&#whY>|}P=!gN02C;cH2#AC3avaBh9ON8B^5{kXguYWJ{aj_ zU??yIpgM#R01c&VgT|XCs{xR0(8Lvoy+Bl^*-6Hz5;aI(%MHn8Bat@-7zK=$q!BU~ z$N{o}EFcre0Mdb~BHVD5&1Ub8?!tDCP6@&SGs!>B+bYCjaZDUgvhHs7cKwL07PfqP zP@oR~xPHuYj0VrZm@yhB`3On=sUKRA?B3W8@koS28_PWt7VTk3K3yOcU62k@kPo)x z^9Kc*5L)0$Sm~IMF!`iTKCD1Fd4QTTVUwKe?C$LNswY`YYwkX}1 zzrwOIH0&=(-C;kb4-#}k#9YbTk_=~l5BmZZ8rb2C5dIQ-m7#Hw&j{Q1?C^~)b)F6m z2b()2Sy0&7FjJ;FTs|oDugSUg%fxl-pd2bH%SVfY>pt4%e0Er&x!=(??0BZS$rCipI^$y zOe`U@vslSoJx@Nfl+Tt>Jpv73?B!EU`Sb}Tn3%yRlFvQm^C^^20Y+Uu`IJwnP(t$| zh&g1qiZM|{+p)MDwW6;b8=1DRC@!g3V4hm>SjFnI)e5COdtesMZP>|tH54&El1Hxn zFwyZMVfwWy^e0pO^;PC(MQyeq$63;qTG-*hzRw9(oOfXMxoTJWFtzW-Sw-`z4*eDN zrGa?tz-GV`pSEmFu3C}UmX#GYIV5=^jH>LU?73J?^xRcG!~J~12aB|)A{WBEw1`)< zW0}S#gY}MVi7{9q`PSgbUZSkgktK{%OCbrDk9nt+o%_M!^Su4$p2`Qlza08%@OaPH zmgW+v4^lLxJ_I%1_vy0^Y)ye299Q}5y36gkt~)%eTbuRHbYSEAaf#i>Or>@U!MrD0db ztL0fPY_f{e&P-Pn+_a-%+h2o~$w%|8?_{J->tWYu zE)mwg+Vzh%QN=J9Hn2EYaovTPiq$Ui(f>E5jc1o{Ss!4wC-^Bk=p-Nb%ctMaio%1^ zqq+Ys^50Kv)wt{TJ9^tdNm@(vG|`01e=Q&%ougdZvHz%3Ve%iR_#D`{-otZZ5vtOD zioNjQUGJk49<&-jGML@;GGHR+qn^Rg;T3%6EURaW^om`k(SB68;&>CKzx>TjN?wWWYa?Wz$Q#iSYTCt2p>HPC2Wpa4 zPq6vJm|%2Sn<~%t@_Rij$w_S_BJNWgT(zdHuH0CF!PjEWLBUMm8oi(+T*8E!SXo#^ zI^-Qop5H1^)NfISQ9yrNRzZv6b|qKzY|24%=ITwkf@|K?!P<-St*u(w)`)Awt_Hsa Kc`}Fhmi#xa$btv} delta 6588 zcmeHLd303O8GrXBlgvw)5FwD6$qoo6WDnUU$s}RR@{+JKETSN5AP~R=Ld47jL7)Wz zzf%N678MGDfJ7*$RPdmM0~By+k)ucKp;oH4E~iDbw*7r?$s|>@i+}c=^PAuO-Fx46 zzwf*EzW3&CeM5eFySzR%@q%~z`Ik$5?=|f@JURJT)NA=0gZ~nDIpyX*lHR-=)Uf4Z z#5zg4JR3Z5cRw&z7y56gB>8Gl3Ft7vcf!l022b=(Q8ae>X{XWJh%oo9&)oIi3Yn%xu=iZMWTr%vigK&3AyC7uPmS^l^1aXwhpajX+pD zz!We~#cnVUJkF>`nzbqIhG^K)o5(*;!F%{&`)9$ioRUK*@W7kF7|YjcbeI!G&jjSq zhXIG$z6_its43{AvIIuU(Z@oiO0N95M9sl&rBX=JKvV`%YgiuL3NDsk71V5XD^{$$ zOszp!b43~5vKEWol&=&ED=ooqAsttWm8AiaGyuHZ+?HmGVS8@0lY z3-iRDYFSfOLGc&?ns29}?tzjyqslaF2liW6M>{DiW_g_67G7XspY>j+Q9leyXk&H9 z8pwwVq*hz5QUz5C6{=a^1*KcyJUoMyIj`M{9UEwJyJ~{M+JsF+u6zzvrM0ngca@}{ zXbM&=XP{i16=g4$_uXc_V!}(5Z+#E5rcZ05W|IigTpreG+yUM}ajRmS=^~(|!u!cEw)f zjscp*iBLS1y4nY2m<-O9-*eDc(QY}$Nv;^TT<4@_&|xRN0Q$m7UxCu2$QA3hq(w{8 zcq)o5u&hF9j8=LVrD0kr8QWjgN{dk%p_R^{RIQbI#G3u4p`_A@xIz(2&G9a82sS$d zdyro=5_YqM*_N=~`BA1_%-9F~;LzF;fW~-+X#L=Xc6}GK9k`)g9T|I&pYdMJKp&$6 zGd2}ZnRYR=L#evd7#my4GBh&}fOKk{ZPYV!KNo*rjy1p zok)oD2BM}0=mKDpwc96xx&B^5PX_Zf8DKZ209f_XLV)`%0=Ry$!A)Qer`h18V9xCt zfG=itYaQo>4G_Tmn8A;Oxx+Sq4Q~hdVrIPq;A;oKdMCjBp9b&%kq!cUF|#AjvB33h z#?-Qb!&tlI#YQu@Yud754}TK`vOGymZ_^lJY9hzn5*w~rAJ^Y^dAsrmxr1;`gO z=jXp)h-~Hm>rl@^hxPbF>u|`AvJTrE{oWKbBvGZjL>oPksES~^k?5fhp{kQqq0r_e z4{b`a(Kk?`RMFo<<^65+Y=2eQ=oZwMP?M5X(UtZlduUIxjch5ZxP!*0cxYUTjZQ#y zCneQG)>IqKO;tq?Iu3OVDke=8kyM-Jp;>7*x&Y-MN4kgX={9;WT@_JuV}OUwKvid} zB8E0+d#EV`zCguMMUIE=%7iaDsz{()P*spJ79qZT8?7x;MK-++bquP=t%_V)?M8eq8+`(mPx-}&uK>9&Rz(5bfI0(J zU80I2+FXM83K1VvF;$czz9Pg|s)|y&1$6~#(m+)VqP+tVpBwQFQpFG&KM3&^BR;4y zQU)VFsKz0xsGw6r5MPOn?i{KLl@<&|e5E#e3#ytD$~>Zmmf&|7UB>TlN-Xz?5!8y` zk@PlxM^Q$FM~tS`_#H#G_*y;@3G5rgzEuO|0Q=Mzz&uDnKvz0DtDgfO zwc0B@6wI#}{uH-KNp+!_pUGP#Z4zuevv;G}XpCzun>ZLGPU z6W|HqK0G<*z07w4oGS}p_D7vp;uj4Yj{|rn`3p$^+=-3%0uq3D1Ds&4XM>!0)@+nD z*YiZMJ)Wc#AQ?ym?gHWg?r$~9y*R_%As#Sikjp&FE~Ac(WdWH0JCg=v0DK=i#)f&~ zH~{`iiwAfRzK{FH1FTKvI@WBfH^y)GI3MLafCu9BodcKyW}`d+FbC^65ci1(*r@5` z?KC^pvA?&YC_rNoz^UXpD*-sQ<~)|6%yT>x7y|HonsYr6O2u z1Ll3j`)edG)e$HR2ZjMPz_E$=!4+FiBkTGGphS!7M$z@Uo_H>PUFXPVt5~(Zox2t` zzqmUl+$!$L$VkmdO>aLD+S~tw@*bmpdXxW`>(^L%Y;KmQC9%vQPEqSTNA?B7%FF`m z!KL*p@?~*PPHH-gNLSHQ=heu66BJlqrB?_S z)z3Eu7prM|y-}vu>z!gFb@e(ZXuebIq=fm^THh?a)-d-Qv^CIYu+T!G3$nzcRJ_0; zcF;#=K(uCoVMl%?i1vH!@|7TZXMtVo?~p$YqVR?Gc9U_79C|t0Jb-$B#Jo%bCr}?u*ZJu+mld0Q@Q7F369%UYt{i!(nY?I~4 z6m-beJMgq*>2b=vLTFo~J=!=o^W~J?eCoHi; zVxFpf-8A46-%B5KFsB=!hZi}cZhyNruktrtsOEvp9P^;-e1fAS=C!%y{)CxlaYOel zt6SOh+N=H+yz||Q?a}68-uD@K7Q-BUk~fTX$MB?ID?t8F?`3$&Ry(g7k$P|w+*GwO|*GfSyNe> zB z_V3vR+CxfqL{gGBv;9GWM=7oMI*n&ew0VfTv*n#$Wi5f>$VZmG$yY_vH9VBGhf3#% zlDs97%6*w~vYnRt>`~_V@UMLP-rDrsE`A^xCUgfPoD~0%J;yx$ed^q%CEI7eUMq{1 zywvQ}jC9F7DBh4ZVQt?dMR>BeWTvNPWTxircG5iD`t1(<>gQ_?zMSxp(wet#=#&h_2_vcH3Q z9$lQW*E;)Z?4SKDH>1eC+}_7Lz#g-%WZ8kr-}Ux)m{qTNC+(@H=H(@Ha(TM*AU>7w zF83|Z%RVof!v226=yLH93Ry9M=B?<}wr#~)(KcyiV^G_`4NuEZYg3N Re>_^GC%4w^!RPw=e*zH2x2^yH diff --git a/package.json b/package.json index 37fbb11..b5c3ee1 100644 --- a/package.json +++ b/package.json @@ -1,22 +1,32 @@ { "name": "remark-agda", + "version": "0.0.1", + + "main": "dist/index.js", "module": "src/index.ts", + "types": "dist/index.d.ts", "type": "module", "devDependencies": { "@biomejs/biome": "^1.9.0", "@types/bun": "latest", + "rehype-raw": "^7.0.0", "rehype-stringify": "^10.0.0", "remark-parse": "^11.0.0", "remark-rehype": "^11.1.0", - "vfile": "^6.0.3" + "to-vfile": "^8.0.0", + "vfile": "^6.0.3", + "vfile-reporter": "^8.1.1" }, "peerDependencies": { "typescript": "^5.0.0" }, "dependencies": { + "hast": "^1.0.0", "hast-util-from-html": "^2.0.2", "unified": "^11.0.5", + "unist": "^0.0.1", "unist-util-visit": "^5.0.0" }, - "trustedDependencies": ["@biomejs/biome"] + "trustedDependencies": ["@biomejs/biome"], + "files": ["dist/index.js", "dist/index.d.ts"] } diff --git a/scripts/prepare-release.sh b/scripts/prepare-release.sh new file mode 100755 index 0000000..05cc57b --- /dev/null +++ b/scripts/prepare-release.sh @@ -0,0 +1,5 @@ +#!/usr/bin/env bash + +mkdir -p dist/ +bun build --target node src/index.ts > dist/index.js +bunx tsc \ No newline at end of file diff --git a/src/index.ts b/src/index.ts index f792e9c..d5965da 100644 --- a/src/index.ts +++ b/src/index.ts @@ -1,6 +1,6 @@ import { join, parse } from "node:path"; import { tmpdir } from "node:os"; -import { spawnSync, spawn } from "node:child_process"; +import { spawnSync } from "node:child_process"; import { readdir, mkdtemp, @@ -10,12 +10,13 @@ import { 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"; +import type { RootContent } from "hast"; +import type { Node as UnistNode } from "unist"; export interface RemarkAgdaOptions { /** Place to output the HTML files */ @@ -31,7 +32,7 @@ export interface RemarkAgdaOptions { extraAgdaFlags?: string[]; } -const remarkAgda: Plugin<[RemarkAgdaOptions]> = ({ +export const remarkAgda: Plugin<[RemarkAgdaOptions]> = ({ agdaBin, extraAgdaFlags, destDir, @@ -48,19 +49,14 @@ const remarkAgda: Plugin<[RemarkAgdaOptions]> = ({ } 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( + const childOutput = spawnSync( agdaBin ?? "agda", [ "--html", @@ -94,7 +90,6 @@ const remarkAgda: Plugin<[RemarkAgdaOptions]> = ({ // console.error(childOutput.stdout?.toString()); // console.error(childOutput.stderr?.toString()); // console.error("--AGDA OUTPUT--"); - const referencedFiles = new Set(); const writtenFiles = await readdir(agdaOutDir); @@ -118,48 +113,70 @@ const remarkAgda: Plugin<[RemarkAgdaOptions]> = ({ const htmlname = parse(path).base.replace(/\.lagda.md/, ".html"); - const doc = await readFile(agdaOutFile); + const doc = await readFile(agdaOutFile, { encoding: "utf-8" }); // This is the post-processed markdown with HTML code blocks replacing the Agda code blocks const tree2 = fromMarkdown(doc); - const collectedCodeBlocks: RootContent[] = []; + const collectedCodeBlocks: string[] = []; + 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) { + if (typeof node.properties.href === "string") { // 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"; - } + // TODO: Transform + // if (referencedFiles.has(href)) { + // node.properties.href = `${base}generated/agda/${href}${hash ? `#${hash}` : ""}`; + // node.properties.target = "_blank"; + // } } }); - if (!firstChild?.properties?.className?.includes("Agda")) return; + while (true) { + if (html.children.length > 0) { + const firstChild: RootContent = html.children[0]; - const stringContents = toHtml(firstChild); - collectedCodeBlocks.push({ - contents: stringContents, - }); + if (firstChild.type !== "element") break; + + const className = firstChild.properties.className; + + // @ts-ignore TODO: Fix this + if (!className?.includes("Agda")) break; + + const stringContents = toHtml(firstChild); + collectedCodeBlocks.push(stringContents); + } + break; + } }); + console.log(`Collected ${collectedCodeBlocks.length} blocks!`); + let idx = 0; - visit(tree, "code", (node) => { + + visit(tree, "code", (node: UnistNode) => { + // Make sure it's either null (which gets interpreted as agda), or agda + // @ts-ignore if (!(node.lang === null || node.lang === "agda")) return; + // node.type = "html"; + node.type = "html"; - node.value = collectedCodeBlocks[idx].contents; + + // @ts-ignore + node.value = collectedCodeBlocks[idx]; + + console.log(node); + idx += 1; }); }; diff --git a/test/Simple.lagda.md b/test/Simple.lagda.md index 68d0de7..88c4498 100644 --- a/test/Simple.lagda.md +++ b/test/Simple.lagda.md @@ -1,3 +1,10 @@ +# Commutativity of addition + +This document shows how to prove commutativity of addition on natural numbers. + +
+Imports + ``` module Simple where @@ -5,23 +12,39 @@ open import Agda.Primitive open import Relation.Binary.PropositionalEquality.Core variable - l : Level + l : Level +``` +
+ +Declare our data structures: + +``` data ℕ : Set where - zero : ℕ - suc : ℕ → ℕ + zero : ℕ + suc : ℕ → ℕ +``` +Define addition: + +``` _+_ : ℕ → ℕ → ℕ zero + b = b suc a + b = suc (a + b) +``` +Prove commutativity: + +``` +-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) + 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 + lemma : (m n : ℕ) → m + suc n ≡ suc (m + n) + lemma zero n = refl + lemma (suc m) n = cong suc (lemma m n) +``` + +That's it! \ No newline at end of file diff --git a/test/index.test.ts b/test/index.test.ts index 519556c..ceada6f 100644 --- a/test/index.test.ts +++ b/test/index.test.ts @@ -1,22 +1,22 @@ 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"; +import rehypeRaw from "rehype-raw"; +import { read } from "to-vfile"; + +import remarkAgda, { type RemarkAgdaOptions } from "../src"; test("simple case", async () => { const file = join(dirname(import.meta.path), "Simple.lagda.md"); - const vfile = new VFile({ path: file }); + const vfile = await read(file); - const result = await unified() - .use(remarkParse) - .use(remarkAgda, { - destDir: join(dirname(import.meta.path), "results"), - transformHtml: (src) => { - return ` + const options: RemarkAgdaOptions = { + destDir: join(dirname(import.meta.path), "results"), + transformHtml: (src) => { + return ` @@ -29,10 +29,14 @@ test("simple case", async () => { `; - }, - }) - .use(remarkRehype) + }, + }; + + await unified() + .use(remarkParse) + .use(remarkAgda, options) + .use(remarkRehype, { allowDangerousHtml: true }) + .use(rehypeRaw) .use(rehypeStringify) .process(vfile); - console.log("result", result); }); diff --git a/tsconfig.json b/tsconfig.json index 238655f..8ea97b4 100644 --- a/tsconfig.json +++ b/tsconfig.json @@ -12,16 +12,20 @@ "moduleResolution": "bundler", "allowImportingTsExtensions": true, "verbatimModuleSyntax": true, - "noEmit": true, // Best practices "strict": true, "skipLibCheck": true, "noFallthroughCasesInSwitch": true, + "emitDeclarationOnly": true, // Some stricter flags (disabled by default) "noUnusedLocals": false, "noUnusedParameters": false, - "noPropertyAccessFromIndexSignature": false - } + "noPropertyAccessFromIndexSignature": false, + + "outDir": "dist", + "declaration": true + }, + "files": ["src/index.ts"] }