From d153b8803073ff2b85b0de18e28e70003071b5e9 Mon Sep 17 00:00:00 2001 From: Stephen Paul Weber Date: Mon, 4 Mar 2019 23:38:25 -0500 Subject: [PATCH] Implement many builtins and do Optional section --- .rubocop.yml | 3 + lib/dhall/.ast.rb.swp | Bin 0 -> 36864 bytes lib/dhall/.binary.rb.swp | Bin 0 -> 20480 bytes lib/dhall/.builtins.rb.swp | Bin 0 -> 20480 bytes lib/dhall/.normalize.rb.swp | Bin 0 -> 28672 bytes lib/dhall/ast.rb | 132 +++++++-- lib/dhall/binary.rb | 18 +- lib/dhall/builtins.rb | 265 ++++++++++++++++++ lib/dhall/normalize.rb | 24 ++ lib/dhall/util.rb | 17 ++ test/normalization/beta/ListHeadEmptyB.dhallb | Bin 16 -> 11 bytes test/normalization/beta/ListLastEmptyB.dhallb | Bin 16 -> 11 bytes .../beta/NaturalToIntegerB.dhallb | 2 +- test/normalization/beta/NoneA.dhallb | 1 + test/normalization/beta/NoneB.dhallb | 1 + test/normalization/beta/NoneNaturalA.dhallb | 1 + test/normalization/beta/NoneNaturalB.dhallb | 1 + test/normalization/beta/OptionalA.dhallb | 1 + test/normalization/beta/OptionalB.dhallb | 1 + test/normalization/beta/OptionalBuildA.dhallb | 1 + test/normalization/beta/OptionalBuildB.dhallb | 1 + .../beta/OptionalBuildFoldFusionA.dhallb | Bin 0 -> 52 bytes .../beta/OptionalBuildFoldFusionB.dhallb | 1 + .../beta/OptionalBuildImplementationA.dhallb | Bin 0 -> 85 bytes .../beta/OptionalBuildImplementationB.dhallb | 1 + test/normalization/beta/OptionalFoldA.dhallb | 1 + test/normalization/beta/OptionalFoldB.dhallb | 1 + .../beta/OptionalFoldNoneA.dhallb | Bin 0 -> 46 bytes .../beta/OptionalFoldNoneB.dhallb | 1 + .../beta/OptionalFoldSomeA.dhallb | Bin 0 -> 47 bytes .../beta/OptionalFoldSomeB.dhallb | 1 + .../beta/SomeNormalizeArgumentsA.dhallb | 1 + .../beta/SomeNormalizeArgumentsB.dhallb | 1 + .../beta/TextShowAllEscapesA.dhallb | Bin 38 -> 38 bytes .../beta/TextShowAllEscapesB.dhallb | 2 +- 35 files changed, 448 insertions(+), 31 deletions(-) create mode 100644 lib/dhall/.ast.rb.swp create mode 100644 lib/dhall/.binary.rb.swp create mode 100644 lib/dhall/.builtins.rb.swp create mode 100644 lib/dhall/.normalize.rb.swp create mode 100644 lib/dhall/builtins.rb create mode 100644 lib/dhall/util.rb create mode 100644 test/normalization/beta/NoneA.dhallb create mode 100644 test/normalization/beta/NoneB.dhallb create mode 100644 test/normalization/beta/NoneNaturalA.dhallb create mode 100644 test/normalization/beta/NoneNaturalB.dhallb create mode 100644 test/normalization/beta/OptionalA.dhallb create mode 100644 test/normalization/beta/OptionalB.dhallb create mode 100644 test/normalization/beta/OptionalBuildA.dhallb create mode 100644 test/normalization/beta/OptionalBuildB.dhallb create mode 100644 test/normalization/beta/OptionalBuildFoldFusionA.dhallb create mode 100644 test/normalization/beta/OptionalBuildFoldFusionB.dhallb create mode 100644 test/normalization/beta/OptionalBuildImplementationA.dhallb create mode 100644 test/normalization/beta/OptionalBuildImplementationB.dhallb create mode 100644 test/normalization/beta/OptionalFoldA.dhallb create mode 100644 test/normalization/beta/OptionalFoldB.dhallb create mode 100644 test/normalization/beta/OptionalFoldNoneA.dhallb create mode 100644 test/normalization/beta/OptionalFoldNoneB.dhallb create mode 100644 test/normalization/beta/OptionalFoldSomeA.dhallb create mode 100644 test/normalization/beta/OptionalFoldSomeB.dhallb create mode 100644 test/normalization/beta/SomeNormalizeArgumentsA.dhallb create mode 100644 test/normalization/beta/SomeNormalizeArgumentsB.dhallb diff --git a/.rubocop.yml b/.rubocop.yml index 2b9f4df..5d06dd0 100644 --- a/.rubocop.yml +++ b/.rubocop.yml @@ -51,3 +51,6 @@ Naming/UncommunicativeMethodParamName: List/ParenthesesAsGroupedExpression: Enabled: false + +Lint/UnusedMethodArgument: + AllowUnusedKeywordArguments: true diff --git a/lib/dhall/.ast.rb.swp b/lib/dhall/.ast.rb.swp new file mode 100644 index 0000000000000000000000000000000000000000..658a5672ab538351f36fdb8022038c92ebc4ac40 GIT binary patch literal 36864 zcmeI*37izwoxt%9UTFm)pop$uIgsoO3^RB{u~%R?1{oQK0f8t;#+vTxnRdFXhU#jV zK@LG9c*OWIiAIePPd9HRYPzgw<&~S{-ZElgaURrn$2^nP_%@R_ke}%5E;Th+ue70znD% zrvx%ieEh^gp<|9dN*(H>%Z}8B4PDruB?a>YB@mQAPy#^-1SJrZKu`if2?Qk&l)x9X z1f2H$LTgF;05ARfdY@k@_}tt3J>2`Gc|iU1r}O8l_l6HC82?r8_eSs2ui^Xi@8bN+2kKpag;v z2udI*fuIDwlqI0YLZMY(3x#fn^#A+y_*eP86Wj3^?tn~l3$Da!%tIZfV=^XTBnIG} z!J*L4a6PWWkFXKzu?}aT8Wk9W(byONIVcqRH#~;BaXW6q#aN65n2QEXKsAQr&4HoN zOL!K~;5K|08?YYh5W@*L9Pb^#Ja`Se@Hnoh(g0R!L0Qk)14hv8rxgxxfVJcp}r zB{rf1HkP3gN8;}=90%h=Hts9fjGJ&7F2VO;q5-oo9n(;b0eG9nnV0bd9>b%!0S20| z7^fkEBQXg3VPEW`;pjKG78heRI$$G(B<5iv#$Xgi;u9Kl9>6`g6L;W3v|%*LFc_cE zaP=Ynh-V@H!r_<^*HU_WQ##XZbhO(>I-Ri0bon=$lUB5?LZ&dx82^WB;t3-e(dNQ%nD0f#-=}ye}Xi{g^`D*<$C0$daQCZlDT5UEHB*#s< zmw~jAj8~}{t4w1>`7Ax%x@2sPyW}d0Ks!rY)mEu3U!^VKL*;+T@}*0))l2;Z^{$-U zCFV+{L}m(d(QVQt0pYNlq#B2^U79~2VYX+SrIl(>A9AH;C@2)Kauq+Ocw0X2n3H+3xtZJUa9+@p4VEdH@_+Vl zjCtE`xt`1zxlQ*Ob12(NEs<@dK1-Z;+-ZtsT8$}@Ycr0=?-Vp=8R*cwV36f7i&}P zPG^0B6Yhzcd=zdal}saPqzuzZM>PMNoCN(7f3J5ym1KVj+Em-tJLksBbIF(SeNDfY z^xQ(S8F0`0b*XmCc4iV1*{ny~)b425x?|b@ptMWV~+eQJ4Xpi?K-5dJDFdkWTnWC zMrPEC6K2fl(8?!NRn1IVx)X`iHO#DQs9SJaMWx0)ik?Y25p9ATwx*skynCCxQDseK z{Wt&?>2^YIPIiC!aL;d3v=yy}+2q(6LyNfI<9aeJmo&MDvW-|KYLsWEsmzzV!jg24!kL!Mfy%g<88a#u5%(bN{^pDmJhzVdH$2&2%~q_l_j`|Q znHrgei-mls-|7sTcjaeg>RMuZg_d^_ROyiESwFK=G+wT}%oOI?JqWx*q4=FloTFiE zjc&K3`*p%qIgq(YvV5rDael0+TNZ_aCTxduxl*KB)H+% zbVo}X1e0rWZD)~c4%uzP+#tv*stmcH6uCu+lM|UBTP*p@FLhkWf~92SbF{|pp&8kG z_OvFa56!f+uJsY7Emcuz%C0=`Fiw%Vke5NNOhwOEXB_T%s7|@r*2>f#-<0+*r;Hk{ z#cgXPM^jo=QJRtohtqB{qRG(}lKTI{)SpkH?k)9yzyJJ6>hONu|8BnDgiW{xYtV+% za3l`La16nLc#CB{g$J+&n{gAqgGFe>Y{)uiBKQ}SKu`if2?Qk<54dK?wvU5R^br z0znA`CGdqQ0aZcoMKgh_o_>yv=6iHYsTCGsXD`F%Dmch9fWlJ4lD5WgG6qEw~vMU=bQI8z-X@<1iGj)1Uu5 zevPMaGtS33ScBC#1K-35yiFhe>v$DA@d&QK24r9&g?eZ>42R;+^zXllM{qsPLn~@9 z0w2()|0~>xHRwbKns6)*!XOO9oAlv7j0bQp?!h&1pkpyk!$cg8;TVDg@jiX|Pvdf2 zhI8S-L<;p7i9;|HL+~E`_%GplT!%|>5iZ1;I2kiA1(Pubf2RNbcX$DhV;dgACg@m# zMOcXAFcM+xg#p+}KmL=r8W*4w4ooD_ia9tI8VP;@6OWrJK~$!B`aURlG>a-dk0f3Httf7j6{v{nMS!#kWMI zUaG}m)vYd{{&xwz(iYMs9f^2BQz|Mo*N0uHr4nXDJ4)?}aX;K3H=et|zJ|Q?ws$^d zIIUK!JQ5{vqoT^On%ZqE>eUzgU%AS`>MGN+Qz}kZ-I?aCMPg~V8R$PU1unK2kG3H?c4#JU&; zjH59cBXKz7S%AIpDdqnO-oZ}1gctD?Zh>r{N{qt+*g>6s8}7$_xB?kiI1>pp;848J z_I(bI;-By!?u3J-kXZktFbexX>ir*KH(r4s^M5bjuffIGfOR+<@(jRa9E`WAzrTg2 zaUX8R4fqM99bi4y;Y`dzH6-T$5DdXU9DopBppO5qxEnWN6RyD;%)&HG!ikV}fv@0& zY&$^M3&ocPvMP4rd9G+bpQZ2}@2ewK;7i325G90 z{JO3=krDaBi>x+o>n&1RtlIx7s}I*K%NVvq8mdosP(c#IHF}1Nt87%J%YJvKZ8h|m zVM|lB_e};D>?__FuB85QI09uQmF`-3M#f8BF6ZP?GVT>yO+k`s5-Oa!NtzH?b>1&o zJrJ7H5)_ClGW>ky_YNMpeSJRgx;L#5hUq|MvK)tHj^;gSLsP#kT|m~GrNxS#zB zoRsniyYv5r;?yOIyWWivESUqfR<}7K5^1tC3IENpuW1}^Gd5&%rz7Bwd5LfCqoP;h1ZZtH5)dWRXK5YKX+Kkl4X5im87si zNVOl)uC87(zh{AjwQt_@wVA{vjf}-)JF1(p>!Xaw}DhjvMbMzS|^!m zxU9Kgcy@(dhxfG@>*B==DQ2(&$)Fa=T|q0g8MTe`Yo||LP&c=s>05QP>ngRQCmeM` zrFJZN)%N^XHYd?Sg`8?sWc&K9G%F`X`@oh%u3Z6KW*yO@Ba9%2F zm2-Ney1IoJ;!JZ@)Jl0T&Q9uPOa9jtiMB*_nRYtM@lT4>L0AO;ds`!yn{ozLs7=tp zQynqwBqJ4x_^Bk$-rbXU>LZ)Z;zi}H$=#o_&*`O|CM&May>e13{R|?>%02<8jzMn^ zt8w&}&)i{36nHinltTVbSuZzBa_;aSw~`^OmEZg?1yk&SGsfp0`E=u{vyXf-TTc&s zO0L{f7LShPrH;~b%X^_IG3RYsi;Z9q$lHnFFH#zR& zvpay>b=GKGXBz6UlFzv`D^&e|1NF&gsDn!Vzuv9>hyFy}{v$k(OK}l4;5;O75>7w` z4#hAG#ka{~dNgp8wyDA7d>RLZ0=n!z@Uj ze+X|=$A1~mL7w^F3VGIFp7TE&2Bd9Z9QMas)b*djW~{{$9E*Y2McsY}UcqCKb^xjW zJ4jz7BAp={1P`q;s9>I6<7%e7ECO{I267Q;2E~XukZx6 z;Xd4jt&lc=YjG8>#Kn+!0TU@SV-}`i66C!BN8nT103L?47u=3bkaq@1n}NJDpbpb9 z8Iv#y`{60t0-l7l7u<_`Any!Vj&`&`Vh0*A7Q?YOK9F_*yajn@z;_|-1?wSg2F<9$ zH&Kl$48q6M`TqrX<3?=4mG~ik0Er(s1NE4RTF5&Cc2Vzt1ux>?A#nrW$84O8<1hvi zH!u?N&H(w>=M#y49w~Vm*|VQg9p8Bu4e$IByeGiB;<+chZclS^#?Rg*NPRANPeAaV zfb1n(1xm*vPt~gHC}BZEsXw+R=3l}6Ly!0 zP2HZQkNl4OCX|S7G}YPNPmaGXH0*U-tCM0>2bgY5A`k zsFI@Uq1d|4pvudiBhI2n}Cx-VtEL{5K}JN0Pe` zDT2ac_0t)=V!^$31+Q4>@_vfo6$|R*5rkO;VHWC4+Mib}sLNL_!oUra^?%ceNZXxy zodI13*{}WVJ&@=B|43bL9d%Ku|NHOP|8MH@A4A>)cn@yC)sSZaF2~teh#8Rg{z+WG z@fd~osng3d058Ii3%HB#=R;xxVu)fIMqvboLD~X#Q@5A+f2sekfr(bMUi#ca zJN_B>;U94qeu{OFHiIV2MIC10?;-64Z{juVg2WB{465u^jWqZ#D1o2^f)WTyASi*L z1ilm{Ky^I`RHG3h`&L|{xVXbrF>OJhS`es~Z8G$`XlwjXFzJo)qQX=UK@h0szE(O2 zRP$Py*<(~&jN2CeR|!;8@6%*&>}w>_3@hWl8MA9Vmt>?%7V0EQk$A7Zufdy>p0+Nl zkox}z^r23m4M6Ju8@-F}fW7esb^BMb6HnkqT!WuL{szGLI0x&IK|9Vw0!uLo$KyCi ztiS=-2Ycf~>iiNn@CN<^ui{Z$iSuwO=AjYQ_&xP~`TGF!j({C_2+~e)4p!kTEXHI^ z#4$J;Bk&&e{ompV`~r7F+6jJug^;#^lOgQ`5?dh87YxJ4vBjzev4?VtTH}WOapUTK zk*?KJA%}khF++Z8CutTj*ftL{N|Y&SmLf2gC8w0D;T3s3#42E0#j>g{>i_%jR8lK{ zO`yqEPoZcLKM!ua?fjnKRML+^PTif>Q`8XNzVB{28PWR})T<*vX3=VSYQeC} zRSZh*G4G1JKPJE^ISsm%wA>^N>uV*-FM}R;OqMODFq?;XZ2qVKKfT5Ue+gYen0Qk< zIgu>MOuY$Y>N-cS!JxUXBOr=Td6%pyTX-q!NBL+OpDt~}m8?k`6LRpsyG{$fgO&Z5gu8?x9! z3b$}>t!~7cx91dwuVp9m^5VZOV5NFhfF6xjYCNypss2J)2W_I!X!dz!@4W(Dc9BvA SXXw$^CK=hJf>OE$3j8ly@g>VG1$Wr1%GDBp@m(FGVRDsK(!S&b>2phus2+ z4@~YPznQt`eD|F1eCM2d&-a~^TYBz>jpmuzr71o~rcxKZG;`4*^Uptg@kdgrTG<`1 zdd^hElFYe3O}WK6+b&McCAqyRxTNOimlR5t<1F^;xv3>iIj1j|d7o<)-Wtp1logF8b#~gjm`z|KAA+bPWfy4rd1riG+7Dz0RSRk=L zVuAl(3k21JQTglFebCfo?u!53jW%s>T3;j^$5=D{xyr*3!% z9)w$AJLF&;^uk$i2AmFyU_R_OQmLQ7gK#5U2VaEkFas6%94v<;;V^jfFm!`^;V!rX zz5%zvt*`?whVx-1oCNzhkMTEn9bSQ#;TP~@xEij2ZEzVlFa*cKF>nMdfHw}sW^fOD z5AJ}Sumeia3unO@a5|g>^WdpNQmH55ao7zH!1ZtyOhX>Jpc9URPr%1v0lZA$=r`~% z?1XFJN|=VNFadd34~yV-?lHa zQ%2sgYBh61rRw=XDrMMif!p=BkuTNVEw!v;yW>I0T(QDjX09^B#A4a61!lJ@t-l=D zzU5?Hdux}@?heJ$6v-zn&oD;T$YGgm!OnXHyUR{%ZPbkumQ%O8%^*FhZmC*SkhQIR zX{_dy^LE!M>1@%lg0YHKH4C0O-DPJGo>sym(x%o@9NQ|41tg|N&67n$t7Wc`|BcLy zxky!m(R4n!1-oe0Y^NCMxJc)uBTGq5VSC%ng^aY-snLvhJDr-&3re=zmKT)Vv~;0i z&_jiC-U{09mUJy5_MJsV5x^ED`j*NYnrB+y#XT2ZhkpJ$TK)~x@48Fd5ytCh{xX<{hDP{Y_QJF9p=@xyZ|W?RYDg0bYX zTdfD-2##e$9WQ0iF{HIf##Ci6`>0_BH8)1tM%y2M#|Vp_gIbrE)>6RSY8x^2)JzKX z9;nLb3Ln0ruRMR0O`@Dlo@=XTW2_8i5~WAEsHbLD?8lw$BU~iI*&AzNRDSyqh#J{f zsRmR1<(hslODVJUic+DWb3@#A?27FMwQhN&$;|IssMW97LCGt0b?aA1Ivq7Z%0F-m z7PUScrJ{Dlb+7m(Dvg4+DdJLp{R-Lz_pus=V7qmBnYVrq0fo+{v?0 zN=B&pI_A}_Ud3y9P3Elp7U@Yn)6{^=E^#4a zN^4saL}<{dqrq^wVyh*DG2my+9+wwM-=%fS$(WnGK>tIy(K@}n&<~!0Dlh%O^V`iB z^}kG<3CkbzeD#)Td#gx)NmkA)OtB1z8C=pNPv%p&g7B?!%{F`d@wyC)KHv9Hx5J*S zvNk9O3}D}Mt%_YR$2v?kpd0ndx}{^RL(JT=5Ygp{*`l)6)?M|WR%KP{EN*hPX_=b? zpYy{V>h8Mh@O%}4s8QK+ZOmHLrG?@{S(;D1ZB1*rx4qRdi$ue^#T0Xm?qaBT+o-id zTQQpXJNq2MB6?)M7h$z#)AP-kqt2q940Aj(i@YU86{^%DsHZC3XU+9`428w?z8%zk z*VIEwtrJz7)FL!39j-207OLFT{v3LS+wW3uS8Iv+t)wXNj zEJkL8t~IPXTum3Oz>;F4hiOal$g)w%K^qYY_2}_^YbtFnT&NO9mX4~K@|o{1!- zBFS`L-8(Q8t%dVBnXu|)JH<6LEc#w0Ozw(_RJ=mnvGv?erF{F+dfB(lj)M3AOLFzH z6JW}Y_6(~QVA+PWl*o0bNi~<*?pRGt$T3Iz95@Vq-A;-B--&;DjiLSjX#ai}{`^Hh-4orji^p}DITVMowU^#peUc^^_27U(j!qsp&Yy}_0uOEjZ48k%v z2;Rnre-rk>AK?MG4$gyl@H9UA{UE;m7@P-d;5c{{zx+jb0iJ=UVK?l8yWrb!Gh7c} zfJwLnE{3x~e0=fmPk^If9;9F&HhK-7gJ)nb{1hGo@&CUMcf!rE1H`7^gyfT0AhAGV zfy4rd1riG+7MR5XYC+oK%!+^273mi{V?6nPWIxt3qHa*hrqiLXs)2B$$H zUt-hEsqx#HmyZJ5-*DeTKT%2RKqf;*JLqlmx6SX=BP(=5qe#O0h{YQ5s3!YRj2RZE$92pux`e7%Jz%s#SJW^?^yF%{ zx;8>{18$^h1tk^m(jmY`F*KxgS8k-N;(S_CH?%BIGrt^6jpa*rev69tG~(H68c619 zokwRcYP%uU97DBIdG+xD5T&cINkdsI-98}NN@t=sHO`ogJJlu{U6RH!u|Q^@J5lyM zSK@WiY|WS(%k;84uAlwVy*;^_=hOpx5VJ`%lP$jTMBCM{H)#136PFqG)_WB#sr>&7 z*+;#Fy;|A-zcze1y@j8@58i;^!kusfoDHktc=!YU{qyh~+y=KoKlH&W=mv=cq~TcD zk6-@^JPx{|7j(68g9?w<~ldtFcI+&Qp2h+({{j#}8kYb7 literal 0 HcmV?d00001 diff --git a/lib/dhall/.builtins.rb.swp b/lib/dhall/.builtins.rb.swp new file mode 100644 index 0000000000000000000000000000000000000000..91f9acfc29dac131acb37dfc172d32ee783e55ff GIT binary patch literal 20480 zcmeI2eT*Ds9mhuslLS=6U%&-+AVl=l9H0={~e;ueh_&ZE$?lFm8JHSZU{q!^=9C8b;`N zLv`OBA2H>{*^jAoofXTn$7f6VwW)+%VNmU=4V$jp88j;6U9MA!PrE7&$Bi5>ECiL= z%F*#!0j<;^(D#qfh0UJ<9c$c1Fe8oKr5gX&Ia~+V!kgC_#?Rm>cnrp11Z=RNAGSgs*1+5JwZFlO@GOkN z2*^J82z(QU;eP0Y9>~F`;p4ChZh)omCJRr0f|KwRxNslz!mVJyzgXP*4q+xfvZJQk zu(G1}^J1(S=Xf=1OvUXpqefu51)PD$O%TtfI&!)o0TRW$qEPo|7dMMO=G7|5cu& zs!YcgGL;jS%`Le-P8j87bj`9wl?^sIuE~h1Ylfkam&?imt0wLe+v43eQX9*w$!tl` z3^QS)ZUyp6#&W}?5wbel3BpLl%WLxJb1A$KShYsglC^e-jeT~$;Q7Ib={gf}-l;;A zDYoy%V)nVRg&jf_LNF1ZCdRAEX=k5Z@EmtbT5UP~i^7&}AcX3MQ9$Q0A= zrP#Q!ZHBmqZ>`r|r)tU~@@dLxk3hQw~@Z;eGW4U7D;QXsQX zyTW1r$ihw9=KIq|T&av-t8H17R21;RS~Ot={^Cq>!Y@(A!mUb2X9iolphow!UrY_8 zQoA~%FoS3^q%sIM-vqIuEn|6x&Oc*}mVKa47NZ)h9z}+2BG;-|IUe%haVE=GV_tmP zIykqrt7#H-#)e!$xzon{S&E&ryeTtPQ!?)ihloLQrmx42#{OPJH9q|+sBXdQdHlS}Dz zCzG6KGQn_I6m4?!G*h@TMY}mvxjB2v>}T>~Mt)E%-s?6(Rdd`4GVL-Z)lFs3mb1yk z@9y-iCFg~45m!)x>_F<#OYeE}IaJfpwBMxRtdlLuS@io>zGho{krX3+ea37zA#69rzQfc+6d&7Lb$$P zM~3FRJegt;l^7~(D#R*rU;Jp8$$~mfa`pD+R3s+GsgkKW&)Lo~hWAibV!Q^#2?9pnt`WmHvPF z{r(;N`AcvfUW0QW*8$GJX?PC44-Y~J4?r32hkIc+?1Ee2W>^BR5gzMuRPG$#B3>2-#)S>{;2%fQjo?3i3^-9d1;i_jIz@xyBSqUqbkj) zQW{k%HRH0)xNIC3>%v{i$=js7Q*I6mw_}q6!x|g9H}i#NgBUCD0Y)6l7e=gL$dav( z9VFSx@@&hHagzOYxoT{><^RDI@M*TS@y%05Ho2!Qe(r~}3f{D*jq{%Put|`*w3%6# zF9KGGg5=}Tw4N!K{oC}+^p>ix0!ijM7no8@+FHymo_^r02d3TOqi0$KsBfL1^&pcT*xXa%$aS66{#p=xH( rvZZydeY4GMSD5}v_t{>>ZMN@SQM;0Liw}60?YtKWhAs2`_rLuY_J%zH literal 0 HcmV?d00001 diff --git a/lib/dhall/.normalize.rb.swp b/lib/dhall/.normalize.rb.swp new file mode 100644 index 0000000000000000000000000000000000000000..21569ab3c1cf09b7de2041aa1669d20cfd5df32b GIT binary patch literal 28672 zcmeI)3vd+m9l-Gu1U+81p!JPQpqfB90u-guOdtdVgai>#ikMzf-P8QiZY#oR#CLbLs3M~iXci+tBBR|uw(I!js5=ib$gc!m|*ER{ol-I?r!(L z|K0oT?(P2m|NmWO!GsZ`wSm3@504*sJg4uOb@h)rT-C1kNghu;7_Ny%LiKfinc4Is zRjzlXu2dJi-+tfDnod)K@v!S@YrS7$J)dhm+w)sn??+qD z%QNO%Z`G5EfQo>MfQo>MfQo>MfQo>MfQo>MfQo>MfQmp1BH#~rJolaA@oa+h|J!-~ z9^Su;7p!?3czy(T;uhS1xrks2f|!VLxB`PvjQ;SUH_pWwI2|Y9>rNiee(b=X5XEKi z;_Z$e&x_cAN3a|Z;5WDr3osis7>ZVStAoe07!gduSd^d;{m~ow=!%Z`tUaF_kK&i8 zLkTWGS9C&Kd_$wgm-qr7U?9iCwOr(KA}PCpZEyx;!W(vW^BZ>upeGM9PoInLjHJM8>?4EVu5k>QJuP6(?{#E znv6;1(L^v3_J_(M;U?y!S246Mny4QYj3?43yQi3I^x99(v)38b!iMtDLvh`B;hNzK z)yD0a!D=nFgfCVb_XXn>{^DF`6Y?4@O`+^dQ*9GVTa~aidYv9l#0%XkmBs8CS}*q; z*&KV0xfv1yUs%5`*LcguPjYQN73F6vKH0~>pJHu>Hgoz+ZMwB}Qc0dR%cvr?xK^aa zlTke;lLNXdEKD%>xGXm$60Y(m^f1^tcG!*GFVU96LmsJWjrYyo3tCZ;Hcp>ze%5LJ zP*N|{a&nrtFOFD8X6303mZQUGtg`XWFeaN@(ZblvdRr2ES?)N-zRaIU#{41UP_x3{ zxB1aOLM>Tl6__i~jEB!3u6K@G*^^lpunuAluWzwC%p)^PJz4jC&x|w4JS2{3-&?D0 z(e4k{>GA*e36~`_);@8a&+;8?tgZA7PE|YV4}B?!P0{k=nYWUo6TZiJ?=I z{!oh!+RSZ8#FEE1aH$oxIBuybniIB`$1Js$rtfd8Q`A+|J`^%OrZ1)kl2v-Ht0c?j zH*tV9aZFRUb;lw5(=6m(4>e|44@(_+J&lgqMk`5e_0f;h!Q8TNPFZ&@_6>~v?Al!W z#B0XwWV6Ga^|(*Fr=!YakM_}5!%i?)^W6r!oV!c&Ub37!O@AU1BlbqD&8ZXov7o;) zl#wLJ=2FfqGAzP_a$Q`R|hP|)r{LzYdvQnQOjp^|? z1>(8q7dnTIeEf{tU}FP3F@0(>7}K>JV^Dpc%49H<2!`W19#40zIu^NJ4_Cw!F$VNk zgn|h^WT;S+uL6(c|NY2Y=aT12{y*AEs{TcOeh>$+9WUc0tir=si6vNsdvQDF;U>($ zwYUVQ;ABX?|1o*}n|K;au^5Xm2h%VT7s7}0a0WW#hiHXe}B z5EC#SBT$MVD1e4f$oto09%^tAeCUp|aVomtb>guNTd@UCV>O<@gLnYH!|j*{iJ!C~ zsE3MxihzoMihzoMihzoMihzp1kt1Lv8m??Z`Yr~C!;wTs0u{s!wC$vKCx?rL<*PK>p&C8>1C-JoF z@_K7xkz_O@*_@QwTx}Hck-?C%n2lq;DUo0}Z?dr)qX*65Z=&*k0Q;dR;+=x1?0v(KqaR_T>hSaaoNYHq$UTh=0( zHZ{mgW1>?*fCIod1>{rPAKM$#>17BT#qEY5CzAQ8?Jzcujn9>OsmNJVY7_D@+JLei zN+YW6{c9dH2$R^TB#h=sTV^HC4!_aBaaXoC~6o4W3YQ3Nx>-De5!=>Dp zy#El}uo86`j<(oMnN3)W6_9*?DHh>g%*PA_P=asB+5d`r5W-a`M=>PFFF;S^LGt`| zI7Gg_5f5WFrl1%-a5mbbHNK{OC4}YRk#5WRAU0la48035c;7T+F>L8{c|u5-Ov_0=+9q|J8?ax!jFjif;;HO@YC z!2E8N?`+liZ~fy)py@6OTAt-1nt8*cI{%N~z>6&Xz^e0~At>gF%#BD(2HhM(2lP1A z`TswQz3Tk8hb*M7b#^i*xAGY`+E(tRI{%#k3(X0e>ij>xo&T;>)Z9&tCh+fQM(XV3 z(y86)^T%qE#%NBT(aiGgm;Lr7^?++FEm(|2QXA|}y|YiX6Y|ttU$xb%?yI8LJ-4T8 zj`Q*D^xQSiS<1X4E;0Ma^NcO9lK!;Pw6CN$PE;q&VY{hP?k^py3MrIo0+1T4#WKE> z%#b4hC1U3Jav&kGNfyz^6z^_{x4(j`;d=I{!a>P zJie0r93NpTWW0Y3evS$ZfGi_p`!9fu?LQ44P}g&i{{1_U!?e!mhz^i3|1u8X9c;#f z&@l)NU$e0t7GymqK#>KFCE5xp~?6hqJp zXQ4ILljqMy84A%3pOMQSgyj6M;bpvlO<0K~xEZAwfJ5Zy2k;D5;6_AI1IhWzA>;i^ zP=rfRfL`c{GjS@qpfwuE=l_j=U@zXoPHe*~Sc@mI8pcEA{d^5`VKQ1d8#TPjAU2iv zbD>GQ)W}=sn(4X*sk}e?6)oe6W!*+gBZwOGpZ+t10(=ZzJQ@y+|S z|NBAza(ia|R@3>>XX7c(9h{TTXIn14)X__jZ9B~huG04Qm|Mm#5G?T=VkWlGU|0!*>6<8$6s+=Ka5`fk8@G zZ40_IddP;!`2Y1JRO86OB>%VnpYJfay0ii8!~56^84K_VHewytLdFIxhl~%9-vP+j zfSJ%S1Sdeo{L5JX2qs}HN>GUY=#6}6I0avj*YAXk69}UhJUBq^{vNht3pQdcp2kWn z!Of7q|59{D1G)Tm$k_drSc-da7jDC?n2s8Zfrbv)MPC0L7GpM&&@mYkFb3r)f%N^K z1^LbY0!+pToQ~G`irjr4_Fy+&!wx(T>HA-TtI!1>lGm@oV$?$V_;b(+ZSX1i`$7C2 z@8ECPgvYTI@_T>D^Y@X{@5C}Jg#6CG9#b&|0aW2KNE<+R$nX8PLHhS^!8I5O4IR)L zlK1b&Uc8N6cmrFp3D08{9>z*6#bPYNP51@oK>i<~4k5^Y1dN9qgJt+0Ka6uK?FT?= zOoAGdU|$04D}nv&YJxDX0?swdHAA&cH0PdGwM{hsiv-m+VV{5BO=Dn|W*gNuq1q-= zf1}WxFDx}CL5)dp`f8-z#vIO-aRXqFLr)!9()FYMkihyAAmg_T>JJH8@`nWf0otxN A+W-In literal 0 HcmV?d00001 diff --git a/lib/dhall/ast.rb b/lib/dhall/ast.rb index 903c932..08cd4d6 100644 --- a/lib/dhall/ast.rb +++ b/lib/dhall/ast.rb @@ -2,26 +2,34 @@ require "value_semantics" +require "dhall/util" + module Dhall class Expression def map_subexpressions(&_) # For expressions with no subexpressions self end - end - class Application < Expression - def initialize(f, *args) - if args.empty? - raise ArgumentError, "Application requires at least one argument" - end + def call(*args) + args.reduce(self) { |f, arg| + Application.new(function: f, arguments: [arg]) + }.normalize + end - @f = f - @args = args + def to_proc + method(:call).to_proc end + end + + class Application < Expression + include(ValueSemantics.for_attributes do + function Expression + arguments Util::ArrayOf.new(Expression, min: 1) + end) def map_subexpressions(&block) - self.class.new(block[@f], *@args.map(&block)) + with(function: block[function], arguments: arguments.map(&block)) end end @@ -88,6 +96,34 @@ module Dhall def map_subexpressions(&block) with(elements: elements.map(&block)) end + + def type + # TODO: inferred element type + end + + def map(type: nil, &block) + with(elements: elements.each_with_index.map(&block)) + end + + def reduce(z) + elements.reverse.reduce(z) { |acc, x| yield x, acc } + end + + def length + elements.length + end + + def first + Optional.new(value: elements.first, type: type) + end + + def last + Optional.new(value: elements.last, type: type) + end + + def reverse + with(elements: elements.reverse) + end end class EmptyList < List @@ -98,30 +134,50 @@ module Dhall def map_subexpressions(&block) with(type: block[@type]) end - end - class Optional < Expression - def initialize(value, type=nil) - raise TypeError, "value must not be nil" if value.nil? + def map(type: nil) + type.nil? ? self : with(type: type) + end - @value = value - @type = type + def reduce(z) + z end - def map_subexpressions(&block) - self.class.new(block[@value], block[@type]) + def length + 0 + end + + def first + OptionalNone.new(type: type) + end + + def last + OptionalNone.new(type: type) + end + + def reverse + self end end - class OptionalNone < Optional - def initialize(type) - raise TypeError, "type must not be nil" if type.nil? + class Optional < Expression + include(ValueSemantics.for_attributes do + value Expression + type Either(nil, Expression), default: nil + end) - @type = type + def map_subexpressions(&block) + with(value: block[value], type: type.nil? ? type : block[type]) end + end + + class OptionalNone < Optional + include(ValueSemantics.for_attributes do + type Expression + end) def map_subexpressions(&block) - self.class.new(block[@type]) + with(type: block[@type]) end end @@ -138,6 +194,8 @@ module Dhall end class RecordType < Expression + attr_reader :record + def initialize(record) @record = record end @@ -149,9 +207,15 @@ module Dhall block[@type] ) end + + def eql?(other) + record == other.record + end end class Record < Expression + attr_reader :record + def initialize(record) @record = record end @@ -159,6 +223,10 @@ module Dhall def map_subexpressions(&block) self.class.new(Hash[*@record.map { |k, v| [k, block[v]] }]) end + + def eql?(other) + record == other.record + end end class RecordFieldAccess < Expression @@ -251,6 +319,26 @@ module Dhall include(ValueSemantics.for_attributes do value (0..Float::INFINITY) end) + + def to_s + value.to_s + end + + def even? + value.even? + end + + def odd? + value.odd? + end + + def zero? + value.zero? + end + + def pred + with(value: [0, value - 1].max) + end end class Integer < Number diff --git a/lib/dhall/binary.rb b/lib/dhall/binary.rb index fe09699..8f83534 100644 --- a/lib/dhall/binary.rb +++ b/lib/dhall/binary.rb @@ -2,6 +2,9 @@ require "cbor" +require "dhall/ast" +require "dhall/builtins" + module Dhall def self.from_binary(cbor_binary) data = CBOR.decode(cbor_binary) @@ -13,8 +16,6 @@ module Dhall end def self.decode(expression) - return expression if expression.is_a?(Expression) - BINARY.each do |match, use| return use[expression] if expression.is_a?(match) end @@ -32,7 +33,10 @@ module Dhall class Application def self.decode(f, *args) - new(Dhall.decode(f), *args.map(&Dhall.method(:decode))) + new( + function: Dhall.decode(f), + arguments: args.map(&Dhall.method(:decode)) + ) end end @@ -82,11 +86,11 @@ module Dhall class Optional def self.decode(type, value=nil) if value.nil? - OptionalNone.new(Dhall.decode(type)) + OptionalNone.new(type: Dhall.decode(type)) else Optional.new( - Dhall.decode(value), - type.nil? ? type : Dhall.decode(type) + value: Dhall.decode(value), + type: type.nil? ? type : Dhall.decode(type) ) end end @@ -208,7 +212,7 @@ module Dhall ::TrueClass => ->(e) { Bool.new(value: e) }, ::FalseClass => ->(e) { Bool.new(value: e) }, ::Float => ->(e) { Double.new(value: e) }, - ::String => ->(e) { Variable.new(name: e) }, + ::String => ->(e) { Builtins::ALL[e]&.new || Variable.new(name: e) }, ::Integer => ->(e) { Variable.new(index: e) }, ::Array => lambda { |e| if e.length == 2 && e.first.is_a?(::String) diff --git a/lib/dhall/builtins.rb b/lib/dhall/builtins.rb new file mode 100644 index 0000000..1f63261 --- /dev/null +++ b/lib/dhall/builtins.rb @@ -0,0 +1,265 @@ +# frozen_string_literal: true + +require "dhall/ast" + +module Dhall + class Builtin < Expression + def ==(other) + self.class == other.class + end + + def call(*args) + # Do not auto-normalize builtins to avoid recursion loop + args.reduce(self) do |f, arg| + Application.new(function: f, arguments: [arg]) + end + end + end + + module Builtins + # rubocop:disable Style/ClassAndModuleCamelCase + + class Natural_build < Builtin + def fusion(arg, *bogus) + if bogus.empty? && + arg.is_a?(Application) && + arg.function == Natural_fold.new && + arg.arguments.length == 1 + arg.arguments.first + else + super + end + end + + def call(arg) + arg.call( + Variable.new(name: "Natural"), + Function.new( + "_", + Variable.new(name: "Natural"), + Operator::Plus.new( + lhs: Variable.new(name: "_"), + rhs: Natural.new(value: 1) + ) + ), + Natural.new(value: 0) + ) + end + end + + class Natural_even < Builtin + def call(nat) + if nat.is_a?(Natural) + Bool.new(value: nat.even?) + else + super + end + end + end + + class Natural_fold < Builtin + def initialize(nat=nil, type=nil, f=nil) + @nat = nat + @type = type + @f = f + end + + def call(arg) + if @nat.nil? && arg.is_a?(Natural) + Natural_fold.new(arg) + elsif !@nat.nil? && @type.nil? + Natural_fold.new(@nat, arg) + elsif !@nat.nil? && !@type.nil? && @f.nil? + Natural_fold.new(@nat, @type, arg) + elsif !@nat.nil? && !@type.nil? && !@f.nil? + if @nat.zero? + arg.normalize + else + @f.call(Natural_fold.new(@nat.pred, @type, @f).call(arg)) + end + else + super + end + end + end + + class Natural_isZero < Builtin + def call(nat) + if nat.is_a?(Natural) + Bool.new(value: nat.zero?) + else + super + end + end + end + + class Natural_odd < Builtin + def call(nat) + if nat.is_a?(Natural) + Bool.new(value: nat.odd?) + else + super + end + end + end + + class Natural_show < Builtin + def call(nat) + if nat.is_a?(Natural) + Text.new(value: nat.to_s) + else + super + end + end + end + + class Natural_toInteger < Builtin + def call(nat) + if nat.is_a?(Natural) + Integer.new(value: nat.value) + else + super + end + end + end + + class List_build < Builtin + def fusion(*args) + _, arg, = args + if arg.is_a?(Application) && + arg.function.is_a?(Application) && + arg.function.function == List_fold.new && + arg.arguments.length == 1 + arg.arguments.first + else + super + end + end + end + + class List_fold < Builtin + def initialize(ltype=nil, list=nil, ztype=nil, f=nil) + @ltype = ltype + @list = list + @ztype = ztype + @f = f + end + + def call(arg) + if @ltype.nil? + List_fold.new(arg) + elsif @list.nil? + List_fold.new(@ltype, arg) + elsif @ztype.nil? + List_fold.new(@ltype, @list, arg) + elsif @f.nil? + List_fold.new(@ltype, @list, @ztype, arg) + else + @list.reduce(arg, &@f).normalize + end + end + end + + class List_head < Builtin + def call(arg) + if arg.is_a?(List) + arg.first + else + super + end + end + end + + class List_indexed < Builtin + def call(arg) + if arg.is_a?(List) + arg.map(type: RecordType.new( + "index" => Variable.new(name: "Natural"), + "value" => arg.type + )) do |x, idx| + Record.new( + "index" => Natural.new(value: idx), + "value" => x + ) + end + else + super + end + end + end + + class List_last < Builtin + def call(arg) + if arg.is_a?(List) + arg.last + else + super + end + end + end + + class List_length < Builtin + def call(arg) + if arg.is_a?(List) + Natural.new(value: arg.length) + else + super + end + end + end + + class List_reverse < Builtin + def call(arg) + if arg.is_a?(List) + arg.reverse + else + super + end + end + end + + class Optional_build < Builtin + def fusion(*args) + _, arg, = args + if arg.is_a?(Application) && + arg.function.is_a?(Application) && + arg.function.function == Optional_fold.new && + arg.arguments.length == 1 + arg.arguments.first + else + super + end + end + end + + class Optional_fold < Builtin + end + + class Text_show < Builtin + ENCODE = (Hash.new { |_, x| "\\u%04x" % x.ord }).merge( + "\"" => "\\\"", + "\\" => "\\\\", + "\b" => "\\b", + "\f" => "\\f", + "\n" => "\\n", + "\r" => "\\r", + "\t" => "\\t" + ) + + def call(arg) + if arg.is_a?(Text) + Text.new( + value: "\"#{arg.value.gsub( + /["\$\\\b\f\n\r\t\u0000-\u001F]/, + &ENCODE + )}\"" + ) + else + super + end + end + end + + ALL = Hash[constants.map { |c| [c.to_s.tr("_", "/"), const_get(c)] }] + end +end diff --git a/lib/dhall/normalize.rb b/lib/dhall/normalize.rb index b36eaa1..435f90c 100644 --- a/lib/dhall/normalize.rb +++ b/lib/dhall/normalize.rb @@ -1,13 +1,37 @@ # frozen_string_literal: true +require "dhall/builtins" + module Dhall class Expression def normalize map_subexpressions(&:normalize) end + + def fusion(*); end end class Application + def normalize + return fuse.normalize if fuse + normalized = super + return normalized.fuse if normalized.fuse + + if normalized.function.is_a?(Builtin) + return normalized.function.call(*normalized.arguments) + end + + normalized + end + + def fuse + if function.is_a?(Application) + @fused ||= function.function.fusion(*function.arguments, *arguments) + return @fused if @fused + end + + @fused ||= function.fusion(*arguments) + end end class Function diff --git a/lib/dhall/util.rb b/lib/dhall/util.rb new file mode 100644 index 0000000..8db6545 --- /dev/null +++ b/lib/dhall/util.rb @@ -0,0 +1,17 @@ +# frozen_string_literal: true + +module Dhall + module Util + class ArrayOf < ValueSemantics::ArrayOf + def initialize(element_validator, min: 0, max: Float::INFINITY) + @min = min + @max = max + super(element_validator) + end + + def ===(other) + super && other.length >= @min && other.length <= @max + end + end + end +end diff --git a/test/normalization/beta/ListHeadEmptyB.dhallb b/test/normalization/beta/ListHeadEmptyB.dhallb index 16d01236240c0c459f72855f1b468d5576313685..a8f5392f554f81525ea46899299c15051a4d056f 100644 GIT binary patch literal 11 ScmZolHPtiFGiYK>3;_TWVFMKa literal 16 XcmZolHPtiFGiYW=@ypLkO$-45D8vN? diff --git a/test/normalization/beta/ListLastEmptyB.dhallb b/test/normalization/beta/ListLastEmptyB.dhallb index 16d01236240c0c459f72855f1b468d5576313685..a8f5392f554f81525ea46899299c15051a4d056f 100644 GIT binary patch literal 11 ScmZolHPtiFGiYK>3;_TWVFMKa literal 16 XcmZolHPtiFGiYW=@ypLkO$-45D8vN? diff --git a/test/normalization/beta/NaturalToIntegerB.dhallb b/test/normalization/beta/NaturalToIntegerB.dhallb index 84dcc71..2584333 100644 --- a/test/normalization/beta/NaturalToIntegerB.dhallb +++ b/test/normalization/beta/NaturalToIntegerB.dhallb @@ -1 +1 @@ -‚e5.0.0lNatural/show \ No newline at end of file +‚e5.0.0qNatural/toInteger \ No newline at end of file diff --git a/test/normalization/beta/NoneA.dhallb b/test/normalization/beta/NoneA.dhallb new file mode 100644 index 0000000..221e29e --- /dev/null +++ b/test/normalization/beta/NoneA.dhallb @@ -0,0 +1 @@ +‚e5.0.0dNone \ No newline at end of file diff --git a/test/normalization/beta/NoneB.dhallb b/test/normalization/beta/NoneB.dhallb new file mode 100644 index 0000000..221e29e --- /dev/null +++ b/test/normalization/beta/NoneB.dhallb @@ -0,0 +1 @@ +‚e5.0.0dNone \ No newline at end of file diff --git a/test/normalization/beta/NoneNaturalA.dhallb b/test/normalization/beta/NoneNaturalA.dhallb new file mode 100644 index 0000000..555303d --- /dev/null +++ b/test/normalization/beta/NoneNaturalA.dhallb @@ -0,0 +1 @@ +‚e5.0.0‚gNatural \ No newline at end of file diff --git a/test/normalization/beta/NoneNaturalB.dhallb b/test/normalization/beta/NoneNaturalB.dhallb new file mode 100644 index 0000000..555303d --- /dev/null +++ b/test/normalization/beta/NoneNaturalB.dhallb @@ -0,0 +1 @@ +‚e5.0.0‚gNatural \ No newline at end of file diff --git a/test/normalization/beta/OptionalA.dhallb b/test/normalization/beta/OptionalA.dhallb new file mode 100644 index 0000000..0d80c99 --- /dev/null +++ b/test/normalization/beta/OptionalA.dhallb @@ -0,0 +1 @@ +‚e5.0.0hOptional \ No newline at end of file diff --git a/test/normalization/beta/OptionalB.dhallb b/test/normalization/beta/OptionalB.dhallb new file mode 100644 index 0000000..0d80c99 --- /dev/null +++ b/test/normalization/beta/OptionalB.dhallb @@ -0,0 +1 @@ +‚e5.0.0hOptional \ No newline at end of file diff --git a/test/normalization/beta/OptionalBuildA.dhallb b/test/normalization/beta/OptionalBuildA.dhallb new file mode 100644 index 0000000..82b6f73 --- /dev/null +++ b/test/normalization/beta/OptionalBuildA.dhallb @@ -0,0 +1 @@ +‚e5.0.0nOptional/build \ No newline at end of file diff --git a/test/normalization/beta/OptionalBuildB.dhallb b/test/normalization/beta/OptionalBuildB.dhallb new file mode 100644 index 0000000..82b6f73 --- /dev/null +++ b/test/normalization/beta/OptionalBuildB.dhallb @@ -0,0 +1 @@ +‚e5.0.0nOptional/build \ No newline at end of file diff --git a/test/normalization/beta/OptionalBuildFoldFusionA.dhallb b/test/normalization/beta/OptionalBuildFoldFusionA.dhallb new file mode 100644 index 0000000000000000000000000000000000000000..e55bfdfc651c9c00b4c0798d3334dce6feaf91ce GIT binary patch literal 52 ucmZolHPtiFGiYXLX2|m|D9OyvOU%(vD$UGENpb{>=E6nO@lFalFa