From ddc44e16272952ab11efbbae4eb21b330be2682e Mon Sep 17 00:00:00 2001 From: lukstafi Date: Sat, 21 Dec 2013 20:16:58 +0100 Subject: [PATCH] Optionally, keep `assert false` clauses in exported code. Removed spurious `richer_answers` in tests. --- TODO.md | 2 -- doc/invargent-manual.pdf | Bin 126405 -> 127091 bytes doc/invargent-manual.tm | 10 ++++++++++ src/InvarGenT.ml | 2 ++ src/InvarGenTTest.ml | 6 +++--- src/OCaml.ml | 8 ++++++-- src/OCaml.mli | 3 +++ 7 files changed, 24 insertions(+), 7 deletions(-) diff --git a/TODO.md b/TODO.md index 0eb7a05..73b4af7 100644 --- a/TODO.md +++ b/TODO.md @@ -6,5 +6,3 @@ Place for TODOs/FIXMEs, especially if not expressed in other places. See README. * FIXME: `separate_subst` has a default argument `keep_uni=false`. Rethink for each use case if it is the correct argument. * TODO: more parsimonious use of parentheses in printing expressions and types. * TODO: 'Update' and 'verify' modes of inference: use an existing `.gadti` file to provide a type annotation on the toplevel `.gadt` expressions. In update mode, if typechecking fails, retry without type annotation. In verify mode, check that the resulting type matches the interface type from `.gadti` -- is not less general. In update mode, regenerate the `.gadti` file. -* FIXME: when checking discarded in term abduction, in iteration 0 (only?), check modulo renaming of alien sort variables. -* FIXME: missing "assert false" branches in exported code? diff --git a/doc/invargent-manual.pdf b/doc/invargent-manual.pdf index e2b309b9f1fa527c1f0856a6af2f3775cfceeebb..de035dfbf73ff8d68e85102e53027c7372a769e3 100644 GIT binary patch delta 17486 zcmajFWmH?;);0{qiWjH2L-8a)60}IM;>Fz^iWP_8UfiWvaVb*Vp}4yhFYa2Tz{`Ce zInSZr7~jsHBPmD$E+B1?iSLqhOnVmPe< zT@QZINpj`mJx?Pkl@o@|`!A(niRq9RzT%X6uqB^|`sSDZl0zcr-|men8=9{XT7866 zzKB(GMZ{{9aBz4xH5cx>aapM)5v{b`(x;a3-tBBZ{Wv}NA{YemdjRS&op*=t4~E0c z#d9Y))96JC=P!eLbT|xpD7_<072^>@Zx}OlR&;g$csS>M8F>ITJruNEZL`1b4%-fL z^R_7FTN2C|HX%d7DaFgLF3Ak5o!il^%ebM56J|eG4x3j|a|$P>x!i%2izYPK}JoVK+5k4sZ~)UTLHi~ z)c(==$3b=3GK6{M9-abdG>Heb!keZk1fM3IAPi9mf0~(imyk?(tGm;Y@8LROroJgD zdPKr(nKr?FCSEE(*47LN~G3ke(&ANcgoWxCdqy* zFULl{P?;it<*#gxgiD?Aa)rbXu-WK_x*s?$UOm$Br4Js%nnd5*-YG72Z!7g#_j*#L z*xCm%p&9bX&SH|z6ht6Yi5LimrVHI`CQ)vw+)yN;sbpPG+m@B=-Ryb@Y+{C(avS)z z`Gr*4%`D?HIgy3Ft?>UCRwa1!)8iO<#ceBK2X#IPD$;mtJJ4t@)atJVlRz^B@*5j{AYvYMzplUKXuoxEK!0R4aPPkVf208VNi>74 z;NVM*3NeG$%-~-${z8;_t(M96?SFQIT6g~rgD{sSc`nyTnaZWpW8 zvj|}_ik1)*Vuvk9VUEN!M7~vY`JEiF!HFuea(S=F(81p;9BpNR!P-0@S5dEl6>&=y z&9d+jeJm7Z#t|@Z9%nn-U3)I8G!w2$B)LRjM>6;#q VlN5frfnK8QYExX4dsTk- zTER}6C5kF={^E;!q|_;K_W~3`Mn8#as`R0NJrxamBNBE{NUF-R1l5=QAW?vB?4yv6 zcrkyLOMmv0v(I{16Auq%`SS?+&zLbU>ordD5r_TSaOAKV+r_EcMf}b|ncpQ2A8>c& z>bca3=(NPq-|AzX$4HCnAKF{QqCnDh9>wD%rH*psVCv>AQ-g47QT_p^hh{C~X`~UF z**&&1jSVoA-yg~o@`{L<+Z9-y+t?K>>2=mR7gdd1aDE4+DHbiBcxk9yGdXZh{=A~A zRDwT-+l;dLB++?(peo7kWBemRwa(_lKKv|RktmfG9C_62-KPfi>QI}>sZTtjQa347 zOX|b61aGZd)%UwSl$qjjzpud*$f>I;P5K2e#-Ktl;(b;Nn$+|*qhRJG+B;|=y2<1q5YuXf<1^JIFr(0oa2rVR^1jiftyr5Og029HHukV^Uh<&pK?EgJ(?^A0tVSY=+`s3Df?Z8QZ&=|1-b001Nks7~8vSu< z(SrH``d%v`nvB2mY<``E-e+IErm)K+cuI?sc`TIoq&ebNl)RL8Y zNbs=Q;Nah>;i4W#2;v(JpeSyV?qFw7szqyAYN|>D6U9sUF5RFoW-&nRp_Dle?EUsz z*DNe~k+z%{!K*f4HsY}N%$xZQ9ZE`&&biC7a$hO`$_He3ZZimPCEqe*x|f{~E;Zx2^3 z!dFu%wH~Wj3aIT4%P_cyR=hy&YuE)vQ|O^&~XyN+XvwrN(`uUPXg!M zleg>4F7CyMJp`(*Imf;9oZDbcpt=U>UOv_Q%nwA{7}FC-)At`N;)oQxmegM zxp{5__`b_*ep!oHfE>NOpRs{-9XeO^9r&$cy#Fc2hE>%CFv^N1#G8alK*1WMy&Njg-V_q<~4-gCH2C&6g zyVb^JbITYbqXelSHe>(K8aPyx02{4aPE+yucZmyRVbi)-7&@)+$T%Bx)Tr9Xh~f^` zEB22=-@&~Ih>Zt$8t1Tly1Fm1m}m7}$OG4K_IFz#jTHScWTD1!K!R^N{Sr|EkBWxA z-!GG-7d1Vn$u+`d-~?E$X5}V33)0(xH}HIKEq`f%#d;l%3<|6b{WUq7MyQl)~y2db1;%_Iy@eN10y7(BOF?K^8 zLo)QSFR{qTbR?@n7Hb<=cEciyA|MaM91+?Z-MB^wrpB)R0o=i)ocZJ*zpZVG_RN+a zTp|b#D*!vWmWzV++80h<=^DDU&2$mDnl(>K9=;4=<{M*(n2PZd$E%K=hTS>@homlU z1dGKVC7`2Mft}RhB|F+B3u-3Li_a3_g=&9;Jgqt1ATqy`#c`o4nnW(@pQ{`w;FJV? zxnF-iEkeFSK*m*l>qR%xi{_YnRaq$#B2`Lk@f($`PC+Id+xw7G(%U{GPG*oILWkKW zll;78jKDc-sHn_}V;o>>2~(szlUb`YYHZZl^n67jy2I$-K#z(EuMe!W=Fi%?FN2Rg)Eo zR%)Y1ikDSPtnbK5blcRk(`OTP1s=c1RU*6f4cK=C$ zCdD*+B}*dR<)f>6lU@gTz<>}6^^ubm@tE38#tQfs4*F0F<2f1Bi?*L{n+%(N+e|wO zd4{iHzJ;=wJR0R2x0!cU<0hBapPqZ2mjuI9Cm))mdEZ~bFdp6`XodI$fHHH=Kb({5 zWM^rrv{SEoguYq4OK>#w-nU{-I1OGhh-OekOE{k%1iNBcTg8LCH`zAEMAHux{#;x% zJbHV%opSs+Zp*p^EXUc;5@2$1QgKp!G_=G-13`h+c6Md(u&71Ja_^5>kN%XC?dr5D z3AT5&^Q2dP8tHLx=XO=*g*NkLp{#Dk(2R%Q!K|?=c~|t+Wm3Q<>`KjY^zc8D-o`hx zi)j$)DVm=XG9ru{Tgan^vTI2FBuI8s*~^yM{IP*$(W{ z*&~kq%Z`yXY$Xe}Mv3vTc6hg#W-R=XNRtC-GPHglx$Myvg!6cd_dq{!)z*DCd^r5b zw#?eJanuU^$@Wm~`WR&g-}XtD+|2vMCtl%;+w61w-CL($zoRaf42!CP(qa5M%|$}T zcLt@i*A-kbQlD~GPp_NnjyI*^w*tMs@1oodLzFI7VY`(Y0{<~peviuyRUP!vE1Sbn~H=&ZW+K_8(aht(RR?{mF5sAFwu>_`$^VpDn*ZKzM0 zYB_?dVy{y$cXI4v=$4DCwy-zwqW}s}o8!y_N z16U*TJr0rXXKoK>-zE2;v()`%F)UN@KkB+JK`P*`t62V~#y_m0-Q@TU)32|hfHLB*aGTX3s@A#Q>a54jwrM((r$2aQX}U^&V%)<< zyvMsiT-7{MKYRy^kFhosG-T=?B&xMEDN(L?ILk2RoQCI=%g9B-fn=#mt=*DirNs?n zpFhA*8-!*qA1G+^4VqV04XKWP5Kx+C>FFYxUduWz!a8kDe{lDIx~2kXydTa-4;Sks3K-lpLl8I5-AvD^$x-Z}&Sk^Aip`yMW(g`BRWXuWy+Rz2I75dyz+-bn>!`Uy`t73(%tLuOu^m_(uIaH1NPKb&)eJ zZE}TVV~f3`LFKFo#5TN|Ts;hOzemVyy#DB9O6QJrHXs)_31rU5i^1Y`T>DWSfyh8o za;Cq!J5OY%Skmi$InLnBtkLX-!u(0mQ8G_5m}{aDiel$p zB~5k*Zz-O({i@H_h{&H!SK`-l>u>JWOh?*h?*}M~U5ibMGlZ$Czax&>FVcfCq3T=U zA$eE15<7-SavV;cMTrUMR#cCKcY$4^hlVd5en)c@5dnqnPVMf6(^`O33RTGG!^|jo z##e)zW)DYlQE$*fb9-9rVDY4lUaDGQ8_~F72ix8p3~2u0S6N!M$wuBrAPj9^pEyY-q zK}E?9AzhN<@qQl&`_P#Fm>?^3v9m-O(e#3xR=H03z66SX0cMbVfY6(2uXBC5UCWIp z)D8F$(j~$QAD!<&(+NbQgp!Ag5s`U95s1CmEe`{)a=ofQ-gAY@(J7^AF<;<@N7 z#`8K|{(7UIzB@dZ2 z%GOy%%@~w$ZTy_HO|9WD%_z>b`O%TSQ&UC*cU4PyRH}Qsin%#GSBP7{Or|k|%_nSG z`qRV~^J-X|=4HX32F5lq^6hjtRed)_#@UhP@}R35iuWLx^8l4+a+fGfXzI2}NUy>$ z^e6HOYghJ-@_7gSWFfH=gT1Rr0fMcj9~9~wB-oLJN|6wF&A@;dV;gOq2$GeA`;PF# zlDN#|3W&{T@2$`=v*NRm)5|oY`Uwoh@Hl2)-hA$K=ZWWeY6pOXj@~e zR?tE(CnfI-Jh2)c-yyUlroe#$c&+j^(Rwc_MqxeJA*5-K)`NV*AcXjMLh(Zy8rfyL z<{R#bTrYI(nwKx)NbclBTAOVIXXrwIZHjvi7p06SM}Yx07*)+#;ZSNviWV0O!1({f~uB76%GgToZ|t z9~3fQ!N4ElGV*mTVk-0mK*9=&I$JmKg3g>N^j|vu+}JAq%2E5y%3Dw~tU3ThbM5DH zhO{D!-ip0rIy|r{gbDDhwxsy~U|>2$@F=-?Gi06K9gLSQt;Bb#-a7NE)r}sXcBTwJ zExm6%zJV`imkWz_G$;LSUS6CsE^3NcX(04pIVZ9_NUm1j|2*&r`F5 z?HNj!gRA}=}$%aK%e_K)~LtgnoCwpG^reIJy z!{rrxV-Ok$Hz=`jHog0%_tC8d6%`>s4I5^oOCR#FvF!~@HaV5~ptPifu3|B&wd_$+g?)GS?tJ?^gH?83Oho{uq^QQ$UwWfi?5X_iXh!Dlb1J@@PV zVSKR(nZ>eMC0)+W6U5hcDTY4iSQ10aiPYLt%?7OelWuNbgq5{7W7a_os_OzCPG~Tc zB9lgDRvcy@A-@Cy|JIWi1-T#E(Ly6vw`wVFLRsTo`#WR!s^0M>ZIgu{ik!VCqiCJu z*#HIqD6b!$UYPn_UhcuZcZVfc{>_jiFQEJo&Tzu?6E#z`G$W!0nSzfV3Ed!O{d#I_ zy*gH+p%($7*=M?58v6)ZK@IaHG}}R#H>>wJXVJx1vylm3_Rxz0LWT&MG0K)c8uV}P zxXNPRV6I8`v!#jFl-NKVl=L#)X!=Pv{M4d*XL?MdzaV`j;}LqTww*%5 zcSYFn#pn(Wkx}5S=!b7MyC6xmqAOI#e2&Hn-0e=vG`92sra=O<33*S6&uX1kFs`X= zm21s-ItAp-fe?NB^~k+WgV&Gg?X|>dQ~vMZjCD6A51?NqT$I9PJ-x_Kk3ZsA9|Rkz zt*C*dwJmn;+bpz&*`#=W6NtLF)l6Qc2s~&g(A|4^>EWi8G?i#2S(+!ftrr;)6J{k_ zs_e43^^yZu$Fi4%g5XjS$BHqxE?fd3= z@4ZAO-X|fB?0$MkbVpPfB#)ivfHb0FmseIO1m~Hf{_2Kd5Xp6ZVLn1P(mSviP=_=%g9A=3IMPW$r zjFTfU3)s+|uOS&f>oO90n^^6iyuO&vl>1(BD{)}(z(a-qt7O6FKbapF26k zv@*aK<;rvhw^Uw@s>iW@-6;?*g@9eVZMI!?_`NyV=7~rm`0{eyFuL;0g-mpmNngHz zQWqt`PH_A;3`K;G6dQ^vclTpP*cW}D;`pzWKlV0oUr82A-H-j?-B}YS{Mc$F$U)q1{^>5sJb2Zd?dJ9s5M4|0T$8jxD(CHTYb6&``7 z&Ne$W>e0F(qW||$L>5f$JA>YW3&T2rekz_w4A@Ogw#LW2UFAp_k&adF1$yiL1cgeC zKMHri>b7uNrL!4gCkqJN+3{ytwDv<=~}CMVEc=jqWRIjN%g zc;^?XUJ!+k_u9uVI;NMp{!pU+KxnRad0}LcmYqN2`%kS@DwYD@R!W#dlbw51I4aJO zVzINtVa_k4{9A$-0khHcN#PFCJlcJ|A6L@5657LP-GG zg31zzG?NbOZ}xcTLsOA-X#n~5jr`x5hqL=)? zbTIY1=w5OST&CNP#wb46c77G5Ij`R{H*MCW^N}IadwTxR)-+#*Q^5GH_p(w;bcUHo zm@d~FoABt!1fzAIKDhOqcoguVWH3yU1L(fGAtErCIw^m|Z3EyGU`jzpYxppHz zZK7QXm?H8@uTTwU!gxdhhF)_^arv(5YC5G`NT?kTp%0MuX2yG-@_tqm zv6eeqtP9bRw!TW_C!WI{mC=!!>mNC4-MaH$0JU5s{H$L2>0F-v75=I}g#A6*COKcX z@jJF(j&ssU^@WODpEco}c0YD61$KwXa;vAdUEohPo%rb%|EvK6?;|)6qNXgi7h`nn z+Z!lhdmifN8&V-8tdv?ymdn|p1;XJO@-(bPq!|ex_yi4AKHH16ilnq`0rARSX-PC- zF%nzQ7x4GaREDU_*J7^ODBYqZe2AV+ia+Q0qdI!L1v=lKRx0;cQw)FSxL+QLaGT6t zt%Z8qRN}gJEU6fzX7DP%KmT{@t-tmN{*9s)jPwBw$I4fY*H{B-bD>f5eF&*j9kmuM z1Hn_ba*V>iUeBWbsbV%L<%M06zmDWwHL=Tq_?@uid`gzNyJ7-iJdE`R+jq-MI3-|F zvj85qvUEcTyFBx3vY*dQ3aPVa^!16S@R|-e@%K9uw%=_Jn`jBTD&3WWLsaH*XYL(- zu%izviV`JL!@KeRl(zaSC0;gfJ3sc1$}k}Brz@|QczBvDIuGBj#QKi5F0dpid?Iv; zmuyh`sv`~`VH6$9kVFW%5?D+y|9mJ})kbG0F)SY1WFf%#VwBoh_B2cg9ja%Xm3Xbk zF2cTLE^*x?)V(`*%qf8^8_WslP?u4+Bergo#(7KlacIBbaq#I8++*eABg}zJD{ zg>fW-Xo%bZPG~h#U`m~t z49+VyU@Pp9MI-Q(c`)pqp-qlnj@Ql&?IB}u`Fb%%XC#u)IHfYg?MYkVCzD5@raI0WH zX#Ipn2D{PuMrA74;ohYEhn%d;)_Br*bJI<=c=5be5DQUU8Bt=`{zSgw;ge^i~-QjGz!|r26js--q5Ef-q8-w#AVZ9JTDzq&Q&w_gE+HnrDQRE*8(S) zju|KDv@_)c#?gPn)COV^!(urjzxx&c!NM;n3ZNcht2sbZF(XYuAZLwW0vNl+IHwU_ zyU(i`kfE^nl|k%&U#jGPljvZHB$=*Fe7b87;{+x3CCCgDQopjN`JO<1?H^XG8YF__ z@>Sr*f|z#jSfl~8${=BrQ8e`>Dml(wYucmPIMuXF1sf9yhAX!>gv*IW3sm*buX-5> zG2qi2yAY#dAZxKcQW5B4Q@w3u>D-MkNK)}&e}BzVV>{YX@UiLaB+f{@HTK)%SGG}r z1pk(JI8{o1^eg&Kl55Q(QmRVGRb+aC{*(wWt&awdOIleaR8GOT4y%z@8=0n0Qb=AM zDgKy$eT-He#>#N1tXgCljr9RO+jwcRn}o6QcZZ1J_1M?d9=^&q=gp0?sXy?cpNjZd zswRrex?K-ieg;w@AnqxyVWrDveZ|hvnRh}&vE1SE zQ)?47=2Q9T1@+TP>-(!gL)YR*S;K48@A5?~@#PvUVIWE+(9q3gZ0|=NO~_m_kW|TI z{6#87AliExO8!iGRVGrmGrT=yg3;BHov#<>L56M+w`1!dzE{!=-vq?K1$`QaqKRo2 z;ix(F@}E-M3rEvFTatS&n9bKD@LX8J!CxQvz|md)=?Gv^r=^#IcGuM<^tZ$&E8>l?nr zU|Uy2{qqiI(<2^2Krc`a;$8w~CMPbJKxVwmzLJ)}}ZpX?Gmp*h_k`sQyJN6G@7 z0u)EU6=COEq+rcf{MMZm9jY;O6|bW z#Kn$#tF2U0>phn{e~T;qc3XXdcP3=eYesiCIw-_gNi8$C0*jGgYeNPDsj$Rf#@)w{ zloqCE?Qx82*xOW0s-^=tp`QSUl@A|)*slZ41dKR^`yd2=zO7y$v9O-;gQ}x*IzDzV zyntHOV1u1e-YYN#^@r6mecI7K^|PO-)30%Ox+B60E=fO?>K+os0Awt)84kS(AU0SV zGlm~@$!DDoJMjHlox0iTVIA-A&OEb*4iVOqQ0!4WS%1rv{aQIP!>)^yNm9pUz-z;e z)=HyLb-I@J^Zl5#OG`O@_fXx}D48NggDqFcLe#{>z)~=*_)Y7#J*#si{_l#;cwhDQ zHS&~-q*utEZp4?>W0K|Tr|Ry9#?Yd4%{DViJ5pptV=hA4s#uG4DZ{p zFRBuuM4sN*FitiKCjo6Ty)Q>17}^`sQ^-+%=Oi-rFgXuTVDLqn<>?bX%(0$^`&zjf zibcfipct7)ov>Ricpj!}4Kbum8iZ@I2YFRoAYJOM2xMgTQ-OiBe6%n1KaNfuPjE=fv}o%hoPyC6|h~ zKCv{BSJeUq-;-wIt=+{EA-i8~o1$XATQzB7QonNvca?k`Zng(uG4%UTbq)Bwwz1C`eE#6pqW#Ch`w?kiH2Bqj{b9!QKYy43z&!r85p}i^@Hw>bEJ-*O z@Qm>ONze-THv+S7RYcW1y&qc^m$bRvjcci@6F3(o@n(~^$y^`3hl|<5sVlpu<_5=u z{&cUuJ}@ho>sjE5Kkk2*%(csKoEr}^?`7Pbr=k8uxcU}zu zYrtHvr(e|QN$!C@D|3aY@5@n&I5&YSmxXaXaXwlS-lqO)HQFhBLitR@0f8`Fvo&kO&tA=AoAoQTf0V8g z4HK0Vy2H_H*0CZLCIYZ>O$hd4R4a5dqBuYPJF^IK{((moFsY^vSZ1C=v;2_tu`WLA zYl1$C^A!15O892gStUL8V8yk&1x!i{;q$}!2&B8KRPfv6C5lUyVe>a)txVK7E^jWc zg4XiUD4|h$M@L)w66vh5YL2KlCC3&Zp6Krg>=kr0CP)E9Qg%`v~p<3m~2h zmRr)k#jH>9!iVA>OQ=wqOrOU0!#>5*4ysB@Sr6c1wB52e#TCLVZJXl<3Fc&7aB$M+ zA%;)at~dDQpT2&fF$NTzvXu~mFJ{+D2))}mNj^N1Zs?Kzixzc`Rq(@zF#Ld}LU`|% zG_4n5W735AqF`hDP^?ePj)S_w2d;H_Y%ENDM*8ou*c7sSur(3MnFUSjs2)0ib6i?7 zSG|S|_9_1L!6R&gxMxk5v*Sy+Ly6XHdJYa0P{wUfA&f93svv{)Gn$XHjeq4v0Pa+SteV0H*Z&(Ix>&ysMG(fV6v244qb6_n)s?0|KbP5^%plhU(v9m};7 z;1P&wCSFh14?1E#_Q!Cqu6U(0oad&CYrb20knr#tI@YWB#co5;j#)0sxPum}F06}G zMbS4C)u)OpuZnTukN&f{cg@ynrcEZ!d1JOHC#EVIA+3eWHkBFnaqPO`(5v0WrBPr3 zCLY&yb|4?3Yy$E< z4Z_4#i`ljCllHu@a?3)bCa;&sHDZzV$c2|T`sS~!=(f*dK@-xd3lyI3cSu4c+dZ`0 z(@4mMhvj6BIc!xZ1YVrwdw%#B?ov_xZIpaB-c4H&Oub^(+8t}v!5DyJH*ePwX`EZauXT_AmQfIe$;o}hRNO^p3nYA)0fR4}}XIQ>#$8KUdaLLt>Zn^fl_4RT} zdO(Snt2EN&(e9T~UU|$BS@0FpA*T>BrqJUl>P(603q z%)x<(?IMl{Mw=1ph+fkr#k3ps_)-2gkLL%PzTYt4nWm7s-|WKX&Y8Dk@QKl39oqZ- zq3LPHp`=Fbv2kAka$U73M!(ontmq*)5T5oZ@_9e`+MH2XwqApYW$*V1gxl1Lp*mgC z#?fh^t=IEoJ=AJbEj(L}k9I`hbvd#PX3rB*l)}T5@4JdqC%&c`0`9 zYLy+UH*{!9y z#1PE6k!mx24m~+uw(cQu`+Bbt2e~15g~W9L&AhUbv14}IsANJnlttfT4>ELDTIVEw zE3Zk#5cdsbjxxoam{2lG7E6>hsv1h4RxYoDaq_n4{~B`dm{kV6^K1ykvrH)@6&Eg) zi;AjSJhXSOW{a#N0p=PJH%V~<1JgfO3;tqGwqB;;baMyw_VN9AXJke|?aylN=J@Gz zyT)sBy$%gF!30T3na+w=2QLWSoe@j%NqhZI$K!B!aIgg+(hKx*Cvg!KlLTGFH@Vg0 zFv-kTg_Ly6ly*}pKB}|*RR8l=ND$oiNj4n*@xt85v#YUbyoahPowt(hulusG@UNW+ z7 z_C{`ANJmPNc$L(F(!xdkr*$hem!D-Z+=Dbtr8|DranOcGFFe|T1T>PoR^GlZQ;O3w z!gCV&f~(=?a5tqUmh}>>M9wO^s)Z8r_&!U`oX`5)2tbQuaZC`;c*(K9+dcAN0fWfM z&Wo40KGJyD**L-uqI4t@g<; zCGhe=L$XD$OloF!$xGp#nnUw>WY?ZkXRY(V{DF1hexUz_Thsd~EUNc<-@@ZB?wMD= z$#`vfh+IOW*Dq0Omf>D)BI#JxM4|bG>(*=u%~i7${)^3kLHK$^FhL;~P5q*sq#rX? zm@>R&w0ViNHc6r}fz~DERZsZR4|eDDxs=kwACctfO{AKdD)#RJRehKxlc>hvnPIx= z$^3UmsFfLRD3m!T20kd($<-TXP4z;{RcdVC$!g&(&z7US$d2_JggzZTc(5I{cMulH zjU(VAEqfLpj#5_ea~nhN!18r?8+S!sa25SBCRU5}cm7PR2e{p9p>H`!&W0KZ*5)p< z>g8N^w$HY8^y(qbb50H zFNa%sA#{Zl-E8SGT@Fk%qc00yc)xSiI_npaNU$2q5hKs0$c{^WdF|&IMuy9P0CMO% zPUteY@rU-a1d704;#5N07-@n#W7QtU@KlZ4)?=EN+pW_ge`QvZ0ER#k;;>$J1!c^) z6=+=12yVrTx5|4=311)Jw>#8$7M#m9BmfA1f?`^3UW7rdJ{9gO5^oHTrl{i=TawRQ zKbVq}>@@lw?Z8b2k+%hSJLK4GotjjAwgpmlv8e=(zbCVZ7XQ6rI7KxpwIK!agncA8 zx@15=cCc9+y}>x89%u{Ok-b~1HmLI8V-fUV-PLBf_O{+_}>3fu>7^>Sm65Oc-!zzD$iSs)ySSOOp zlj|bjQS|LzC{`VHRC|1Qa1mQ6`sGNX9lXD*?fj`&{MOmn3HU*yzZ*uCCfzPp>vS6q zc3pCryx)9xwMNgd5Tm|*cUtGDrOu_Gj`9j-)~g53bRis2@JDi{t%(UKz)MPMP{jS( zFJOv~w41l5^ag7_iq+V_*~V95p=*1mQ-rz!wS-e|~ak$*Y8&NDg87*ve1i%9N z>KiMnlr6>WGMOV9vn$xqjYSYKqEILfLs0(#^w@-?;U}9_Gkf^aH{Q8!m&2DEnHfcz zyqN*^$r>^o6=EQlT_;a^^rX4LJY%<(LY+4bOuiqp0^I!B-|^_Tf?i-+?xL+ww$6AS z;sud0yEqEy&?1FdLa*$<)w#3o*F^BmIY1s3?;emiSih%YqM5`w&Ek>(xB>rjs{#Q- zo={ukf4%4j;En@8@ssoh;osDiPQtq)!BnNKhJOT}x#}dxs~Z%CA{s^f*pY6G&S=8X zLo*<@GmV}K#HA7e?fPIU$%vLxGl(@AS*bOiP}Uc-2sz6}SZv7>gRpE|1p1-BmmOo% zJg86V;R41olc_$@r%2P~{`sMiO$6V9Xwm*ICQbK*YH{0n2i50J@7qXLR@6JT3mC0U z?ztlAaDxp499(*429wK(;;WSJuq{SjJ{01Y^Olaeqvx}o{B52E3fghiC9erM@O|hx zr>lUj;T1#v#Pj$3MvDzo3*hhQJ%$B{jzIO{$=2o?wQxgOao@e^`z0myia;@1nK5t{ ze#!^EGk9gFl?SL993<$MDItD8R`~fR0|4+ldwzg=zfR4X%TahRbzt|iju_0{<yGp(}_&Q?276Dp}N8Yu)52pL9D-^Z(7U-If}Lhpj0#fWjepEIzM;o2FK zrfIoNlbXuqw=>JvnCGQ4rB>W!GsPcgH5$Q3fR@{!d@Jj^$=$2sGHE{ZLt+xqPbGaB zk%F%Uwr;i>XU67;YAiR+Wykc~C05#a2y0t5B(y%5FW^}r=--WGEna=^s@|#k3|ZXf zD*`>j_mhpc{)-TfP7WppaUQeiNz9AznDBr)$Ra!p2?hZ`s5t+*sBAIO{`G|m0_Nm; zhH-O4Ai!rBmCa1%mt|m*lnq zPXmL1p6?BWK)AV|=>tN6oX>21ip!G~&*Yxs2K-wN41Q)SC+KOO{+C|Zza97oHH{_p6{2x@|;sJ3!caDn( z2>GwIuz$0fiwDg4{5-iJJdnRUfdZhRDUrFKd-s&H+)2J$@OUtu=QeQz|E9zf_Lt+_AWq2h06o=~=b6jN&BOIqUE=29 z{_lYQpP+H`K)IgNqkC>j02vHRzxI$NAi20Pv{@Jl_!bRNMc;!2i{c{!L&2 z0Lb%vZU6v4PvxHKUrpnGnf_0kf8L{>FrMeB_=G`#e<^-SvHv6&Cjh_=d@|!dvgrx? z?}qu0fw2FYl>X`NfWM;f)I|RZH4pfCO924DoX=azKiKoS@Pu)3KHrb{X(aiJNKXgC zlSF;+RGqd(>~79Dbn5DyDVFDiG-ANH;8nD#3CWx4H6>VAzexc(nw3ENGd2P@WbbQ z-uL-D_&tu_{~P6oIbF?3h`DDotpHCjE>7 ze{4uXx>`ZEh2`y)gF8%ehw@9R=)8Sw84(6*jCkiwE8sf7hX^wvJ#^dTs^8Dw=ZAee&el48MRtr_Z&9kb&pvL|nCi!1{cu_$zqOji3qVN#D@I zP!#f++}lZD7Mpa*{6Xf&C4SS7N1buj>dEL47aZA3%Xc^VdKOmM+-5A@OqyJ|rA3?f zx%G%jK&FEot8HL{vBB6gIFs|!gpUj=JgOH){SrPgrulI9?U$8MY%Anosi(^+j#e3W z_`9{T!sL>(IFzN{q86BLh{gYPgD8POvdV&7jkebQ+wvEHU0 zpGbGP?e0aK@zi2!K*of7FD&0EpSKuU#pLD`!E$){I)zj3+F(SV;$4@I`a+*mLHvB| zg{0upI=(t-uYG0}%}j+V6_#aaw;wSAdD+4*v8cJ_)T~*8+E?w#W27aZva-kJbUxwN zi;Bb`vRJF=;8)v$6TdXYGNG{YUu-#BCg}Vzj59$}C*T(1zOtC&F%jU06ayoTu}tu@ zVjNdiATk};seSAC9KgNzavNN8tvLW(=MW*0ZT;ub7^Oi2!eVBxU441>dNK(1&$>!C zLqJX6ol7E6i{qdxMO!R22)M$1r^^rgz#|zteo)hUL59txK*gf;zF(VSA;l5oix!}} z{{g)aB~YC-`ZkHh_>rqHay_PFg#zMuKBcwJnH7E6X?8t+!&u>N@bjI6Y2E8Ef@I;g z2t&EHS77GEh5Qd}Jr)|dOkRSOudm+ZWRZ=%?{TLlOeo1VhFB)8>s-^Vyat||_%mml~hDWi%pN_Ao$4;te%d)Zse;`!wK1A}Vs2FDts z2xCCB*WOAPDkdEFvq$T}8D$e;<4VeO0MU1QCqbAFNaYm2K8uO^U4Yii)nxehi`c?9 zP=_c4hmTczOt2uP4{|eVW8Hscl{RA!o7AJJkCiq|;o)V~QJf&oHpYV>LnRB-wO=_Q zeM{!1Q&=wzCjv|YRYYq#iQbAz?09O~3$L(Ri8*<^oH7Cw*YXDL3^rfWu)Oze+ANvw zG_)(h{LMwjfE#PKg;M~`TGki?apeT|E$0OHs0(JBvO_#}^O2?BfrkUJt!6D#*=RFD z9`3D@nAlc|lDT{m`ix@)!NW5Z5Rl92(oXw(I-I3`@&}V^yiJZGPI=D`pvn$y%1rIU z?p@roYzc=UO2JxEbyn|C(6^nzPi?U)#Q2quQNrr?R&0s6J{e7YBXp~zctNzf>k<#_ zye^r2;UA{XGliTR(T5l~OKj=uWxjZWir;5`R*qVz{h5rv-2viB;o{UxmC{P!G*s68 zI3YM=yOSd#1=kyk6KP*ALY!mMB<%`dWwCzO>X4;R*qkFzhdPhC4N^?ok++a-;G1C~NE+TtSvQL6*M-$oesR(vIWCGC5 z-m1r>1T(0qPut;B;Aorn{VGtRDykCsWcu7P?m?dBpu2t5!)A2@KF>^e5o^U;%Y4I{ z-@@)THTp!VO)Qf@Q7q4*77kawdJ64bIlI|Dc9sV;`&zL~PAKVU6w=&l%TTWx63YHm zNW$P6XA*MC6Z(md=BE-Bo{sxvXiIee==saKE6hiug6yPP^?jZ2ULK`k8vvu>AddMm zWoFMOiL&Ed1E$u6>U2e{ohQ9fC&G2P)V5LU zE=cFcSw`0xcyvTu3VuS2S6!nXb~!T2HNgJ1!yDPz|L`cN1M8^DQR2}4dX?;EIcsC- z*Edv~fN6hO3M3-TT{$U#9lx~xHf7w)20L3kdwkMABTZSu_Gp}IaKn#dd6^Og)Q=Q6 zjm)2=2miE7>Tx{)n|FxP@2hq-uV7qMq?kbVAau6EbG|dfQ67*LsmTjt)_|wcHfV2(?3Dr9BT1x~_w=Cg1_Pv5lRJ_A_VLHe`A@aKCE0l; zTvP$e>Q5XSm9J=wDS@H`IRQX0Do5?R%H9mYvzBK=`9;iZT61}CEw0AtJnj}$Zq}EP z)Ri zq;cld(U;#P>2g8>9$`HAu;8cijsrzb)U>2T-I$jB@MPO>lP|8JX{|gp^wTDU~>Ubf9z_liaNWvy|)x{^}X;T z1tx3U=>bC8N%U1c`Lm}bk`YTR+`_p{VW+fGrm6<$8wq5?5N&&JRmoX*rN=Rn8{Dsn zxJ+&j41)Jd!478wbonkEaz+a4xQMRzv0HPP`IC=JIQDn3TlCD`uql|iDPE?bx$5*t zwy)yV{sN9UjqO}T08d|7{xHi&UN!Cqc-T0?xap2`GXhkMUVBldMLE}rON{G--&J7F znoL$S_s-1ikQ|N+rue=BKi_CZ`(@CyMT)2EV6?`^y|@V62wXyy0ck@Tn&QIXyoBx0 zm~24Q1a9Eq80jFR^SYF>G{~GR_QQB{eB`q8TwhEQr1 z;C3jhdyoEUh#%v5%m&B~8LWTA?a*L8WTcH7n5=>788|gie;6LSwb;k~Eb_ITT9VYKepyjpwDZfz+4sWWD(^(S zorRN(w>rWi#tFJo6aJfHhw$e%flK^LoFmyd_Ipp@pA5&30=kooYt&igDstk-CiAU?4GY%S_sgL2k z>XnCYn_3qUE1+XNh~;P1>s4M5O?H3uQB#f<8BHNq^}{@(762A(m+H>!A)uU$ZJPal z%(P*rb9zaXYt2bzMt!6y<6-LHjV(~yX0o@2*A8B`E$~E_O`&^6BDXsr{x(AI({rSM zt&Hr*!4DZ`#k0XsjCm2^3X}p<(}GF;Z$4T+V}T3{S5)HAbWz$O-zO{)ubnC*u`1;B z5OFA6x$iThKb~s_Ujxu^c=E)FzgmR0s9#O#GWD`*N58uYNj2as>ci?fC1mYt9#tr^ zBK*it_I@n(!gv=~L~VO&rXg*I64rp^BpgLB2s7u;EZ_>qcocH$3=S^Yo*dOl%zO@7 zJFEg2PaTeOo(^|fo))By$Ou@lkvtdw@S&Kek3pZA+WV630LU_4=g=~&^I{~8V9DvR z=l*AV?(00BSEv2usf#}(%u^c;QF;OvjokJv=Tcd&pReI-QU1It;M&{v*WtfKGALg- z^x%Sb*B8h?>rJVfi(%Z=$XBlmSiFPbiuRhpL72#xVC@-kDyzQ@*fYgLy%j0~d5LOlJ(jYeRh! zdc-E3epWu#`}=eP*z_Z;$}FCpLmfAzce=dEo8KC-K-KjkRDY>n(vvgb#pNQhtE2s# z;^xdGO)3X9&7~4RmXzy^hYE+*S2$M!kZv0vT?1Cit_l6#l|7+!`*6^nJ))p;!Mdfn zUMWmCpNz}Qgk$_LPs+LB^6XpAVGdO|=`2yj^cO;A^wGlNtG#N0w<{}MN+g9kTsIsN z_MS&8*AKb^85~l|wGztwAke$tC)aH`Ipx#dXE#f#$Xl(-!w1JZUAH$kMvX7>ka4BH z!2#VSy1)Cv;*M5I$vTXv>jxVe%Hu>{9Bq)x{cbY(4vTQP)n;&7>AK3DCfo~XzWE$| za4@}#)M2(C-i-cBP-Ti1#joq;Hb+9dcVZ(ZN()gx^8>{{ zM|{&_tyWXePClGC0Jb_6MHFEXo*irlAU~)VZCP!c zZ#5eLUsMSU0#pg17Q|U1h^bMaYxbr+j>qiGVK%Sov##8LIcU?b+AMO~*v}MAi>G*) zI@@&z$X3(_{RKhgvc%!ruNZ-qiXJXJ%W^0S?(4EIG~xtu1vJvUzD}KN<+tsxl2`gU zs8P*wcf9-UfH!WHSt~`Li`?T?o_lzt4mRNzI?25BobL_jjUm1m6EnkH?$8o4eWPL=R9UTj+#%RU?goxM}xPw zk$6~xLph43O?r9lr*%kJLa-h&pONP)kFNKpnh7R`0kiGQ3JT=3@Ax{`_ERZ;TCweh zIczjPSjB;ZzeYNXtCdD;apP9bG@{NiIbV(;OF@jTtsI?>Xm6Rize1JkA_3yPGC#^>8`$E;;B^dl+pNsQ2$FS1CQp{ifx83V66U$bEx zm3ST%DtwA+wdJ6XaBiHR>JPpmZZ2Ymj8&{nF)X>ayE`9k?i2PDk(s@mEcOt4H`zgh z$BDSQnw+@c+$^vFIZzg$Y@LK?@9RqNrg|;AA5PHK z5t?~0nSBe|Pi;i@Cv*@z;X!Nk7isYL`U;qjALiL~6p!;oxr4OTW!H)6Y%02K@6y`W z-P@huE9wN@VdWB}$0Z`8xSC=u0B!6RP355~W3Y4T)YLaGOqVzq-dv+^G6!NIFsc0n zkfJzn9i=<|&_glOCq1*H{zULZU6Yie>O?3dyiQ&tve^~soyKvKVq+#!Ro4>mQ6rxU zFHsbK!zMx}bSj*WQ?Dv&6=45NeZXlkfVV>a-GVKJZR%CoFKc)3%=Pxo<9=>%92)If zwQ?!RIs8F?+tp!$21a|~2rzcUOyZ}3&4;r1YZ2kldb}UvP3>;ligqqgO>ZJUMURhu zG1`V>V7(FKthL)_3|0B{$I}LqBpmq{f}frD@dOVgIl#v|_Sr|TTqNDNtv%@9j zXwR^3S<&P*r4~fh_gMq2J^Cw^bWt$Y+R+^|8w9MfpC^hGiv^D4&+-dl>>r35Av%V| z=4E^ukgtGYKQh(Kk5w8K75D`kYcK6T{6W3p53`bG zNJWP^h3QL#onY|HL~F2kr~ViZusvT*&Y@xHy`)#&aeuE|?{R5ivqR#Sv8JvS>13W- zdNSqaSZDjhkBTt-7o6>NdA$8xSij9g1kq^W2J)Eu2ki=%cEWJDQ16vl4(4i4;pf0r znt;k|U^r0&`pu^7rX;qBM*HiYaepG#w5KxYa*lkhmI3TSGHA58MQy{iqwgqtza7W3 z#f3$1q{eUlzAUx_!Q^92?9r7#t0Oo#g^pdd)E|1 z9`(vA@a{xcqcOL-knBD*3Sy@3dd&Jrt(gJ&fP`9^(V1}%L;l$^Hy3$4aH#v+r&Imp z61?C*MVxuF{XzTj6*+86cFv%5L> zpc3A;>!*b7knu&0+V172lrg(=%;px-_cxi!n{d{fwfo169QBj8drgW!!%`qW(0q%L z7gWRc9ew>IuN6Og|7dn^;FEsDO3uPABb4=eU_v`oBL6~&o@FfmwPYa=-t)eYS3JFg zHYGXs8Z!I+sEgChngqmF46d|v7&8eZ^B;H1#&D&Vz0wu z#lDXVH$&59oMPb`d_9$A_+d{VZ2bv($nz(Qjrd~GU>9j1IsR3qG=@EUtfxHX=q5TP zmk0gxhdsvagrb}Hl;K;O5Z<%eqfDRXXEQyW^J;Ocj^k?oE@ouhkJCVDumw{0&3#$>I&(Y)Ld03R2NKD~^&L2gBI z7nrway?N<20IN*T{AEjy+C_o)p(x?ueoJSDP}h{!6F)!xazYNkzzyKvP3)>A`lZLYo?hMpNC-Y(5v)ZWL4J%l+@~``k=FB{FV4 z7cIK->&Pn{2PC;flQ9vN3@z3}C6VRS^{_)L49XF-=CeQrw=a%uTg@no*cN7_039k~ zLua`8>GuKj8NVT2@1oa8@!*n{Um^8{a~-Vb*mKw_Ywv?z%D;^aoI<(5)}Fz?Or(I* zWn=T83kPL+jr6KozDZ8w^>=;TxU-Fmz*0mtJ658l@0@FxWYI9c5PvMhj)x>5T6n4Z zVv79z^aK32?+WaE1Jf&(L}hSw)u`pkNpQa_y_IcIuWEk7$e$9-R#na7I-}^!OZ=Gr zN1v2PeOar8M5=gcw;hAt}rr4>8a==PhQ;%Ir1|UbdJ!%T8GBw zQ(jyhWak#5o}*A~%jn$S7pqwClPenr6?_^LB%ZfSf{ zxB-L3%Oxh5ty~yNx{tEz+plo3)?f_PVRW{!IGm#+Dd_1&ty9$=23r-9_w;5ZMd!Eg zW6^W^KLc*>WkHalU4=akuDy&7XcUP;hw8Mo$ftjJ)rrQ74@ zb%RknUyTQN^QOZdt30b=7O%%g>3QhNttBp{>S`W3MtMXn9bj}G(Rg4MW(enLWs?+Dv^=RisnkH=? z{eWf$xo}s{_gtM$;erzlaB4>NHEswHNll{)#EfR zY{Vh=UpE>{g5nc!c7@q61WBu;@vxUH`6xkp9niYvdEE6rjjMzmc*^c^SqRuxm zR^gXvQKWHY%SZidc5P@mOP?%qcMlMan8$11Q2KFf1D}82kw-#3TS@Eu-}?$ zmLXp3tH;NjWJgMCe{tvuQK=|D#7vZW?l1WJ+w4bA-`Q|%9)($AvS{PCM%}4?I1ORC z`{N;kZqL3ayJHgzGwdi7#97FTtbYm`d*ZiWoSHagC5WdI^FSdPETi0`&b_0>{o&~C z&}-96#nIR_50&@ulJf7SZ?^sX``7!;9pUGczms`mcKHyzeA zhqf)2uWM@>W6%g1rLilwTS7}3BZJs!dZ8r9ua?H_v2|ST)zXSKiH}^?9(>vk@NUjO z%%V6}P)I&&}!3GT`MPs33nn27%$p zaihkaRFT)1$)Q%BirFl>Su*jDj%|9|(>qTWXDDa*N;-Bnr*dh8Za6vheN&il@!fBF z*w8AQUgjrzO~h-cu5qj>e1JKCf?+ykhfsTkpDC0@&$sZgnOXs!t@HTLAo;>h164FuJV_2lS< zJ-p?4hO<)!Z<^J;Xsqpe3)Y|7KRZl7HKB$eL#}r1A>~JA)0*w?RkVe>JZC0C*M?QO z`)asRCSLLO3cNd{M|tX6+Aj9=c}b!x(Ngy3P7ns*ga@{dp6GpY9^HK<419L>xqM#E zhC<8b`2#%ScV(@HHFNHMdjul-g^nu4v`d(lD|XTjk~>YkHc*P-Un+{ByUPiVXDwCp zNM|W3@v!Ftw-XO~UyrLZZy6_erpN+gS=ltk_?)RR8+j(EXA?H7ijCCkiO%wRdZS*9 zR9>^AeHB@lr5rI-eIxS>P(ylJd9$rHWo-L-91RgQ`JLN#@g&!ljKMAsJ>voBw#Q#4 zPLN^bmG=IV(3_X=1UmqFjst=5S1X??5v1-{T&f<{NHUKcpW&f8`LwE%=@5=Dpkj=z zI#pk~XSZ*Vhec}$Q#MVy;tQGB#B)<2^6sdk9=zy?g_B9={@~vCkx2e@7kS|*YvWt? z5!t41M$frg@jMM(OVxH=K6cC+bfe`2xNVMTFZ-VZ6|Sjf~`+YaArAUb=t6KINWJ~5 zasX0S$!S6EVJF@=(lnUfd}?t&%hFMKf?6Ra-vND7jiOu5a9;M@`MhQwxiXK%r6`Ck z6N09BDn;$;<=L5WVQt;TPeDmUZF(|`oF^UX)A2?z@nKeYXvQ3@FF=u-8uj^;g4zl{ zg;SMy;%ei!M@SPs3g)?%+_}!R&J3(YQEz0EKEM3xax4`d>z1f4*krlM!kSik4P_&P3m#Pq`^*n1)rs2q1%i;l(_ud{a(t7qg$RYem8!Vk%m~gO z4Xb$F80}p}F>aGtKTen-r{cRguyH)UNKMOaUA+AvV&6mDRpGZNHRVR?^JuX1B}j2!-P7xZ z3jafBHgbV~Y!-Sts>A%ir!_WmuVBddkS2D5<@EXn6Vv&#s%81-cND3{7C{#+dZi;4+xwKs7!&9L`jG%;GX zlU6D$O?v=qA%%blF_oy_^lKwwxQ^Y1^5Xqd{u;Tq{kl`fR}fj&BwdF#*Nw~6`WBAV zq(A~6cH-V=qKCouKG+!U!HfpTB`V;n9pZJy)-vA}BTzV7kkP!RZ6=kAi3=0|tI8}y zUX0R*+ej6YnjYpcH*gZ^!3Mb>bNre1mG{xIDbDfl%wP0{IdrrpKovDvQ6ul5&);YV zsB+P*=`F&)9UoF!sIc^6ClwJf`$G*E8mCa^Nff@uV=RAfsF?Tyd*eTid>T*b)p}S+ z?{ck7cGhybfU{1EMqpcc9b2pV#aF9bx~a9X?AfA@@<8YFuO+!=ubL@xo9jxCvC8Q+ z-wr&M)W0}s&eza1=95crLpvgPNoPBx*?E1W4+S;>j}j^L3dK8c9GoB-0$ zML%|`JC>S$IP94x|KcOz5_12UlE96-n>hRfHUsp+%7fcy&+wcLCe>^PBrZ$}6r zbbL->TY7KGs~R#{yO$?OE$n428HivoU&emYeU?I>`Vp;#%PgoVU`(jbD zrfNiwGyO@0BPc6s2u*Y-D+&>F+`Q$3`i^0HUuHWgRCTqexDp|HgM$DxlkTiX(zB&FAjc*|osuSZp4$ld8 z4-PAi@-6{N%q!RhFUn2d3reemQU5@Rk9q@B^ZELC<$Ah+$`mPuLidQ4j>1>P)~WJf zZkRxCy;9>wbmnu_!SfDPt`~DXGQXS_U;6}Pv*XZJ1Mw-$pJ6OL}yaXg(-qvGWfX~Gz2hL6=aFAFZZGt*?Ul~0zQ_oeh;_Z`t~E~ zxG00gCN)d9GWI!LWx z9shvaYY`(u$P4>M#`+ZCf;`D=`d3=-Td9#qz9^>JzNxvPiC4e-)~WWbpS9nT-cr{& zThxaZ8;(Ll!cVHonxJ#BqKye{G1GY$ysi(?ub&#NHPZ|9dt8~5lzMv$vDO?&5iU$G z_;v&zY&RP>N_6-4e2`53g%$D;$$*1>YWA8g7Ne&<-h9F76}s8FoJ}!jOyryr`E>m%;K-F2Cg91UNLGuEx7ZeYQN7cBLba)bGsOKnA&}`X2EX zFa^gMt21*lDxA0;B8DeR$vDYowHm?+1?c_V2C1}^xoovU@Sl7+v$TTRIa%pX2tI1R zmRfP-l2YLL@L<10BoCZ6XtiabM4xK9HnN`Ih)aF_H5(KeM&++kyhnH_-8WZ8nU#x^ zBorXzU))(W64Noj=2q{>hAdai8wU@y{BCX3)qQUg9dhzZaAz9IJfOgqm0U9i6W>64 zk^Th?eLZw(FtCv4kt}r}=evl5V9pI}RZ{ zF*qzWdKlB=-0~Y~l}AAilO?G5heJ6z?C12F9eKb2kXqxGh9Q;)_(viXO-v1dA#`N& ztm70)*YYqQ0K=XQZxTRL_bgu~JFdm5n$c5@-oarA7xy@QE>UJkhVxN^w$!W0oqci! zWHUZ=ggoiGHeJDR8+iD}ZKy8fx8sF}dlPy++rm-W>(`G*KOt5KgUw09&C)~GcNQ93 z3*5tuDU|J#KgTDJ%2VOu)PJr^$Nz~OoPiP7Xpd}QMV#N9Vyi^PthUNpVM;&oGoKPq z;x#BpQXbw)F1gYnjx?j}{3YL|l9pCJS;+@7psx5Bso0jTm&3L@TRAjFKD+C_*SoGC zJgsYNO{_GupYrO9U>ogJxX8$sTyTffFmK7b1-`x63KuwSi&aCTVSPhBCyxQro$?@M z{Xy`EssBoi>f$r#d|#zi1E$N5@I_uyf2$}@kcN3x!_+*1cI{OAm?`9wt%vo@F68p} zF9Fidi_@^Yy%OahZQYe&GP0RfqshI%*>|4f5rSG8M=oE%| z#y*XTDFmGgl|n_C&S%CwNLNcX^hSna+uxkU38@;YrUAvd7uR^Hi*Lg)z6V~tf2hpP zHNC0Dh>(Q($wK306ZdIQVBY7(#l;<3T@gi&{nZ+ez*bBQxE(@fk=#zm&%N^_*YD5V zeO@%&MzdpW&F4OhLjm)#no+1bvP6t6J;&%=`eyGX)$bg9+B7_7ORt7DPO0{|1EWsRW?61RvXu596BfE_EDbGYR~LQe zyPvcftC(hUYk`;SPdIi$kY%Oxw6SKCQ^bh%%)I5Jur;ZQ1Vbey6{R6vTels)HwzRg zfoF}s8iWuA21e=PhI4tMuGpK(7pa}lBU2q@7snT_lVqf>J$dY_r=8*-$7cT<$7`DZ!HgH)NanqToax&C>|XfC#SehBQXjLywbl-JeH_W ze3VIYnXixKy}Mb0DeO0Dwmhgc(J`n#>ehb5vm)szl1U*>rck zA5Xj6FK)wc{j*xYtqkEyz1h+a^Ft=b)UKG@;Xbh$*%qJp6B-% zM_UM!oaDY9o+jCYbnO?i zCM2on(C0mbEgv~V-_pDYI+>Sx)r+C$n*1VUwd`WQUn;Y9yyVhQ2Vz{c9r^`5Q~k!9 z$yW>UX?3&A-7WUQOg*6nXf0u6=bm1fs&O^;`V0w=gm`ciCNh~HpT6GQSq6~BMtwSx zc9Rv zkT)5A1mvJ2%}j-*c^IT92KVyt7>}tqU!o{VXV%24o}-V4MgcxH%8Te0X+M#?vGrkm zWs)2yDHVmm#VU(WL-IsTKKxk_(MHhfD@Gg~hLtI%Qo6(S&Bc27*X67zi<o}@yG4a5jxJG&#LGl-k&6hhj=(O01b(#NDGFvuf zShp-0reZkf3;FcZ1baJfLsP?mq30PfCA;3x>`WGcaED~S=Eu(p-@e(pxC{0aOwP-V z+Lu@=yNmPeAXs?LGpSocs)d}T#pv8*1h5;ZA|kZQAuk~_Y~QVowC!mfAlNTj)5|x8 z30t^@!;ml>cYxjIGoP>!-Tew(Dod#$8aqBzo1&8o?os>WQrV|dKiuLgO^WP;H{jGx0j7~w(oGTCZA zBb7S6Jzv4ke-w64PdA~*N6NZ5*IDYKP8l4xHzN<-vfTw@*GtYQUIzF|GaE0odBgEWzhcWna-PhFh8sEp+B$_jgOCWL{X9=jdxO+9U!A|78vJ%}%smCIQaz9u8$9E>0h8`3yGWm>-_ z-XZ%EF?Xq}sKoTe_fbmb2QuxBDKR)&f5|uD#{^>%RpAoclH3J1^}aPJZEP2a_dkCB z_BzkF{8S+yB3qDZP5qIf!zD)ewZ=?srXx_Jtr-NzDm}AHC2d?g45s#g^e-IE4SS00 z?-cA;o)*0dfLDk+(UCRC30$VfAo{}3k3T%B ze)@|+ubXG*e`LQr0%$^qVQW%DnjPV+Qe+Pwm7zf7-)R*ZXYzmIZrqiap%L&TX`6E~ zx2bC+5%J`;he{e~xnM~1NNOph4Sxo3BV(1HzgT0u)YFq5x)3HIbr; zCYlxRIbIW}__DEa(~5mlPafy#k1H?RCB8P(QOoi7aF$o=ht%;{KFG3i(VW!O~0+&hiP6OZq_RXe2^hJvDfj#oP_xB%9ciulizz zM!O(zoy@;;)jlhhGQE}>Gz=b#iA5R}lu!qnl09R@I@WCZRXRn)t#FMt8eHx0?!d4< z)*SPkfW`OZ5vkkEuG;Kd;KwWzU@fQSv~b0b>k(n0aSybm89)(%NC3|DrtHG-#*ih= zlBIZvK^g8_9r$O)n8W_Q5~-@Bk4e_&H_O5wca<^mH@|e}exsviITx^LQR79v$2Cw% zAy)ddwJ&IM7|%_oWJPX<%RWn9ZcBa?ul&MIJs2^Ns#NG|>%*tLsZ3Wn?meO@qR8x= z1Cy}XX1V3@0j{LBUFG#J|L#llRl)DbiZl^T5hl=?lf@vnE7unr^FKa2>tea|WXqjg z6*g4;T34VfjZ%hRv;BB);N6*X@SO=*m*Xm)e!a7^Mu zfuJYWV?F|t16z)I8yU{m;hrhJrtU6L% zunZpbBYju8_AB0fA;7hAO!KG&5EDQ^j6g;w^XCM(a2TxV;SAsd26Be05<)^TxX}XS zs_j-I!TCrTF_GfVB;v)=N!kru9cC=WW0MTA{tTcgNPnd(^CaA}f2PWPO~P4ACt&|c zwC%PsCHO(5h^p&o$Jy)6ZDVXddK4yn)?#^+CxuC+=|B(dZ+enrQq(`yHVbY12G-j7 z{iU40P8K3a*LA1lOpxFQ!gOxqL9=E-DDV3&N{@>TF(z!U>|DxD@B&}PS2jSgf}9b| z*gUYPLJzj4)ama}*`qBYWc{eBv87Qt@MJ$($x;=|@+slwZ$BVbp#UTDD>n-5^ptsw zV&r&I6lHl!67uUj#oD8J5PVTb#3`I{189D2oOa$?ybt|;s~}nTbI@d+LoD{R^_U}N zH5*Fe!>rVwvZ>E3k{Sclu;{Um{2MVZ=j<6WKT-xzX2rK& z472xTcM>{#c)h&>j`n&ZfnO*pR)bu?3OFggNMI@Y3d&0Qdl4)AkYoiGc)x zg&2W>gMt}tGp9O&gh3@fj=L-sf zq&?gQAdoQF{WJvOFvPtyfPx5+(EX6XLcsf}0q?NC3IY}q61o=@5DYV`Kihy7k2!3B$cl7>MI4}YV zyjL0^I4y4nK#BzZZ7l=@!tPrO-DPv1?>iy>6}k`v2)*9`cV^K0A`pT=1^;AoN9}*K zc?aJ8`jhNGusa#v(|hCtjemJl2Qy3ef;9Qr?<^3VGaK=41f{o@}96hZ+1;ztMp zzAtCsU5mo*2MD>->3z2TBz!+Wh~VFXfCwUi|Dxfa8AAlYi2HQi&5*xj41vJ@nm-T- z{4e_Nn1=%04{f9Qt_ zLjN*^fgyiM8zz(n+P%~4zvtgSstUW~=YA3HFv$HP+>Im1eQx1*QQkib7eqksHya!b zg#Sy4|KtpQHzx1P6Mh%^eU-q4{_cyrQ4Ide4grMzbsqu*`-f!z)iXdi0)qJa@LdV- z^$+~6Rqkbcw=4wjXMBet?hntq$pHK>$9JW=!(hn!EA9@2-fu_{5DdOA**}X$=pNO7 zItp@+>N`vjdQUlb81&z5f&9Pe@CStbbr=r3&%&SG^mi}_nBZT`AnuCy-wcBOMa@64 zyZZkD?@xj|3X+i($**m%2 zUp=6^nft%B`@hl&3JO8)3-b>9OZ|d^@PE?p?rLV6wtfWQv$O;XnL&jtVP+OkxS1Km z!VD~EVQzJ&Y_KIr$Xp06&M5l-Z(>A%D=toe>*j9e>hA4oWley47wlaR65z72JyMnX F{{T8mFW>+G diff --git a/doc/invargent-manual.tm b/doc/invargent-manual.tm index 48c50a1..435f944 100644 --- a/doc/invargent-manual.tm +++ b/doc/invargent-manual.tm @@ -732,6 +732,16 @@ with the nodes cannot be eliminated from the constraint during initial simplification. + >Keep clauses + in exported code. When faced with multiple maximally general types of a + function, we sometimes want to prevent some interpretations by asserting + that a combination of arguments is not possible. These arguments will not + be compatible with the type inferred, causing exported code to fail to + typecheck. Sometimes we indicate unreachable cases just for + documentation. If the type is tight this will cause exported code to fail + to typecheck too. This option keeps pattern matching branches with + in their bodies in exported code nevertheless. + >Limit on term simple abduction steps (default 700). Simple abduction works with a single implication branch, which roughly corresponds to a single branch -- an execution path diff --git a/src/InvarGenT.ml b/src/InvarGenT.ml index c42a53e..d07abef 100644 --- a/src/InvarGenT.ml +++ b/src/InvarGenT.ml @@ -84,6 +84,8 @@ let main () = "The exported type for which `Num` is an alias (default `int`); apply `S.of_int` to numerals."; "-full_annot", Arg.Set full_annot, "Annotate the `function` and `let..in` nodes in generated OCaml code"; + "-keep_assert_false", Arg.Clear OCaml.drop_assert_false, + "Keep `assert false` clauses in exported code"; "-term_abduction_timeout", Arg.Set_int Abduction.timeout_count, "Limit on term simple abduction steps (default 700)"; "-term_abduction_fail", Arg.Set_int Abduction.fail_timeout_count, diff --git a/src/InvarGenTTest.ml b/src/InvarGenTTest.ml index 241677f..1d3ef24 100644 --- a/src/InvarGenTTest.ml +++ b/src/InvarGenTTest.ml @@ -145,15 +145,15 @@ let tests = "InvarGenT" >::: [ "non_pointwise_avl_small_rec" >:: (fun () -> skip_if !debug "debug"; - test_case ~richer_answers:true "non_pointwise_avl_small_rec" ()); + test_case "non_pointwise_avl_small_rec" ()); "non_pointwise_avl_small" >:: (fun () -> skip_if !debug "debug"; - test_case ~richer_answers:true "non_pointwise_avl_small" ()); + test_case "non_pointwise_avl_small" ()); "non_pointwise_avl" >:: (fun () -> skip_if !debug "debug"; - test_case ~richer_answers:true "non_pointwise_avl" ()); + test_case "non_pointwise_avl" ()); "non_pointwise_vary" >:: (fun () -> todo "harder test"; diff --git a/src/OCaml.ml b/src/OCaml.ml index db5d9eb..cb71877 100644 --- a/src/OCaml.ml +++ b/src/OCaml.ml @@ -8,6 +8,7 @@ let num_is = ref "int" let num_is_mod = ref false +let drop_assert_false = ref true open Terms open Format @@ -120,9 +121,12 @@ let postprocess elim_extypes e = | App (e1, e2, loc) -> App (aux e1, aux e2, loc) | Lam (ann, cls, loc) -> - let cls = List.filter (not % single_assert_false) cls in + let cls = + if !drop_assert_false + then List.filter (not % single_assert_false) cls + else cls in Lam (ann, List.map (fun (p,e)->p, aux e) cls, loc) - | AssertFalse _ -> assert false + | AssertFalse _ as e -> e | (AssertLeq _ | AssertEqty _) as e -> e | Letrec (docu, ann, x, e1, e2, loc) -> Letrec (docu, ann, x, aux e1, aux e2, loc) diff --git a/src/OCaml.mli b/src/OCaml.mli index a7920e3..02f6cc8 100644 --- a/src/OCaml.mli +++ b/src/OCaml.mli @@ -10,6 +10,9 @@ val num_is : string ref (** See the [-num_is_mod] option. *) val num_is_mod : bool ref +(** Drop [assert false] clauses from exported code, see the + [-drop_assert_false] option. *) +val drop_assert_false : bool ref val pr_ml : funtys:bool -> lettys:bool ->