From 1f73dfde2ad423c3f9d211e984c879d331239a77 Mon Sep 17 00:00:00 2001 From: lukstafi Date: Wed, 25 Feb 2015 02:20:28 +0100 Subject: [PATCH] Complete FFT example. --- doc/invargent-manual.pdf | Bin 176579 -> 176752 bytes doc/invargent-manual.tm | 11 +- examples/liquid_fft.gadt | 2 +- examples/liquid_fft_full.gadt | 189 +++++++++++++++++ examples/liquid_fft_full.gadti.target | 83 ++++++++ examples/liquid_fft_full_asserted.gadt | 191 ++++++++++++++++++ .../liquid_fft_full_asserted.gadti.target | 82 ++++++++ examples/liquid_fft_simpler.gadt | 2 +- examples/liquid_fft_tests.gadt | 98 +++++++++ examples/liquid_fft_tests.gadti.target | 81 ++++++++ src/InvarGenTTest.ml | 22 +- 11 files changed, 751 insertions(+), 10 deletions(-) create mode 100644 examples/liquid_fft_full.gadt create mode 100644 examples/liquid_fft_full.gadti.target create mode 100644 examples/liquid_fft_full_asserted.gadt create mode 100644 examples/liquid_fft_full_asserted.gadti.target create mode 100644 examples/liquid_fft_tests.gadt create mode 100644 examples/liquid_fft_tests.gadti.target diff --git a/doc/invargent-manual.pdf b/doc/invargent-manual.pdf index 9cd91fb373b0cf82a8219f958f4a106400e1b1f2..8799ae33960e181ff4a7a0189dfc93525ff832e8 100644 GIT binary patch delta 17944 zcma*OWmsI@vMr25&|tycg16yLg1fuB2Myj3EV#S7yE_TN3GN<(6Ck+5$9ukW?%g}t z&vVcE(NbM=%vm)?)#|l+cJEKr-&?4D4X`rIPys6kvLVOyOV)KeKP`m8^q@7%yJLMr zjBnwto5KFsLH_>k0T_KMTI4ubWN6Pfs+Y1K)yB&`q7zIP7hXT~{E(%XU3I1S&gJ#4 z`U>eG)t5q_-{XqO!hb+9@WhDh3Z59g#W-$^^Vu2h;# z`Ggs{&fe;KDwnw%MKX?-SmniNYeph4 z^CZZ4zg>)Gqsz=*HWx(VE-FR?KBNVCx6+T2tlNP){zD5yXE(~;l~R{cPO z;bHq`q2Zyn$ytf8eynxa~>OZwE~= zN(^SLGb0gaA^P-H4~9kggY?h2;1Z4M4>qf>)sRreM|8Nz;x&dVvNox(I%~1#1uwhv zPcA>?s@%$|Y-$J}$H1kZM|e62j5YcPA#^qeZ=d2uN++&{OGoqBPaBRL{}{o#xSq^P<9WqvXbREUmu67I4 zyDFZhnNbIx4tyLbYu4;jk<%X#%!IPthJ)4?X^#Xl5~Zc4*9b~1ZIYYx{le;@$a&98 zzxC|6k2FD5ABqvCen@zFCB?#o{_^XpFOr!4*a%QHAjhyR1k7LyBvs-u3h%c?KL++H z(VuP^CUrK>J-*+1hCzUrr9$Liz%E=pAi`c_Hik>SxU%beg7@^0i!Q!!*G;c`syW3p zl*||y1ZU11Yi!CAn9;^k6RPV&XH4u+tmAnX zqo!{#pHW|hj(^+Mmywl7X!5c1SfZNRLvc6P6DbLsEDpFo(D zkqm#Y^}cTYvV+5DhbxoJ_5{@+inQ3@2Eh;$apg0=K0Ft}tDeiX0!u49s99YxWKrf* zIeX0$K}e(Gkd5b%;iHk-b-bM(*?MFi8}vE%umJ-mv!y1`x=%56ZM`>YU=3Lb7hY^M z#+G-Fw4>(C*T2h3Ygw-sgre^@cj2jcJE#^GUl-$XzOZ>s(Z}-Sfn2{(Jm4_w5Ai`* z-O|hm{SIa35Xdv3?dp9Ctu-P*ktCH1WdG)l;C9yh{pGPP9`R`EEsFehPXy5~BxKKT z0}|d3x;O4$nm^n2AbQ_tQcgj@_)+`(-PAL*v|j9a{fGi_E~fni?^4q59*Is=DXO{s z#G)EKwLH8TI68BWHj34=e3N8TcV;*hJojf1Hlc%BiAe^t#l`QT)GL05B_k2#)D`$X z3YUDiJ6o*W<=N?G5pP54l&4BCo0qHt+qfV<8$v9lO04xOMr7JS7lUc?#50!qm1x35 zUYCaAEnNg2Gnbf%9d*L}Z^jXL6+N(9w-xwmVro14gB0~aflz~PcAiYm*2PGdI}K87 zro4uSvW`x?_ElwQK)^m@xX;W z*i|~j00V4eAg*hih*ilGwYQh3!*j@5)-=i}q^q!L{(DQ|7o)x#=&y*zPNJh9uKw&K zlqIXaMyJo2gU0OEAN#*97Jw7RX@IRg;=CEX{O8!%Nn}&d$y#_QLl>RfucH0LAM04p z#L|epzsTkqCzREhB>BzkGvfS4uIJfb(~*2s5E)9sLmlQk&Z;eCl;Fw_tVVfUggGfa zV)pDv)RmFQR1zrZv)?+K7A=3*jJ+?rL$Jb2^TulsyUkn3+9hgARiVm{-%2ecOK9== zPDXhn9I5FH>ds^}n`}I7^QuIr){0L3&7ft2lSu3a0__d*@yQ7t9#p-X4f{2&Rr=XR z=E9kHN}S5;PG1R0>R6acCs>{DF=N)I4VXPj!FG&z$ z+U|xa%%~WZD9p%R%vXLYNkFr`J!js|SK@#9C?$p+nva@#A1^o^N5{CmeUAeRgwRHw zJ4E^kDs|#E9ouUqw${P0)aHoOabS*kkfg7*mfn;#V*M+ zuHLd5M}<;;ASEA#*+8GPS&J?8s|QnC^EcExnd=>9B9mH?Qo9 zCrvNIqO!mHzSrB4IxoZ%PC2vY*@s3^As-dou5P<)^I|8dFUWtmS97S)B<$(Ag@2u* z3>_wFh!jB$>9B^aI%l&8uqi%PKto@6v#g~T2z*E1o$Sg%@!Ra6vB?{JfVtvQlVzBh z>nlm#Inc0^i^{%(*pV^%?zGUZ2c0EXcI}}{mKH-a9=dnndM|g_Yg+ao6*9Wq zO3O-W%B8Ukm7~=--EQE|AwHJv_lJ&H*xDIG+#`?t?DmxK{KX@C0o2)ha=`v&%FhxF zwzcNQVobbB#5KklsB|<5SYocio$K1^`&)X&u0$o@ln?Fx=eY`#+IrjGe1qbU3{&IV zqSqXw8MDs7R&m61j`w*X6+_fjRR~M#_pJHP~K>9r7QXwiA>4=)X*= zW*xINg!A~yYr7CMNut9xC~@B*MDaw0xk_86YHy#e5cMW>=#OWTclYI)WwO z|AcNW8l@wvA{0?L;M8h7=R>FE)3@afM3Lg6JpRh*7;AxzRgED%xd7ct4Kk5-=31>I z`PLiw4t&POE_u|cx;MJD80?nWlx&oTa~qs6%D2ylmOAk&Tk=Mvtk0r+J^@!-o(}nU z=OY=VKl08{Ws5S_O-cPLR-s8Vw5BQ(ZpI>`j#6f=vZ{*cElN|8)|z6`k!UKZso(aJ zBJsUGXjHsXtoIFZvIJ1r%#kdR)WnPr0T%kA$!M5K-)8ddLolSwojz3`jDO;%%D;nY z6it#8POERBul_FOcoj=of_^ z4OfFmNF~0*JHxVpNfhs?NGPla#@nw>EbyvXH{1K0&bK1)!8*`jV%2qR<0Ij5DJpN- z(8i6mZQI03*J&Dd&W>`vJ|37O`4JAGG|`Zrs%k?|vwYFK`=Me*4u)lK3zzRMisCH} zN+L><_7w!qd7ycl#?LI%4@aY`>2~obt37p!Cb3+S-aTghn5N5BjcY7OzYk{dKEdNo zQ$vPZ%!>>pcq_lNxM+wi)a_Z_tLY9~2}N%;_0y^h6?SVmj?2XEGl#}9M2+32;SY%VI7;?uepXb?ed3?QOCFe(KQad?ew=e$F?J4HY)Rx z&Ieq}I-SD?OlIcXIvwweZx}1M19ScKg=W;bIg3@$2tr<(QQU~%CjNwGMZqe3t09J_ zPXia^r&-Kyt+R}^cB-3xTAL**6`Te8HJ&}ER_PCtcB9jJGeCOuV{6J(XX|5}`L)L5 zCLW=TQfUIogDNiYIAQpmy;*UcS#Jh4$0z1=ON{)Cd)I*E$cC=YcIiR^Mf`ZgNODyy zv@&5Rsj3u=>ng8%WJ|MW)a#qQ0eurd~^=x7 z@S-c`X+8+_%(Zi)?`4At-zb!X@TCyQZo#!dzr&NrqQXxh-{|puNcE;bMk*!$V2I^J z{SC+FN^s|J)X!NHU%bfx$q*3U`;{ob4TfIB4TCuX=e?BGH&t47g=V3<2V1jMU_Hz6 z46ELiMiPvBn2-aLiJut?>jow;BaS<{Q61Ft5$_-6HsZI1;IQ8d!x;Wd1sB9;b zcwnHL)sur$dhopIE2Oo_GlB^xQ-d7)p#tl8%p`4_0+)=+rI8#aF?zJ|6}n!XuX{^H z{CbLQ(T7=lFax>7>S`Xooh$v`Cu~U*S?Wvt%*cVds95+KL=DSeMt_ljCc-GA3nMKO zg_PgCbsdO^Ymx-wMpPxwdl!XAbXuo=R^qtHIMDz0xQc3KO86@yc_n|jZSVypIrOMP zaujs$o7N$Lfgv06ONkC9w=~kKu?2L)rNd6h60WcDCCEkyr;{&1o>fD)K3&+rSwc~& z`6;WbyLA0zZ`;|^Tgj=XJNFpk1IAWRBfj^R^SIeUy`waW{+*#d>rQ3`EqZ$9rVage*`HzY2v7wF|vFy!l|pn+qwIUqvFiiC?T4~zyz_-=eSun?A28UTisrM9Kj1gki`qb%k zB5nq*&j{M#!E!b45%Nr#I8^nNN3o?pqVS+8(c!K{tjdY(Cx-^l@D5bxt|oo*g!oq( z0ckQDMca4nrS%W}aOsBtnIf}D0=^W=pX?T2D^3b@({$D(wkNWgD~`s^V#KRz#ga}_ zimqJfEl~AP_|A1#g06V?tcD{aX>4;wMAKBNy?@;HCY^2OC!HBDD?_)u&}q%bfazwm zN`vR>npZ@VgUETLwXbj04;mC$wd`@Hk)ujk%NL$7I$a@0+51N)?|uBwVA9gVq@f<4 zgd2pIv+X+VOfD;aT<1TlV2szagc5R8y8+OKXZH3Mn`*ch?h;#BftW>VkT{newhHg8 z?Y+i*|K2_I_PvJP7$_*fpkavMC$)LchM(P(+-_AEJ?0?#Wij10RfCAFdwL3Pz4j*2 z)vuNbN_eALV^rFgY^Xzum~$H8eZNQ6$*Tm}cNDouFt^UuBW zVpQs#$_g56%Hps5kwOY401!yR3SR7#k-hEr+c~9-sms@+@E}nw7B>y!MeN&^#pUbw zmJu_%DURPTlH2MI}w*%bz)(<!sfQ4p?zcH~fcRyrZpy*pe%6UQmii^W0TlD}&k^B@{Y zv{HOLum2T(P{&XwP69-TL9Q(oPg8r46Atf{=MaaTnQpi>NOL!r&(yCFHon(W=z4W* zw^fTD)&u1aDCr$dxBEFEF}`0BNf;UK#DDJ>$}_B{BTI`LXrh9pY7t|iZ`c2Ev0K_& z+2vyq#w!j!78lxW{2`BbqDh4BIC!pY-$bUNSXF6CH$JFrNJp`fl%LN7vA)?2W*$w- z(RUUbN+gtu%7 z&I#Wt(}rSrss%(LU+8T)v5qq;j=&WwNfui3#IYJ*O%${dy@8-P@uwJTMPL@QXs*J5 zaE)^`HiH|rJap`Rtmf{eo|hc&JK2E+!etR3=(L@^h|igmPNu#)h3SdQw2p1!v$^o3 z>3TwcFP0@E^_C@*Cs1>XnHwA%!y(57+Lv~a+NA4SIBzag@vAOInV?XbTRKGh8@%!k zVr?Bts#FxbP)4qZX^2&xlChe>Ywf{7RY!()6msh=_n$MHc?0S)a4;X-Q<;b6V>K2L zrG_t5TSd~L80`z-P(~7CF*zN{MibN@jJwb@G_ixP2o9gQ07{JX+K`~`PX#LpVm~Xn z>^8I4(R@$?l-*f+vlN;>`mVsuT4B{_c2sMYPLQa51;&1aGc`fDrAW!zNe~mz?*npS zolqXR63f^sW9_(gjbgvS2_Vu+2(mhhU4mstQf8iKL`yRr4mp2(iieI1JtKdyw$P+7 zvp02iaWXTqLw$MWU~G*F1OO=kl>fZq;D&G{&xpWEKy{n3edl$u(eQMHj-)yvCtI(G z;X{uI8PSU!5%5alk=kS~rR(UJoBW<`#xk4-iH@DBn|@uu34Pvi<<7X}&Pc6y5LYgV z{RZt_4>-?6X8*dk<+=ME^J%?NJ}OV`Xz#%CqIptGgHb|*VWR5p?Dy`5_r-TM^f~L9 zusItC326HO-(v-8ksoiV#Fr+~`^n?mv5`|Fu>TTaBKe8ZsU2=$LuG@R8QYrjsq3-l zjBJMg!Nvg8L7PrC;cj=e``256C7-7H`#wF^D;m7UH%B)zW%)eeldbMEZ?^+4S#jJy z76{~D)#t88R)?1|71ZxfXCUsk9uipHh^_xJ;e&SNZhC-~0RBzZ;dYxVT4ky~8IPuJ-hiW{$XF=1Mpk~ufxVvLW#o4<+htHB{$Jjp&~tXMl= z&}cO`N@@4fOJeQme%s>}5a&2Nw3}aNqvcM$-6PPtPNq8*$jr?V7?Be3I`GKmKKn`B zo?>|vG?^dTByduU2sa8lXw~S!E;C9cH3QYK8U?y`luG>&sg)NiWOJSm7jG0DYRcD> zis|HxGk+-0OO0+poqz-Zun^$i;ktEIOKz~MBJ+>t(|b(3EAw9GW@u>Sr816e*yWhX zI!gs3lNbH)%5W;`Pkh%}M!F6Zs@KgJ8w+#->FVVsyBY#<4VWtum;7dWF2gl^2B1$T zX`y)iQswPI5Z&jg!_#(g5~EKTk{M0f+{@H;+}Hs@Bkw{{Hf{ZoVX&KAD@8pW8xl1k zUlA?f!pJSd5zzfZ{lq?$-w~&{)A7H{nr%jE&$Hk{P1wCRrq~C6NqM7%7DHEfj9IWg zC^k=;iA6clV_TjHmlh%&?Nopvdz6eJ2Kx%y&k#v4OtM{z(`2Y)mjtHv98JL&R%SIH|ifw58HUI{1;k@zr67_M|HS#8*Y_NIv9roiy=Q;9K@9tMUdu;l$L z#^f+zk7Z{LX6kc@>cE_5K;N5X2PPBLtV?9i+$zrY2D>BV-LO#5X5of?@$fRW2Uns=WTp5-V|)f3jG zhSj(dTZFG;0gsrwhb34vkbp~d=tlG$O!kDID+PP%JsDnxQ(sy|f=9HK<)rl<3gU|L zvVXgIX9YA`nmDYQga6Io=AJ%??#K;UD3Fo(kq`}!6`=Gvhqouoh=0{!HWdj5$y-Ry z29ql@UWtxHUDzu68T3}w#e~K$kLYAGkyx0dV;dLmHG=XqYVQ%HTYS+wPBoDZN)Da^ z>O+`KEA)-PP#a5x3%C|%@7qHps3N_ll{E~`hLc%N&5@Vw5N__3_+d8OK5WfkMwI}f zFYUCa(DL#K5J$e~Q>+p8`%g+7@Ui=jjd;{z`TQL?I?JH}Vd|DR!SaFL%bq3{HEfw0 zYMs}E!s)`9pT1*SPiqOQ@c!KHPmz7EUjg`*>hah%mzZixuu><-aBJU}4?TH%{XjQQ zrZVu3=_$^Od@CzCsGSDizyg@V^K!4vCDE%cDC#VSxeTv$SIV`hcjf5~CYq|`ecI=@ zJq+2b*um{6Me^aVSKz`A2>nI<=?ZvoDnJLA$P=hZ>wwm(E>+}TO?F2g94RrMsNfG^ zMcCiTA`QZ~NR7aHN$WW{mP3Dw#s=rw0JEs9tKmtviE03cTTNoYY#P`Z%M1h~neXTjO>Ke@n$=|`gW6}%(K4f9rQSK-&O^0oN0Z9M-$Z+qa9~UYF!Y>$_*th$j*q%_QjWq^m$I-@TF=dh z+amTLSDsz9^3EQr;e6+c)C*Q=ifiQWP_uH-k`&3LwAYaK>I^3#%A@_@hb> zXU}Vzat|nCSrCC2r)c?2X|gzGPDNp92&QKhfxI_)cvBe)Mb~cZ*IP@+F9q5g$+gFN zQGo}k(^L*!M>!*^snoy){$9M%1n$vP9QfC%EuR^GX^n4Ur!pqto(CJlbK#l2r9oYt zt6MN?xWSQpU4}7Bis~&q%GU=>{RzbHw()E1>AZu|XQ2EtjgN0WM4PcR@>r-DUm7-w zT0n#ecW3Wd1Cs684x$e;qGpDX^;Q{w7)w?v$lzAPdIvT$#vV@NtQV;m44NdQ5p}ht z_<0I)`UKE6U6P+KliH7u_xmg*2ivnxB)kUT>d@~Wp(JC!0QF8ÖGY~tI zfq@Deen%XWB3MYRtkPyHQGYs9e;F`*ks%mLyAs6bd=%r8S`Vnyig0KNFFPY;^L{g= zZjr=^xH~AI`hLXul=7N?+fA1E+t1@t6Cdif$1_z_NM+drpn3b7Ka;9^4{i{Us*1dM3OthyKt6Iu z8m*6IZ8LVB4Yn7P(|{c`PZK-?Ogb?rs}O14N%L|4k-odG3ZJw3@vLU;XJ-6npT{px zWpC8w$-Nr~f9P@}at>n~=?;cEdNm9s6Xnr8yB&W)ONo#})gW!g^U42&pUYG$@@;rY zXxCM9Cd}uzuz#epHG9`_idp!ynCZ{+_UrDQdD%8#RT)?R5&bD<5z|BB6aHljbYR8c z@-vH!g^_QSD&J5(x$?I8GUKtdyI?Bq6WC*?I@s+>z(`W{`&RS14P=E;xyk44m{!k3 zJ7(W12Ym)!$zV>~gI`q`{O3T5yu02vD1OK1J{Wi%wCVPYlzvyI4>=sLKk&tS{Jzx) zpR>q>-$~?e1lvZIm60#iD^GTKK#QSeUN{!}8hh+o$-d+9HfV|_PTBb7iW%CmP8#;% zl&*!nj|Y*h{J%mCv_WgOeum@a`rn+FmddG%3v}m7XDwwAu0Uizf}${+U; zjeA8k^sekN&APg*uk+V)YoT;(7`+u>j(oeyfvdOf*d&@yfw{$orCg$d5ef|!NP4Sr zoDg*co!MLLU)cF^;u;aSy_d71ZhhBbu9HDPTTvr7H~%x*F4je_I2F(HR3&Vf$)H}j^x0~{JU^j8{gSu#Kc9^~Q+#`SC)#`Kb z<4d_v2p;(gj{8WQo(2&qL(k6*@cFbEe#%?Dnir4#V3D9c`&RYQE6P-1hif@*x9n<} z*z4m3s&CSdCduC6z7ud$)e}Nk#n%j{V8&F0#%mA`+nrqK?MQdlI%KAD@Tvc_XCu5R( zpCpEFBD`N1`DET~<(T%ls1K+Pof)M*(v-TvdYH~`Whs>Ue8l${<(DSQp7>1xx(#@o zevbHJdJ}O7?lv!}BZr1F`L3Bpt}`k^`TI|uj|visd+t!%q~m%<(@&Zux*C61LSRUdYJel?CWPcit1ED zblK8{Ajw2EJx$zBnJ=kqX~@$^1;SDc8xef50qrPILeo7TctNoB8Q=O>9gQeWS9 zL`IOa%63Jyae_tE>i%eA_X4qbUeg%7eq!CdvVC#B0ciM=vKy;)(?kV(ikKG_F>_4EZ}sY<55rEE@Tw)63y&;ozh1S>$kI$-C4>O zl~GAh$J3?d{OMhVsgkhZ9E*6tv?Gu;)W!31i+x}`7}t~d)6~Gn%3Gt9fg!f|zU$^n zkJU7b%W1COQ1FHO)e6f=_Utvq(tY^dZ?juvGN^SX#HZ}Ch4k6HCY~(w{&2thyh*gV za%i$ip52nbD5YPFeTE0RaI_vN&l=7~(Ypy9fGB8wJ%tt&3$hGQ=$x1N{Ql|aRWYJY z8Y!;h7=JY&gc;BTmSe7(3sDM@N)&sT&M5-iX=ztG<#Wos&30pEj@SEvdO+MgqVRZH z?Nq#d<8ciB*_AV{N3vhw^IPXMz@WLfP5yVe$h}oY!cJ#KN#E2Yd8TE$`g$!KKvNL9 zk-b!ZjWeAQ`tWfrE!nJKUimtkWZWliExY-89mALW@@u*xZY?QUPw12x?k9d2p>^q# zaV7HM`}8aFwCX;&nVs?NONP@+50A&9tRXqRk`cEO_GPK7_Qs?c(N$J-jLlnb4w)rU zvhDk62Iz3w&X+JLErGia5QVaXLZ}rq-n%(%D|Sht6|iIn%CXkKOyO;V?_FNyzLwr|NYjqO)cyGt`OGGC?#kVy zCY^aG!Dpe`dQ1t>F6-v~ z*{_0Ew+>=d-O(qQ%hd6BzFeF0CEL<%EtjsY>5N>nr_Aj21MKDkF zW*@~p#uWG>b25k@w>~!A`{?|JW?$J|`(aq3K^ZoS>f63@+4++hp~l>{c6QsOi*>!> z)oYd)&TT5`S2?jc)VhEDA&OWvWnl4**;+V;BJ9|+fcAY}n*ZlA#aD0Vbt1{)??1w! z#9K<6lFeG#^{50nDIi*ZWKb1E$Xp{k^x1~B)n>o=@cHdNB?%chgEl-13bY|#iUh8V z$wTav^of5o3%xDdgR!4PyMrQ;Yxo=HIIOYVeTBRCAHTA_nb0Tt;_E{a47nk1ZDk9njig6)nK`8#LBZYt7=k&-@{m>O+b*^mZ|sJiioA9Cio<5!s`bgEXwy_Et3S>Mqx`6Wq2Y%ZV;@xV+R{ z304)i1JJS(RI8i3TvOD!p>q*TEfquo=j6@vC#shE4fZDsg0}->g<(#{Xw6dMs$$Uei`9dnr^ql(uPlxml^;` zsKYMXm(oX;WEx6@!e*WUnBjeD_;g(VA}|G@tVGZ_~xzkMi?II_rw+ za(cYZBiGe}=LMO-52Xn_k&$)J>EGh#VHZ>y(kRkLp4bp5N@pWcH|2eC%;1VlPxmz% zJ99H#nF`$arG18eMICcru|hAf6?Bs>w-okh zR5K)z|ADm&7|U5b$g)SqtY8HVP9VH4F8l0T_PYE$#i_j2xfvroW282Oqn>b+t!6p9 z-Vt5jf)B5`tI1s|9R{CTLK8H~_A#6nK~VDk+WCF(dnd7#^P>G6t{?_k4xu@Vi+-je zM$VM|j{QRD)wV0yQywcq16f&5*+@-$WLAz;nmIKJ)&lHJriN*#`u7%DG9-768@*fx zSopySSQa;>a;3pUoAMi9ZmQD;^ud!Q7CC;Y^H@y9Z`g~26CcpRymxdi`1^j)*2U*Kh4e9dH^RC??E&?Mjur2#zXJ=V0g+I_>C$mf;>7#< z9!ue0^%yfr9gzAok!D!Du0HY9AkgsnWZFyR^9U9!vaapIE!n20lO7z*E7(TeoSP~s zU*n-tX!@3I&&VAA=)~o|yrnn3YA~#}=7GRfh+ouele?8PXabyI3?BJ1oPlKaT6)kc z(q(Bg;i7h>xI}iCH%a-l-|n2zFY*~EVkI5MzjP-@-Z;a z>Mw-ONS)w-#v8^`NvO$-^$t$@#GCHj%}7qU3v@aHN++)q9B5UA9Xzu$5*3D0zge$# zGI;Twdv29be)SC)^@dD#N2}4}J2jUAHR6ysNWl>3P#6E6-bWub++|IQsDtZ>G!i%h zXNs6jWAuHoM9|pH7_M^Mzrno5lBBY8>GKq@J|4Pn(QIT+VVPNJzG3Ud&;e(HLfmDB z47F3OpXVmY=t9V(((TEU(KSD+i$caDHQ!go5O`!9-};a@LN8+h&l9#Z3e-xCZT=?F zY}Id-)m{=v#{o#65K}BPvt|4Y=XY=TNiv4M>{T=(CNC~SOb$s#naEzWUHW_|U8l|5 z#l!~JUN-|L>@%4snmiv0SGgl5Wb_;r7m8MQRr`wBdwJ{4Z>u?F#)9}8`{TYQX?X_I z#zpb%J0h9%BG+upFEt^@d9G9wCoV8nLNwj(sv{kE!viJU(k6Ky68oaIX|CC-_6_1> zc!GNM5Joio9#d06L(6yec<(u4`i#F{oS2@Gt=iDkwpqO4oAwj z!6T{QOn?L`@f%lRI+GGXn6x0O<#Vt6$SZc1;O6mhHx)%u! zsFQx?%S$m|r5~#}IWc!t@qDRjK=g#3RKwV|;3-G>Py;cbfL2YLM@p)TGCG&BQ!AsG z>Sol`xqY47(cc~;{#|7!-S${i={e`Mtp=puoeRv4V(IWLY+vmrwsxyR#^ak#S4roC z8WhK!vh(O2j`hY73IPTuN$`zvDfLy=JxG-o`&E4X99Q&fLp|Yp#sps6P?ps-*uOE-kCm^RqVndl8|8seXW*1c?DY}anK1;))0+&Kyl%f%v^dX z!m*C$Zx>^bi{jO$LY&gqk9`e&t%;R)Tj!|CRxrVsO*-)O2v`O#NF903s3dd2e?W|p z97Onq@JQoy_~{AA5Z!X@QC9dt+99AJ6}u^9%LaMsV3QNj9g*i`2h(95xF1R_?|}S3 z{D4-3+cHzqw#PW^#0zR-2PC?!i%X6%A<43?v>Visw2(P18iYMEog9bIkI+z z=&$d1L`r1K$(CoKn@;h3&v?l92*pd_r#19QAjtQT1^UFIi0#jbvb-K^BS$}sd%g4! z(`8vl$MXe{|0|QD$?rFG`IwFCD^VXBAK~5dko?kG>nDKmiB}S$p-X^|-){MQ9 zKYu%m1%cF<<`0dN@^JDuz$J8wo%;9w@lz=zaP9cQ5vwvqjD_>9Ad|`RPek1;YYVPK zdPTUu>SZLiQ|BgUGNPo7DeQa<80R%~SoJ!mOq><3Q5UOq*LI-LrUq$vv*b%VtYK-~ zm93xhg2pwdkTCsH2y8T|(uR&YU7! zF|KE-i!h@}wqN{c3=-tq{nL_=Hx@2g9eSrYM^C$f*~BuVIAJZ~$O}PAB*g%yIpZ-Q zbOu?OdW4xHLk4+h`K)xJbp{*V;RNE$)Rn6i$2d&DtY*TY9g#@7VUY{Fj6#y$1e3Fq zB8Dw0mxWTj`X1g+?M~M-{j4qFEE?^XQ(^@1%QMur8eQ!&O>Z>Rd^qY2yv6rD{A6!L zHWEclEnwj^;vIsUM`GslKqoF2Y%oZHH)8Pqh^4J&*fGRVma;s;L25ucj`)6)3p`T# ztFJ3A*`jTDU1P&}@AOy`5vUG55%eyIP0{N_Skq_bV^R8S6OUMo8*OZp`UaJ5@js0u z^c^CKYH>qEKqNxW_KLXYfvsGQe$!OV{@en{{q1qvD5{EZ+hRwe=Zh5AR)sDTCS&fe z53kMjL{spgG)Qk7gc20D<#}WJSHv}lVx&rpNFb);#k}NRBJjwqnaRVt&E>M>~Cu`Q|1sG)WXfQlgq=P6{S*pOJ}vM39p5Eo#*Kb&^JgIl5(Z=v!+6;QPG;k7h0u6CLqVF&TLAd&_~aQCmS&f z#oyfG;-FJj3ln-;?MeRGslJCG(AGqiKi~wRyw@=+lzX{--0&elwM47s15G5x`3&1f zxo(OHr~|UKU`;{oZ{9&vP3hO+!8VJg&iHj2mVz>I6ZXVYfknG4xLJKoxj(F@#>Lbo zl32vw$3=UI4)pa+`kB?sDBGsHRkHjf$4O;+*B;_+_fE~MUe<6k0hU!2mO`vn-j4T=9W#wb7*Ats<*2Vvz&d@yl;S7UyZ+a^@hkL zcIcJ7ue)Wb-%p@v#)pc2YHE+dk5+Hpo(!SCzdXA;-Wyz0!?eorFqSxdF8X58)+JsMuZCw$dT9Zx-(NqLP(whvR5BC3Qx|IA(Q9Dvg| zat3WgF!o=^N{dM<(rcV!?8YQTaW^$B35$zxYpv?z!{nw-UYAp6zn5!P2CH)Tw$_CV zP=4+0>%acwZ)7wkN|<7d>t)?^mTHH0t6?@HVNsDOA$WmdbWG|=V)9-sex-1&D_R&t zcT!;(P7(pv0zYOt9)g3jo8TA@eO?dqX*jenwkfWn@|D?Dt;M zjvdQPYUHmc<_~jwQkeMx_;#`=+kWN5TOBq)7;P;L^!ShBq$cN!&5y`yLpYU&6pB#n zEWyJH)m%i0(7}^Q;;+UN&vu~rdQq@P6Yr{Sh@?%vkM_65zF&^qqGEcCW;oYoDC(g4 z{rkSl;O~3PUnm+48-XapSf(KQxOlZ+jVPPE7iA1}rA=NdM$2OzW?$7_;j-^%sPUt2 z!WsHRi%}&@`1rR2uZLy$e=~id!=!|A7eSjx1F51)kgUyM(UCP{;qO=8l_|NBto;c^hLyt>J0VT%v^A zHlHFp1yOq?B@{Pl(^HLKpEzq=t<>Ph3(Z)?f%FCICH* zz|RF1>-gW{^Ihy^7BzOmP*>Z-R3y<8H zi+&X{X#$wN6JQ(3#2jRMjAjdj5*Dvi%rbhlNIXfjJUS`0i0*P!=an0T?uT_v6iVuR zRH9&Oec6aWnH)>Di=TplQOh7ZmONOgmZ^gmp6~qO1Mp3{!}a4`|Ep)b63k7#MN|OC z797>mw11zE(PQc&EPFA2e3Pq%{M!$mB&3<0joKZUm2EG7^mHtF048NwuI?)hW1oBQ$AdPB`$Z_IyBMj~1TIC$BovO|U*GmU>d2CJ|nl-qOnnaNg^$7F2k zyz;S4_>SsI6i31KvZvt;FnWVxNxROJA{EDfb6mkLc{^jH=e#>Pd<|`4nxV$Elkht~ zJVt(>CWJu%gZ1Dy_+$C}0lNHFpT*kJ@_~L;C0uRnC@Zak*exz1y%DR`bSpe*PA>tC zJ9pkrQANofCseKRy0e&R^=6;{TZ$dH^Qg+)y4*CXP0p*X&MUt3^xD9yaD>!XW%0?` z>qbI~rEbhMZ#$pd7*W~f98BLExtP6u&kF(oIbQZS{5Cp_S`A<>+ zl=hUU|2zY^z#LpJHKL3fq?$D0eN_MlAVj-c%U4BKS2OMAlIKZFb@|P^6$Vv z0Dy}N@P`e|$;JJb9~i>P^@kq^4=4A3*`WV-r7wUW5ab4vu7*8aP@gHwQPzAMw0s0QmO^Zs5xn z!GDhbVf9@{*pvWySfotRP%~zx@7Dbh1q; z91k=1e*od;_ zxB*bExViuACqQoSUnc}0&rARM_v8aX0PtS|2E7#X zA2htQTMob<0)EjB2+H|KodW-1|4;RUIl+)WvH%3Xw4Fa~ke6uw#Djo9;6L#oT>sM_ zp#QgnzMN*ke*$uV0DwQ__R`+}ws8W0e^bH*`g80{$#R4KZH|BP&%+G?{xQkRDeHyM zKT`eT%Kb+{y_`Ndx&EZ?h0wof0suMxq8I=Mff)Z93;_cEOc&QnLxLnT)WQiE03e+2 zM1kU5obSOeUnj%?;vz3}iHW^`FZx~_3GVQYaL6w-$G8@gT*$xD|?fi(7G*q6Lb(yF0yn=dSy^ z=g_;>J^3T@teM%fpLu5X`zATr!01}X@T-BBV}}{&IZ*Z``p(R^GPjpiwvUjeeVl0- z@L zlH=bcN`DLfDsfT!Trrf5I8e8ECp>)|zbx%2X=sA#J$kq$8eNs9yWCauZtu3m4^275 z6jj3}O8-cGZ!vf+>;;Z4(FC^aU$XuAW7Q_m33M#=sM%4v)A zLp(Qlf3V)cbKG)`Y?6Z5bY|< zZB<_}vwu9K?es_|Jhzk632#671A;54*S_)-Rw!Oyk-K`{N9)>=en|ui_Fp-5t&VCr zDw9p;$;2E%qP(#EU~A!X@z>?zt$<>A+B&6vA*#T5u9`smp}CC}%r~?q@y@*~#v*;} zvPP}VH<-JxuVAyjc2mvQ<5$f0o6{1AaL<$3So7Vj?%hLH1r zn(N}f>`#XNa+!k`UwM2OH*kRM86*o{-2C;y5P}P9xp~P@oOg+n6bV#H3%yH8lXBe4 zr|b0(?gr^1>&c_t1xhw*9xSygR`Z$&FtL-x_C8S+_*k|4q-}XE`C%>jgDi)HnAc8Z zyY7*+{XGKX5lt)GkxblDls<+|a^2(e;kkf`d>I99Yqf&(`uo10rN<3J*MIWC7X(Y^ zp-qs3n{%kBMB!x9a&y$4f<-OKZm$)BICQj+VpC$VccaH zvxt*0yPEKR)ZSD?g?jGOTSEP=s`-GdGiD2IM!(pDS_?VvXA?tDOX=X)D3I(-`U|Q&xa^{g|_>u z=Lqj6X9X3$5Y0vkO;*o6>SpX#!6F$5kZHEef@~$#nvps;&Qsrj{Wv21v>v{UhdZGI zPBl~Fc27{n?88t2v^-Qsq4OcCm@_P!eEZFmEGPn#cMW6y`FC>L{BH;9BbF8+THk~zJ|u*7x)QZ zKu%04e-*7g2k}hp5ie!{u&|m~lNxMax{vgLIGF8!o&zJdW7#_P)uRuRmj=DJ;fbh~ zPuG=C31UJITMg9jGikcO+9(!SgG!|AWNk~~+D-#895@}*2>OlX%c5P1m#5?;+DKZZ zfr)*5s*`#m=t$Zgcj8t0i_H{&aciLFL!TnLrHbFnX_5*SYaS!x{r#fFFXYRwZAA0B~Gogq?Z*{pemJGud zj~c|+>Dl5dQViJhuSJ#ohHKg6|Z(S|VL^XqQN`V{~g#_;uI9#Kc}AM$99U3yso z(#!*|?)S*vIb@yA|J|(Tc1HpP95);)fb6XtRpTCw_ont+oQNd4}yh4vmv(4+{yY&p~+6}{QY)9eIxKQQ`D3Qm>!M^;c$6>*0I z>-h>PGT0XuL}&70eUkOhA64;=>E1#RgcsQrM0fKUNR8q?WS4cmp1C0^ut+);hjAdi zBw|-HAxYmaK0&h3WPIcqfM(E|1xb^(Dq;R0s+3l6cQ-y>D9U&$Y?Y)zHOh#6_s-Un zo^wypR(BUhh(HvD!exmgBN%|X^7z;oxtKNeU9JW(z*Y<6C%)bih8o@Jk9I;!155*D zd;-@)>1srDZ2{hr%yug(u%ieF-LMUeouO5>CxnY}6NvDX?I+5z^8dV@%#*!*>Um@5 zPiSgCS|TSGQRbO^ET@jx(C4`+NDOq z@ATi$CIQW`_MNOZBl!^?vC4=bRb6hPcE0-Y(db=vSjHgK+y8ua^ zPJ&jxpLiwY-u6y3)miM`Xjqh`jN=a7zQRvY9ZWSvWM2&WX=7r*4S`1K30}gUYTzR5 zDqmxeNA7}dh0B{gk_~$mZ6ZQclvX}U-lI?N4wT1r2dJpf*k|vYgPB&7tiuVD(8@06 z42olrJFjK^u34!Yzkk8>_ST9gD;l3i@Mw?v)~L@a=Aw0UWn)OFY$XgAatTjeTUt(b zr(Qste`)kho$U_Sbg^v-pSK*APN05ck>33?Gh(7w)-ku~$%d&hoO^qdws?8Ol=3D9 z>w^vb*ouPnTU*JPoKWyC7z^+AjROX$Lm-XFH?s)dSL~{Rukzv5$A4=eeEZ2>A~|tg zUYn}8WD8#PO7XUzWTOy)V7u~OIz@c3vk(SgVR3ztrr#>7?q(piD#E&eu`k(o;ashx zFjZLVOtB8O_jQ*L=q$clBB5!fPC59hh4J{+$hvZ7HSh7xU6X`{`Os+k*bDP>=*K7& zC2dU_pH9K;W@E4T%|Z=HdQr@ZTNMAdrdZ>tWXtU8w3ZON4id7cnmYA&d6J$K(soQX zgRNW+7mDbNA8LFi<7;RmVFqJA{7J*AT+d$P;%wSV`Hq#M+XizenGGM=gSe)@eesk| z?`QWbu&QOcrNi4d;(f%7%gX=e8a~2+ndGifxwEbc&=~mt|$%8b;@pReB_!HleMe z0IwP%8K}^uX`+-!J1B-|z=JD=VSX&0Jj`OfzCsB>F0=Zrc(}8GP6!($EP4gk`Z;&2 zu3REv##%WQWfo)bgoPr2wM5NOuIsvPvwwUxeR~E%w-hL#rJ*?8!gir&qB*R}6Q{pT zRP1xyul+9PV@ljx6&NN(rPjc{PMW^Qrdj2{zU4bwCmDd@A9{i(jaC9Uv4iVOOUaa?)Py3-g8F_@UZ#l)U zEI^^ug-bP5_H7adoYRqlBcx<5KC{mwcA$gUY49!XUlH6gu7@<{n%&~f~1j3j*q zpW(g1`vn6yB;&ih%>(!O5_+k)!$ai~f5Z(uc!oK;K-B=4{BPSEF`D>W9A+OeQq{Bh za7FLBSgxxf$XDfeC(Uuv-dwX*TKsu*h$a{=#{i!9`rg-)!Wa8UXykQo`Al3y#m_!@ zeD`}=R*y-N`O7?zZ*fU_L^*&WT1ckB;N~4`kg`DFs*r+~(s@hZQHY*FB9#6;Wz4J@ zODGysH?`6Vb}WA76cFRORngxhVbjQIC>_AImB$~h)?eKLcTGST523#mBF`+wx((m0 zbec$DphWck#d z#mG7$6YB;1jB3~`0KR(vuvPyT@xu!QGx>)3^f6smn3O&w87KA-vO!;TakgB1A6r)0 z`%ZSN$i)yGg2!!5(opiDEg6w(%<890aE-gynDv|!$z3ZgtG4t$9dPMqTVf{7YP|Bq z7-~$XdsZ6)B>Y>b)qB~*L3k}?RZLXqz$ z-~SR6-Y?d1$znJQ2Y3GsivT-~umn7!nG%o?B(P9AX66$NgA|!3w*b{!M_B?4= zYE&z~z?^e^Ypf2I>BfSswBeTwVOng3JtfBv{PaQ2U(glVs*e_8ZNo|vA}wt%SP$gR zVPA?>lI+jhnKno8b|>!)1RYZ!Sg?i0T*&{#ccV!Hxm&2KOvEy}N(RW;5!=&xOwfBx zA&kw8x9I8whJktS3Ysk?u#lbK=6>qdoEA1s3Of3}Hg2m@pN)>0B*kmFC7;z}K7rNk zrN*yItU8A;2#^D--c`Xe&0>Gzt^_R9z|h|j5m>QmqgG+oN>)=O{E!MNJh1`>*OI0v zq*E>AbO{wwBI(d@+zjoXMMF|yw_`gZ1DF|Ao)XUMF(pK`#Sqjo#iil{sgOFi;)q=; z(sP>p-ksYgtDvMhV)Esxm7t1ts@QVACnWKslcByz`9z~50dZ2Z(u!UjCp^s+*c_hE zGAQKQeXIHXW}4*X^+aK>d_c{m%BDVDJmt!%XU9A?6P`S}N}}u?C8k5TDZJ=bgv!Y- zZFXA6Tu*H%E3e_Ca{h`wNm)TWO5?lVDe;2JaPOY#QF5wtA_1WoLcy}z~r2$W}IxnF#d5Ygb{5vrT zHHt}VC$p2$>!oj+5bWaM!W^4OHO0+vwT9i;SJ||i&-bBRcUP@jeawtXS1v~*lYFmC zr2GDCt0}6PACCzR$olqjif(?^K0qQ1$#5L`=2Su1+84*GL2w!80&_TaGlgwtB*hOw zH6D}=8@u$-O?qO6z|}QpO@q#mv+^LL^YvFETMpCjH{eS+HtQWjtkb<(U%y|1ce&0& zWl{1S7xTD#g|JCAyjhPX$`Z1*7qMG|6O%eH-=~^#aV?(1oqs9uGJ_@vGFDj$4-|7 zNHY`tuQ|U1$1eIfzWW#O#5P_a4lcAB_q#+1pJj3X=q+k}G|lzN`dtXam-Fr)$eug; zOfX6=!t=gS|Cd`}niTY!`yF*CeXBKIso{if)6e+>;#W^7v*?+na!#Y+zmriLr~nC= zCY^k$TYImsRN}zx+7TRoHBqcgNe{k9qBi|mPnBo=O+z_2vj$&NKdY#AltH!*w;VRs zerLE3I}_iBRXIF5*Vc8zs_?^T-wl476g2rxB9C*NBGWxMBv?F&U;p`p1Tjy9w1D;(gL_QzFFcY&>B`4vm&-&*SmQ&n9dIaz}yPaoR zwmbT*%RNCslorD9Bwn4?@JWX1|rGn`t^y!SxadP>Ob7Z>4jO_fTY%+XbX(>=rV zFz~`b?W|e}^Q-$&betzuYbZTg_}drzo}EYO76k3v@sr^yogaI7g456|v+Y3O9dRk^49R4<= z-;{7JD&6*J-JP&wSbSiQ*j3IRpwMmO)sKm27_0ih;Oa+&%3aR};-MtpOuNa5abNSO#7LDV3HPA;CZlp1Sd zJQ}>BqllF-29yD{B;B*o>yr|-3Qa(xvpq`IuCguHw`fj<541|8&S%*N?x;;fF4pZ4 zL%9%JUoEuPIEe`^y8UhQoCOIWOq}0>->#{?u$3@>9T3p@OdBgin&up-GcZ|W>GY?# zpDs3-{1eP5c=QzpU-vK-|1pL~J>O8X@|$DYSg~x^K1z)1G)h3P0#u&OQq_Z? z{(^Q*U#zIg(H4Vl56hWlAA_jZ4%+t4T6OGW0XDi6CLaEmiJ%SFYy#t0(7IUA=Qwlm zg0R@F@O<@Qp`P50SSQ(Yib=tR=!IG88l+v}9zbvldSJEwaq5x)Hk`+MJWz!O24+wA zri)r2OarIMgfnlKN!7L+>tI)_pIRDUMuJ(L7dMFxIn;P8tu-k(eDYJ=P_0m5nJzJZ zlmuHMW~D8Dd;rtbFEI{|eiK6+75LZh=WH^azgiTY`M11ndD}b{b0^&N_{k89H69UD ze49^6(+K}inCVa!(xG9i9HY2j?A1_ z#S^&Jexp}}Th{Xp?)j8B+5N0R?J=J;sw`j6CK%x5WakWG&&h#z2nF$ys<1V|H9;HD zF&Oe_oCz1<4#umWrb}?Ds`8nZ;Z(@9jqJg_6rxuT6HBC8ZJ$zZs5-v4+2-sGkC7-P z7$JKuvnLiDYl+My9B0vHL*^!xAqGgL>N}Ba_*w9R_!WqvH{TPEw-OYHKa=;Gwz>ZL zP`K_Mqy z33y6GJ}@v@NCN&X>~%f9?~Gm+CSjqkK>FR-&v*(j3c);3l~gevjYXLm+ckNgejtg% z$nWW9MKn5b^JD3tbK=e(pbIIxLcQ`#!@0Oe2juEq?kO{>YdoSPqj9i1wQmIkn9EAGkuC?E5! z@~S(x_53rO4Ux_-^iua;M5480x6?_DI4-{7`6O&@J|gCJGMSZKRBKsir26`oPUJ{W zt~4uinFDP0aVUBsevw(Q*=T{-U#aNvcI>D?t4BQ%`^WBNMh}Yf4EMyzdFyQ7M^A;G zYV!hP1UsT5m|K?tmGWso_;%yIhFh|d%l)}}ae>QRexfFS$cEp=8!qATfRh8NfU<7s zaLsza#~m%1)K`kN<%*ePJ#?IEj>2kAQjxomgS@NBtU~qXw>`~|>XlKGZMe0E7uyBn z5IDxykJW!ZCdiw!ya`DkxcNBj6FVOv-soOSoF&dG38R=cuS=5FNb%t-uZ69{#oBmT zA#$O!PK(guh!(DCY@IM|S1HwQb}ZcEqZ7Ncp~stB=jfsTOh+<9kxzT7n0?%qzyiHP zU!ib=X%Z|?l3~nMXAssDe*F|iFIrw1kveTiDx7LHf9`8Y(~b=XEr%SNg+Up@?%1NB z1<^CSFjgU!>Efc_Qb(RkMVc(LA8Xjrt7fDpB4HZfb9gQIv;w>>e`90I&XG?<=nsi| zejy&eIdGel5|7EZKi6q8zbT8mstKNR5pmgSe*}BSsEzz?aArwPTo>H3NQyW=m1kk@ zLMHaqK_v#A)^_R^W6MMlpd7D6KQ8lvSR>;#KYYTpYDmtXnXHe3bRtp2^4rxq)=8N< z(V<`_hY;X*&%)ut(b?|n23@RKvR7Jue*WEnPEqv zdTBz&^6`(Zut>YAFgvzZ9w@CvgaRK#Bp7CQq(R&yZ931p> z(VHpW@j=pdOW{JC)W0F>ebb&nJ;d|h**{=>y+p#n|cU>gmR>)?aNlz!wq6I zO-AkdPOFJ}$mQskDOeYOD^++fvMwxLm*L6D{q}xpp~QU13`}A%JBsjJ=S)e?3?;SH z=;gpG^!_m;t3~hJlU;FVAA3bLGR+x4G#w3-FrJV7Oyk-M)DyX++|nAatk6<;L*)4S zLfUqVFl*Hkv5D}cRbCbME?1B8$bFgpfC4^5IQb6qi?Jn2Twv7KgmiAkOxG{)NgpNH zTHpl!5LZrzX1_MH#lWUCCYGe_jIb#&_5OC7iqj@;sVXL9bn&yK+qR?>MGB>{P@gys zHXOD7l_I>sS64m-a#2-!3HK28dWnfgk`f0SvOA%|zq#JtWlTs{g!99KROwpFtpMH+ zepzWUtxI9sR2@BnNO^9(4GV*4@ef+IWkIuhKFS!1!z~grlK=0TPDjDe#k}2E1r5AW zSp}TpegQvsazuWUHF9$J7Puoyqo)#hSOU6c8o3`*gFYFH?LC#=*_)!4@w-AXPdE;q zLK`Ljtp1v%(W@)x$j|Y`#-`dxamMOVG(5r;NfLRM2_ahVZ3LZ^$1xN-$HHPA^c)V* z_9r|vro3XXYRG=G{yE5oWFmtLL5B8`18+8NF(flmXSi()QU^YcaL&7aanKUFgGD=! z8o4Y2-GuVizBg`*A9<)W2&$f%5hJFZ*RV+^H!|z(u;4c3y^Hhus%{}LeE5C!hgeX} z_pnd|@3UC~lZFW6y&AL*&L2h5_$-9l5^3}uY`I5{aOK9g*zx;&a&GPR^V2vasB0_K zJlRxu7d+jjenNifHIzTLe_smQ6Tu8wCIGISy`VRTZhpB!h!;@tGt|@&Pz~<4l-hGi zF$Z_1BMTyY^;=Gui&o8{$>o51&+^8BP6ltxbP2(aPGcm>aVG-~Q@*Zxjrw&D&B+kn z#HKaf49E1q2j5>7orHF`<`N6Uv-JxKY_G?H)Q<{2nsLr5qLVn1d}>XYi-Pei;gV7s z%ibJaI^?QTG&Ay@*g7!u5y8;n*SX^req5aesl{;wT|Xcc-O1UHqCRmhds_dEc5tqg z`^ZpLn%x(Oq8sp)tv_$D^E;nN##cevpK`KHE%Jl>RV`J9)7TYcq=E&G2)+`nqBjZN zMnO0CQO{r1)^_tnjckRv5ZJ`{j-^npixr4q?t|XngUfVkE+LPb-;Y=%1{$!p0!bL4*+VXbhJ;7HcPW|!F{xXm` zc}uCR*5bVHh#8NYnXk{*XVKxqgIl$3xj&ipIMX#BbNMa>*7^*YZh3yfUQ?K_qb(@h ztKM?H@hL_zNwCtxrh9XQ1xs;Xpf&J%#|uo4qtz(I2!AeX;oENv zu&=9GIH@u@M%<)piW)SAEIie1UECH?wl=PAb{9+c&;%@gZfgiWdq7sj+#xQIwi80_ z?=*6oyzEYsL*x{nrOx*PrG{H77TTizqWEK+%Y?v9O3dLLmfaPdSvT%%2F!4e=2ioltV4KOjNVfBj8 zaiwikYvIb(@X&-z`PM%Fd}o6B%JSDF{2*b(?~%3G%X}_pnuJYln!mh1dQZeyU2IgMBu9V>C;Upu=U|U2*#8euyXyt2#hU8Gcs-yxcft^M}{!o9MR~4$={r zOj8JLk!}ty4C*n8AwO^H0=d-8!n=*nLs?T;ol-!IC^S4y_-cQuzxL4csBtiF5%r){ zunsCq6E>BbRd!jPBFECGQyV><(^H+@hEj-w%WRn37oE3GsEgtMzE}ngQ>-VX>c^9W5$eS8=-#Z}CQ)5`9w9 z_}UdTN;kVVJW;Sh*%%UT>A^*{@wIRvS~k#qLD;QK=}o;6?}2?|mW>9I2uX6t%D5ZV z?qGjFjP9WXNkE~bxr}7xl}gzH;%CR#+^-n1GxS}B)Ce`uTKM3s2IQS(KR0|eS<Al14L+Tip3|_~NFkNo{0CeK+U77&e{e^b_Ovt{lySKvWFd3>B|ax4slkMUuFv(c`7RX-1&k-iERz(qq1`PXLY8 z?-#J|MSZWgo=V=D>Ih(-yX4R5P`PEX@y#nbX?30tFq~3vrnZsJ&0c?|RpA|UXq&Wb zP|LHuSI(&R`&R!tyxC5kpH(?d-0c?LfCv>2UG&Xm2qzxg;^sX$i@P*rQB@4?aQ#-? z2B8x((hok&#D7aCiTE-`x&wQbTth>+#v&h<<8iL|SN)nHdRJ?QTPN9fG~NbN`Ga#7 zQK@os91 zYZKhRhs?gsy8p}olK673e$P8)s2Slk`}h1Sn-p7GUWc|Q0XmD_d!IA{mf=s9VsL(IGzI>YM0pyXoP5nl?}s1B=Wj(tE#+<|MR@Jo!OWqB1Mo z-h28{sNibxZ}6i~&K0%Dp|8lO&)d^eSP+>i-*y|v#~Q`n%n5>uD7w`VmhuvnqPuI# zfv>|3b&R7LhxNQy_Paz63|)3{!HE&e7PbbD=!7~!&`m5g9(3ztQwIHubOJu^zn;F6 z%Jp=ZF^r@eM%6d_2y1Ga>AGjE`643UFUvM%F!p3bPBgNW|De+!W_2*5Lxul$=V9xBK_@g&m1t7-wHo74u-SA>-W>8qoI<>p$n&-}Hh}9a zZr*RYVEr4o(@KBoQL0zzD@GrZVBZEk8A@)P;(2|`iypvs>D27xP-M*j{`;UWhiw?G zyUMfel7j`0!B>tQ5yM}eEDJ;eGs!Mnj1Gs0KXi1(iJf7toy*W~DuBGbB?B*X=~xyu zjXFVVsSo9@hmL>anW87}EpMwQ`eN2x-^bBxU6*)-$owXD{}}>2zR9g(f*F=|376!D zI@20l`+}ViB35K%8EQ zALAW8xq7Se$#sE~dbzU~%_+Z)k)GC6L|eF-M0+z4&u>@08gjY;X``T)#%9b!MAlF{qSObH8{=p-vx800Q@a$9My2qoChqFVSJmjZ+;v(@7) zd3~n&m3vxsW#4Ggt;r{XvdpCQtesh}C$lv3w&ACnNU9~}^Nh4)pFAzyYonF&z&=(g z*u+xS?Ga1pJayF zMxGeA0+$ql)QsyW^ADH`XN%Tf-trWpdz`(Gma81~)uis#F(~=nI+tq3b57tW&O9Q& zB&!MSKX&k3Z-#sjYF!yBazXW-NSeNat)JeAiB3Dro%G6@?_@nS(D%B_#_WHMEPj9! zynT$Hgf+Qv*WY{Lug&fDBVEe_+#Ez+XSHVY3RCR=6|;HDYY{EHb_gZZo9~LMT>QBj zu|IUv`=t^&+QJ9Fl0}0dvJ+iy@(mkQZwY$cl5W|GMt@h2^n$=#l(aolj_n{t; z2&qtVtj_qJsHpWjOeK_9O6bxTR`Yc{gc)2go0?Iu(ae+lzN@Hxsk^E=`e9 z8fwLRC4aPxPBUD>I_{P*HixC;HYlu7#Hm;W>vwJ9pS~YNthQ3!nWc4>wW#X&{KN-C z&;@D7n!K%cd&@knKBhaeI@(Owk=^%M&S|`3ZQV2ngiq}!bK4`Z5F9ZCO9=EYNSDCi zT8)lO-OA^oyK3=orR{;9x3RC9o zOyNLjCMttqx{(u=ecHM0ju6u3^nyB(=KWRMr<2thZMVx4rb5O`m;?KE9#@caKAJkI zl8~Q|q1%;gw@796=$eE@R*%O@*0gK8Ska(rT_)`0k%GK5c8Wu1ifsIHwlEW(3|UX* zcVoz`Fsn;D{&~U{Sq-jLP)=-l;3ILoK=)&KLc7ZtBQ%J{^%wRTFw2qV&WFEn^(;G+`z1us^0E?rdH5B%8V^@I!MfJ-_OiH?5cl~P?|QzfYf6S3V$Rq zH;?>@{3cxFC|1iBtsjyZbI~P8A+Q;a2CX}-i_t-w<<;VaL8x?R219J!Y^gu=H(@7) zSB8t%??|de;Nw(Mela3mmLZWJc5`*-e+yAfWgec5BwCe8bjpR-_-nVQrx+c>JH@$a z;*KoLBDMThn*hMyQ={13JoW77A4Ln)J_PK+<0NM^iXc`(=f$krrw0CkHUthz4 z`{LW!7!ZEI7`Ad_#Xdd#qNC$d=s1INp^oiSeJ(-Onud!WzQwBAih*JFIoN@nf-DKG z_Wy*kzFNB<4`R(%5~Qi~@3`gv9+ocKMq?o*N^2jN6A4Fy#N{Tboib?hA%_m}jpg*& z_hRPhDD02obc33X!RsSxC}!s>EaesOms2?Yj2QvcumT~*g2mpi_8&>L^;~03;AuuA z@gKo7Nhc|~5etnJopjrt2PVHbaEx)P=d;qChQ}d->UFJk?i%R;Hp1u=;}pq#O;@!0 z>?6^F04)Cvl!k5I-Rzl6<^_PL2;?G|EtrrZeK+HRz{i6(xGg&fVArRyGG_L(nfq&Y zX_`3-3~lrW;`%53I8@y@r&MGV_nF&8N2LJlY)Mq}%4S_o344U{wfjZ%(89N3zH-&E z?g3kfuZ{ia)8hPBiMh@?SJCka*ABo;NW#P^P*X+7dFC>9`GtxP47en^spz>qlDwd@ z#ZvH6tD2>Ec-Dx@bX!IjD!}{w6cF#9+u5iJ?VgI344bt+;@H1 zvftekf`zJY`{!18P1@0b2ay27x^ZQ#ndvqRwa|XL8lJn@gHJN1(Cgc&hH@&lm`U+9 z?58N^4hyhg^!Gy`@kwKT$Scm1psU>$9n$tnYIXB|SJ8J>XUHi*JuK)yeA)bcj|NB> z=nkRh$8Pjbl)SBB5WTID>Y$ccS|dMN1A23$CtDe!Z{G9cDkfHe?L2QF43fK@TF!oL zl%EnS25xZI#(2Q;EmdOu*qBpF zh??8UMIl6O<(0t~j?BY$l^U)@Q!~jWa_Yt3WZMaE)H?&oWw;{HO6npxk;mbGU@;XT z(W;cYb9@*hzFO;>o<^`H2Cfbvhf%{P^gNh2*QF)i9%QP##Dn4C&UroQ2Y==Mox_S z?(SwAKkB|88J~|Z93D=J6hpws#W5!M5}NJ-jI%)y4k%$Z z*^1>W)n^PzpCcQgmQL<^w|nnWaO#@vPNp{OTimVehp0<0w!Mk=fw5B7jM#6J<9-!g zS-E24(SEuL%t0elkiqvQXL#jm`ddS$Dd(uaor+i+gMuggyt|b@zV*pLnmhHtDDhG# z+gK7$h4q2JQ|b8+q^if4aipS#=)R_|P4NP`x4&q9GkIJ^D9S`5mGdL-8Tz8o!u|NF zalScJq%C7&Bhnc8*bFl`Q@e7J#1eNN!V?Gn8c1~-g5njBvYLs0H**I0Rg9&3?+d;@S3DucJ^dBwyR;T<{il|@V&`uS!t%E!57f4(Fqa;y|h=u=D%A&?=gve=a)C7 z`E$KYJ_SErRmH;$1++LKS$sxY;iwkHs0nJ9C5dZ|)U!t`hGwM_LFzYM_XOizT+->Q zT_2P5S8Bjp!R_|QcyiZYtx9&?%7(QMN{pGfPcL5&Rxu<*r?;-lo3di6K#0{m$IU!p=mUZ{hx)fA;#u%^~RC(Mi+|r{^Wy* z#s_yO^{XZnM>orHN|~tU0|xpLh?Hlh1^^*vY2Y^XM`jthdee&e)J*=@nx&d0CQXE8 zfoMfjhx4#j>kNNv$a@v>IUYaA?611Pg@bYA*F1%&Qz;4^=Bm8=eu_{9`s+u&V)J#C z7Ayk&3h|R7Lp^`Ap{e|mo_cu`EU|8WDL#B#Dt{^d6Kfh(ZNJE=jr7$+k&VQX;h^Xx z)OIY|=fBYyzqK~eAofP zBjC4~^Ym7UCn$VzV|WLgHx?YNoFj6$>e*4bB?_=f*qp&ksB)Y({UZAi*(i=V93KyM z!YZs@K&k)5JDBt?1r_^g zP0EKl+#h)#KRm?D7W!RIqa1vXWz$%e+5WJjn&b8M(AMATjVfsaAxe>q|7OMzlw1FO zP)aoNSjiMm`H+Uxv^+smowp?yZ}+HiAsZ`f!I83v`V@_!h%$UCv31H`tqO1ITyXs| z_cmS=wNsgM2;o3OGi z?I6lJy}}Gtn!({A?sjyKtRxuw!V4LfEC9V*KdSI9auWw^jNFPmSb41iJGU9naMvsYclmcbZ zthGg*%7$n{T;zy*7L(8gwh1v#3pX(5o2G2}?BlI1u3A)dS+3DKc> zqGSG46=SQ}sIMeLI#X5%n~or?;Ac)8XLy%3Uc4%+gv>`bT<*~%3PtcjFG-j_)N;q> zkVMmS_cf&Ghm%R#=J-|4!Olblox9nde;uTxK$8zw?}R+p4TUnaA?s8xmsvP+q>Kef z%Z{o)MN@B33P0A-WSyc<>O__9(0VAkqL}m^*-T8z<4#_?SP?Ulz<(L`ffF;L^2wnz zRX#XA%9E5ZX1^E<>m;0!S( zl5E42$m=km0jFh-%(jFi2Dy%Cs~q26CdE^B+jd2Ti3_WY`UlI(Sqir!-0~Z3XIpWWAt!$&-6?}aYV;Vu4w)it*WpSYd?IInCpNvbo zGmJ}uGcZ=0Es(5qu!~lpSf%eB9v1uufu!A$R1#bpLx$13>7IK9HI0&7sRgy#guN-F zFSUm5T(6Eg7Y}BRK9BDw9VzCr5ceEq_%~bPr&aR&^%XVZH;a^qF+;WysOx-}y100& ze~B^bfH>K}JHiP0A>7Sp&R<$dcQd)HIExy)2z}yY~bYMPJSv zhRB2_a~c;ka_HdGPn#NFF=1>J-k4IH;^z3aeLG2M23{6~WmZv4A3NzBd5ZbQi8jT` zWjI%B79Ous-BNGDu7;$xG3KX#hFAFJ7qFXtlS_s;sbm>AyMb85IOqlK*&Qj!*ThmN zx#PSXKI^H6=ju5+I(_9^rn8g8;mpC;l8?T0%{Syt@po6Q>giMpd< zR^*EMW;l!E7LD(c6sHl)qDLq&dEvq&E%Wy*U%Af^X`_xsV8>$RUL;K=9dAIdRxG1MScK%MLnBt#2Q-ie2NnzN5~=3PNCG-8s7p*}6C>0_=*NKJX1U zJ(LKNvITCbFI!f_yEF@BFG0&2tbnq|}`_JALswfSs5LL{_e>NhKw zOm__owhUH7|0wxC%;4B1oVx!6Oi$3=i7n+Xndyo(sIfY5iC%7&*j)e=!Y*#es;jp6 z4+^u&-A$nu>W18-du#Y|2s>S90bPym1VtW9>OR*DwqcVfBVfS*05J501qck} zc^MtR0|ERK2?*u`yzu1%@KUd;^1_T0ty#G`b4CLeeM`mE&|1LeM z|7i4?BVN!yhCDzpe==za0+b!{{}Bbk|E~iG2uSw+j{_g{Mas`B@bmnG@qqbwl2=L) z_&LB(o)=Yk_JH#KgYiH>;N&-@&ppBm;C;aW2*Cfc(9d1=Oz8_dUjF}&egJ@YUor~f zg@Rso0DuPs{;zn?b^AXZ4t|#B3xz$G1IqVezd$eq!uMj4XJ!9WA|Q|t`Y(Ua`~C09 zy#BAU@dEh&JNRE14<8hgoKp5&1s=W^6ak>TpqI1(pgd4s{^W=MIDjGlMB@cR|G_{& z9ze2j`Ln|_mH(66=M^9?TN(fb@$mB`cmKzMkLTZ%_;~-pKwvO9nWf@c7|$#G(>lET zFO~kh1Oxy{j;ugnGzIbf;{XBtcgg>UrRV+w{M+Nt!{cRr_<2CkmwS939p6e2Ucn&$ zXzMvF@ZWqvP|yo`0Qe!iy#EX@Apgrr`W)|B@h>Tc{NJ-X`BM=B4vY`*BF^*p;`!&S z073yT%ko@Ao_}P^^Q_Sq^Z}nU0KK3E_}uBx|7ynzJW-HL&cxRxfGAMq&S}xgy;F_d?OC#lNJ&B|Ftl{ g5D~#}aW!#vb$2#1$9TSW;pOMSU}Th1lE(PI0N2iFfdBvi diff --git a/doc/invargent-manual.tm b/doc/invargent-manual.tm index 7161b59..f13c9ad 100644 --- a/doc/invargent-manual.tm +++ b/doc/invargent-manual.tm @@ -1142,11 +1142,12 @@ because InvarGenT, noticing the failure, generates an OCaml source with more type information, as if the option was used. - The example contains assertions, but - despite them is nearly as hard as . It needs the - option to not switch to settings tuned for - cases where assertions capture the harder aspects of the invariants to - infer. + The examples and + contain assertions, but are nearly + as hard as , + respectively. They need the option to not + switch to settings tuned for cases where assertions capture the harder + aspects of the invariants to infer. Unfortunately, inference fails for some examples regardless of parameters setting. We discuss them in the next section. diff --git a/examples/liquid_fft.gadt b/examples/liquid_fft.gadt index 1ae533a..fa7f13a 100644 --- a/examples/liquid_fft.gadt +++ b/examples/liquid_fft.gadt @@ -64,7 +64,7 @@ let fft px py = (* n must be a power of 2! *) let cc3 = cos (deref a3) in let ss3 = sin (deref a3) in asgn a (plus (deref a) e); - asgn a3 (plus (deref a3) e); + asgn a3 (plus (deref a3) e3); let rec loop1 i0 i1 i2 i3 id = if n + 1 <= i3 then () else (* out_of_bounds *) let g_px_i0 = array_get px i0 in diff --git a/examples/liquid_fft_full.gadt b/examples/liquid_fft_full.gadt new file mode 100644 index 0000000..d4709b6 --- /dev/null +++ b/examples/liquid_fft_full.gadt @@ -0,0 +1,189 @@ +(* +** by: Dave Edelblute, edelblut@cod.nosc.mil, 05 Jan 1993 +** Translated from C to de Caml: Hongwei Xi, 07 Nov 1998 +** Modified: R. Mayer to work with hist benchmark routines. +** Translated to InvarGenT: Lukasz Stafiniak, 30 Jan 2015 +*) +datatype Array : type * num +external let array_make : + ∀n, a [0≤n]. Num n → a → Array (a, n) = "fun a b -> Array.make a b" +external let array_get : + ∀n, k, a [0≤k ∧ k+1≤n]. Array (a, n) → Num k → a = "fun a b -> Array.get a b" +external let array_set : + ∀n, k, a [0≤k ∧ k+1≤n]. Array (a, n) → Num k → a → () = + "fun a b c -> Array.set a b c" +external let array_length : + ∀n, a [0≤n]. Array (a, n) → Num n = "fun a -> Array.length a" + +external let n2i : ∀n. Num n → Int = "fun i -> i" +external let div2 : ∀n. Num (2 n) → Num n = "fun i -> i / 2" +external let div4 : ∀n. Num (4 n) → Num n = "fun i -> i / 4" +external let n2f : ∀n. Num n → Float = "float_of_int" +external let equal : ∀a. a → a → Bool = "fun x y -> x = y" +external let leq : ∀a. a → a → Bool = "fun x y -> x <= y" +external let less : ∀a. a → a → Bool = "fun x y -> x < y" +external let ignore : ∀a. a → () = "ignore" + +external let abs : Float → Float = "abs_float" +external let cos : Float → Float = "cos" +external let sin : Float → Float = "sin" +external let neg : Float → Float = "(~-.)" +external let minus : Float → Float → Float = "(-.)" +external let plus : Float → Float → Float = "(+.)" +external let mult : Float → Float → Float = "( *. )" +external let div : Float → Float → Float = "( /. )" +external let fl0 : Float = "0.0" +external let fl05 : Float = "0.5" +external let fl1 : Float = "1.0" +external let fl2 : Float = "2.0" +external let fl3 : Float = "3.0" +external let fl4 : Float = "4.0" +external let pi : Float = "4.0 *. atan 1.0" +external let two_pi : Float = "8.0 *. atan 1.0" + +datatype Bounded : num * num +datacons Index : ∀i, k, n[n ≤ i ∧ i ≤ k].Num i ⟶ Bounded (n, k) + +let ffor s d body = + let rec loop i = + if i <= d then (body (Index i); loop (i + 1)) else () in + loop s + +external let ref : ∀a. a → Ref a = "fun a -> ref a" +external let asgn : ∀a. Ref a → a → () = "fun a b -> a := b" +external let deref : ∀a. Ref a → a = "(!)" + +let fft px py = (* n must be a power of 2! *) + let n = array_length px + (-1) in + let rec loop n2 n4 = + if n2 <= 2 then () else (* the case n2 = 2 is treated below *) + let e = div two_pi (n2f n2) in + let e3 = mult fl3 e in + let a = ref fl0 in + let a3 = ref fl0 in + let rec forbod j' = + match j' with Index j -> + (*for j = 1 to n4 do*) + let cc1 = cos (deref a) in + let ss1 = sin (deref a) in + let cc3 = cos (deref a3) in + let ss3 = sin (deref a3) in + asgn a (plus (deref a) e); + asgn a3 (plus (deref a3) e3); + let rec loop1 i0 i1 i2 i3 id = + if n + 1 <= i3 then () else (* out_of_bounds *) + let g_px_i0 = array_get px i0 in + let g_px_i2 = array_get px i2 in + let r1 = minus g_px_i0 g_px_i2 in + let r1' = plus g_px_i0 g_px_i2 in + array_set px i0 r1'; + let g_px_i1 = array_get px i1 in + let g_px_i3 = array_get px i3 in + let r2 = minus g_px_i1 g_px_i3 in + let r2' = plus g_px_i1 g_px_i3 in + array_set px i1 r2'; + let g_py_i0 = array_get py i0 in + let g_py_i2 = array_get py i2 in + let s1 = minus g_py_i0 g_py_i2 in + let s1' = plus g_py_i0 g_py_i2 in + array_set py i0 s1'; + let g_py_i1 = array_get py i1 in + let g_py_i3 = array_get py i3 in + let s2 = minus g_py_i1 g_py_i3 in + let s2' = plus g_py_i1 g_py_i3 in + array_set py i1 s2'; + let s3 = minus r1 s2 in + let r1 = plus r1 s2 in + let s2 = minus r2 s1 in + let r2 = plus r2 s1 in + array_set px i2 (minus (mult r1 cc1) (mult s2 ss1)); + array_set py i2 (minus (mult (neg s2) cc1) (mult r1 ss1)); + array_set px i3 (plus (mult s3 cc3) (mult r2 ss3)); + array_set py i3 (minus (mult r2 cc3) (mult s3 ss3)); + loop1 (i0 + id) (i1 + id) (i2 + id) (i3 + id) id in + let rec loop2 is id = + if n <= is then () + else ( + let i1 = is + n4 in + let i2 = i1 + n4 in + let i3 = i2 + n4 in + loop1 is i1 i2 i3 id; + loop2 (2 * id + j - n2) (4 * id)) in + loop2 j (2 * n2) in + ffor 1 n4 forbod; + loop (div2 n2) (div2 n4) in + loop n (div4 n); + + let rec loop1 i0 i1 id = + if n + 1 <= i1 then () else + let r1 = array_get px i0 in + array_set px i0 (plus r1 (array_get px i1)); + array_set px i1 (minus r1 (array_get px i1)); + let r1 = array_get py i0 in + array_set py i0 (plus r1 (array_get py i1)); + array_set py i1 (minus r1 (array_get py i1)); + loop1 (i0 + id) (i1 + id) id in + let rec loop2 is id = + if n <= is then () else ( + loop1 is (is + 1) id; + loop2 (2 * id + (-1)) (4 * id)) in + loop2 1 4; + + let rec loop1 j k = + eif j <= k then j + k + else loop1 (j - k) (div2 k) in + + let rec loop2 i j = + if n <= i then () else ( + if j <= i then () else ( + let xt = array_get px j in + array_set px j (array_get px i); array_set px i (xt); + let xt = array_get py j in + array_set py j (array_get py i); array_set py i (xt)); + let j' = loop1 j (div2 n) in + loop2 (i + 1) j') in + loop2 1 1; n + +let ffttest np = + let enp = n2f np in + let n2 = div2 np in + let npm = n2 - 1 in + let pxr = array_make (np+1) fl0 in + let pxi = array_make (np+1) fl0 in + let t = div pi enp in + array_set pxr 1 (mult (minus enp fl1) fl05); + array_set pxi 1 (fl0); + array_set pxr (n2+1) (neg (mult fl1 fl05)); + array_set pxi (n2+1) fl0; + let rec forbod i = + if i <= npm then + let j = np - i in + array_set pxr (i+1) (neg (mult fl1 fl05)); + array_set pxr (j+1) (neg (mult fl1 fl05)); + let z = mult t (n2f i) in + let y = mult (div (cos z) (sin z)) fl05 in + array_set pxi (i+1) (neg y); array_set pxi (j+1) (y) + else () in + forbod 1; + ignore (fft pxr pxi); + (* lukstafi: kr and ki are placeholders? *) + let rec loop i zr zi kr ki = + if np <= i then (zr, zi) else + let a = abs (minus (array_get pxr (i+1)) (n2f i)) in + let b = less zr a in + let zr = if b then a else zr in + let kr = eif b then i else kr in + let a = abs (array_get pxi (i+1)) in + let b = less zi a in + let zi = if b then a else zi in + let ki = eif b then i else ki in + loop (i+1) zr zi kr ki in + let zr, zi = loop 0 fl0 fl0 0 0 in + let zm = if less (abs zr) (abs zi) then zi else zr in + (*in print_float zm; print_newline ()*) zm + +let rec loop_np i np = + if 17 <= i then () else + ( ignore (ffttest np); loop_np (i + 1) (2 * np) ) + +let doit _ = loop_np 4 16 diff --git a/examples/liquid_fft_full.gadti.target b/examples/liquid_fft_full.gadti.target new file mode 100644 index 0000000..9ff4037 --- /dev/null +++ b/examples/liquid_fft_full.gadti.target @@ -0,0 +1,83 @@ +datatype Array : type * num + +external val array_make : ∀n, a[0 ≤ n]. Num n → a → Array (a, n) + +external val array_get : + ∀n, k, a[0 ≤ k ∧ k + 1 ≤ n]. Array (a, n) → Num k → a + +external val array_set : + ∀n, k, a[0 ≤ k ∧ k + 1 ≤ n]. Array (a, n) → Num k → a → () + +external val array_length : ∀n, a[0 ≤ n]. Array (a, n) → Num n + +external val n2i : ∀n. Num n → Int + +external val div2 : ∀n. Num (2 n) → Num n + +external val div4 : ∀n. Num (4 n) → Num n + +external val n2f : ∀n. Num n → Float + +external val equal : ∀a. a → a → Bool + +external val leq : ∀a. a → a → Bool + +external val less : ∀a. a → a → Bool + +external val ignore : ∀a. a → () + +external val abs : Float → Float + +external val cos : Float → Float + +external val sin : Float → Float + +external val neg : Float → Float + +external val minus : Float → Float → Float + +external val plus : Float → Float → Float + +external val mult : Float → Float → Float + +external val div : Float → Float → Float + +external val fl0 : Float + +external val fl05 : Float + +external val fl1 : Float + +external val fl2 : Float + +external val fl3 : Float + +external val fl4 : Float + +external val pi : Float + +external val two_pi : Float + +datatype Bounded : num * num + +datacons Index : ∀i, k, n[n ≤ i ∧ i ≤ k].Num i ⟶ Bounded (n, k) + +val ffor : + ∀i, j, k, n[j ≤ i ∧ k ≤ n]. + Num n → Num j → (Bounded (k, i) → ()) → () + +external val ref : ∀a. a → Ref a + +external val asgn : ∀a. Ref a → a → () + +external val deref : ∀a. Ref a → a + +val fft : + ∀k, n[1 ≤ n ∧ n + 1 ≤ k]. + Array (Float, n + 1) → Array (Float, k) → Num n + +val ffttest : ∀n[2 ≤ n]. Num n → Float + +val loop_np : ∀k, n[2 ≤ n]. Num k → Num n → () + +val doit : ∀a. a → () diff --git a/examples/liquid_fft_full_asserted.gadt b/examples/liquid_fft_full_asserted.gadt new file mode 100644 index 0000000..a675de3 --- /dev/null +++ b/examples/liquid_fft_full_asserted.gadt @@ -0,0 +1,191 @@ +(* +** by: Dave Edelblute, edelblut@cod.nosc.mil, 05 Jan 1993 +** Translated from C to de Caml: Hongwei Xi, 07 Nov 1998 +** Modified: R. Mayer to work with hist benchmark routines. +** Translated to InvarGenT: Lukasz Stafiniak, 30 Jan 2015 +*) +datatype Array : type * num +external let array_make : + ∀n, a [0≤n]. Num n → a → Array (a, n) = "fun a b -> Array.make a b" +external let array_get : + ∀n, k, a [0≤k ∧ k+1≤n]. Array (a, n) → Num k → a = "fun a b -> Array.get a b" +external let array_set : + ∀n, k, a [0≤k ∧ k+1≤n]. Array (a, n) → Num k → a → () = + "fun a b c -> Array.set a b c" +external let array_length : + ∀n, a [0≤n]. Array (a, n) → Num n = "fun a -> Array.length a" + +external let n2i : ∀n. Num n → Int = "fun i -> i" +external let div2 : ∀n. Num (2 n) → Num n = "fun i -> i / 2" +external let div4 : ∀n. Num (4 n) → Num n = "fun i -> i / 4" +external let n2f : ∀n. Num n → Float = "float_of_int" +external let equal : ∀a. a → a → Bool = "fun x y -> x = y" +external let leq : ∀a. a → a → Bool = "fun x y -> x <= y" +external let less : ∀a. a → a → Bool = "fun x y -> x < y" +external let ignore : ∀a. a → () = "ignore" + +external let abs : Float → Float = "abs_float" +external let cos : Float → Float = "cos" +external let sin : Float → Float = "sin" +external let neg : Float → Float = "(~-.)" +external let minus : Float → Float → Float = "(-.)" +external let plus : Float → Float → Float = "(+.)" +external let mult : Float → Float → Float = "( *. )" +external let div : Float → Float → Float = "( /. )" +external let fl0 : Float = "0.0" +external let fl05 : Float = "0.5" +external let fl1 : Float = "1.0" +external let fl2 : Float = "2.0" +external let fl3 : Float = "3.0" +external let fl4 : Float = "4.0" +external let pi : Float = "4.0 *. atan 1.0" +external let two_pi : Float = "8.0 *. atan 1.0" + +datatype Bounded : num * num +datacons Index : ∀i, k, n[n ≤ i ∧ i ≤ k].Num i ⟶ Bounded (n, k) + +let ffor s d body = + let rec loop i = + if i <= d then (body (Index i); loop (i + 1)) else () in + loop s + +external let ref : ∀a. a → Ref a = "fun a -> ref a" +external let asgn : ∀a. Ref a → a → () = "fun a b -> a := b" +external let deref : ∀a. Ref a → a = "(!)" + +let fft px py = (* n must be a power of 2! *) + let n = array_length px + (-1) in + assert num n + 1 <= array_length py; + assert num array_length py <= n + 1; + let rec loop n2 n4 = + if n2 <= 2 then () else (* the case n2 = 2 is treated below *) + let e = div two_pi (n2f n2) in + let e3 = mult fl3 e in + let a = ref fl0 in + let a3 = ref fl0 in + let rec forbod j' = + match j' with Index j -> + (*for j = 1 to n4 do*) + let cc1 = cos (deref a) in + let ss1 = sin (deref a) in + let cc3 = cos (deref a3) in + let ss3 = sin (deref a3) in + asgn a (plus (deref a) e); + asgn a3 (plus (deref a3) e3); + let rec loop1 i0 i1 i2 i3 id = + if n + 1 <= i3 then () else (* out_of_bounds *) + let g_px_i0 = array_get px i0 in + let g_px_i2 = array_get px i2 in + let r1 = minus g_px_i0 g_px_i2 in + let r1' = plus g_px_i0 g_px_i2 in + array_set px i0 r1'; + let g_px_i1 = array_get px i1 in + let g_px_i3 = array_get px i3 in + let r2 = minus g_px_i1 g_px_i3 in + let r2' = plus g_px_i1 g_px_i3 in + array_set px i1 r2'; + let g_py_i0 = array_get py i0 in + let g_py_i2 = array_get py i2 in + let s1 = minus g_py_i0 g_py_i2 in + let s1' = plus g_py_i0 g_py_i2 in + array_set py i0 s1'; + let g_py_i1 = array_get py i1 in + let g_py_i3 = array_get py i3 in + let s2 = minus g_py_i1 g_py_i3 in + let s2' = plus g_py_i1 g_py_i3 in + array_set py i1 s2'; + let s3 = minus r1 s2 in + let r1 = plus r1 s2 in + let s2 = minus r2 s1 in + let r2 = plus r2 s1 in + array_set px i2 (minus (mult r1 cc1) (mult s2 ss1)); + array_set py i2 (minus (mult (neg s2) cc1) (mult r1 ss1)); + array_set px i3 (plus (mult s3 cc3) (mult r2 ss3)); + array_set py i3 (minus (mult r2 cc3) (mult s3 ss3)); + loop1 (i0 + id) (i1 + id) (i2 + id) (i3 + id) id in + let rec loop2 is id = + if n <= is then () + else ( + let i1 = is + n4 in + let i2 = i1 + n4 in + let i3 = i2 + n4 in + loop1 is i1 i2 i3 id; + loop2 (2 * id + j - n2) (4 * id)) in + loop2 j (2 * n2) in + ffor 1 n4 forbod; + loop (div2 n2) (div2 n4) in + loop n (div4 n); + + let rec loop1 i0 i1 id = + if n + 1 <= i1 then () else + let r1 = array_get px i0 in + array_set px i0 (plus r1 (array_get px i1)); + array_set px i1 (minus r1 (array_get px i1)); + let r1 = array_get py i0 in + array_set py i0 (plus r1 (array_get py i1)); + array_set py i1 (minus r1 (array_get py i1)); + loop1 (i0 + id) (i1 + id) id in + let rec loop2 is id = + if n <= is then () else ( + loop1 is (is + 1) id; + loop2 (2 * id + (-1)) (4 * id)) in + loop2 1 4; + + let rec loop1 j k = + eif j <= k then j + k + else loop1 (j - k) (div2 k) in + + let rec loop2 i j = + if n <= i then () else ( + if j <= i then () else ( + let xt = array_get px j in + array_set px j (array_get px i); array_set px i (xt); + let xt = array_get py j in + array_set py j (array_get py i); array_set py i (xt)); + let j' = loop1 j (div2 n) in + loop2 (i + 1) j') in + loop2 1 1; n + +let ffttest np = + let enp = n2f np in + let n2 = div2 np in + let npm = n2 - 1 in + let pxr = array_make (np+1) fl0 in + let pxi = array_make (np+1) fl0 in + let t = div pi enp in + array_set pxr 1 (mult (minus enp fl1) fl05); + array_set pxi 1 (fl0); + array_set pxr (n2+1) (neg (mult fl1 fl05)); + array_set pxi (n2+1) fl0; + let rec forbod i = + if i <= npm then + let j = np - i in + array_set pxr (i+1) (neg (mult fl1 fl05)); + array_set pxr (j+1) (neg (mult fl1 fl05)); + let z = mult t (n2f i) in + let y = mult (div (cos z) (sin z)) fl05 in + array_set pxi (i+1) (neg y); array_set pxi (j+1) (y) + else () in + forbod 1; + ignore (fft pxr pxi); + (* lukstafi: kr and ki are placeholders? *) + let rec loop i zr zi kr ki = + if np <= i then (zr, zi) else + let a = abs (minus (array_get pxr (i+1)) (n2f i)) in + let b = less zr a in + let zr = if b then a else zr in + let kr = eif b then i else kr in + let a = abs (array_get pxi (i+1)) in + let b = less zi a in + let zi = if b then a else zi in + let ki = eif b then i else ki in + loop (i+1) zr zi kr ki in + let zr, zi = loop 0 fl0 fl0 0 0 in + let zm = if less (abs zr) (abs zi) then zi else zr in + (*in print_float zm; print_newline ()*) zm + +let rec loop_np i np = + if 17 <= i then () else + ( ignore (ffttest np); loop_np (i + 1) (2 * np) ) + +let doit _ = loop_np 4 16 diff --git a/examples/liquid_fft_full_asserted.gadti.target b/examples/liquid_fft_full_asserted.gadti.target new file mode 100644 index 0000000..82f278b --- /dev/null +++ b/examples/liquid_fft_full_asserted.gadti.target @@ -0,0 +1,82 @@ +datatype Array : type * num + +external val array_make : ∀n, a[0 ≤ n]. Num n → a → Array (a, n) + +external val array_get : + ∀n, k, a[0 ≤ k ∧ k + 1 ≤ n]. Array (a, n) → Num k → a + +external val array_set : + ∀n, k, a[0 ≤ k ∧ k + 1 ≤ n]. Array (a, n) → Num k → a → () + +external val array_length : ∀n, a[0 ≤ n]. Array (a, n) → Num n + +external val n2i : ∀n. Num n → Int + +external val div2 : ∀n. Num (2 n) → Num n + +external val div4 : ∀n. Num (4 n) → Num n + +external val n2f : ∀n. Num n → Float + +external val equal : ∀a. a → a → Bool + +external val leq : ∀a. a → a → Bool + +external val less : ∀a. a → a → Bool + +external val ignore : ∀a. a → () + +external val abs : Float → Float + +external val cos : Float → Float + +external val sin : Float → Float + +external val neg : Float → Float + +external val minus : Float → Float → Float + +external val plus : Float → Float → Float + +external val mult : Float → Float → Float + +external val div : Float → Float → Float + +external val fl0 : Float + +external val fl05 : Float + +external val fl1 : Float + +external val fl2 : Float + +external val fl3 : Float + +external val fl4 : Float + +external val pi : Float + +external val two_pi : Float + +datatype Bounded : num * num + +datacons Index : ∀i, k, n[n ≤ i ∧ i ≤ k].Num i ⟶ Bounded (n, k) + +val ffor : + ∀i, j, k, n[j ≤ i ∧ k ≤ n]. + Num n → Num j → (Bounded (k, i) → ()) → () + +external val ref : ∀a. a → Ref a + +external val asgn : ∀a. Ref a → a → () + +external val deref : ∀a. Ref a → a + +val fft : + ∀n[1 ≤ n]. Array (Float, n + 1) → Array (Float, n + 1) → Num n + +val ffttest : ∀n[2 ≤ n]. Num n → Float + +val loop_np : ∀k, n[2 ≤ n]. Num k → Num n → () + +val doit : ∀a. a → () diff --git a/examples/liquid_fft_simpler.gadt b/examples/liquid_fft_simpler.gadt index 6c3dece..5ba1483 100644 --- a/examples/liquid_fft_simpler.gadt +++ b/examples/liquid_fft_simpler.gadt @@ -66,7 +66,7 @@ let fft px py = (* n must be a power of 2! *) let cc3 = cos (deref a3) in let ss3 = sin (deref a3) in asgn a (plus (deref a) e); - asgn a3 (plus (deref a3) e); + asgn a3 (plus (deref a3) e3); let rec loop1 i0 i1 i2 i3 id = if n + 1 <= i3 then () else (* out_of_bounds *) let g_px_i0 = array_get px i0 in diff --git a/examples/liquid_fft_tests.gadt b/examples/liquid_fft_tests.gadt new file mode 100644 index 0000000..b36b92c --- /dev/null +++ b/examples/liquid_fft_tests.gadt @@ -0,0 +1,98 @@ +(* +** by: Dave Edelblute, edelblut@cod.nosc.mil, 05 Jan 1993 +** Translated from C to de Caml: Hongwei Xi, 07 Nov 1998 +** Modified: R. Mayer to work with hist benchmark routines. +** Translated to InvarGenT: Lukasz Stafiniak, 30 Jan 2015 +*) +datatype Array : type * num +external let array_make : + ∀n, a [0≤n]. Num n → a → Array (a, n) = "fun a b -> Array.make a b" +external let array_get : + ∀n, k, a [0≤k ∧ k+1≤n]. Array (a, n) → Num k → a = "fun a b -> Array.get a b" +external let array_set : + ∀n, k, a [0≤k ∧ k+1≤n]. Array (a, n) → Num k → a → () = + "fun a b c -> Array.set a b c" +external let array_length : + ∀n, a [0≤n]. Array (a, n) → Num n = "fun a -> Array.length a" + +external let n2i : ∀n. Num n → Int = "fun i -> i" +external let div2 : ∀n. Num (2 n) → Num n = "fun i -> i / 2" +external let div4 : ∀n. Num (4 n) → Num n = "fun i -> i / 4" +external let n2f : ∀n. Num n → Float = "float_of_int" +external let equal : ∀a. a → a → Bool = "fun x y -> x = y" +external let leq : ∀a. a → a → Bool = "fun x y -> x <= y" +external let less : ∀a. a → a → Bool = "fun x y -> x < y" +external let ignore : ∀a. a → () = "ignore" + +external let abs : Float → Float = "abs_float" +external let cos : Float → Float = "cos" +external let sin : Float → Float = "sin" +external let neg : Float → Float = "(~-.)" +external let minus : Float → Float → Float = "(-.)" +external let plus : Float → Float → Float = "(+.)" +external let mult : Float → Float → Float = "( *. )" +external let div : Float → Float → Float = "( /. )" +external let fl0 : Float = "0.0" +external let fl05 : Float = "0.5" +external let fl1 : Float = "1.0" +external let fl2 : Float = "2.0" +external let fl3 : Float = "3.0" +external let fl4 : Float = "4.0" +external let pi : Float = "4.0 *. atan 1.0" +external let two_pi : Float = "8.0 *. atan 1.0" + +datatype Bounded : num * num +datacons Index : ∀i, k, n[n ≤ i ∧ i ≤ k].Num i ⟶ Bounded (n, k) +external ffor : ∀k, n. Num k → Num n → (Bounded (k, n) → ()) → () + +external let ref : ∀a. a → Ref a = "fun a -> ref a" +external let asgn : ∀a. Ref a → a → () = "fun a b -> a := b" +external let deref : ∀a. Ref a → a = "(!)" + +external fft : + ∀k, n[1 ≤ n ∧ n + 1 ≤ k]. + Array (Float, n + 1) → Array (Float, k) → Num n + +let ffttest np = + let enp = n2f np in + let n2 = div2 np in + let npm = n2 - 1 in + let pxr = array_make (np+1) fl0 in + let pxi = array_make (np+1) fl0 in + let t = div pi enp in + array_set pxr 1 (mult (minus enp fl1) fl05); + array_set pxi 1 (fl0); + array_set pxr (n2+1) (neg (mult fl1 fl05)); + array_set pxi (n2+1) fl0; + let rec forbod i = + if i <= npm then + let j = np - i in + array_set pxr (i+1) (neg (mult fl1 fl05)); + array_set pxr (j+1) (neg (mult fl1 fl05)); + let z = mult t (n2f i) in + let y = mult (div (cos z) (sin z)) fl05 in + array_set pxi (i+1) (neg y); array_set pxi (j+1) (y) + else () in + forbod 1; + ignore (fft pxr pxi); + (* lukstafi: kr and ki are placeholders? *) + let rec loop i zr zi kr ki = + if np <= i then (zr, zi) else + let a = abs (minus (array_get pxr (i+1)) (n2f i)) in + let b = less zr a in + let zr = if b then a else zr in + let kr = eif b then i else kr in + let a = abs (array_get pxi (i+1)) in + let b = less zi a in + let zi = if b then a else zi in + let ki = eif b then i else ki in + loop (i+1) zr zi kr ki in + let zr, zi = loop 0 fl0 fl0 0 0 in + let zm = if less (abs zr) (abs zi) then zi else zr in + (*in print_float zm; print_newline ()*) zm + +let rec loop_np i np = + if 17 <= i then () else + ( ignore (ffttest np); loop_np (i + 1) (2 * np) ) + +let doit _ = loop_np 4 16 diff --git a/examples/liquid_fft_tests.gadti.target b/examples/liquid_fft_tests.gadti.target new file mode 100644 index 0000000..429a116 --- /dev/null +++ b/examples/liquid_fft_tests.gadti.target @@ -0,0 +1,81 @@ +datatype Array : type * num + +external val array_make : ∀n, a[0 ≤ n]. Num n → a → Array (a, n) + +external val array_get : + ∀n, k, a[0 ≤ k ∧ k + 1 ≤ n]. Array (a, n) → Num k → a + +external val array_set : + ∀n, k, a[0 ≤ k ∧ k + 1 ≤ n]. Array (a, n) → Num k → a → () + +external val array_length : ∀n, a[0 ≤ n]. Array (a, n) → Num n + +external val n2i : ∀n. Num n → Int + +external val div2 : ∀n. Num (2 n) → Num n + +external val div4 : ∀n. Num (4 n) → Num n + +external val n2f : ∀n. Num n → Float + +external val equal : ∀a. a → a → Bool + +external val leq : ∀a. a → a → Bool + +external val less : ∀a. a → a → Bool + +external val ignore : ∀a. a → () + +external val abs : Float → Float + +external val cos : Float → Float + +external val sin : Float → Float + +external val neg : Float → Float + +external val minus : Float → Float → Float + +external val plus : Float → Float → Float + +external val mult : Float → Float → Float + +external val div : Float → Float → Float + +external val fl0 : Float + +external val fl05 : Float + +external val fl1 : Float + +external val fl2 : Float + +external val fl3 : Float + +external val fl4 : Float + +external val pi : Float + +external val two_pi : Float + +datatype Bounded : num * num + +datacons Index : ∀i, k, n[n ≤ i ∧ i ≤ k].Num i ⟶ Bounded (n, k) + +external ffor : ∀k, n. Num k → Num n → (Bounded (k, n) → ()) → () + +external val ref : ∀a. a → Ref a + +external val asgn : ∀a. Ref a → a → () + +external val deref : ∀a. Ref a → a + +external fft : + ∀k, n[1 ≤ n ∧ n + 1 ≤ k]. + Array (Float, n + 1) → Array (Float, k) → Num n + +val ffttest : ∀n[2 ≤ n]. Num n → Float + +val loop_np : ∀k, n[2 ≤ n]. Num k → Num n → () + +val doit : ∀a. a → () diff --git a/src/InvarGenTTest.ml b/src/InvarGenTTest.ml index 012312a..5af72a2 100644 --- a/src/InvarGenTTest.ml +++ b/src/InvarGenTTest.ml @@ -8,6 +8,7 @@ open OUnit let debug = ref (*[* true *]*)false +let short_tests_only = ref false let input_file file = let f = open_in file in @@ -631,7 +632,7 @@ let tests = "InvarGenT" >::: [ "liquid_simplex-harder" >:: (fun () -> skip_if !debug "debug"; - (* Can take over 220 seconds. *) + skip_if !short_tests_only "long test: 220s"; test_case "liquid_simplex_harder" ()); "liquid_gauss_rowSwap" >:: (fun () -> @@ -686,15 +687,30 @@ let tests = "InvarGenT" >::: [ test_case "liquid_fft_ffor" ()); "liquid_fft_simpler" >:: (fun () -> - (* Can take over 180 seconds. *) skip_if !debug "debug"; + skip_if !short_tests_only "long test: 180s"; test_case ~same_with_assertions:true "liquid_fft_simpler" ()); "liquid_fft" >:: (fun () -> - (* Can take over 180 seconds. *) skip_if !debug "debug"; + skip_if !short_tests_only "long test: 190s"; test_case "liquid_fft" ()); + "liquid_fft_tests" >:: + (fun () -> + skip_if !debug "debug"; + test_case "liquid_fft_tests" ()); + "liquid_fft_full" >:: + (fun () -> + skip_if !debug "debug"; + skip_if !short_tests_only "long test: 195s"; + test_case "liquid_fft_full" ()); + "liquid_fft_full_asserted" >:: + (fun () -> + skip_if !debug "debug"; + skip_if !short_tests_only "long test: 210s"; + test_case ~same_with_assertions:true + "liquid_fft_full_asserted" ()); ] let () =