From 82cc947959dd6002fd94a4d6d498cd04813c423a Mon Sep 17 00:00:00 2001 From: lukstafi Date: Tue, 24 Feb 2015 20:39:54 +0100 Subject: [PATCH] Cleanup related to the Gauss example. --- doc/invargent-manual.pdf | Bin 175420 -> 176579 bytes doc/invargent-manual.tm | 20 ++++++++++++++---- examples/liquid_gauss_harder.gadt | 2 +- examples/liquid_gauss_harder_asserted.gadt | 5 ++--- .../liquid_gauss_harder_asserted.gadti.target | 2 +- src/InvarGenTTest.ml | 3 +-- 6 files changed, 21 insertions(+), 11 deletions(-) diff --git a/doc/invargent-manual.pdf b/doc/invargent-manual.pdf index 40a260069413d96da49514d8979170afb7d47e9f..9cd91fb373b0cf82a8219f958f4a106400e1b1f2 100644 GIT binary patch delta 17781 zcma*NWmubQ*DZ>>7l-1m2?>GVQYaL6w-$E_w0Mx>Ufc@By~VA#6f0VwxVyW!1=f@02=PHJ8HM~4KOwWPxXM)evYzuQ+X+_%*Y3hfm<^f+s zTP)_Zws7MbeI%J5N2&}`)|{V-W#=RAu7ow_H8xAWjDxb*{`iS+iT^ri%)BkzST8>O zU99w&|ER=8?R~*eI^;mz>=pm;Vf4JDy|}&+s(0`1nqYKMlIDC<-m|&g8aFWE5M5X` z1}pg^^{v_9rLZSBs#p`)ynD{}=Z{sZK%>{$)cL6S>_-u4hrOG(RT{;+?y8Gb0&`u+Vd8@*>OsQ46OUDYD%?M3potIlDZKJwkfO?{M$EVor% z`PA;=fVR^;o$$<7b_cxu_;(1dpkCY3j{=x@U3t#(=}%gh_Ox>%Sdib+u}f8C^FgU> z8czo15EA8??K@iw@3Tkev)2NOWvQ!_`UR*0qd95VzA&&S;CYk@IS` zR-Yj5pFi{0>uT23eB6IUf4e#^h6r~*n2j{uT8LHKevS!1kt#H{{fZq+6uyPMmV2BL*OvXHnP=8>4b#p{SFiX8~P3$DH_ zdSrhv^pnfzxA?;2&A5gGY)dDZ^W^5Q3xW`wSw2hM7He~ zLEGCcFdE*tv>Cy~Ek)^V=p@%QIvbV)7|WAU;I>xFPpiBA`J?2pe&F&?9{7x4;WVTX zvUha~6_qF$Z(MAO+)=QoA=&P+LJ)@z|D;%#*tCrw`eK~-_P5uCnTA)j+-q)FDaJJ7 zILz)UACj)fL9SJ=#;|?F+1lJI6BDwR+$uRfzTKotTFf3D6s1bK6Hh&$5=NNiBK*_7 zV_BT(c*`rcQtbw6rZ{Mfh2r*jJQnr!qALgsA%V5`c7mHx}f*-;gpMVqEX|u9UchfYK#;?5q(@fa|DqX}+ zO(fJjAW!L{t$F&O+uWNQL=z~MMIB0uC$++=rY$KfT~~VEsaw4Hc7qiuPQ_jN8%hSm#ErZ_@X|B#-nHW@t;9X zOv#Um)*k(MruK+uQ-Dxdb&N?hwh!G0dO$49_Mg825t}h=?Yrtxdr1rZUYqbl)XK-J z%EtuJA^R-`>bDs*onUPg3#@)6Qg*V|g)nWWzGx1d_DKZ&hO$M`PQ~+MauRJMt&)I* zpM0w0dLrmZ+U_^vmHOnq`v~sn#t40jsPcL1%;(!cHPjhQUs#Q?9MN{^m1pUqxJQ-q zQnrtME%2=#LDc69m&z%QccsniWCbAkpn&4ZuG$~fHl5KUE~+WgHr9H?>iC!Jv7mX% zkt+68L~}RV7~lTgVa`@TU*EPpatm>H^!kTdAEWo&`zPP^(2u4<5Q$#va%n6WhRz?< zi?7nN#Z{y%B*PLqRF%48jp4tGYty0)V8Z9sUXk@G05pu@>&V!XnNqKcMzt z#|?cKjz$`TlNLz%=DvaU7D>>g5WaLV#32Q}$;!j*=oZ#D{8b80mHK;TU}7b4y9Dd$ z5-Bp+2NpwGS_H);Ng#E(2@yBm9{EoekZDwntyXMI$9vgcr0v{s6jQ%h<)?M)`OmN zN6}Vyn-GRT6p6xRi6bNEkGgb!-w-jMIq^-d8qwcY3*!gA-U5ai-SPJ}LQ4Zo17&;y zmwo9fM09Nd-r|flD=M&~2ngM<6^xy(Rk|aDi*Xfz@Q~#z%ChvoUykR>onK&0I2hgDNX`}A{4^~lH`XG6WKDpgj7Te{oqC#VzwRH++T28bMBTPgqJ)1Eo zibn3Zl=Z!2rEd848Pm&4D~_yibQZzAE%IxFKC76s*1?61A)&IBFkJ9CJatV;8QG0` zK5gE)(N}f08(h=*)&+dtvNRZh`jtgm*N=?wu^w5+oW=(mriL)?&2`$M#UWG5t7xou zHuNJ)3f8Y}C8M)Lz}sLfyz5sE7^DsXG$LQk!g*h?s|LKtgI6E@t%30M2Ya#P*kxHw zisFJTc-b@A%YK}VLIi^C!h7x%{@Kn#7=VSv^;w#JqqM4vf!L}L>x>=gjO%rwU-WM&5`!7b;6;sQ(_cv~uBs9$XMw5r0n4dyEM4~8Z zYtndk2yQkRd&aF7Xh_nFVwPW{_`Np88ciWvWLKxPgxIx{kVRJ4s=vvV^q`QoW3uUQ z;c_@rL}z?g?L8h>O&ehV8~N@>8d~Xc@)8$k-B!wHqy*hIh(pP2@W39#HTm_khjdym zyKlZ#4bwFp-mVevJ!WiX-dC5fAqLDu-&KzidYPRmirv1gU&MP6$1(U4J%tB1OLw+K z3CU5#ACfT}Py7TU(~1yMLMtfmMvg)mA@Ndd)1;;oBwe~JOS9H=Fwe}A1Nqc3Z50K0 z)nLg0g-%Tqr3Bi3F+>9%Tqz9mL-C|R7VFg|N(geP)o;c9tvPf;SU+Lm3%Hg~IUBWQ z67f^k$|)$*82v{q6#lHmYKC&1m$mD?qtj`dQxLj^00Aux#mQ#2Gd&Z{K~(X^xSh%tcQ#$?)f+FYC3wFb%UWjw{*c|&@7m)L2N=7S6a2~o z6iS`AR0E}7$APdJ9Vs|MO6H;y`&?oNI*6SH-~2Al)`7ok^*hZK49uYefTZ+~Nt|V5 z#Dm{dFDC1wne%Qg^yJU+3NiF!DD^&#&|FO@RgipQ`50Cm+=C>Klotve#m~Y>)MxM> z-08oaGk`-fzR6wRbDJ%umx|rrS1$HLT*HHBn4t?$^_PeJw!IRgiMz&O_7)>mJ(&$t z^s0^Fx)^|bQGRpO6f5n;HEpHEpG${mg5i7!;CZX>btx%)wu^*DUi+HQ#937QU^5{k0HzMiJI^*mi}} zSUe+l183MIhlj9Oe@56{u7vR);W&oPu!S-TL^MeEKTUXbc_tTE8yH1JT>P&m`Emu+MGE>FC62X9xOw1302hmV)Vl0 z&{>s~j7SAJ+Tn1lQNodS7CAQy$HQ_#Vm4Ou9AFwH2EZ<+z7#A((zcB`;B6 zw(twgysvAC(ZMoZo3oWR{G2XKi>wx;lYjK<=CTCQAt{ zCD=}*%t0>~XO9d7jSpkD;NRt)P zsOGXeg$gKWxB=LizfuG~@2}TD3;-qFJ7-hBv>H;{=uA-aOQyE?PEzGBYY&I3Em+^Sv;U z{`qH9O;OGKa73_A)~AP4bp4a|9uiq_y5rDSr*g`cpRv3e1n05NFo#1|({)&SV%z{! z<4)PIp;Hgtq&s>5TvdJ2*#91KQWj`*y81$7!(sC68hkOwdYxmib(&|(%eM>g&X<{} zEJ{A3V(vFD5Z0*%*Xz(kS%Noq!ndn&qEq^2f2t;*U5aOO=bcMD%?|6e;44xE5>p)W$!nDe|npX(;=rR^Y4arWMr=(#clg7DGqc zZVY!}C*r%XN{9RRHML!pF#J&3H~nA71x>z@$m1L)%XIY*2o{aw*L^x-LGxm{_U}D# zxGGz^#OQ!vIz%uz1lGh&3Q7>+Hc-nye~Jj7@8ii>c$q)4TWXX`4#>7HP^ z8+hWNc2q8f`qq9gJj|72qP?)W1{J}ff#4}P7} zZ;U?`m2UmG>PFZ;DBib2>>_6mQ0TJp?8QVhj8T1OaPd7{<)(WLabFc+WBGQry6aWt z5+F11X%FHulaUngdjv8qR;6S88Xcd!=k?e=opgq&iLo@T!CXPNYt6qArRmqj86|=^ zLy4Fb?rge_*ZMaJFdQW&W8G*sJA@+BxXftrUdPkrEwLG%4LYGAsv=3#kh&Q2wVG6> z*}~CkX7x?=wU_ee8*Y`>k1g-(F@b5$p_eB``WQPDQn)u9QYJzN5H(1Fle32`rN)XF zj|Q*kFk%G*45d#kQTJr{@~Bv?Tocgn-X0}$TiKTDYZRx#J6a{u_a|9UoWXXvlTOc=@ZcTL>nVSn)*IMr*FL4(&&|Kc8Zewj6VBXiCRN)mti5fmUTSH483|@}Ufe`Fq1H_8q<;+_0Xlcgv&1$?9bdY>WP=QEB;dI^F;;J1e^%dqxhtMJR}uSc$C(t`1y- zjv&K^V@*P)lSc{xFj^3oK;6CGkzuXPQ7BG(1m)Nmm@LOO^T3o?#imXr(dAFF(`rf1>&KMGd(qsL;i@DI zF?dQuJ}@weRSaGOHu58m0*pd13sfalj6-8lX2y0&+NJMHV0v#l=}_2sQ|%-r2oh(CF`5 zN3Skv5xRr&r+HOj2GpchXP?i^_8lB6ikA4ZW-0E-elHt=`BZw=p4xi+8O(x6=M{LW zd(9)!+OgZ|q=X+9UGaPrwl*IUb3Gc*%qpz0EHF}i`Aa8as5?iRmATXbHhn)3H5NC| zEZAf;N9?Cmcz-=|kgwIPo`C&*dpx}x<^2@**wJar^v@3-3f)!a`Njx#L&22{$& z{$ZO9yBe-ZFeT^PQ}v>J=b5|&P5$6D-?LX-!lV92dsP0VUD9Eib$}0BS~4jw6l=;9 zGswE>IMp15)tsavwjq1D7vq@)>P@e^o9@*sBF9^CYxd7J^G6|Yj4$u2{(Oj+H)nYj zoYr^sVbD8fHe9^Ht%f*LoK=!y(!4fNS|iz;udD{P3WJNW@w7tZLT8;6p~Vp`Skc%x zV%n@!s#$NJyTwN*c4I@2Gq=vxL;sP6WQHQ2`cOW7zbSzQdV{`1;R@3vSR5zAn5jx9 ztS;`d$B?B`IN5aKj=o{Pb9!g}D=%*h2@E7<63Ip<9G4 z6G?z_xD<82$O~ePh|~OtX;q(;H#J@t3F$zhfW`3J)i~BlnL5#-U?v3<;CD^K;lk0` z?&=1ftyr>GSblo?rGQX)gczL^;RSs7lKnX^;P{POkWh&O_6L<{K8*Oy+qcx)p!Q^9 z9n2WUyaSxv#a{O*$_!kZkv7|s420C+H_`8NvE}!9UPtWmuax?(=QBr=^i!-?5Y!s$ z*})P)bRI)0))uQJ@#*7NUp7ZwUTvy)ro=;QhHq7X(%{#Q6QtoP*D~BD^_ax@)K|I2 z_x^=%VN7sv&`*W0CU{5tN!u)i3vf~%gVldddIWY8&wgWnhwT-r=y%J>v zL-Q+%K#cYUyq1+2M9uKnK=_E?yG9;m6=bmY#^bl@?1dNT6CzK^XKQRHM^jnXLl7jC zBSmdnw7MLu7o%x3YSVXGPS8UxL$^%EI(w{8;lao}vvgU6Cnxva`Jsgp{VpRQk;UvF z++&q9IVmHA)Ka5|1FyjA`;@E}{rm2$@*De@3#y?>PJg1wC<)`)m`^k=JwQE?b4u8T z)@Vh!mclC{$Cqc)wi|?*%a(|Zghws%s<<~fdXxuli|l(8@WH}KH<+J|Em2|vBEQ6^ zaWiJPe1=c_Ai>rQC-8^3VlpJ_rJ*ebHl;DKByC5yO|hxh*XtCVR&h&JF(IR~AH`j^ z#U&_GC=CVr#Ib{st6wO>>V0(OlOboY%93-qyU>>lOgxg5IM|TwF%|yx)wWJ!Lb^hn z?-ry=ms+m*@V@YiO5>@W3Y(_t=;1`lGpnsw7)0}b(6TJ^o80nHMo=8Ck&u!6eph!m z3Wm(*ZpSES;0?BGv1YvDn_isPs-= z6*iCF6o`4iaqtw_DEVdfRxb=+T)dC?6jx+ys*MzDtR6|jBV3*+k!u+rto7DL&`Eg| zL!o0NG{!;CVGnJ0%w1!`Ga9R!>^JM5y(~xuGPnR_Xdlt{YV8_BGCgIA+r}WJ@52!1 ztjlKyEuovJ_rpfc^FUXj+?8()uubs;ca?fU)nhYa#MIMjHtD1WX1y&I+{WBDv7TSl zEd&Plzb$_k3#|SY8iL?;GEHDoA8x!;jn>Zjy)X)&g-}}}mA;)V=fDxJ%=j8RZg)q{ zwatEZ5{CqJWr><6iwf_Ir_0n=$TzK;^84oRb76ZTLzXds3uh1L)xN854onE~3@Uzt zni34E#{HUHb1Et3;Kp=dL4>b<%?WeXs@^v_?{n*3T-(!0=Z&5$CivcAj6^x=WWZs{ z*IB1gx9YAr9?YB2xT2fxm=ns>M)8XM!q9k2Zo;~b+2)PYc;FkXgalwe#m0-Ow<(-jksMU8Q)L_STvR3B)#Vw`}2 zkX13ai1VfGgiw1sj9kahyHe#4ImNB!7xSjtW?Uin{QKK$q8|q^u@Kv?Yu0y<75Hyk zt?!vMc8$+WTMgi0!#NFZM!z|~YD8_9b&D{IRNS7rVPlithMNnVJx~u;YZF_r_=|(W zab{!uO$@48J;QZeXdBd;xpFkzH6ar|HBUd}nP9%K{51~WPZ<7tXeH)6kLx{6{JJ*H zBk%W~BQaLz?5UMnLJf`!CHPr5$%xVoqC#RSjcK&9l>$R@7}U2iF`r6ctHF@}*qvjh zn9l1e>NSRgbT}r{1VU?stAjIxdbDEjkL%h1E;X~TF5}Y>)?`+vWDp|?4UZGP+MlW~ z-Sj+a9LyU;-6-X({mRmWjb&yPotDSQF*NEF#Zba4-}-IBpQcg4>UZVvlL(hPX^wQ? z;}jGZ%DI(uV1erx6-d-BBi5K>p1E7FEUc;^40- zJQZkW3Te|cnrj`F5%^yPYNL7~f`nG-l4b6Up)cj#eHOLxmx;7j zf3hU@5P54?EdU)tP87IOokUW(0~}InU!?1y#}8PS!%*}#&4wCBXfbJU#_(NKkHJ7< zc_t~*wdyr6k2Gx#<0h-V`c4>Sh`11fg^RNJ0yj{`O^J>C%-;V?>Zic)4r=i2|= zH*|yPs|h-59!zLggs>CUdEd7`WD{#DQhC+%F6;9nL;CSe^m{{{JgfUG$g<7G*-YMg zNVb{Us@AX6=WS6Cm7-~cV$*3(J}`dk%+}lsK*g|4SMfY{{h7?END>=4e7NwKY6RNu zsV`k1J>(1h2+&ymcJ{6C=gWT=e!vmD%VUlzF9>lt&Y<^hGXjWlvdK2 z>B~>FD!ly;t>c#UYPq(z%IQ_UU+Z3mHQCAYvnt1myI#W^5TW9si@rJ!=EQ@WU%w@1 zag&D3tBS$xuU?DWAar0x_`-*p_-*JU5}!v)w_{I}YiI~pTjXWCpDI48Uou2(Yi)7E zbdr3A<7_aM-@VTyDp5|?jeW1RKq9{LCb(&W!rA@Li`Ht>AJcH{Uo@LTEUIfrq!eWv zN>$R9DvpI}pxk0#TLpJ-A=9rjZ$B}BBtGA&-||ivYKD7GKc0SJlVVHFZP)gUZ)#b< z8fc6bwihm2s;wxcs>r`1yU@h;3d==epGu^*U)ds3!V3B!8cwe`-lvCzdk+=Bva+vY~}b+t=N+>1|uks zq+1?hDJxbfyt$<8`!eWI%Q&pDU&ni4zfE+<&}kPNln}mXVQX-YPN)+IUB^=6LAO3M zWzauMBjDqH^za#1uA{?@W+YuRs=C@mSW#O~(>-C$6A}4#Ub-%Wu_GgLq>=e`!eH_B zfbHfVMz6TMjiuSREOrl;`AzKhBN%vi zl~c)NSlTIEoEP$**5J|y40A$|M^i20+E=I{Hh@w+@Mm(+$fIp_`hl=2*od0YepD8} zKzA`jv1l{~4pJ(2EmtG^$}meA?<^e-VZAKdbsdr31rWW`!CyPtn%^5i6aIR8SKVztCHF{ejUiC*r#NFX+k==gEzfqutQvG4-7zi0fXu9i9q{aG+V{D zTR2=^ky;-Eae5@akG6N`=q<}9)dq~~;&m0Pj^3Hc`zJNN8a%vdK&Q_Iu>9ImkY#aHSDl9WGW8Swqe2O`Tod zo0-^QJiT&wYmEU+l2?YuM1Vk&bd=#`V6yL9b`SJAm&&f^ex>#c4>(egA_`+ufKbfk zjd8}``6;}~)+Jz7p_o02{`krsUxjjSK$>&(HbrZuVqYI+I3H#(B4A_kJTo~JE4}PfkJ0gpRvTri&fb1m6+(H z!^}~Stoc^vLp^}dT7xhVc{>uQ8+u@O>8X1}jca#_ zLm`Fx>S zf31lp>1}6W+t8zM-Gu=!h%Qx;Q5tH+dm(?Yh)y$D%sT2CKQe=*iH-{+yJlPU@MdK8mwrOK=8M_+Mx%QnO6h|M~|6miKuFRE}gKGFv5 zQ0p({W_gr}7Iu~{pYr{(d~cZw3?{w4SW`^cKz8+vUY+Ti7E{&R-p$YoyhWL^WljT$ z+3ot8`GsEejuT4LMjMd2&p_c1BxYujKayXCi5$de*`oDAGNR8q1t|p9!_c6$$Fn5I?rn&X|yA?uYf`px9ednHID2HitX;HwVWo+*o z_%opGAcUsAo)zf!K}vfo$MNMQ9QbEkD;opCcLvx-PK?;chhKDbTngYW>=;`M-sx$+ps1NQu(g z$7V;s(I9cTN@^$fo4m`WLwsd9dGf7@c`_3FgE(Ekreo0RkQ$2FsR~P3IsEwqjvr&X zKXpD#h%tY@=ZpOZQf)n#7!!D!AxZpuFiql7vTpcX14RejrpKPiFAf}IoT}N(G^fE) zh@g6HORbwm8i0*3>c}`*a#zy@?KbN`G~XY~Zw;k>lXp97Dua0rASwbm3t|f*q)6LN zKO^vV=M8Gj3Iy2w)L0rZ`_aVxC95RW90d(F{2g)iqkb%^Zmd%ZGK$;O^}M5!KX#TR zs(D3|E~kV&LfOjgJbFmMYcU_Wsu(x_4aAqmzVxZFe#^vMCmqY^_=GEaU?wDC;$*0) zBIGn<5xeY6#Ty1(5M5XF*c?ilQ`z#mOQdSiBz^ecC1cMOdF6M$g+o9Q)5zZ)XmS8M zBID(*kJDFBQP=nu-pd_nxagm#=%!rkyV+Nc#$I%6&++A2m3x9$_+_U3h%0#Uq&HeZ z3u;=?J17s!VyYT{_dEUI+)g6q5s&D(}T6jg;(SQe$0K>XrX{CwjIuy0Q zezFRlyU3kSGP=O?>#>G%3bvR@(d7@ADCQOmFn{>>T>$Y>LtgL;&ZEGK?PeX)whC%> z^IjLxH_zb1r$M z9;dw?lbzZ$m7v9xJ|PN7GzX760j~_i&;2d&X(LqDcx-%3=an0?x1-ezkbE^UFgD?u zlE{Y1!nA9z%S_wIcx(N;OL~ZGX!Do(){Wg_qt^`vv$pv!i`QK!l z@vqc70?1{!!qJLrBRG*q;lE=s6(Z59l(})d8zJL|N18t_LX&{y+8JsjM);L(8w40R zKQ>pQpDyY+bX!?;L|RiKVzZV3D(GyeWwod480xSxA)FeL0ttto31?|xP>EjYIBDcK zJRw{1N$+OIpvnaY2N6&D6s0Q^;=>^K~ zo^b|Np?vUGgpOqXy#2OKJHYhkgYB}`>r(_v9oU*$YWm^w50T5HunnmZh{~YTgzUhM z&Vkx*!ujUi6m8bQsoQlibpmIm8#Y_9Jf*ty0qIj@Bh-@dZLc=3Z3<3Zv+ePe`dy2g zrQKk4>G{@IQQoXD%IYEeO>*2XqDxB`Y&_Zz7XjI5WC}9)KI9B9Tugs!$TVgj^tMqE zYhzIGgq?P^@W-`0I7oA+>=`AT3uPHg;;FFS5qKy)-BhZ2cpghCYKZP*>e3h|kaPWu z<~Ni3MYy6&6jB*K@{XYo3N76CFB+%o1BKc$CN?4s5%*07uoJZlXGv_4K6NH>CX{kg z22~z-Pw_|pxmP2tYirPQPeU74|B6`}PTGzrj%zlt8SOcgjVTrN5^Upd_$Ja>GT&$6 zVTr=7eZ(YoM6;Hw2P7Hlq#;twwlchivm!aP)h@J{)!$w17>su+jkhqDTk)C79$q+V zkg8;Ix_BgkV6Mqrw+(^BY1AfHrz`J2=@J{D?2?UAH943t#J#3 z#z;MDxO`w*DgmT^)p<)W+Q}uIw%qw4QGcl#yb;u9kBldG`NgVu+qHC1d#~7-iA&DK z$3S{&tLuW5K-Dha6c65wF@|U8C6f>tYhYECfPO8ML8)6dp*Xl&j8)1&HSaUf4@aatF*N`Py_W`V zQh#8Uk*hN;pH0c&f2mobS!~isSQ>y{)qT0m{XqJ6rx#`v|hi4I|I4>7MY)&Lz%8iF*wUZXh* z1q|JP&LvZ#k-WveUm}a^4P!;jIX?n^vpG*srFgu;XIF+dz*%F#;ffg|hl}nlm1`n@ zoA~u9%=k*jNz>1=cM%QZn1gX~U?;4CsyURO+nfNdH;I_a%LIko*3_v5ZXDxp&a(;< zkKrbh%nc-y5$Vk}En!*`M1s>;RCZoCka-1>-Xx=9KdeZ3Q-}E>@8X9Ao7qCY$!U~%cS-nyvttUh&l<`|nAAoY}zYR=|LLMoe;3*r>keZYyXsq?JF3KoAXU3gCn2c4lO~o`QhS{zM1$J!tB%_QA8W@6TlsS%2V~lX+L= zE}f(|cKC6tPS9G!P4?ZUD--+EEwr!-8vSr4ijtU|<&7$4^!t3;GD`v8ln|EMPeH-5 zqFNg8oH~&q>eQD=QJCR5WQlfMvUPS4Wt|>jhDyz#uwXYkI$}{5(EC4_O1PS+z_x)s zs#B8+P3RK!jnmlD8#5U$`-t-;fcoHcGf7_g5;hm9!`Z+v z8MipPup0NKvnjFPQ3#hzi_*p&KelCTR)A0dW((U3c*K8@$-Ef&WJfO7Sx77$qKZL* z{uvKs{(4un(nY<=vMSclR^~cJTjgNXEp``&={CDJSFRe*RA)p5*Eocgy}08hbLqlf z`Tg+;ycfE$-{L+84JT$(_9Tq8Wr!5b&D7K~p)+g~Vw`4fVD?v8dz(WR z`WP8>p<-jmfmj90Z~A>ad0!Huee(pzyopN27PDa=Nrp70%wRSh!F{!mQPHnt6 zRaOa^53ab}!-*7%;JF@>P<^Q7md!qirpNY6Na1%UlhpOmi|oCvv2r>$vmL)$NO8U< zAFkdJd5$XzWk`MIv0e_daKun43y_u_Reyq}&Y%Q-q`lEPS)bI2D$Su~Uvx<^@h!5M zn3VgCympZyW(0xX;yV~8W_ZPeLrIE!P+DKr#CEN~D{YFsacBM6UsOT#@}mj5OvlPW z#*Cn}79$;pg@_h}J0Rvah`Ij>VsZr8nkkXzzJEPV^9-47F-bIXEzw39zP(JchwP^9 zk_rUSxJ8zS3x|?{Qn8QNceUR?gWQm_z z!Sm=NYQ%3AA=URAP&WxMyVbl7d*5|kHyKCK@h6B^HMnA6CngHJndYwNK#&^xbE?UB3@fD~&I)=kNBGH`MwH z?dBuD`NNW?vBLuv)$bOWSvP^K(r3l`l+gGwNNqIbw7{){%3T?kM|Un^wQRpJUf8|% zowYeeq+3&}!u0)k=i579w|QKrlCAq&%<`^rL5*DlHsqqDpoQ%z+w*HCSd-^ON^Y0y z205L>m7=6*i!b!zplC(;vbmsm{tBP!ZC@?aswp^ShAkz){?xB@uie!8`d+KZCARY$ z>MSfj7&g+Cy*-zui<2zCuGrxXUw_q2i6BXyygk%}!*JHtNY1JCLODAO2SOI@dv7A3 zHb`Fzqc*VzeE+1)XY&Cfp%q=XUa?@hZD6orupIJ7$?t9o$1eWZ?FV3TjP6EkA#cG< zSFB!*)qzX&e7)H244@Etc12cIxxv2|!R;KC#(8!42&Xx~+5PuLM<9>}K=aS#M_wQw z&;Py@38n!gy)cEh4NiRvUzhq8A%-6wRL7o%;0I3+0fBhX;%*e?h& z4F7}Rc#>XbATa(%Am~$UlwT3Z|G)o4z9QI*fq8f#H2)kQKx0pX z@y|1m4+I8){*3{kPt^Q{0r`0#Nqb)r_+elW=(!aD5CC|NfuOvQr)2%}_&?qN0A48H zGYkZQ{FBsw%Yk^HPf7h3#tY>I{)54u(El;a!S20;0MJb#@84B+Gcx05G+L43~we8QdtpUVNE{E(!W z90Y!0J}B^6SU@2EQ|_K?KtTLFe_=`OB?vEI{7fqDO~IxsKjFF76{m_KPP7lEGx4EeuU zf$;yW0RjS&Wb*#e;DbI3`iXgdp1&|2Fdt7+>3=k!JkOYa(tz^*h4DZ@;3T~Kr~Y_) zllK`3AOQdK>^`;F6RXeUc=`V?y#N65J|`8#3k5x^J|KVx1pdd~zxo6GRFluj>M5I0 zzGnvpf*}yTXHK5V`L84afqc-v34A*5e+5JJPk#WONZ|i3@PA=Ed{9V|X~9z-czO7q zarC4Cdd?dF$^+%)PwM@T1{m^}Jzg;MFAN0a0VHu0{^R3`&42UzeGY|*lX#qGVBImXjx9$tPP3`RyNC25TR E2Y^R{LI3~& delta 16629 zcma*O1ymc{vNnvnTXAIcc;Z&in|6Y6n7|Apjd%Iad(Oqr$CF97Kh^QKkvEU z{q8yRTkF4B3z9Y2`!)H9(5;t}lP}7qU$BuI!8z>LpD7`JLHAn_|KP~8LLd3e(sCu z_<1m63M;-er|G!xa(-N&0#z);lsQiN_Y4@{cHGCv!HoC4_X;k7einK*%P-4<-ntr6 zdG7&tMdQspXRnQY3-5N*$^9X$y8>rZNEU8#v;Gtf21cd8PF$e*UfY@cseXgtM?NEU zhW$Bgzw_ErV!f@MDcKjqsxB!d4ZaJ=aD}JuVa!Ht?@K0l1}9OSbu;eBnL`H)ov2Wk zU#0L{`Mto{_Sp7F6RuiG?h#)#&tT^9_!h7EU@rY)Yf%1GS;G9C&(fQq z{M?&abbi$Ym5D=#iLE7{{)Erh$F*J}y~kG5i#Ioleu2h$Rhv(->o4N?4EdI(?m51j zgjMIWtFYE0V-u!fNicEZ5wi&vqc@m+t9XIl;6$o}!kU}W!M-HE@N9ZLE3(fILqFL!V7)0gIlWn!lw@v3CYcP zd{-{1(|E3MPC3=Y)2q6JL(^9}nmH3+9z-NR$oLC9?3Q$Abf`kff}ENk;=+zv8q_VQS;@r)O?sNIoHiBt-+LophNH{-@?rqP}kki|jV>o(l znl$GbL?zPsyJ2yO^1-nw&PSQBFLAWe51su_zYmCny)y~0O5N7GuyoUfaEq?Qqw{2= zU%aKixaC*azYN8hStX-9)d=d*9zHu)EsDkrvh+mjB$*sh34BCCogL&rs%EX4L*Ynp zF0O*aq6=4_oE5IOfKVHKhZb>^O|Ne$wRWy$0{uppLLLy*xvn&2gg9V9G<*J&E0mN1 z6`!*mmA|E@7Fvo>9e8|wXYcIOPZl}ssy>^opCQ}EdxvIZlVW#LGKZY6*xW_PG;>bn z-ei!h0KeA>W+9?yf{f$F>OxC^*fih zt+})n&})XGNfYi|J_j8J7mSS%p3gafl>Bnd!4%S?0}toKdrU4;)Gbf9@UY{`Xpc;xie4VCyW7OE=G_N3BuW$ ze<4h0i}-HG1^tvB?+cRGP$`Pdz3yu(x<8v6X+4*bVv)q~(t(k%N6xd6jP|{J`9@3O2bW(@>swCuX7EOP9!ED~iX3h2tOJE1N=wFMJEr zXvk%7vN|W{$du-#7`IOzKGuK~^+bejeW&Wb&B)!F1gUQN&jssHt1)5TX#Vlzg7@U` zstmx0iXK3CYLj&s6&=FSuVcfK1D5lB{uOwc#xmrUXc6adrX*i|GmQ4CH*~gW=#5?$ zKSEGA!^me;6G6Bn0&B{GpG~rm$MGs!$HU+sOoPQpS8-9U{`+OUEpG=5Xz4p=O8w6aZ_(z~|@6j;!ZlIHKFXO(}bbG+c}b zzmr*C5ar!(;|zZ3Af}oGuM$|2)}(hvzJKfb+TJUBcc~@(=!4d`F}az!&CSdK7dh8Y zF$TLtpu00Vc+)rj?8ynx9}8DWTj<(t6^xV8+#5ONV7axrT~LPx8v20AP2lQ>Mg zX(q&%{YW7C(W>39ts`!#SF17E13*WN;xLbEU!JC-oz0JQ_|wCQadwrRt(1Jty-GNU ztEY!U#qd`uO^tAF!CLQ{r<@^#RRk5PT@?na8j)ac6L~%I1Kpr+RR!mcOvRyfHm`M6 z3+flUlWnOQv0sVDL z)P1X+Agn!x4D9^+1N$4PV~F7Dz|>NZR`6Wa^!_{+k&B&7aNjL_UVTLaS)_-G6#HJ6 zbfxwmnvbopx&r$J0Mol879)a{aTz<B2{}?*^sHW;+3^6 zG74-W8s#Yd^25OtJkM zA$9zTRpj{Ayh;CickCAf!TxwTSfpPgf!Oz1kJk~xYF4A0PJCQ*Wy!v>*+Y2Z^GKBn zHE2aQ^J7=N>w|XexwU-5Va0u}VYB$4^XzdyH@`a6Hay|=@I=1yTRMR*xCY*tpaz`N zH&wANrLKHBbbNdyUlQVSzB5PEDl*Z8wckkUzv4cs1lM#-G#x0voYtRGhQaHi7WI^v zRaBR<<84SGzT#DrLD^jGNgrjjU)!eiLN2!(RozEB^dN!_QGT3(4?z65*;y%(Y6iAd z4s$}b@R`Q$A(~<9n;z=$lz^i6pWZCU7Wo6V%7=#=^+fJ$WhA8;0cKHZSY2#D8W*B|TtG4d`jRAJv za1no&2B&v+L8MIR6oYTMeUd zm0%b%=E{uVe$VeensWIu)(;ALSRXk|ovT@$`COgpIjy9(;wx?G^ihtuZ7s`Cr>7aG z71l?7p-$rbCbn;e1dhN6M1I%=jn<7%h2w4Y?M4mQfHpMZxYF-*Xb>?T=fU4X=*U0| zpr~?LI?gWaYQQ({WKtJP*ZL(mSM=i<1esM6{z}QC+5uA9_F6#l?hj6`gjM7Mwb8kz z`47WUEK(c`c*%y01slnRIhY7WO*rdvg!`56nbGdHOJms`)o@{=ENkY@A26t2ITISv zH7CYNiJTQuXX|bY9hXxNa^i0*hmn`u$Foy$ddYiGYOYRhbVn&1rr3V%i|DlmhKnbp za4IPB7nOlEO0t)R)+JdO(mu)XQVg2OlYc4dRyku^lHE(rH5PC3HBWIP`ErBQ<-o!n zb66TB=ch{OU;7%?tN(#+CE>b6SOKSkV73nlu18iTBPc_nhQw+fJL98SgWoG&%}1z z#L%S%bQB^IJE%VDJj*E-2>iWW&US+nKWV+5ROmZ7o>Df9S-%m=4*f=9`KG#Gt!#DQ z+aTzARoAgv#70ZfEwA=KKG1#@BR|EP-JfT&DYO+l8sAw$6?K?#%Yw$`$OYo>FukAe zqt^H&)vfYPXz9wwxNPKW+z>_L>qZL{!ft$cD;)wk5AqKaH7+3L9Ov>h4xFTwukW+y zo9*@nve>X-jI|10pE_24TWRxwSCd!A#uv84ZP~Jrd2P2+e$QBl^MzH$a3pD#=PkJu zuYRizO)<9-k=qma7>}XO+eZ<-f**qO>h8UarUU==p@ozxCA8!a?)VZ=L`m$jv=^bF zgc?;cnI~Fd9{6O~3y%_|Cf<;b9A!YSXnX<@-Q}yFuN% z(WE)IPesx>_Py1Ad~`)LJ!`TH8$Xbt2eYg%dqPUOf!n#tqt1`qS^LH`e-rnva+dm9 zIPl0{Fgdht2N6~Q+rD_LC9};DL;Khe(Fucbv(&TR1VsM9>GxXKi@4J%mgFBRM*l^+ zZr-3IEZpp=9beEAtiAH{w@%#j)ox!jt5zjlDr=x6KGV_hIDvHTeh6;mYtZC*>8ID> zRVQ@rvsBuourZd2`E2!vfVhp^hVvNJTRH=E!nCWz)1w7`6W}Yxd54e&LwWzWbeSI5 z?YtFMz^g+~DgE;-Nn~1Oe97~oGIpHOqXiJOV($)A5W9I;|k38!)KOG`J)+K~K{@}jah~Z5h zlBJIj^zAJ7;P`VM`{S1gUzGk?5C`@GZ0o(cG#Um?x#KUdZs+FN<679p+|L*k_^rsS zw$E1W?c%2VCf^*IBS=c)i2TWLMQ;eOL4$jY>md!roa-n2~yHH##wLQghNDP z$mfAO4@1(Xumwq#mrqxBtzY88uNk1`k`D*sD%>mE6#@g#iK1IrR_()WZUXk(FTb~* z7c1(ho=Dxn@$yd66=?4mZ%Gyq!7AKdn)N#rq)dJ}$T~Esiqi>nF`ar`9L;P=<EW0+9AOiPDVa z=%PrZ6Z@Q~L<2cgD_)3lOnKM_4#uK<>P$5j)hU;>Yax|(HgJ>m-Wa-nDba@<<;oj{ zxT8HAKt?sK5WqNL;4o~W3bXk*vm9mWHg)nlz`E#rfIm~Ca2z<*tY~VH-8tALF`{_M2aJA>H00zD;%AB`(tCw4|Q;U&@Ai_v8`+=3twlB`VNQ9B^QW zf)WjV6>=;)$6yIbWfiSW9ru)};fp&R-ISBYmz}$Cu_y|3W#;l#XzWmwYca-PbaXzh z6JfxN^)V zLY~jrC-b4(vh|6@*)aVY4ZiA9lY)SE+O%xB>SMxiG9&msMS9>|pYB5$w)v49goaNp zKg!k2drw7f_>KPyv=VF@z|<2Hb)HJoOF6eX_{40 zwXC);1-+{yEE^)PGNC+dCM<9y{GB!;5X`W}jvyAu{8nd=vE&a469#knQb9+Ty#5~v zgAq~vn#sm*6Cp4zpJ)X4ughp=A$pt?;!4r8gen~^`HYa+Nsk|HgJRH3C$*nKDgg=W z^G!zD9b~BYQ_vlM&Wpi>kug|+=00`4h>RJB;eIEvMC8s3nl*MSWcPWVuP&^9k#G*l zU=Vy+O_$>?p4YXBCcA~r73bvK^h)M*{EpFvx>F(iXW#)+S^vc=X9s>vf z(gJ9mQJ-Fd`GBB|ZxZl2FhF|>1qg*;5J*6(kb<@ymV(l%be?3Xlg%=+4s=-UysT;4!R5o}c5|jt zX=Ily#dnd|h*GyWPB-yM-6l0SKKim_Bl&Xr*Hx~nwho?6YTsAta+lSvu!H0j#ZW>^z$iQKn$&#%e$L7tjb_%V*E%V%jW*^Qe9?E!~PEzz<)5!-Zpgz4tQhB3t%V zX0&Ycs`RZEbOs_Xr&H-$I~X(R4D%d< zi$Yl&;tqPtc2?mj{1@_fjtyGXTLsfBcGD;&UT+u%JSkmay4`LwDFc`raVKR2^3|36 zU&-)AHdq@|j{m4~y97*}+P11>X!u)kxWCT3EHsauSqz#bt{Rb+Z^ zuSFcl42RW%r0uH*Y1Zq7tDVREqkaW@>uFi3SN6T+g2Gz4zwUvSUVE3eeTIE16Qz`^ zLz#k@y*s}KcBGR*Q%%lP(sdJ@yhn@tl#K6-%SIC=TYG@+B`bSEH~lm&@kwXmrR*{VUDYLT&aXIBWIV!7*{JQ zm$W)155X7@*z}}}T-KVmA|$KwbP26PjlCMEgT?Cl7Td@0BBc=NjYKg@11Nn+V-?ZL z5htegxL69j8`JMBA_?k5G(Iar>8M zAHmX2(*Z*f#9uJAQ=~YPacJKUz^T4#j*u1S35E&DWpp{gS%s!WASS|PaKOJw!$pRp z==dR3z}r-gDiMUj$y?rn+M{M`dibKkA1d2B3?L;Vkzgd%VR$>L_Nf?;jeO(Pua}Ea zVWFjkvS!=TLrs+suW--ncK!1eDMUvUPmH%z-%9F&H+=@a#sM=SzBRp+EV36$RUE({ z+#g|9*=i^I(WO5%cCH=Dga+ax_3s+agjq#+YOX0`cw$Ibb4ovv8l}CrEGXpN#^8|I z@$DV=&|fg=GYi46n}~Xg5OC5@K-Zkz{ml+P^p&Xw6-&OlDY{)WQblZQAAEgiF+{m+ zEn_!$xv`RpJ3c%N#vbe!JgJ120(S!EG_48ies3|qD9zrkUPQP3GLGf#!XBKAFT%Ea z`1(&v>ha`2wEhpdUC3t3@I%r}W-=g!jwUr~0}eO5ED38Le49zyLWofqR^P_& znbWn9b;|B^_57C6nE5P_)>`s1$2B|jPIL=O7u}fi4zEe(f~#z}7_mLk-oBZ`0UZj4 z8Fm{j`D!;)SSjO@Qkp7U9h^HCYTqYf=cIg@cURI7^A=gqj3jPnSw@jBA0Wefw9oo z+KTdru?&xIm;=f{e3@YgP2ypK7~@Yp7~MmVMckw&*ReWF#_1OsT>d_L)CPV*HmDbD zCC}R%jo2max4-bA49bPF#1B~NOpsvxBQ;K2&?jx4H-19hTpPy+KUSxgL3i*}pK^nv zn%{d|v(oQ~w35^v1=#+ImX$Wo#h=-xVlirOx(^+(JW#y5`GOA9Ul=|ujm}CGf;m%t zvfGz+-hKMArCoW%%14ZUbilQ_?V|YP)!Q3QY{i-qM=%+v;Wc{7K(eV``8lCb4~alYg0n+eQn>Mi!0O@V?Q@X0jm zZh$NkKn6X{zK+Ay{G3fF~}G?CmUKS&=;tbswMe|WNX04I-} zZ~3%)@-tO%78AqFjOxpLViY{++O#^V3U#b>d1plzy$kcJ-=No*?7(?O%Q&&P$_JHw zB|u|>l0-d{>s#37rwUB9G{d-LpFXt(no^j)O?qt{V$VRS#4l-Z_f3fbRef&ys37e9 zUK(NEz=z86-pE7Sq9dpJW^;lUS4^M$U(px%c?fQgHBotxrL*xOXUi!oWD-O&X_>>( z6TSex5#Cb}{s8Eo9&7LY-i<9ww)<96?j?R35m#q87uqZeeVlQQC>9vCv1~L4V zpx57*HO1!3(E`}GaeIUmxXtOW6e^6iC69cDkn8|+qS0yo!Fc6so*#-rQext*qnU{n zS15w(Uo*FGN@`EQG*=94V#v3`qxa!nvr#5|P&=bTz7@eMEgupho3Iu*hlJwp%YThU zUE(DBv_nl<<~x#>BFMr#6mL+B7urREF4D2%><9uL0OM8G`_=qo=1W2bB)!~WhRpq8>BviZc zxs|sOyjNq6d1Rfq>z}OBxRY9$W$n6`DEy_GRJ$+bI*t&r;>~){3H((gDT6S3ZsWm; z!^n8YRW6no40o0|4gRwVUGPwXhp$iAM6E}OEO-(#_6XYXzRCk4ZuyL3!e6T8G$uzt&!PbYl6suNabp0O>Ba`#RHZvr&-k!8};Jj$Emuw8kN4Ed!*=J zrzBb`znuw)iSh{kpgp@1$Y*zPKcrO03}X0P@dYv7)f`tM@Z;35pY1uYcY<=RbAOxzxf(BPG*}<}<6o<#Ll%>_$}bkl{V&fjf^=6K z75mux4>2379*{69dz0PLHF@#vX^0pN&%P3P^T0&A>^{CqdLu`GHRAm8&ar3HeS?Dg znn(*qGtvCsFutfeejCx`oQ(YNM)ak%&>*+GT710ar0=p=+fYXFo5(@!8F|&ODa*Mu z5ul%Ourubs*6lUM4WGqdavBeQHV0fVb-4zGyNVVo(U}oA@v0=w^-<6X1(#YP%qPg* zEt&C4NLloCQG89ZWgo$wocVs}eu0XXpJ+eqVp(UAVL;>H3MukYy-`eG>^^~XG$Nr{ z^yC!^$F;on`5Lpsowdfj-2%Uu0mu#G6O!u*CetE}IAFe@HY74t`Ic$gMIq)(a*%V0 zXh<&EMc|hUrkJGFU-Gm&$j7cl_@^c4qMbbweq8veP8B@AhBu?`Dn0hqA5&!G*KTcL z*LBl_m%lyelW2cm{%)6IwZ{}*>3ipWrZF7#V&{l$&Rp7;(Wr9Y5aLj>pOQ!0ycuqt zkS4~Bevb^fBe6Qbo;Uu%u~@oq;<}HjO+)%Mi^!x}I@R3Oz1=JuS9T!tb1maAwvTMc z2ld;X1ZGunr>9RfzG{!I`wJ*;)y-xl!vt>d4mjWRr$rmhh1ZsAt*yJ@jC;TbB}OEg zqJy;Ij=Xb1`=_0ev8gKehMT5ZQ#%Vkp}AejP+NshMTL(K=!)o%==y*Imx4oO=35!R zYLYrkOX{gW7NDAfiUsZ!Qj96yJ6_eTDh4KO24DLR_zHNZvSl;Z%eTKceN@3AdIdNN zjl+pWUdFI#)vf?_fU}glvI#U|<-0Uz)eb9$69_k4a6DYPOt?J3bn#GIQ!5r7UY}op ze2WK9pqkn!JCEdbyc}2;aWO8FT%Q-M&=80`(*;B9Ddb4cxYU5B!U75W-@pHX8TcIV zgc*FA@Eou~{La1iuW$~nJHJz^9WF~ycEeLLgb;S)z|*{z%U4kNCaL*BJ`>|)O{-&W z{?zYE-T(!G`g_h!Lu>ly^k3Oy!ck+Cu#v-*Q@K3Y7XQSGsNX5;gJWnW#5kt9#jo}{ z$UTXAJiEf?%y`}F+S9G``YS$mx;bHqY4L1!VQB*F>ak4t1p+dR4E?qrLnV+e4{xFJW=12i4?| zUv%7tfF2+Eemz@G4))zYeQ~*t(!Hrdc90_o?eM4jsq5ZN?B!X}{$tkVozvMv_|H5( zwz>EhxG1I2!LeCK!_z)Or}wj`@AHwml|8TaV822>3)*jH8pn^HzMpXax^>N@>TJDp zWI69RY2f|l)Dp{W1GX3X^N6{#d;-T{=uw#HMB{WLFroTzL{PL6H)?9}qkGUDTMD8- zCI9r>_p=3D4GbvYG(>WV&P@iYdl;VO;}01j=j5%E`Wdv|x5MLJTg@iN5nUa7&Hk_9 zoMCs^pZ)sA)*Act+I!*w*BvV1Y=_R*)kE`P5-)_&SifYOzxP{wx&X39H^J7}+cvyY zKI&fs&)$9CoD3(Nc76G`};8Sz7fmd{ioqX1@h11+y~}c-AsUgZsVwTRWUg{I%~KG{UBZ6XG<2IKgB!;^>7ZWaFxgSVI$4q}EA2pY(e(7X=n!T) zq5N$oJYc$|H{Hisb0n>bN|HAPpKfU3Mb$y1SKcZATLs^OQzQ@`bK-~ihF8DN)<YPI z_;@q2T1RKNkRQIae1~*f3q)g+gU-OlY$2_Hp?C9FqZffn?U?^Ah&+A9fO#YXxvca;hU-OX@@&0*LWpB>E{ zh60_E%$5psL)0xYM@VUrQafMC3|KE|OWtHCSk3Gky4V|HZjK7ss?_8Bc!Qf*xzCP@ zS#~77Awhe(&gBR7+2vjWaWToeX*a4=%*a(Hpu(dPTUqB%{cGneR3J6q?~4MTb5cQ^ z4Vj%UcM4og`bEAf_^GMCVmF5wn17%;A$pTE#DJJsxcllW}a7E{Sai}osaW=Y+#w79sExs7~=KRDx4C8L9HHK)9$wyhi3?5C!gN|dJQ zwj~7_K26lk^!?~nwximnq%kT4Q-B>#opT^jA-eG#s17Hwrs-A-As+w$Ic4` ztI2hN364$cIi94tPw(lSU^_BU1UL)z-K^^1kq~GhJ%coB`iYpP8UTw~$O``r73HAs z)^JK~%TB89Z1CDLe~48MfsmjWbkb>GS#Ob4AJZa{4xM&f1^<4DR(A`SM$+c47b~MW zP!q{i#~KPXZGy24OuaJrqb_(e{oBeBL0g`(U>K0i%ejNMojBnPGm?yuc9U2-jrN?Z z7$Gdrq;bUbi(!u-rugL1>lfv3T)(5{%aFgXj?8Zq(dT)Bq%#NNlkn-r={|Io%d+hs zusQ&AXOA2rh@ihS#iHsq*K5cMHzZx@*ISe#P@{ss=K9?GTOljKBbYXxRW_moll3IG z&w`Wfi$UDG#ItwsFn2Un{;P54EZtVJPBF(rn!*(0mQ$!8Mp}Z&X`dcqM3*DgkFgE1 z&t}q|iKdd&A5gfln)?Qqgk@Nu+4Mr%9V4vXRMC* z4U9J>@eCz$!|>ga9snD71p&HK8s>KRA;mQSru?&UJ*LM`IJ`@bf?je98 zaGtle^t-h8T(T@BHf!Hi3(B_$%A2lrzOR#hqzp;aMvW5ckAD5ln55ucP%FQc z`)$~NhPn{Qjzr6GMM>r$$aM4eN5M(G7~=HH?hn>4U%_e!iepAqABsJ#`$t751s%vj z>JD;`P-5w9uLK2cQ(Sa^+q>K{Y-9ZjWo`Xp^)k{*IR7_5rKx;-XTpjp3^TWelgfEm zBXy+M(n?~5L9}&*V|?6G16{?wo9(BJy4<3^79KI&WluPrguXT(^(k;$IY&IS%7rar z5)v>PGYU(ds|GJau9(@OdO$X;Olj zhlV_jDsF;w4l3`{ltZ7s^;@`{nyc6@$hI^>JEPc%y=Cm-fzz)4Obqj<9_6Em=!Pdk8^X$dEf zpA|lyL1|cM<~e3=94?~*h+mB(=5^5$&e3%Gr91blORn$|9-~WTB6+gEf%GvOx^e@c zX0QqCu0t5a@rnO%H9_I_Czz%0ut%Bd2ua$ct%`PH8HztWuZz0lAQyi2l}Illmw0Z4 z!V~6|_>kcJruFT{Z=J0oowMu%EjKrCz_MGYksW4i1mzYj(@-;!W_%z$P^}Bn!s?(V zkJhmoK8`M0iFJZ57OwwYb+(TX%?AAECe=NkXW>@uiq4YIvW5S&qR=;@{?iJnBusJM z#n|Z9Lgw^S!W+Zp0U0K)Z*@zhABW5R=lNg~Y@;k~8{&op?n`l0)$kdj%k&uyn|w>C z-*&V`;Y@Dqi7JzqJgpD>dZP@nUC#Y>4_lBuAAXQAm_Wqf7o^9*=o0LJpaEck z`70HC@M6XucW539O1X1)_4xK_!fi4voN`o^i3r!6Jo0F0pKc4Tr|stS<>}l-p=0;+ zl`|>x?h@Dw=Vi(f%5YV11lYXrLK2VRORf2^kzs}^|11Z#*u*{BF_~~jy6c6I`o)6|7Y(J%kTzmA|6`?a|PKHc^i*e zF*nSBM-3J0I*j4smgHwMX=kKHUYci`OrGOAU6G|^g#^3JKQt|gtO6&A!5c6Q#%i^JF-2))j2rH1G>+B~nFx1Cvp%KW!5 zdf#>&8bE@l;S{Z@+)#yWa-1IvRgfzPxL(b_8o3??t3V_oM=Uu7a}+Z^=-`_tilINWl$Xz z786ho0>*s)okeN7#!?pBJw!H`)3rh^`?7phqbV#`z+RU_ue{%b%^;FHKRtnGuWAhg zU=Smdxsr}we{7#_uxU+YG|B9~mQVgY^}C1E*uvArC9SW4kIb{LNoP+Pdv^HHVt3Q1 zJj`0!XU&eeSYuJ%25Sv4!w}|ns?iWWBhU+Bu3CVv?S0x*eSzAWx$!H=-NATb_O#XX zV8ULwvYrz1=nzgxORZkkk^4&$xM91%tQ-&(Jl62y`F~ zv?XsKX{#d)W-q+i9H&0BD-M{_8ur24yR;4r2T;hKsoQq(6p*7TsFAx<84-)~OJeWk z7x;*d9XAt#zR)(+6rM!e8;P+FiPX1Kqey%Hc$##)>0dq@7O}Zvi8vZWC?yaOe!}KOf$u2aOh;}RI0Gj{B%Y1>qyNx>C zE|-hF);fK%cq3-hE&K}J3x^3Adywj!K@b6*J2JF&dcN>88=dsIhjV);7)CuC0$2Wq zvs=|lNAJ!fiqg>6yQ24_{AMj`tqD-Ba``g^r1h1=Jgz=WVht>D|*JRj`lptPh_J1eZZqHfv|w`(_4jp}%~dx4~mXjaLA zDDzh8+ITZX5m^;UeSTRTv-*9w)PjgdiPLYTFGRgw=2fP@No=b+@y=stWkK3wqSr4$ z{d3AcVR;*kxqXy3j$c-BU_S4AeEy}oM~Lc2*Noe@NlchYU^BC!F9Qx!@*7Nq+`D~g zvA`c_8P**OFa3zz3LedvmRX0IUl9^l()oDAeAIU>7s`9vuHEtR9b7@HkUU{m)Z&XG zcz=HR`=FxM5t&5m;O}#xpq#J@5it_Wy%=`A;6wZC3o406lB6T1J2Pu8sSu!KY?leB zCcv3Y;}#9pKWIU)kN(kFCwqK(=>95wlN#5yEPwOIiR{nubQ;$if`>{f}0*)cuuN? znVQf(9tbRH;Gs304K!ilhOCPCRSKP##OyBVGVsIh;@ffQ_nB#ALsVE<4it0bl5XC! zDt;BhRa%f200aYg|9eG7e=&lSI3EBCq5X#x z0Id@(#y`(M2rn-P^q)2Wlo$H94ZzP2$#5@05U}P0LY|=jpilwOGaHak00iKDjtm9y z3H+xG$Oi_2pREHv1)f1yjX((F1B3r_IRGjk00sP~4amm}<$n$f06yvD**Y+Q5BPMc z=by*_5CGu+=c3QQ+n!j0g8!8c?B5phf&}=VIR-$%Q2xJThXSF`0r_}=&jJKM`JND; zuLB71{yUEu^dAwpVEhp9vj~Ae2pIA#yQg4ydHJ3Lf+2vvY!F`XGaC>n01@~b4+Qxq zktY)VhpvAl^Y0PKrrO5ws>l@r+$8h#|MH4Jd@=U z9#G()%>ScuAOSG=ncjc^fB^7W!axuh41DGU0OkLyN|A_l(@Bw-GGG0{v;{(k9cT`W^{yb7%UIB21|G#!X0MEqz z3?STG|vV2|E*5{q6qq=!M_^pX(m4_-P4GAI+^|x?`g_B zP3Pw}pa8qTU&bfFJ*Vp_J|J%fOU=_iZb2YWkStJEMnD!M1A_2N@j|5lPsf|Aq<|#o oi55vw;s4(iMi`=^815csZXP~vR@N9#vH 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. + Unfortunately, inference fails for some examples regardless of parameters setting. We discuss them in the next section. @@ -1376,10 +1382,16 @@ with the option . Additionally, we can relax the constraint on the processed portion of the matrix, coming from the restriction on the matrix size intended in the original source of the - example. In - , the whole matrix is processed and the - inferred type is most general, under the default settings -- no need to - pass any options to InvarGenT. + FFT examples. In , the whole matrix is + processed and the inferred type is most general, under the default settings + -- no need to pass any options to InvarGenT. The reason + is too difficult for InvarGenT is that + the nesting interferes with the propagation of use-site constraints to the + postcondition of the nested definition (the inside + ). Inference works for + , because the assertion + provides the required information to infer the invariants + directly. <\initial> diff --git a/examples/liquid_gauss_harder.gadt b/examples/liquid_gauss_harder.gadt index 906f269..03210ed 100644 --- a/examples/liquid_gauss_harder.gadt +++ b/examples/liquid_gauss_harder.gadt @@ -88,7 +88,7 @@ let rowElim r s n i = let gauss data = let n = matrix_dim1 data in - let rec rowMax i = + let rec rowMax = efunction i -> let x = fabs (matrix_get data i i) in let rec loop j x mx = eif j + 1 <= n then diff --git a/examples/liquid_gauss_harder_asserted.gadt b/examples/liquid_gauss_harder_asserted.gadt index d8ef87a..4d9ff98 100644 --- a/examples/liquid_gauss_harder_asserted.gadt +++ b/examples/liquid_gauss_harder_asserted.gadt @@ -87,12 +87,11 @@ let rowElim r s n i = let gauss data = let n = matrix_dim1 data in - assert num n + 1 <= matrix_dim2 data; - assert num matrix_dim2 data <= n + 1; - let rec rowMax i = + let rec rowMax = efunction i -> let x = fabs (matrix_get data i i) in let rec loop j x mx = + assert num mx + 1 <= n; eif j + 1 <= n then let y = fabs (matrix_get data j i) in eif (less x y) then loop (j+1) y j diff --git a/examples/liquid_gauss_harder_asserted.gadti.target b/examples/liquid_gauss_harder_asserted.gadti.target index caa45d5..2ece992 100644 --- a/examples/liquid_gauss_harder_asserted.gadti.target +++ b/examples/liquid_gauss_harder_asserted.gadti.target @@ -71,4 +71,4 @@ val rowElim : ∀i, j, k, n[0 ≤ n ∧ n + 1 ≤ i ∧ k ≤ i ∧ k ≤ j]. Array (Float, j) → Array (Float, i) → Num k → Num n → () -val gauss : ∀n[1 ≤ n]. Matrix (n, n + 1) → () +val gauss : ∀k, n[1 ≤ n ∧ n + 1 ≤ k]. Matrix (n, k) → () diff --git a/src/InvarGenTTest.ml b/src/InvarGenTTest.ml index 6b851ae..012312a 100644 --- a/src/InvarGenTTest.ml +++ b/src/InvarGenTTest.ml @@ -673,12 +673,11 @@ let tests = "InvarGenT" >::: [ test_case "liquid_gauss_asserted" ()); "liquid_gauss_harder_asserted" >:: (fun () -> - todo "FIXME"; skip_if !debug "debug"; test_case "liquid_gauss_harder_asserted" ()); "liquid_gauss_harder" >:: (fun () -> - todo "FIXME"; + todo "Too hard for current InvarGenT"; skip_if !debug "debug"; test_case "liquid_gauss_harder" ()); "liquid_fft_ffor" >::