From 8c308fb4f0a909f18a68c6ffe333f86f8938c9ff Mon Sep 17 00:00:00 2001 From: lukstafi Date: Sat, 21 Dec 2013 00:27:56 +0100 Subject: [PATCH] Better and simpler test for violations of the `split` condition in `unify`. --- README.md | 1 + TODO.md | 1 + doc/invargent.pdf | Bin 296146 -> 296316 bytes doc/invargent.tm | 7 ++++-- examples/non_pointwise_avl.gadti.target | 26 ++++++++++++++++------ src/InvarGenTTest.ml | 2 +- src/Invariants.ml | 1 + src/InvariantsTest.ml | 1 + src/NumS.ml | 2 ++ src/Terms.ml | 28 ++++++++++-------------- 10 files changed, 42 insertions(+), 27 deletions(-) diff --git a/README.md b/README.md index d6aa6a3..391469f 100644 --- a/README.md +++ b/README.md @@ -28,6 +28,7 @@ Version 2.0 goals -- version targets may be reassigned: - [_] 'Update' and 'verify' modes of inference: use an existing `.gadti` file to provide a type annotation on the toplevel `.gadt` expressions. (v1.4) - [_] Optimize, paying attention to the speed of the update mode. (v1.4) - [_] Support OCaml-style records, with some desambiguation roughly as in OCaml. (v1.4) +- [_] Or-patterns `p1 | p2` expanded for inference but preserved in exported code. (v1.4) - [_] Syntax for numeric multiplication. (v2.0) - [_] Add a new "promising" sort. Candidates: integer numbers, partial orders, ring of polynomials... (v2.0) diff --git a/TODO.md b/TODO.md index 8fffb8d..0eb7a05 100644 --- a/TODO.md +++ b/TODO.md @@ -7,3 +7,4 @@ Place for TODOs/FIXMEs, especially if not expressed in other places. See README. * 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.pdf b/doc/invargent.pdf index db04b8f45a58350c9ea8afe17613ee95be3b4448..a5d0e8c93a598800bb3e2a1c6d0fd280de62188f 100644 GIT binary patch delta 28815 zcmYhBQ(&My*RE@KYE3zv+O}=mw(X~OXKG_=+qP}nwzc1HAN@zUSF*B_ljvHRi$MK| zM6F441+<+vhHCxPlfL@-B2|f*)O9Mxf~F-ioe1Kc3RDOxGL?7eB#74_)j*OH?_#&J zTV0+J+yrB_DB?2*+*(DDu_t8Qfz3}>q=&Cp=46LjqbL23ey`_`RquQFdvVnQpCrcY zsE+yKagzslD&OurD$gLG|2%aErgKggJHO*vxj%9)=+VCd=jpTW2EIEy zzoM%@HgU$)OJiTpCa1Qa&5Vz3`UzhmneY1_@6GwE^+uu=_0{eDfT?yDIOBA~`1`Op zVub!_!cb{~Ay3`wr}Z-hhd$B`g6qQ#fC%=HBQP^;HoD1341d}*Rhh*R18>}Yj3?8XmmqajHeJq zoWE1zdPY-u*m_oHg(ormQC0KgQ+_*%M4|mzyH&shhq|Z$rf1poa#*FRt||$Dz%o5a zG>rze)=JI4z+JrESHd9IX!G`7rp-{VbHY#yE8N~)x!n9zs6>i$;Wm6PMidVTv7#8XOXAV)GI(PgU5qyDoz)$rcAwEq;H(#p62O<@5F0UWf0fov8=^ zx_))0U8x9%w&qI7n~^MADK*4S7&kftREh@hM zyayAA5St-vwu%@S*&pRM!J@+FNS6JH3`JZ`Sl}hDX`A*Bozyggi2M%eKy@V z(mkAISd0MCUsrv%ZLRWRD8;*I;@64M=>|oltw=)+*Y|bF4J69(-c;>WB{c0Qq4;QQ zk4jpS3@{W|Pf=ed-N`t*@ADaN@yTn9EPW@yi9h#@V~V5mw`ZkRA&jFi%VUL+lzOh0 z$>i-eRbrhgrm)*1q8|XIq)Ga$+nrNV1$CVAA`gjh{?12QBgi#3;*3BxEukhkmhJElPp_`* z89QWoQVmrlfWa3cl!g7?VpA0vMH;Z1V?jLWq1BsF8idM!#w)2)fW4_Tw_*>f5C3LYX*Owk{~`tjgxiAS6`91uXu20X;j& z(u_>szUrHcm%YH>MADEaistLJ^6`;<_>6YvIoAZ==RXn>Xp^J;8?7obOmQ!@zB&dD zNVzleis?A-=3h%-zYKSeNuX13^0AYQmQzObU)F6soS&YKtoYWDu=CW0-aoAwMAil@ z351JKqenK3XkRDPa;A>48`Z(&PA_Zymu=03dVSYz&W?bguc3kz$^ja(s*5l$ho4ry z6;jG`8{2qX&md=n2~+K}e4GkTmKVihYd#lU%B1Uk1@Zus+ zO;N;{+s=5FO2EO=IGD|fIa2`Uwl`z5A${RpD|7dyz!uaFC@Kare~OS1H42I`qJc(( z5D{Na#8PMTxo$YuEdfa%6^#1{irfGMLrO5;{p(pEmnRoe;jz$j zu{_E6eyV4rqkC@#I@|>2godJS3{8W0@L>Q}Lo&~!!X|dXs8b)xc+UG8wpL4>T{ygy zrQd^DWn5VY-Exq0wyNA>-TV63W+9HM=aZ^=4FKH|uQ=)hfo+F}#s(LyPr9tJ2xxDs zS%XJr&g^G-Q|9mWR6TN&)We*OL8fKy>~*)?*~d^@l0?EL1PM9ifP6zfPAMPTUW_J4 z`ogosLp=^vz{7?uK#ULRD;0!Lri$djDKXqLV^8I}V~HdepiI&$`3J-;QuoHAmzTvR z!VXWfR(i)!+&rJ7LMOv2x?N%*0}fAO4fSicKJhW&;q@_6H4@oARL!gQ=Z3xT4?brN z-L!_glu5*YpB_Y@+ELj8$SFa{QNlo}Lgoe~TF6Q9H7)Q^japialyHa=lf;z=IUI`! zV3|+BDTDIVAEC}%O3WCK4@0C}@k1d5IJ0|9HWxODM{#M&XJFKLw4OhNfGyUPzaHu* z(lsHnE3v;FRX3+>i^ZOdHrav{;aw~=XQFQthI%(~&T00`(su@14k;po@fT?WGrSe# zpio#S6NFJpAsmb2p>B%oH}eE?x`R`9?qkUH<%-x&(~~UG2Q;V_$*A{f=@@Hp4$LXI7E@x#rAPOf36$NH%;SCAx$P?C0tg7rg!@K=Qq*-9jh?;`z9U ziLVs*?~hnhVFQ~1D-f&?3H3%zt!I>`F={V;Tk5hPNwk3=&=(Rxg=Xr`KY7`1oqR63 zi!WjXrQsL6UM}eP1K7}e5+G)Vul#MrngRUwZEoGr3akd)c{Dc55jj_FHf)bW&mt@1 zCsgCTTr~FuLe=KFK=a@!>4%Ws#Io#`PqxrXJZ3#%mq4lBV8HtCOb0Ic1|^4_Nptwz z-&gg|@>BPr@NeYvub8VT|8nxVVi<10DJpt9Tty`UBQMX+F{MD()62SAJFSKnWhxgE z2Up3RWl8O)dx}8(WgmM5Gt$V}eA6n53-(HTjlYNZwIo`q0q-!`CV;=E9TGgaz874s zC{VUdWIzwr;2wWK#^dj>d~~7EIxTir8XnZ>y!D+#dDecWN4Nv~I3dV}`g|&6-whgC zNZ%IKGC`)9BoFEGc4}H&ex^_XXDIdzyR}`o&pfqzX%C*E{gI}t`%PQoFX{V4^L<)$ zN*7ZZUUoHhpxL=;JZth0^3%e5gf%;HchY;bn0rv+S3709Eh2gi+!)6bRg<;Lfm&ij zzM}}e8m$na)PZ6&!@n5Z5y$+5T+l{-n=pct6AHMe0@aZ}CW0TWrahg6P16GDu8T>N zZp zb~bjq@nV%HOby#1Z0C8@_|6+O(> zduIQER_w1Di*NOSUJu4*vtvbCFV~enCR$rX-2ZQf*r(|c;vl0JHsu?Xz0a8Z=Tn8n|L=i0?QS8 zpWU!Ch;*vg`n*3U5rdn8amOaRuW3p#4}u#inIF(nnu+jt z0e0^1{X0ZD%rG?al20_jVA*X=*SUOC@cODk&&wGO#xbXiXG+~&m2Q0D3M{w>QxoZN zviN0N;_#fsbaivX4v?R6p$@vFkGQ#p;4N=nGhyn$%3Kv)&sc(e?Mci7tsB#e%@$ARaNEjH%fU<|UYL5@7IznlAw%3y5_JrbW3fd6y06TAVCQf8 znZb;USv-s%T1`t8odFO+M$AL?AjE4*5XqbJA=HiFe zpb@OB`TOv|N`=6Z$Ek>2{QEk=4`@$jKWDqfM>)A$kUeJa@d}+5kNR%xp4oY@dA=08`6aK;2Jz zz@;j|vAzoj8ilzpp5`AHYqn&@cVN*)8Jv&(jm7Y}j&@(bo2X2xzf0Wosq+~_s54PQ z+VhFP2<$#Om&u7KgCeh@k@Ko2zsls>?->v;mzLFA?1s<9s;gS%kYLxu*i@9|b>Y8L z9QgvoS4X8jjstfG;q6<;z-QPh=twk1ZC^+g3@(fzHq!e9u^HrN4jR>X0>usm1(>gc z06h|!1Xyu`=fB~z!@#jNp8~uaL{&rmzAt}H{3qOS_X@^e!s>6ftbTaiX#NAFPy&ZX z8V<6qg!m-Xk#YA;Aw+~UHL-Y24!;Nqarb}4NBKvFC~Sjc+*ML60cSzXo-Nz){o(3J zN;+Fa zG;bm?L3yf2?ygB4^vxOZN9Y?Zx>`0pZp(M&fU2w1eb46Yk)dpm>K~0eiLRf@S3%)R zb}tPk5Z?i+`eF_SN@lj-mTa_j17(hAW$MCV-pcz!zUe^oYO{Xf{rzEH&8v=2|94Hr z`y~YW%IR~8jqzs-BBJoM%*y%S;IJCtqp(rYL*BYE48#!J=ehYese^PZ%V|JdZ$UHl zIp4sl-`z#qhTY}HL=NYHU24Hb!|qj!OY;uNa-jpT6o=ZF2G2;GD zUm?ssy7H7P?@~9L_@d5DOzyCK47i;=`Sk!EuqMbxLTMjhtY8SH(BzQc-$r z=8S4GW~B*Dmg*t2=Uj1%d_2pHxaidWt{3pe{%M1_9|gwkKI|e- z;6}g`T8L-niJPLMZgVwV-$eu0is$R=}R z{7L4Ty%|bXM=PmmP+F%*+|Xns=OVJvCfp9hnClk`EaP^?o2gb1CSI=Bfrbv?AJ50? z=&hNJuWfoSE@ja@_lo4?+jorFy-@r63x*S}WM`2D-lW*Pv|fSx$<1OY|EQ5vJmwfM zUX@>#e+qeY=3B0;l{mb$0QXx>?#X-7)s9ell|)>D5b$IJ%MM3NJ}aP!pk?f}znyUa zD`=c3Ju=nzW!qGp*dJqe(eRy!S+{xzXB`X2#o`PNl>Sk2Xw}732T^>aNz6kUZT&9H zZD5Zi`W5A%RQl?}vvT?2-rtq3Kl=(?KnWe-|ICr8xC~GTsR2dvwoI%bXzui>!z?d; z!)I*IG51M3uBRr%K(nP|{v)<7T5#<%Pla!}cwe=5s@+g+S=eP@zD_v0p1q%zxwck^^)DTuAKVT>UY}$T4+Bx5pF{xI=OC`M z#in#smu09`gVoM_ml+KO;{b0?$p3+80Ky%sha_v3yb-6cn9 zYJB}7w>O}H z^NW|QF<3b=cK|!xgn`Vh_#H?s`VEqhb5)Br%z?9R+c(i}rEi!M{`mltMc2dU(!($~ zoI~EM>+k)Kk5)p~T|MT7%lYx-TAXv5iljDn%}k?&%E{DI?_EALo`?R&4o;>)j~nF4&pc&P48_*UJ{m>*^VNKHDwnI z6z{)h31b3f6jB@^0Vqqtjxi>nBmE!KMd_-K{5Jf%1_x_QfDPi*suY1=9IuiYIXDnT z;TWJ1E8>Zz0j{BV_p6(icYYJx082*+e)N|qVeo3N0m0`>+dJ;3j~^zK5S`FF;Wz1a zX3i%9e~-Sa)d2C25KWfB*HxrrbBv}aQD<+zr$NH)@Il*g+3oM!4;n3CW8e71YiIic zY3=Lgz5JfJwr49s0!ysS!?Cf~Pn{b3cKvz>3xnd>+|kw9@2PsQyg4^KB?_Rg`r`R` zQ|5oWwTDT1x{nLHf7NzZXL&Z&)}g^lkvbznjfb79-sW?Jwsk3CC_7*4oc%4;#|=KW{b0SMO>2;B@ji6$A*p zq*V5vCmQ%!)FX*URW*K;e<#@!L*IWQ9#ea+cWco_V}8|i-w?{b{S^-b|9X0OEZ!@z zNM@I7lR=J`Fk1|RCyys)SeZk2t*1(_YiraMMjH_s5tf{+w^9YF>Z&X(Mf47;&c;|f ze_AE1G_^ThN0Q7awItUavg*Mlh(t-Fco}wO11ZoZx|K{p0qU(L0G#xNkMZd$^Dq2X)VGg z&F{)R){_!AG3EhIGTPFN2lE_=X3)Iewy3vyo@7o=)RoKF8TH)XbW}Ya5RPCP5JJ3` zPLJw@cFCg&0dH+U9NJ}7w_BKCT1zZ6#dz{DD|e1 z`M|#>#tD1`CsxuxNz!tW$j-uAwZK$N2p4_)U9GdAs6+wyrNyRSbAm#=YOg;-ddk(*uM;3=6QwbI zdv3Cb{_y}<;FRt*S_+!SHGgoi{EmyCmMZ9?Z#t)GhNdw_Dd`Ou*MN4}di}vxT$k~? zcQwQ%`SPlbx}ra*3hH^qQyexhK?X@=j!YI0Ik1hsoqL)52TQid5f=>JO%bKmbGu|< zI0&YMepA4_EnX@!718Uo8Z|nNrPANmA4NOnyrdjJflw)iN;5sKhTD6gG7HjANp51o zGZXyo!7?yh1M{_o#&=3NFhS(rOXLT{2?xI~#CAcf0x*gccgSGWe**C;FXYdDdswN< zs*r)_Cc4AFD1VeB;F2OJZ8W$uj0jXM%dMUWHvr3!J1NjCR_hC%iZfqS9${|I`lX?7 zl|&B!4#iXP!mq~)my;N0Cj(33cI7!+irUB2fj?G?ChN$ zxZ6^GQ!1NK1&5-GnI47kt;eUM5h;pZe_u|Y5xjs&n7sg6rzWV%FXtKou0vO`X(<_R zdOMUD9LX}JIpKkT-}1^%7@fH8hIIJ!ucqEcHr{v!sHN9?pEd6`*doF3Juj?}Rw-D3 z&jAARu0*Nz#LXBlbv3c*QiU|00>~dz%Sp#A&)dU>8C`aqlSo}vi1~jh0s{gG9y>$1 zAfs2ayAn9hQR^nUe&RQv4}pw-^z*?%nbh>YvM{A!BxUw4OGFusnSUjWkcUbj+3E!j z3A8}alje8K-;gee;PekA(B}+5UhW@6j+66v4)EoU2y6@n(Y#luz!1S4pY*e&06tvNZUr~^i%v8gS+~dj(AWw{Y zEkjO`QhrZfM=e%q^`2`;NCftZdvzFrg??b;2^`C*1{bW#sx>jkm&8T07te{y%>?0oJxDYE*+yqy zwTr3MJ(xERiY$t`2?foO1Q(0ls<2Y)K~=8yT~*Ri$czw9z0JqtKfBHU$u9=MpyS1v z*gt$(MY>T53e%no)qT|jG;pzf;`%3K++hj*_FYUO)&S|vMBG^57E$Fgq%n2h-F*ot z?}0tGk;2L@84%942n`PKe*`@Ux?=?&_49gtGi;SG3cX9kj2!h72Dz!y!9Yh*3cvQk z9x_??OlFJQtq$lb@LPykg#%m1u`f+TqKy#tFOu?Dkm+ULv4E2Rpa-c|n6PL#(aV*e z5Wu>NW@%Gr69{-mXA^$%itZ+{JPwx!vdK>F|vh;@dBkNCHnC`ZDFi2&$kLc z6y))nFLR!sXHlG9K&sT3sWHuP#MiZ<<$_xtImmCASJ0|}qmSk7nr3gL@ZpbTPdU$& z>PP51Y0!%^Ams72->P&vd)xK&$ww%Uc5qf(e~XgC)L;KPut0?(InEcoAicz;jfgK; z(UtAbH%J<0(}ic4f(RZtw6w1^R!M%Kg?tKw5zVSG29D@9NsQb^|F@AYfYRk3#pkIt z1NpJFi%X_5g7`lCcHH5JXP#YK_<#GkUY<(_@-TKMP|d5W5d7Cye|1HML9>@j5oPe@ z=Izm1of!6A!e0pNiTHmLjPLho8xPH+y==8>w_O(;Y04dd6;&I2ue*$d3ji_S3Bfy7AdAYEHj(fY z+o@Ujn!O|7C$p>1ToX^mANG7U99$7QW%4Nj@_bt;2fk*uo*a8$0u3~HCNb979@*MW z(TjW(uVc%GFwDYRj(bcrUZkbDIw{LL{-N_HNXFXbgZ^_|$_1Ha^wd;oEtee3JGL~j z)oo0qJudh!YpwVS_FYD>h|XYW!2FnbthH_a$0g`5;f99+GzZcWI_~&btq5z;Ax)ey zAXek0i}~l;R>c6uirM}ykc@}7zN{y{T9QYs87HoEV-U)L4>sY)4~ zzt4YrLVKxdNgJlg&qwP~Bfj|x{QCP2tepe~@Y-5(R%T0GMh8Izm2}%{tVfmD z4VBWvXTM8{Xt6U>$M!&o~E#!hZ2@8EyIqco&0@Y`c z+cnKUC)Thqm|VyF!LmwGWi^xq7=zaucKQlf!9 zxEo<^{F2 z%V4OD-mqn6psuP&ZsXsjR*<2o7TB>#?91%yxjHKQ#8YKpN}6SOg`PFpNjs4w2cA6# zk7l`zlvEc1M7YQF^2X%I(pw$6QO@8azr>doUjn)5u@MmMjT=NlX>mpKz!5T}{6j>W zh@IIBD!`d;S4rDBeYS@I512akg&l)T!f@zd$!D`~B+QHMHT}lawJqP+GhTOKG0!+k zl$!q^T7!>02?A8ce9+}*JB~4h9g+toKEux%(AOX389CiE?z-K^zT6}!8YJEN^w}-3 znktu7y=0`HoeVnZ$r{7@N`hH@d*yE)%h|$IRThW~VOAP!_QC&vJjw{yt?ItK%p%dQ z(yPUj>Kol*6!orB3o{*jQNQ6RrW)Q`8WVSVG2-Oq_QyybqWnMSfj;Et5uK)OgSybX z4~D%p+wmq)WtJGrv$m^Bl#QGVT1Yt^y zh-TzNGx&cHt8Z#!sp-1>$R>zjSMru+ND-QGx%exXlZY6=SUf>H$27{VpzHJap#Qvz zeiif0(-3rm2Pkyg^92mnbI1Oo<%Z=N6i+o$6m7C~nx27kde zx0BSuHl0|Coltj*i8PIOoVCH!d&_g|*2=|(^b_1Q!wRTnO20wa{9mf1{T6s(MEP~> z7M+`3iH!o_c2PkV5n3F|UJvHl?mJi}k>mui{`Ay9La%N)4s8x3mZ5{Py7$a!z=%@z zze`F^Svcab9c^Jzg?qSIa~*9!$P*%42;}I)Z98c+FpX@@*-`7%|VbU zb?{(&SUe#bho~O$OPJxjoJ0&n|DS=dFtH@) zW)1$2fTZB*{YO05h!`0Yx?J#5Vmv{SQ|OaHQCNr=+5U4^LWF~bg{2phV`Ly=WdFYv z>_ki~|JP<@Bw|V^j>d;zC1Pbr2r$M2W8p~HZA7bo&R&-UV`ZpcIKdYFuWY`e2ED-f zpV$xuJ;eT>=+^_4$Nir`_X1sK`k%P10JWtAWlzyx0;LuC|HBf|YiMc_v9Pevu`>~| zGqcmNG7;Ii+Sm~3{%?l#Hikx~Hcae9+C(h>$DNU#osOA}h?SkWd4360@5g@;?N32z zn)MDr!%$HFi^29E>0$Vv3p+C#9WztP`U@ygGuAU`11J(36CEcL5hDllf881BIKuvG zYF>W<`&ACqcjz*j{ktNfkeUgE727O8WxYd-`HAJx_w%c+z3$h)U|q2HrwclmcH-1T zQb#7XMKVO$xz(SQKP@j(lTQow7Zl9X-PT01xM(e>ji<{xqa=Gzx$mzs?wz~uH}AW~ zonfi|9D82w-AMrNzesYaFnYM5jN&ZO7h6sjx*Fnd_q1N46; zQ0AqsBc~1{PVt7tk84yPH$80*nO5^&FF!n9%3C+Upr&CnqwXERHyp2cukfBJ-ILzA z*+-pysJ@ZE8FGgChxjM2r$#l?vJ&cze2tZ(Cbg8$8O+p7ah&1d?qr8BI5{DQhR;be z8pq}U1DaY6t3t1+AWqkz%NSL)(OIL355da**#@&$r{eiE+tOxp_BE@>IvKIzMMY~L zu{!A{v(mMe+S*=2pEV_VoNIg*?kL<<`?15K9Pix6m`7P?y!c6tISty?pXoGgrH1M9 zg^fjXW~E+&P79LnW}fv4a}|jXwt1RfqrX@ImGw$QR@XTey^gXKE#{!l%6r+pFPX^z zDC+%5g$kR-)k3Oa_Ai&bH7onF`i6-;H6MQVqq_OYT~({yfW+4O=&0rtK6UFuj~(BR z9HbjwA9^75djI{Eh;Z-k4fuzmUu*{Mx8vdl=@nGGN@B=q!?WmP}Z-2<=<{ zTzfYBJpDwQ6hsyZ$Tm=TYJB|p^ACF0=39ihKjN7#s3~G*$TS6i;45M8^-iD50Z*pr zr?{`*iE%xGmlqe8w_>YTyB0M0E^1L0=h`_m4C6(Y9RDc*dAwr` zDsOS%Jl(zNWpW+y!LA3I+dmH+x;>8h)`4PO`r|t`RajEm^eu8*y5iUb#h*$*CMvHv zU+Qk^Ilx{CsE>q2{Q-WWgvs~7e8|k~&su+;;iaj3rL@Ww{JOLL7|QnugLS_4y-#=g4~a2pUd>2 zk4R8^bzP;|@sIk=XM5xxjrKTj){M5)KT~^#sTkm-7%4=HlT0QCBBEM$;K;r)IDww) zu=G}T zb3-FNR~IXqkwO*NMxxxtqluDe>lVFSQhI`!>{Y&O(SF!?M(o@4Z$2r0pW-Tpj9%Y? zar!%H?2fAZd~iVObkSWHx9$EcY5zxvI!>}m5pF-WLu3Fo~)sHuvudcVok73U}eE0xm zZ&f{?hWv8i{I$3&6pLE6V@&u%%2_uAS)~asg5Mp^DAR^zf%U$vE>{*})jxa_cR=5- zNsxuFTM+vSjrHE+=H>Yq))+~`@VQZVvRF2Md=-8^YMp_KKVNh`n%0d-{u?{D}jZtiNHRt3t zOkb?A^6+#hSIu27oXGLC=ZkVx6ucFNp?ihcNz77j7Aq>x<&3GqS<>cbaeJt)J{RM5 zcXlmgwHRsS~ADEy5R z!!q@%xy6@W!I7NLWf3O1;UlAyO6!%V05tfW;8;wImsk*)cTqX&Aff|?dH<|HFC`FX zj9I^<{1dc`v9%%=I)Y1REdraEt9SSrxit?ktll`>Mz^n^kMx`tKtesT89+($8W;b9 z12ynrB++Z{ACpcxC;h^*_J*|nGuBKx8$Jy!h@J)$v%Yb~2tT_z*)`@C@v!{HckaE- zQm$nN>7T8L&!&aCBhT=)LxPi)0Z$I<8_Zrm&h~fM*ge)J+f+oYd>vGdg&;j#=9LT( zM%jBhej$Ge%UiuNIyN#tI#^Y&L7s_eO>&t)_@hj)oEp`Dh?wr;|5TrG>l9mbY7mQF z&1?Gt(wrnjO7rFqyaxi3{*4;clsV}^o&v{y;8D&@+vQXt>psyg9y~jc2Z{sI*G98x z)l4aZ&Pka~%v(hNRG8AF{=8TEIS~Pr(u5!bd?Re`mulptfoVK5(wz{#7T?3~wGU@f z4D}Kf+1Z+bFmUoRtG0Hr|{{%)2RQP)%P9`0&Jju{3p6FSWdpj`X( zf?!3wj7X^JCKt0bcEd(|*_5yjd}IOQ-hV6*)vBZn#Q)4_SiD^?-yZ!{F--#kl@L4P z)N`VSeRpAg`AL)nMJ3VG-Q8~LBf&4ZsS?DseA@9d^q`~GB5&PSTf?U~IoF1~prRG- zgNTM};;_dg(y?NLbP7a;mW=L_}fm24C9>7vQS_Nim5`;>~;Wg=!2bb0)dNORZ#X)@7h*q80BU`?x-C^3?*F1&y)jp z9Xs9Wr4}E|*ehJRdS+HS^Aj+KHSH3oH2M~2*#MWAag@IV*l4B39V`&NSe@t;Gs>^) z46gum`i}VMY~of4 z;rvQ?oaW$%;E%ZL8l|SR&8HD^{O^|6T`Lx;B0W7Es(w$3qx!q`;Kb#4OqF)ho-ELnyP5l?2YiB@+?A%vN&dBH0-5|XG zT%2PiycquPf=!A9twc98j|r*bK|@fqvsS0QwXEkGa7dw##+z=){@m%?0Bx|1`@(@- zT>c?lTVX2}{Aoydl)xwP6!7}{7Fg^dcHIwb>00cWqzW}Ri7(wVWNXF7M_gZ z^7nrEtLhbNR*skPh>lw|wTTid+b^dqwV5Y3EgCl~nG@q`6w?F|GyYDv%NqMNXGE|8s6^>M(nP7!tCmHBu*VvY;uEWw18 zTGwiKvotkMCP|G`8#4s{tR8o?E(kW#mWjsljsTUTyq$Sd@*JaL8S`Vg6orcpAo?() zL9Y{yXQxRc>jd@BoiX^6j|Ks=r}0YOalfWEHE-MK8ov;Yn+-{N<>eiYVpzgi@WhpTlH zo&QZ372TUuUk18b3@*y1hM8x5Ne4+EFPua}1;xc*Y~_0d8+dacKm*Rgk!%(LMK`zO z?+W%BJN2UY_{h*jY+e+vF> zu&ZQ#8I|R^s=VvM_Z}OMj7lGSQk+CYOnzv%z6R)qe6S9Urh1q=Kyl|uZn!(?VE!3o zRWDUQXGQ)Tup!hhR0gaCVHf#2)&Hhmk0ktC`k@wII*o-;n)&GFbpvO2{Cys%@zx(W zqj0RiJ+tH9@>l9*0bI@r z`iIYGKRrM(gPzV}l2@+MAG9s8AAnBN8^QsfvUfUvYvBgUI|4|?A^Bbgc?9`}W99ws zFaYb!h4Qugjx!>V>dpW1X6Du`GfSB^P(In@&e0o}BbrRlRI+LEpxLPjJ88Hc9#7Cn zHdiq&Wim*3g9vAPEf8< zTaP~{FgC2=GXm(Xz3wbf^eZ1<>@>;um?GE|M~hr657{=tf^85_{sY9diCVC&me!%n z77-%7=(*27X`vKADKna6sLR$Z6;kX{X~|qud-;42=wGiOvRy8@KAXG!mK{P5Lg?rX z#Ak`~)z~AV|Kx+(pg@-%9K}g7T{F%@LN$*i&*xLdX8^2e()l3 z+UGNh7^Y%rFOcmVy5d5NK~yG1pGW?%XaCAHiYml|edSP8VDiXx1mC!4LICW)q*JErKCBhEW}# zOfsm-c5nLJ1+cIB>FAeWZ?y|MjL}1LgtKMQ>tuC zI|OKO2`bVQKv^~#mVh(iruou?#?BK6Vbvz^-*RMUI(Y+2Zl=DudQ#UeoG;HIGIRjtb)@|9u%AIk-9qsSGbk+q*f#=_{d7}EoJ@aLK=yJBn zg%i))7*V-b?koWAG_du(e8_>J?14%ULU@%om+Jj{X%~s`J~d<_C@`|BZ)sUF3?MN2 z{%`e(69VRsm-EA1-aqEzVvZLoV}p}DjLkd99WXB_{y`X5t`aRNl`T{2|D;M}+ro4s z*R5uR{dH+5A z$DFu*HUcR~C!waAIfLb-7*~vADS*~e*zLTsaniNNNY8`@`P%jqWh9oP$S(TYn#0Xg z@&Mz>G1-hV+3&4S`31D&Am2W4$}30AoXL`9A)fOBy9BJE?&L+Ae7W3s`f!m*#xv`?uz3|eY&;3kYKyFRND=coz&g^$Dr<``3;oB=dbQ0u zo3DQQ=A+Lp)1S3Tv zg!_F=u4D7vZbP1wo^=;ijsIuF)az*_#BT|Q>x~1(O9XubqyTW5e*8o=HMO4quL#-hr$?(qs*%m`BL`{dcYznn%-Slg`!NJE1WJGRJ zDt1QhTvMLmy zdc_Jh&GWVFpUIxlR&Oi@lyqZEcwvh@T2!LVIEY{1sKf8|q>16EjrWvlC3G%RNY~c1 z*D0HJ2=5^y7t`pwMR+2{w9M@v+cSQ#=)~mgz4x^x>XM zBi_+UnmZh3k}M^c>- zQu!=Bwn1+$SvY@(ke-JkJ*%&pGN*dOEwvV}WZzk~!5r8qHDs?(TO! z_S@!SgI!urFWW|a46P3hXn+rp6}~)wFf)_cm=UIjlMa`=RyKnQ?4V+4#-F z{RmheR>=k$zLn=|eA+STH+_}O?L1+?fSf1K$PsWCg;R11iRS$N?x zET}Lg|C!?brCM3mkWX)SLBrShkliK)Z7;WnJJ$8JT;k|u9kc7UK5zA1{TYi=_|%Ef zTJ{Is332wj{LH0D-Xp3G`{1;cFRvy%Y&#EGfUQ8R74(5b-+aZjrB$n_)H<6}n)I zc|IWR!^-9P%%#b#k6^ui)+$z`zuWF=nKFHe@si9T?d(cIb+R{8!KZqdeSS{=^h*ze z?IY)HNPUzw=;^fD6lXai}ok?Z_Dw`cMYZlTVEbX5!U+s+IQ@@Fc#xQCCrr z&-9RQ$WbA+JZ3S#OCx;JN%^*y=jr4JvB`#OaO{9@-hz;ndawD>z1_yS*>f_o4B0{w zVST$+BKn&z;#S^?ob&dcih>Is+s?+`f2b~ME;+=hz(nB6T{9RiJ?ggeW_eD}`fhjK z)S2Wx)fOV|9ZpX~^pBfm3E#c2lxk(!aGg^jhx09`Z~36LEN6H#mqnDeMu>B!-L(j> z`@#~wZ&b?p_V@ePuk*yotIsm8pB2zx6IgW=K)v%kcI~RYzv-Mt)uP{5apCbs|A?D%rQ_*jLWGT5;A0yRapAsEVsU?!VE&64k*n@;Lkl zYogbVrq7W)L-C6e6XXeniBa<_*iisH8UcHw2XBaywV#{SF@RYFB*Pq5HUHt~xq;esIn|EHh~TxK(eB z1%=}EsGP2TWH_?L^HIZV`NlH`9!<7yXkgv-rjjzTWI{Pr-rewsoj9Gdbigg3`YF5x z`i)5BXXnmS!qV5Tl@R!+B4HmRJDpy^g3gH@eD8U0dMz*W_Bij1*E6pzH1DN* z>9Wdpv%#*jX_!s&gC$G(ka_<7%7W_Pom-V{)ywxq@LDHEd=GFsyV{eXak%nC@{Z4Z~FWMQW0Ok%F-M>jM` z_3V4#wcRuUFSj70{>GrFLn&){>UzNSgy7rS`pVZt)>H!c9OW(PKkXsvC|I5W(INom7mWUx_U6HN7#{0n5 zI44Q?xb-gYuCDC8yJ8QE=07PEZsb^J&1APP_T&f;>C-F~kL|OF?{yK7&{pW3_Imwl zP|k98Y^C-2(pf#W=lVg)?2JN7pd&V@?-DPYaY%KQeW4r%#PYS_{3gZPEo6^ zq?DbM-SsP1v@|bY&9KHNqNKYuleVZWZ$6ZFO4~6rg92yX?x=k+$o5QTxH6 zxG%qlKd(FTj+h#^S^}$!RCZ>bqtPDNT*nU0Eqmi0@l~8NQ^{ueJH|W}e2$S1ibAt> z<8Dgj=yIzZ<>KTIv-)AWVY|;+lq?T_!`Nb+&Bp$UX|J8;WDfFNbnz^_KcusE`@=Yy z=t{A%_88{KkXplrvkh{-ti<<+_~Swc3baM63Uq6}YucY&5K-QSIuy$JNO*soFRZsn ziV05e^IAbi4}Fd(H)69~Iwvo?aWbKbIZ^nSB}qB5#ydIhYU7BPaHiB2E-sGdg@t!_ z0~E`BV+@2g1^Hn&zkX=xz;oWebVTVoQ{t-Vu$RI86Z#L|mO4zEekrYg&Zs%NRJ&5w za-*!xKYu#^nJ5Rt>=3^%Nibi>WULQP64dKwoH&&i+ALqw)!aSFeodkGg+bkfZO)0q zU#EPpS7!HZzPBgqdZxIFb<3*EXjH(|*7LG2-)jakcSR|vevs+EK3y;wx9wQP1Klc~ z6EBXw^#0!V)O~gn*21gVG>=^)<){I(oX6tI$(1)6De)ULm%HW}?q3_&=3J$;&uHAT z?nILF&I<~7NWO=3}Stt<=M_xE#Jrw$Bpv>ACw-;%h#npx$)Rr7N$%3Es_*M zfb{Ys^-Vw2pP+oMj0iHPN`Buksi%LYZIWU5*3&kr8=Lu1u}F&qaZ8ygXK!sW4m@xIb%WQFjeA#;dxVvf{cwZ-Q8@mK)9TvHsNay1 z|MZH&^g)ho(t%=Ho+gXjvOVLY*`Z6)OPnexx-UG8Ay~f&D>}ZluY#eYD$Rarcje-4 zXO-2s^TI;{{Nym9#>QTBYhs2_x`B|jgHyRLkA~_svEvUWuBpe~%Iy$y)Ez$?VQ{)I zd?sYm@a)5fUEah~`H#E1~q~AAw+0nPfFuXPAnzeiKop#B-7j=tmtb`=8Umq0q z{Ccj;1BpafcKOC8ZPl<2`>o%^@@%DIuhbsNF-(fjleu177+Q<6E-IqG&K-K@ptCe) zz%@qgC5Bt;reU_cW4(3DY}RNTcLK`bKyJ8Ht+6#9Ci&gv1eCt2RO!}F;nu_S8|wX`3&lP7PgJa;_sBYZNS+|``vz_;g8si$uIskU~^tnSiT_9fF4jV87w=rtCj zZ*4tvophIBaQYy7Ro1O8ji!*?$b&)Wg4lgs31>F>Y-R0WeOGMubbNSbtAOXkL{N9Uj(n=0t(d-fv#qIIc{7Y;SCe%Q;TIp$wJsW(%1t9Zv#>)r1-&Gww! zcUEM#(6l+7{0zEm(^-AF`V&EDM$xbQZ%$XenmtoKwsVW}de3-?()eo!;gAs7#?9{%NVz^7O80hIu>K{=%Ww zyRH}Lrt2z2VHxirCY}8JO{q2RAK5b6PbgVim^)GE_se#@x40S#N&R;tGWN# z=<ckP z1(iED&Z^fn&lnuqe`)^+eSFNf`0csH)5`)UZYccl7_QV*{HSXaStyfC{4}Xu^1OuZ zL#S1oxPGrTHkM7JjoC&grz#-n@Oz2zAj5=jN*8*%_1IP;5>t&Fwq2;LF&)%wE5UBu zIQYDs?o?iteFS{lWp`ZBO^J&d8pUO6cke3+v^B8I$X2lms$mi|L#&6QGZP&81L3b( zk*8UzAAEBlRM)u%WXu3A#w5ZJj>aa)Dz4r0qz~eqoF8|=2R2Pm9XnE7H|Eqk+!py@?#_f6Re8Ie7 zM|%hvuSCNh<9fQWzQ(E_*-_gJ^@ooJXDrUP+wR|AD`=c|BPMm5p~gCU@;2p!Uw@t{ z;7757?*=^PM^*E{J9yKL#bfpsV%fij(K~9WW`#OvhHSMyBF1}y_udqXtF4@;oT-dh zDJu6X`Xq|qariX-$NKoj=;Zq3OWDVtGvY9xhuXuUJL_X_O^>G(KjI1GUK3?1CiAaCHt{hB{kv z)ncl0jq07mcrS~<$}BeIw1j5#$D@JU^2H4fYM6FfpHfIs6?xCr=w6n=mh6eoR8?ik zlp#fTSCWDs-N+4v_cGc>USX;*PfKeRi3r!fZX?QPa@}&16`s#X6e7q+bTJ9h?Ro0t z&#;q;Xm#E{`EIJP>tJ&6xOT2t@^SEN4g*R5n7J8Ue>p=o_LjrzeZIbTocF!k?sqEt zqTKzIWOEvy zv(kI+iM)xQ>!ZY+Ck8t5%&apHuTN##>x$X-F_r?Q{)JM0;ASnGEps7V-&BtibqYL;LcaV+PiGePDfn{ESxvf-I?^D=8A!Y zq)qd1X(Vo}wx{Ir_xWg*W}@MKwr=HZM(tf2V4+q)du(5QjCg1MBTKjD9|#RI$qkzG^?IB&-SX+>RyrZ2y6d9 z$SV9?;-H~MtMTFR#M8I6eQIiF*awziGY{W{*1g9K#8t{awp5vweYjHk$vRiEnO{Xp zx;~yi()`h*LRqbq{1{vB7d38m7wa>xbbsMnB)_3cmR7s0686iTYG5buV z@!C7i0oyW4?x6Me16S`dzAfu}_P(%tjQyD182mClQ4aI@h~lt@m};EfD`9~f8}IfG z&vLrkh&i*q$h100+VI< zA8CxfGS{Y3xlOHXMqu^iJubPUn6%FqLtWUXbTM6Ctzz`E%h^yBo{MMo(a(cU7dTEBE^3rJ1RPIniz$Z^ z(mLN#8s|u+-?_j~mOFHG^y}e?obw*@F*e*ev)ZS>>^`{t2_bZV z#B}5^J+s)0OV1afXSdXQo_*}y>lK;2L1ut%H|k6^hc|D6YJz_;(_PZHex}d&a65IJ z({Z6!BE7IS0i##4Bj!6!o;#x&-fpqi%iZP5y3OiJ`t2c&OG@2Oz6WxzE3UXXjjG5l zYfbd|Tfyy0?F(e_xlYxUu~?5;mx0w}E>pJybXD%_1%d({4Lg|$lJ+ad;_G%;S$?iM z9d@rRP4@9E-i*xW8#AA8`++U-lhvu13WH&KyOV+Hi@egsh=^&{>}rZ=*Y}dLrysVvwNU#F2rg}~GDz3(ZDNQp zIO@4A`urKAg`o4}aurf80&T5JDScFfz0^{##qz_y^Ross-jvg=&|XBFXVx{p%$lkBoh9q)^S4iTr7-H1 z9;@7%p;v-mJ16hnrT=nnUKRU+6fMhDXZuaYZ9$DPFgP7mSEuSDD|SZlz;17=GiTB$ zpS&xX$oj$h!9kZKCs>$;;r$$28*O4LIaxx_9~ixGKNuyvzw0&SQ1*#Sjd3zJc`HAD z9y7EOt{oh|y;zG=dcoR|LGLZI^?k)gG$r=o0fD(wY$B&+IrKOC27aqkUs8=5?Lw;z zHmc4Cmfkt*x5X=xJ@w9ovAn+c+$1?|GlmyWKTJIwD#iOZVeY(mm0%0L(~rNmS`~2A z^T`o^5f#4pHSdSa9GWo?3$KOljP+&QC;chSp6;mtWKJ)uN=H0n3JDHUr%W_ViWt+sYDg-(nP4j!7(WIj!H044^MkNDA6GGE1+ z&QA~CeNg(gieEJIXKa=Esi7KCaCVyg$N_nCPF*1tsd(ipp{7wO!9hDUtL}NGv#u3a znmTZO@=6y!cwDlCYoI?--8JsGzB+lbCf;Wu&|GUgEjo2un(b<;vi()8o= zV(Fb*#k3N4I-PL8CAiBwa(=+<1@C^fcb#GcXLS2;tXw%(hSPoIF`j{zdrSq2_SunZgnO+ethVz4x{E8f@9J@I6FD zSZ0Dd|Hr#7O>cJovk`meCH8%-fiJG^nt$|mcahC4%Bck<+bI(!5t8-3`D|ybz<$Zx zFVC`)coeFH7K6Yq+O~@NkWxw9qvY%C0yn!T{n0hs0)t1Pgx&#u_Xr=Y6!Fxqh{8}q zdC6m%#d?aJj{Hw#1I|EFP{Icp+$a z{HlK@yUvl^Mc=@8-;M-3l^EWk=Tt9@T;wb2X}8t--ZQMQ85<%Zd&AzUH)D&aj6e@h z%3a_4b^9_l`O$4ZC`{sKtmHe$+j{d*q3H&PXD9FS@Q}>$8SvHqgZjN8^LESa%N0KHO59!Ix2EWO|~9}(nZz=FPIHUcTn-` z1w-jO@u?Pp7)_B$cQv57g@C^r=%M=*7gZlrytZ#7Q7eRUNfX7hh59Ds=M55p zj4orQ*$(sW!mTj(XrTFp_bEOf-OW=GT@ogEI36+%-#LT;>^ssG2|NJJtA zA;S~NRG6iHevc!e@dPwNhQ|^iQyZ#G?9bjIA{HVc72`>G0-o~R1tm_8#ZW%F zpyZ6GPfz|`jRc{oZ+NJm{|o^U&}1@l9D#^NBTq{pV6a$Wt&D^`9R`a*)j#W@fex6)gm^5iS@C2n z@+1%*izd-5NX8NnRzTy)BgT^;Llf|r|D}iaZy^REl8|`>LYIJy1u%{b9#s9a zAcz?(21^ljL5aZB#mR_GKqNBZm%smP0?2R##5!OufrOZgCStIpzg-42V<0k~j7RQ) zOa?F8emeB`p}=Gu2C0OIAt4t;6A5@MLJ4pK8VML61kgmpIO^O#2Z4V9Aeu--BdrP2 z0P|1qQBQ&e;f!!2kkNo5buJP-fsBCk1R5rh@ibWkWMqUAG#QOX1~ZyW03rFWS*bES z0#nccT&b@Lsh|I13WEly31H)={eKHV5+U&b#1Fu=eVgDB7E$vGX?_fv zj0ex8{@V=vtNs8XO-;g}(RgIg0EdtfUPwpP#cMe6vIGRP?~?6 z@RtQ4ERMF+0+6LSF_!Rm1^?-P41^;S5GMgL46?!j8JfoL5DrIcY8;+~3^)h}N*i+1 zcq34%X@nRgDq;Y9Vra+VXstj1p-Ex)LWu)lquBv%!NLGaK|)3{C~J5cWyJsEK2L&#_aCHJqC_~lPf8E6X?;6F$=Q4t@x9u5b9fofIY z-QU55!$UNa0ZX9q2~a_k5kQ7SM+}aDgOKS7Y)SoFCiU}EFEzR_I6ypTc1WfL1{|4) z#Cb56ND~Wq0A@(D;{miHGXjr;U>ahI2N-~iLOhNZ1AvTn94NyyN{D16xd9l3hkogR z|Ck>n1de7hnTA+m0P@qA6%Xhva?^lVqLJ$n2#5j$?2jRUlt7xF01o%JpQvsk5CKE{ z%XhzIw3Y#^lm^X60C17(0UnEmk}#w2|+W1Mk*$QqKMoynSdlJFd7^U^hXFKKt=!{wL;udY|FK&L2Z4KA zk&#aAgpdUW$nY5Ci23nD}2Q3VZ4Emk3|D`Oow?oDZkRdrfAWO8D7@!XQBrjC^|299h=pao^ z?c|YY2Cj^dcTo_KA!#)P>Kd}ef(T^n-&pa}|3FAY5(XecVm07*;6LPMfQ&{l5e<%v zupqcx0>5hVZ!8e8FcH~6LPQ)Ed3gb3;3&w+fG*Q00as#33xckfCQATk`c)~x`G1=q zw7p282&-?Jp}>DWWk*TxKTnXCey+)k@kj! z+I;>&xL;iokl~OV6Ugu|l0*O@nI_Om< z5DBm=r0)RB`8!&v(F1N~AR2Tefg2TMaFIab&?v@%?&9yw0Q*CrAEf~cz=miog9nBC z@5$7;1W-?CWCS#=j5dHtL<|A`1BE}k8o=sk!27BNWiH7 z(<}Tt`hk!px4|tJnF0l)6b^!dWQVsQ+k*OlwY3JbFO+<$i5o-l-E4v1`LS6rNKxK9lz&XbI`nxCf(W%|&x1}jdtFV;4c)=z zKqgWBR<^Gy%O@&DxuE84qlg}~69@?q6iX$JQqv901Bvy!!^lZB>Rwa7YPY(4Z$bS* zfdz3|buIciHI4u5)Kn%s553Cvj#MW9`}ga?v+5F=Z{YDgl__B{=$)n6qg5!~!166* z#~|x|pr^<0RkU(rQ!A@Rx$JInJ-g%j66)w?l6X*h;HLj_99yVTzpP@>K*QnNakL`= zV>sBTU_4Z54w;;h_}7o!;n(i1%a+B(Gwr|PNjAxp6&mNwr=iuAnSHt%taHi-N7#px zN3}#}%>c`?3t@Pr1r z{Tzi{A-$Y3EK^mccj5x}79~=LPpGhYRjI|}3l7){lW1+6e#U|R*`$v~@3%cc9eApHuFRxh(}un@n1B7{r- zw~TS;;YkLu?rT2wNGDS8V@)b@B4mAg?1cHTBbfY1a6Pu6#idA3SIvpQvNQ}R7{-0W zFOZ$aazuX8rYJ@3u}i)6#s1GJUHP9y5i9x*nU~Z)QuUJCi^LU>7F5BE{Pm?OUflw= z(ZIvX)~&PmP{y5`{U!O0!vW$n&7$nJV*{zgnfKlRwtf>h_2%A3X*MAjWI z^&WQ>Jr+4~Yk#oX$!i8vZ>&4brER}HSp$%YBubl?{%^34mro{5AdB}q!jGrjpD}-? zLVB2Zx~?}dH#I35z`uqMT^ROO$%&%QbjQiUl?iicp-OdQd{&UnxK;|GK8E{&fcJ}i z$e`*D*S6}gg=sE#}?+EEbB67T)7>f00(IAaEn5n$e+Irk88-82Mh0ej$C0w&cpkSTcTs*ouB0@}|lH zdC`l47s>%qFJbPhlB{C-+W0TN4WQBpA~Zs1+#$fdd}K_S=E> zd<9Q#!BBP9KPH#0dyv|J_g*z7o7|ng5lZ!0e$a+b8q2CN4f*OZgB;8T37FteYjxXn zzqALvk#VEC3A%+A9>l+=aSAiRsvqzSX9MfI1EGsE{x$OD5HIA*fC~xER%mXPJQ)?X zSSekXJqmd7fyY0ng!bQ7jQ#6RSEQi}%BVfv?LNbLv881+_qZL0q#^}>OPe(4j^055`)g2{+#0BWhu56bDv$5Y=ZB|cIVf-NHAoA%3I%#D^wpxFLu!hxhycGd#4 zr=Iw%Pr9_Oj#p008Spr{0H*-z>X+nZ1tE={Z-<6KGjAU!(RifmU%_ueGbV`6JZxc) z_13w}TM)zp`Cv!>uBr~uIW9~EGuj0{mFQE<&zMT}y7x_ER8R<|z+#R2Qs&_47V!ju z>(r46JY#-a!E8eSDOnWEHH05=nCb6E?{|aGCciWfoZ16n#EDe?P215NR!(WIr_#m@ zXMLLmED)M6K7>~P%fzr&vm#^-3jLjto{L(&-L)1pe-x&SNJ_|RgteH+{x7ZD*%rf+ zddO6Q%W%gK3pogWk1u<_HDE33(U<>|Qs?AVvWf}XK|DDIh{lX|5zTJr;_Ie>NpY&> zWS&;hNx2oA$i(=S%l@q;S{1JHZZuXTkV{hf8WO@xTYqoF{>W_IeB83twcK!xk8`C# zCSZ_Kb9-b);aiFktBe3LIf2y1{A8@CdSC80s;}F4Vk7iHUe~=8Ayv^MT$`(eR3&Nw z?U(KBXQ1&1SiH->pC#-U;FW~Tv~~{)A{ID9Yy!y*$P!O^8DsO>Qz|qn=NWexqk0$zJAb)iwHSJkBQqKFJrg@KTSNr|UuBDBq?k*~jYJt$!1g9}y2po3; zM|?`)wMLpEX;Eie!v;jW@8ou?oBimZx7v-bs2=2O3^G0ow$ns!t~7ATgu5-kb9_dktO^dO$jVOH_5WQ6HHPsALxpA1Uk4dpKd)i6 ze`7nf)$yi+xidRtNH3gkhY-sgUO-UVYQ>v$0f$&zBnEvM19D&Z>`tJ?i*wf5a4cDcZ$)?WepZtxWnbc}k%Gh+GfhbUb zz+milRL;-in17l3UIhNQTI3z0p4u|sgz=rV$?%-iG4)H24@sA;1mL} zYs~k_S4@qG98R~cS=oByghOj!bfI-sTsS}M>9`tf^m?e!B>B&8)biU}Wd^p?+jDzs zP3>pcmN8gw13S9n6-4vF`~)e+qWxunC9nDXG5@@LXc6YeB>&uOAvp+KArgNKjLLlL zhr{K(lZcQ*yL*oWG=+SD61yqdntl6u{ptdKsy#<4jf)Zzl@6?ewebRiFv3j_WxkC5 zgi5_bZm5ZYa@XDDbR6Wu?`R;xUiz4a;0eFpOJV?fo!`f5iJ!7AkDV^NrrQUIzT+tf zFiVN=1v{#u`-O&Po7v8$7`U>e`ndTi$0wge;jJqYif3`|f;Lsm<4i3MVp~qk(AdXc zmIFaho^a0^Fnkpau*TgeK4WFdTGfVnfI~r81c7JC`eeIqA?e;4-Y0kMvBe+>(OlhN z`jx&g^GIvS*Nl?d86zGKh(!S%D7|vvSDC2hw@7L4hDyx60_+=Y@WF;_Uj~O21 z8H*M3wBcwbr1A)%=6abhVPX_t8s(@xqZ*_R9UNxe+qQgbwzt>;K<~SG; z?}AAEZMS-LZa0z~#)#!bp>ho1Ip7jMe}p2)jjocEhGV?=D7H6DQs8Vzvh0pZ7U&Li z>8g^}K#03*>faKiv{V3?n@p{Jl~^RyAWVjb5MmOmWmlC|c&~ADj;Fw@As4jRkFOOW zMP)fiCmVY&*Sl*RYI{U>XS;mVB-Db>OG^8w(=t2GpA1=$3hc12NqZS?VO=>Dq(4Wj zs(hD7T>c3ME{|?}ec#P{Cr@=!7SRg=sIR`J(N-Xi-urD0Iy->k$xEj|XFwTW3F{Jf z??`N&NscqY>qMkn!~K0`u8=otZiKG~CPcrMepKLYO-sL@Piu#SN`BYn

vPtA0yp zRTa&Y^TJ{#+$ZiB?fMTSS6x{@yT9XqU5``Hg`7mXH z-oMHuD1T79xK{y)>0}_ZEy#Zd&AH~NpKYkL|E(V3icwCc;ApgBfwiSSAC|?-;7PgC zuc$kB9S`mm9(ko3b|gQ2n%Jr2+k}=JM!Bcl$(Akuq{P*cdBPoysafCrV%CIFFm|O^ zcjDoigSG1X}TJ;9{jx-X8s$T;zj~R#AX9Xd5a)$5QWOhJ!$ORq5m0 zgWqNkkdn(~@)GW2n+zXlqmDcV;`bF>#yL#CbcPUZpfc;j8M_v2v}b0G!eD4uiN~I+ zqk1H@gfE^X`-HFHe<8538eK4)sr*KDCj7eH-|gjlUC-a;v9^X3wI(r>h249i@d%^Z z$%tp?0^^24;iQv7+Jf~X9+x)sd%qw$quH-uoT%`9abKmVX%LoS z)Ew(fF7fi6pB`r>Ij^>qy1E8Aou%w)AErbWZgh3w7kAoM&}wEjV#J;2g8Gf&e`TQt zZc}c=k6g?wq@c-|B9S7LQN+uT(~7^P(V(D;G)V%D%)>8I_K0FMDc!p!6j`FNY0oR` znki~whha?>f*IAU?5r!zU@E$)V&`eD@h=&3SWJe?+8lYN#x3LVS-em1C3xm*CBBnq z!+wWhBEndhb+fP5pmXa~zqTRywAN3hlBR(^NEPKl{yPI6GBP49k?|i?N&640@zGKq z!ao2-rP>f}cL$p7+6N;I&KN?5m5dcjwAf)jeNrl%=cp@pi5iU6urI$Zz~yyHFEcuz zA-$&K6Eg?VldBDoeVN8SOgw(L4Jr|gI%Pwh<+N7TSGCVx;U9K&^h#(@A~Q=^cAB-WqcytQe`+?2ALiv;~X$H zdE3XaC^l25jA8Ofq@DW0mg_w7Ybx-XF26D1`2Z|0qO0OMAmT-xcj-)`;?A>&G!(Xm z=x^(U;7kSK3Y?j@E3=~BG8H^lh|oUTCMVSp5}T&p?ghcfS1w_y zYP-TG9buVN3?h`>YyUuo&O;`vW^>$&-~UtM!olC=uyvm~)E4V!i79=Wi7q1abh^-U z0{va7Eh`|oES<{$W5IFwYBcnWtN0*u_i&O4dVw37oC^;kI?;jzc)ZRG`T`Aud^d#1 zo8D3avP4BJC1XZ{^rS+^)PUQe;6iWIpGh7w8k10-G7=Uvf-DIZ6|Q)G1#;+K)Dx4e4d{lGVpW5Uv6y_#H91ouDhC9OEIOBpVZC-i8jW5&J7Bk-+9u% z%x_zdKSpgqgUPQ{ScdYHm;u&ZVm59j*v5T&?m6Ibh<|h7-!V>e?L-f~?YiXD@}5m! zNV1H!rXZI`Q)7r3(E{UY5b87xLQN zeCSiml^|xB{Z{ah=f^r4q=?$n?^b2T`qXRpCvzlRsi3Edie#oK+uvCHuEU3<@u=$Ilig&nL~Bc_?u!&l zxjr|)go8BRp0Msu23CgoG?~&~rm?GDsfsV{vdAXu-5uo*-^cu9kq%JKe=A-v<0%ug z7>0)Af)q1coU~p^%uN_QLz(GeZb+K(^%eQr!F1ep%MOtLRWJ>$(Y>1NTEbMu z`09^~fgiuiE3xY>GotGKf^llVix0wuN)YREQR56LQPk~(2H<(%o+9|AV+y*Wy2HRj z5q)+9f5dz1k$)HDjcu}QCcbA&L>m1F)!G_@Y_$ifOPWR{It%i^`_tyk2fv6zoYGvVKb(U-5|c8vTt0Vin0=?)wFJf?FN3H1L$XB}Z_bEv?#ICt59)a&Ze{VVZjPnw?8-74bG z>2+*D;CIbsfTB;!Z!jN7QT5nyeLK;%Z{*zY$okP z2Suv;;=K|kzDeg(7ANnU&1}7O-BxIO!;m#K**OGo2tr$pj#T_ZS1kreG$Ro!OtCf z-ty)GytS^fXsv%O6lCvnaN^y1ihl{AFjbCijjy)9Y6E7~tpzU%))oT=8Ru4_4C75~ zV{(_6)i59d2}9NOgqU+G#6=0pAx%BfxJI5Y0nDZsM)6$Z2XWQ|^!2N5?p>^a(VD6p4^UHu83PL=JO@s7wJ|d45riyc?;S=yMTXrg0CR zJ{Ql!eJszmM!zFbI{kO?*{_8B3!2K<@=vO*;E6W`wpFbo*@89LU(0AqbDQd5ismYZBx6;qFb>fzCx zH%92kMiM>rSBawBgg!~X2pOf={#HpE%h)9HM%C!@8xA7=X#Xg8{b|OQ5gc)_EOKCm zwQ<f!V&Yh~%2ZoV|lGB*lSqX}gI)x32 zl=vMP49bzJfCEaLsFsTY$-+j$&XuUtOpw?g#RAF`k4g{5!JN2jf(2~4>^GwV&r#pd z0y)K;V!kL8O!J|fR;+R*=~h$O{10mg41Ju`38isKeyO2fmwJXCBFY73xt>y&GDNa4 z5TF;!4%k8;&i+^uqEp7t#NTzAxw)TULcO`XT*fIw|0b+`{Gaw;SE1GiE4u}R-uKo$ zjNR8A=aIK_aw!|2eSs)H(?IJte*Su({p@QS7L;GLYwl8u|spKor zP?34x08DOm#)|Xie)_mS>V2P2f1Z@|kg9G?N)SzzSY19nypCwP6;|}m5|_Unn+tX% zwS_Au;-pV(HF~%;b#w)(|4opzN)|QQB{Cx#?3Pinx7S#D24>>rlN_VPb*jo}CVgex z#HRgKw+$kHV5Z~W7MCxVFv(KXov0ThYdrlP=Bz(YC3t!#f0k(|+;1wGRvVNsL&+Ar z`x_OKp$Au}U;Zn$@_Eea->9>Kk1;Vz>R!9mxiO2l_NbGSpVQlnHc|GwgUwlFN4c)1 z#RaWAnZuB{9k4C0C`fKr;&TJZVq~FNK7Y|ivB|9A;`ko_Q$ZC7cC*Qrpp`&gQm-bR zRr)26;@0#im!L=FO>bwKGz5-Zl1RZl{_HS@zdim_G^V?e;jEcno!xzE%6XoDWsO4` z_2>qATdMZG^0NI0*N(McL--v6b@LC-ac8YY{j{~P9{~G%46U<*oKCemJLdPj+w>Wu zIKh*ZQdJAx`r2QQXBUBpp(4)zyR96IA1{d?; zqXN@#MH92LNrFC>UGV0o)nA{<)Ri9|b`exb9**|*YxYjZmbMnuzSvFeHFu644FdH8 zNo0HE;TU_%5#LpWD!|*z0{b2pCyoOBYqcjg1b}2LpM=6#K5v&dVI^Ru7Lq17Y_)o3 zmQ<+G*jhOeYXp|DZXyY{)9myZD*t|}-5^~abt^qy>d?${T})evor$l`@DU&M&Qnw_ z9zt>b3JV+fX?<*xoFZW3g&^b3S+Ym}VvctdD41H$OG_w0J1X@={CQn#Q3Q?jP#{j^ z4%ml+@ux|sES_M_?|ebuf3<#g7A!JJHv$d%jZ<+efvd(UF$5xtc+EfKpjuI+QpV)^ z9vY08kA8DwbU3sfZ<;%4*xFy-v3$=DI^ucy1`03@C<9ZfD~S1fQLp*8GwW^SCHWBG zPmeb&9uR`$(mvfI?|2VyOyl5`Oww{4z>h1GXk5#3Wme$qe@9fncpOD7@$fUMdK z;1GhQjFt!~bf!2lBR7Iz47Q6^FQ$>2$AZGxCli%|Y+x*tL}SZ8c&8-0!;B*ylLI?O zA1RyVk!CnyZqUV&fo&E=z~)RSm5|0ph*&@(wz7WHPS5O*Gg{4~fv}-SnV=cxTG8Ig zz?J4}##^d$v%-TAH9A}U$aIzmP?^qG!zTN;&|Hf&IWZRo?Q>^sKfrtjSwHVXrQ58I_Seqyir0VMhC;`?j#uh+IL?@xmp4V{#5KT@X*mF?D*p79d&!9%ST0b zWHqY=32eh_t#%J9cOB9kyZna(GW7A=&^pU$viRXNd<^VBipmn_#|qnn4OqhG$J^t+ zZ^~bU!#et;gzrBPz)rWW_81J!;IjaNN&O|eLgwhpv#^n}5bn?hEZBScPMNACgUvYu zl3p@QX?lV~?`%@s6H2MNy) zmjTw7__F5sk^QhnD9WZs1y64dP$HaULOoiYAlDe~tQ$y|xE+BPTQp4M091`|UKd9* z9Cg8Z*cJXIF7_a9Br}A%ZIWmF2mhco2S-j;%O7!%Ai5 zbhKQNYgmXWfTZkC($Q?ut2Hom^=B0-u{iUNps)!T+)C-Vs!s&{{z{JL znXd>SyrPvH`LlT-l!RgZUu%%54vUwbD5+0(Q)7q9QBS*4ETcXUCe@7u(Eo-uPV#a*>A8sVJ8gk1N>V(b;MW|ggK}= z2xxl`TycqSLii&z`McqhIn(hPKPA6G=Xzk{B?Ux&es8+U5*cu+5&i&ka_Wc37|*B& z=n1*)JM88~%bSY>Va-&Z#8w;KgFpi4u0@e-s0%|2TugsKQW<`SeI_Og_(`u)i8mCUzf%t~@}=IIP_Kq&idG^Meh?937@&Me5A%qwx36KfM0KljPw*9$-j1@GuBq&> z&~M~t<~h~mtvpn3(9yDyq6*455!FW9(r$Jn zRCf&lEyO9bTE!jO2i9Q$kW{32M=A<#=OHPv1Frh;16r!<|0mxr)#HTOPY4B!XSeEp< z8fi94ZA)o|k0=>G_hYh97A`rxRw&YVSy6x^RW^>ULhZMjsO6$A*;ekz*8{NnTQ7M^ zg?nh8J8{`6=nF-ue7}dYRdc6^fiRUrv9!x2E>H16jVrJo-l3P(C?XF#213j%5a)yn z1Y{d7fpB64acDdgx9W41sgV|NJ;Ykt#fsfd7D3|TxEtQh{H+EH?(Lj9)o&EHU-_ny zz0akZe|x=KHn&1h9%4siRBhN+LFukZ8!9fBeyZ4gQ7@^1cIbzrYwws;=h)G!(n!)p zh$Vh3X}TXlTimdj9AV!I|HhBr>IXTirZ=im@V8yn(-DDbo;z(kAkGaaLr}5quKCl{ zqxeA)p^+C;O`Y4)(N+lM43%6&QI2f1Tms!oF% zwgl;yF-^rem_a}4l$Cx%ToCk4z+D||wH6HC%6!e#Oz&P%KxHVB;O!ZVbzMd*Xsax4 z9Q$pqK{*jBisPxNKBEA@l_Zur*VInEA>kggV&^N1kqX5Wf{Urt8Jpp(;kG(((n);Z zrpk-95yL;3&c={SVLsn!oJYg)Gyca3A|~22L_BQyRa>u8MhIT>yYAi7>G%ozbsYVr z4^$}qTBZ%0Q)DsX%k|0q*cABY2jyS~%ZxV!)6MYG%GS$iXyO3wGpiMJDz|ph#4C(X z@>lMsFLo|PnXOK}AQ$ivQs}M4;2?K>W^TN#A=8)%ZTE0Ka zYLqQJzSF}HF!fxj3e18?MFIsyfQm<&-}T~E#9-Rsb~x?e+F3jws+ny(7imTQm%I&{5&HnSOc|caY$=-pNnS}7% z=V+z9_xhQIGLB*GgQ0XvupY>sL9hO#iZ=u>ieTeG3b!gQEa2uZ$Qe+Nx4YRKEJOhBaX%Yvuz9P zhe%5IJZrJ3Ml6L^SMWPqtMzC<5n4T(7+-DEBO+m(8KL`aJh_ob6Y{-Q?6|64HC)&e z6-A=wEmXTlB~0$~#ytlaS}&Sm>!A)|TqLV!?k}KYdf{5ELrDHbbhcyt#&4~Q`Y*+1 zl`+C86_Srs_dp%i>&3VP@i);N-g!1Ks<(Mb&6jsspL^l>s&wc~zX;F z@KOt{H!+AQ2g~7O2WaCJdJp~n2L2wTasEG=LMpF51ROX!GiTy;_F!TeI&xyJ6iRC6 z;D2HQi8m-o;?)U?I1332CkZo&G9nx-EG*M6c^(oLuK(NSBw=O$zik#~64w7u02c{6 zN8)c20x))-hS1zADKK`f29Hx5vH!-Fc>4de=l=oV7w93*|A4sxr~>}~K#Mo%I_v*H zQWdBj4Jdai!UiZc{(q@;NZ7gmw;>6Wrj|AdJ3Big7b^)D8+R(`CMX6GE7$+efrX2U zk&TmtgNKKanZ3nj8B`zXzhuZ~p!6+YhoGUTXx#tJ|93>@|9Nq-aWe9-rh31ElC-ou zgEoSqaQ_#^O~S&>_Fo1rMsD`d|JGW(U%^N#fP2pl;|bwS5yhlDNc5<7DN5@DYCI0c zn_!L)GY>N{VZ;uIr^{766nAlEnlx_QOzXryRHwGl>e1}(vg59EPS&Mta(s3L^4Tek z$8{EqTZ2VA57}PNldo;tuUB5%hiwpu!}pzEw=WG=qiYFn(?>@GgM}m!&G4Js0td{MfuLqJ&n{4xmKOYy-mo+C> zY@Z9*@lmI)kVlqJEZ?x-nBL*nl-vzL?wHVk(8Td=?5)B*pNn&f#qj~X&icxNam(TY zuUxvCR`Et)pl^efmc0D$(_8OV`-*x_AWgb*O1o|A%v3(x%ElyF&b>K}6;M2P<*d?f zUpRC&(>W(xjeg1~pl=v8b6LvBi6^Y@(yHdHa)3rZq!`5Ec z+-{tvS(l@XUaarRAGJ=!FMd&7v!=aVD#tdp$nLcG!^K83EjhYPm2sGwXRz%ow%&%-V z7h)1grV9)=I@+ANG;zj2Z%sqLkZeyr--N#CcgG^%8htTuPZRG#x31n2YfS3x+245k z3!BVovKOu`uFVEBz&cQU@ZF9A18)OjXN>XMe+Gl6NQov*v^g{=VnN%J1JE|Sy!%@* z@3R4yZ}@Hq{x|%MFq)TaMHny?lz&7g)^zI&?!wx#WeV|-BcMr6S?+tjvzDlYa17=q9J=?*y>}zgQF;g{w&#aW5cyw=^ z`d!rLJ?sWkRy+OA3-uO!3`GcqnmIPluf*T}r@3j~xC{YEA~i>KROGYas6-yomMmLy z0e{I&W90L^f~6D9)iD|(x^CfEb_r>#MDMd>ew}>CnfL=NPU~VHoHRG19^9B@MeiHQV&Q~ zS4S+t!Vj1u0HP-dUM2qC5o<8k8+>Nm9QV$>#bf3lc1~ro_IV#-N62@f^P_tcsQf=l zSw5E{Y7i9jl`cY1Gyw8=#{^X2B*|sEXVcsBIsAi5A2fe+{nQC~{?QeIiftQY=hR$j zMPu8Wyl!QNYx_H)OcF9lWz7Yeuful-i@$HGmKdAho1F|XJHX_IO(YhG*(6YBVn&M; zn%Uc1Y0byX2#xKVu}SdO^1%3$`TYCbOsdA8Ql60jE3vvxdK|NAjY&QO5!9e`6Zv0V zkzuY7J0*?DB%c{@ETbq!P+tdb2wj@##E7(`t&5Ey%FI}a#O)~z8mq&Koi@^%W9>c< zMqLG>4Y}|IifF>v)TQ=mPx8e03EH~76B7;Qh^>>kA6H13ORM0~y!YCjejb{r;! zM5^s;&F`w{pv%KiSj?g8`iXZCHVP5IOVXU9eBxF=gNzA?-v(+}B8$98g1m{&Jqmq7 zN1JHglNJ;ACkN0$d>$wa)EE$85hDzl`Kj=gg&DNq?NNI+dBDO|u-LKTrT0qEF~eE2 zl!})unobPdMsi=nQGH{!2{WSvT)lX$uccLEjvmvks!HO~Qf)g&TokY&Y47Gs{JtYi zAqbxw8psLmmL3SW7vLQ_)@_Xm1$Qgwv7g3CJ7v7%cBb_YaCCh{rlWkLL3 z#0UuWnZ$7)Uot&kTz67H`t>i(+f9~F%W2&* zPjrlg!Hi|xa6N+JF~uH4e%0E@Arm8WMu`V&2CdRiJwT>bSDCu_UL~x5HmdHMbZgae z1-V&8C?qlHR+^r=Ig&Pw1%o!0T>jYMv=)U;F;Z)Sb;U7~!tdb^&Z9m$`Z06LGL=wA zaWo(Z9KS*mPBOhnVw-;7EnAlL4hw6$Z4;B3C}CG*xZwuO>fOiEq>~E z6;`-x@m#xH@89F$d-@6jG8&Wm{*4_#%kwL>O-w3XRp*%4hqR7Z2#RVm7aDMdI>5bd zYj3࿍$Q;&=K&Kcg**(lY>-y?N$joy6g`O*Atz1E$qvL!E{QEgYjbM=i?6Fx10 zCE>|AKYKfH6%#Yuv4|I>?qnU7aKYauQ{U3yV$gAL8xtchm8x8=mX%aS(Zvc_OI9Z- zZS>b3l)e>-%HvY-AtNXy9i0mJ3=Ivrk0-TnT3?n~xHriRVJyTQgy~W*$BaQ!OqZ!8 z9f+qZGnQ#I`e4_X`Ak|Xo!jjGPz$CqOWg1-yJ#y7 z5VC>m93d;voC%^8b0(jtd8qcWZsxqAM{rxZHlRnRUfl5F(^@y2Lb?F|F>Nyxt0Sk? zAJlBjG*so`70WPD5F7)9@Ny4Lt+G3*@NeNOP4(F0B-%>_I;0 z879t8Xd(VE%H`$2bTi}6iw(G+ik{v>=59QdNTQEJ3Jlxe>?2pf3fSA){uVg{@AbwF z<1mGWd&TLnGq?aO8uNKfTYM>*S*(QC$O z%@(kR6C#=|bBE8^;$V8ND+n(6j+naI#+&Nm3d;S6VXb=vU#)9HqIc}PQ3XCEX^o4F zC~_lS0|ECS`^9-__Q6gFOZE{2z~S;@ zbW$k405m`&>7(2vduxWhnE~?)U5Z>5F>2CrTT3-sA(?hv=7SFyyqdo0G7~u@|DdiD z!vCUtQF12x%XUJwsBY}5-|d+ucEDE|Y-i%Zf2Z^;WZ&IG6rE6(TNRzMONMd3I`^S` zVOOogLe7my^o|Q{bb^PA16GtX!7$K|4JPi4ObNJW^xEOzCp{wffLWe+zAYuU@dqDtOegE5lNmBD5@Yw!a)RF_0QI5q>QImkZH+J$=X+Ftf|i-*z}i zelf_KXggm_gYK6LuveDnD(I)4jGAF6jY92sX$AvTz0BRKd!d?v;sMoW9CPIL*UA!- z!$l?qSdSVdTc6K(*pJ^FQO{jl-)G;}H|8N?Jgi=~aQ1;555xP1Pci+&@(8FgneT}~ z0o^sm#4gJfhF}eXtlc>V$M*As>0A<%SZ#j6jaKvy+z*mP(`xPH@i6Mg8Jb!bjC(ml zQ*X#;_IqWMJ}}=$T^rIb8JXYUWp)g6|8L<5*!ZvTFt@~PfVV;chyBmH)O6yM#_6g* zMm3q%7?P6Au_NK@U4rK>HUdTSTRUqtRi*uTtaNEVGsPoQtG)d%+vRFZkKyj`;GZ#) zBgV}z2^bw2bm^9daHrG%<@3yQv+*==_Z;#MrcZ12X$@*kdga`M9g9zCPw`Iuni|hy z$da9^$Z}P-j|qJTAf7AUFFFr9@wPe&i=!g$?o}`f=V!oA?r>()kcSxYeQb2qXr-HC zr{%{b-z`N?Kj*I;2sFW^j;^H`?fTs**^Bg4Wc(I zM|(nUFXcnR=7~s_sRmXqAuGv1$VR(Pm~#BaYy8!u6}u7&Ko|Nx+Bdkvl7yhqE--e5 z+V_|{DD)T|wNOPdoK~X@1kuK2P#7l9V5&Dk1{y+VPKM4wVVpsTQMWpL!Wwi;nRwrl z2YxX-l)WCcwOD`{ThzwZs;oruq~;8kek+8= zX60w9XQ{dYAiSykME8k3v~p0{;nkQ}=cjEuApuJVkNVcg##d#} zCxzHkf1dl~EVa+{uP0cmoJ|vI=T;|h{CR(0Q~AQ$N;{_8Xn28_O^ElEjLQoS%BN3F zWi#flczxrHb6ItHQ+xK>)$z_!5*!Y@6O6y5VQ_*2LSES4Pn|FSmKfhWkNGTiO$O{u zu;Hzvw8dyt#oEMeo_W!+kmKIcf}nzd5H1*!2HVlMKxvD=Hf(u;%d)Qt^8KS%NTDT( zSEZICzxBehITH_Stz=pr{0^EttBB6@2zI%ESDG)xUjb9Zv}?j8h!=(pXcLzZ9)_%9 zu>Un6nTWb0g>H*BvP12>5sM92{#Zmh+sdx_AJG>_-w=(`oqyGFL41189JQ>zx7;0I zp8n;(_9djqhTi?46RwO!yl;B^g?crn#CL zsq)nOw7m>>=5LJ3Za!zZtanwsdgMTpS}o)eV3Pd6D{Yc+H}5&9=r=F#^8N(b;pIun zh)qy>8sIMMGu{8inJ-Ym34gF|Syn>@=H&V&|GfE!oWwiG886G5E6>p62f-$KrR%&_ zG^C=KWBgEzLC23{;q*b-<5B%}$n%+qicDtYY2MFNsMM*lSzJUYa>~^%iCdVyC-)I# z;OGyA-3*xA?tbcX{#I?TMI0>i~)1B_Y({OEHgz-D>2gM%f?ep7CoIOn`I7zF3o!3EAd!st zZ4LSs>K%pYr-Wx8gtr*t+r}69Ab(Pz#OJfQd%fx;V{TvZOoxYHS4y^U1_#gI728|Q zUL)jLtL@lS>N@t(BI-7ct2?MK{#xxF=JrMHL@7OmD$TK)XNPW<4<>M(X{ z?64N!H}Uy&l}3%Flxu1e%O*Z!;D>Y2wIzan?dzw5CjBu(7_;I;g`4Gx!0MksSJ(^C zaB*XrCN$^yB?OBZwD3S0(Q6KEggh{1PP=q<)t31@#!Y4&*)!%KzZV?+yG>aB(>1p@ z2jH`M7hx1$Pro;&K>SygJsK{d1o#RWlJe*zd9vx2NijTveIg>gVUuPCfH$*A=lfB? zv~||C_n`HG6-L&wlwU|Y7R7oC@9xwd6Ko8nHX{2z35vcTqE;uX6$_PX{x0}0^)<&n z^8G)>N+it7Rh~ny{hwk+bpV*6=0S?H4JC=*WX~nk`*|P4H?;sqQ2lTF9%)Tpg#VO^ zm<%0RRN*Pq@{~-vK5cOspvn-OskQ6gOZqV$A)c~GfDzk-Hu>^Y$%Oy{nmNR|a zD!k29(wcT4B_hH()3+5%2t6yeNLfKyiL+r+st z$ScilgFSAtjJ9(Fz_tADxC^EV-wx@aM`mG+$QFx>(u$_8v+-w3{uM0t zkAw^DvfXrvOT>~!4V4Xya&4J*z%XTZ7hG=s`aEO9{Ew%9Oz;QOGT(*5zcOrRA7C1F z@JQk0j&N3#ONO+gfI8Q}0!>N8IqQB!Xj4wscYQFD5`kbwV`^Z}iJ#~2>8tW`>`k;Q zN&S*}ApnfwEAK`7yRQa6G(kP1(VASXgN}(BUs3DtwQJ;kQde|yOT1g>PH0y_%vc&X zi3@sisu9%s0ho^RQ!*4h;3>{%v^ll6w|=3_dk({_ z_ags&Vi#|Yu}jN=bD^^}P@sx_YeH}!X7!Ce4_n<0n76fY=bZJx0R^pE^aEGq265_` zt@!ZB`&=G7UFdLQrSP#v*BR6}4uCoc>-w%4ccLx6q2PxT+7SQC^8Bl^pIGpS1wI`b z5>qdvswNQ$5E%IS@AbtBeodXNm&Cd~5fqW*PnYSC!ZO?rO?fKp(61;7!wzXTh*bVn zt3sU_2;b5=G>Mj@ot8FLYUE*#9@LL{%h@Yo z<#m26(e*eCKXVWk#cuKAN`rU{)mKg#&SgZq;_WK~)Q&R1ac$eI-=K-UDHYtE8wXh& zsgvv`&i1n7#a+S(-Niorq%!^ILrBRDxaX+EHbnNLVDyyfoMkDc%L` z9dt~tbQTHJSz4L+&!3HFN+ai4@Lt-ni5fec0qeX@QZS~3cOPyO7h;pK z#+!jeu(?$4w#+$dV=SFhvZ~cb*2pa`$Sw?kvW_k*Pqe#T7<&EDFV=kGHOg=iBRfS!0+3%LC{Qi2)>h$y*$*JOTUEoR0v_6r* z_9BAFf-Y`cVqt*ezTG`8|MlEtgGf1s19sdf8_faaYE3GtP+QZ-NZA%Ae|b}?;D^6K zqYn)1beWv+1ykg1ERkoDC3y5?Jzb98X*-ZN=)AB6pQ zNVLNGpD3u6j}RCw*)jdAY3oYvin@MxHtcUZ-l#X4{H=!jA9S|LGn`p;q$y@ zJv-O0oVm%ZS`SB0InneE3^L0|A-gRrqKxH-8)Yq1pw_oPBFR%0@x>wZb}cPEoIT9O{zJ>Aj=U0zi})%v=gUP73yLU^bgJ} zV1_dkqYY3U;D7GRk68-^YODqU8jTizZ)i_M9F!9|PxFzgcr{!vAPBxh$swArui-y?goshcW}onhX|f4tNv1S+qgeY3JAF86 zynao{)g0MwOPd{E(M&0!2u>0hQJD9sopTV$cSyFEB?h35;w>UZBZ9^PLC&5VK7=e1 z10D;jdr^G*F;v^66&;_7dxqO(=La{&tJ-ZWk%wv)^KN8f0-&Pi*Exwo;G*jPr;sZT zr?Tt%;Yh|zA(SEWc+P!hWS)nJhzcP?h7g6KJ0+1ZLx(~c%B)aGhRPI@Ib*4i5(y&$Z7!g>FMF^vj8DxH^qBOz{^^ce9TzGIRArcfK z4>%pZt*ZtO2Mj9CjfR9;=it)z*~PuZFq;EjR;$f@J~u~p*}>|2U)}DUdUhwd#@MLB>uiWDx%9xRFT=$OQR(W^ z`TM>ujpq{+85J@@I289J+)FUnk@T@ZHo{*&`y0(1%~WfERWtFPpU%vOcQw{QW;zer z1X$pni8Yd4OG`Vt&!XQzlu zm5uVVx7qH7ujvg`^%b9|nT_S_?LWV7cKWrFlce(P)pd!=6{|T7^XPkzN{$rdn;CsP zXw77(Va!&pyu|x}^4)FeiOz@5pN9ot`?IYRlD5ZVbgRv3Bm>zzrOei{8@=w1lH`0% ziq}owT~{4fJ{(-D{VuEjoK8l?eSNJ1-xkyw>SFgu1{zD&NiO?5YOy5EnSVR;BQr zCs`s6lC8B<m>cH)^{R(IOY0k{S+N*)_)q<%Gr53 z&#mx|Trtk*{WNM>E}CL?f!PYy49#9e+>f@i7`r?I|682viHIjls-L#FZtZY#Brkt9 zZ}VBMp8~j9C}Aj{_jSs$*iuXz|r?wWsTHFS=?ozrdGoazBhtc64#jJec0|QoR z!$(OkJyV7rm6{LM>@I&p!YFhq2^Pz>CQw_Ifv z7Uiy~g`R!91D%0K(tN8lzOSxs4rVl^5m@(r&){zZuJv7D&BeB4%d!b-rl!k#3bHXBbv#aePUfVS>*n*ci)=yvxD#Q z>$lloVp@%({be`eu5e}bdvzdx((T3{+E(dwqI(%uQs*CKCkdns;*Y+aK`}S&E5o#1 zB$Bq5f6vf57U_OS$132sYkt8aZQ9cB3sIdzaI2@NQOLkZQB@VNlk!SdC7J@UR@oPw`%Ds;Y!>k|_mDcbCQz{TXUM1JGKyN%4wTX9OliB~MwhHpemgqDSJ;;PJ@RGQ?1*|k{K}=o+$C_ zFAwSon25I)NVSNA z3}tTNX+AJV-d>tqI z+-H`CXSGOY$`#-3BL`1fc-<4sasDFe7JAIqK@Gz+cB)8KG;RbH*NiqZ)0Z0?yI4rO z^kyMaFI0?WX`k$oSLZTqC+3G@*R{=Y^LmZ5Sx3kw_g_`GyefU|6?ySn{KR79_oy4P z-Zy_*kJ(((6JwgFB`o`>TBpJ}ZRNzhX(>BXZWi+weAtqxcraI0ec`CA-VRFQ)nJV$ zmGe5EUrGqv$0weNy}B*-{mQ{-%%Q1TVzwy_S5X{!%mz9iWQVWL-Tj!vk@|30_cfQo zr0jd;wL5S5RvJlG=Zx&NF7JseltQJGe}vo%`Mk$8nojJj(jt9H{0N6fjhe$;_VeB& zH$3=)RmdvJ!)TixMmxEgQ!H8wy*(X^Hux#d~oZWjKzd zHhm8Y&Nii0Y4qJ5W}0N6alMyr)bGp%YsoKuZO1Nb)!3Ih08iG*m;JuK{J@D~VIlnc ztOla^3ZhgiRk={6C~nx8%ayP0)00<`^z$wGtzSR;>pr1m@}hWP*bL)Ezh5szgZF^; zR$24==M6=!=c6uGZIi)F3(6=F#(5h0o;M1um7GiYY#6*AxS%>GG`6PN`8{4c?252~ zdHT+hAL7F^qe*Ccd06wApMFq@;d|*ItHvXuvXW}odHdwn{fX=TUJ*By)EY-}wO@#D zgH9UqxtdzWcS*5hV3Pc3U7Wb6euDhiS?g>A!!9?@2NHg%O?kw@#;OZ}zB=yiZRVK$ z*#IX$#K6!4WSXEk#=*$TRUPqu zZJ25P^ZWV2$KGf(^uO2B>X^zDTCKnruVL;UVs4c?rg=xXJ#(eUZc9;_QE49D=ZR6) z@R;=1gXn9@llg>sk1`xX#g;lPHQmSI&LW`@gpHc z$D#gd++GdEu^9SiH{dz5Nh8A&4SQeR>NdO5m$v&Kdhe)88Y%x!>6HHKNyghyW#Suh zRMr&h_)Zc*JZNP=ZBA|4!-EAkJ3IO~;K!LY?d|vOu0lNt(Ks2p{4 zHdz)B%$*Zu>R8-JIJV$fR2HamZ+*+B{I5xmV%5jPR<~T|h$l+h#m1N|7<}Ey z`#34B9j8?s^8Ndpf;aH|&G9jv>HVfMPGPT(*Vvfam+UNHROe+0QaJn6?s_VYblQr~ z8Jf5>TE#?!xD1_NtS<+-3Jk3)x}VX=Z2Ev<$bQi9YM^uJdjPA3a$4cn>+%^rwq{Qc z@z2iAn!K*?sIDW`Y*Bn#K7TrxrRkXPjw?aLaF@)F%7UjO%+g$`>kObm~{PK=nmt=WUPnPYo00Q|vAgGctPi$)+0P-Z z#;&cuH`0FRm3Qr$i7Omc?67{Z)uD4P`n!IrE!3)){AM$2K@=+uq0&VVRmTe}qc!sl z#pLc`w|}`zEA6C{6Yi#eiQUmsjPD5Ft`XkhXa3Xv_g*Fpa^8B{aGpa<^PM;CbaTqH z*!1S~Ory$hRyW7N+R)3f7VivR1o(B@ykZV**eV?6JWKzLh`LZauy4nO-Pufhmowj1 z?7Z+Q&wra*^=zkH>b@HSsQO@eE^Sy+@xYCz?}IEzea=kMSN-U=w14Nd4(bxkD?REV zrHCq_JAX00GqzJ+zsKON*b1$?%55D6QKbUrpf1Mxb^kpJ1_?qBWUZsZC-|7!&Y)z= zPRL)(JIJb2nxT2hi^DeV=5cpJi9|aagFs8KH$}M|;@M|Vwoe#~UNt%N= zen^YPgDXwqWi^75$LHhfrFKacRBQ9-P<-Ex8)?Bb#1G2Kukb!ieSI^2Wsl*ipNAeM z?-bn4n-WlYv3;-b_Exc*cCGt5RIjJPuw2z?W2@BM;vl*yk=aq`*NLH+{z#_lKXox) zdvMQt&s43b! zuTy^A0XJ*GTH^H?QIjy=xwyJX+eqTbl--Wf;T6ZX1vZWk`^wCml+xE-ht!x)j@$os zBM$5itH(!L zJGAeQM5|xNdnN31%6qRJyuz+9l4|)$!M5AZmPK60MoUV2h0pJ2sX!&qHSv!TmI*Wa z$m~`slo89)QCpGSCHeU!oU;iB_GEnFXc|Ag(zKN_yf0Y6QZ2B_WoTB!-C9oVbxA>} z6XCEFcUg6?Mq$wr_}twrLzbYv)AJ#mVulRIxlG&7S$g`fL{#Au9?&|!9qy5DkzS*{ zS*Xn+FhR&#repF=Byh4w?G_TTd$;GDrD?~c_*t%}+;Q(nW!Wk}%eyqRyZO%vs0~Yn z#agmREyjxU((k&Ks#9H+(-ZOKFd^KLW#E^9{*xoiwNaKWLczDy)%6h{z)R*TBFk6JD-W6; zwLJApGTLV%E-CF_HWfgRRatehdjwsE&wtu#-Cc97amMY!J|F3zZlg1`-F%%_>|ef* zVcEXa#Zf}+znQ`pV+xyodH&|V*50`PaS6fU#fQMxpL+<(qi)?&j9||+y_VbwOXr}zE#sCNE=DcW`?@0 zpXbbcb!29>i?r^u{HPE4R| zQ3cy2smkvY7pKfn5_y-l-}0|bV=T(*SxS{7z1VfST(>RtV${x-gsY6i#g+0KBd0!h zwMN~L=!MTdQG42WB$t&^W<|Gy;;jlI0#_NVirPyr6B-kCp((GhdRvQ1RsPx&6~FXR zZbF>vRB)$f)orfwGznJG>Ij7kS!>;taV?Yx9Dc)ZuBPQvt*_Uu)KUD*Gm_CxTM4=w zF^N1se%=|n%$>GKjw zuKhN6!J%G#x5a3>n{Xqu=zyQN)V9*hy1HY~$A!zew%yCimad8v7DkQF1htM9*JaEJ zF@BD!!@tm-yUssM%VAx}R`X*I%6e<9`DQ$gsMOrDM=V#DeOgzdjQ74)^7ObFRyFv} z^yFO^r?L~%a_-JjG})ECXGWG9#aohOj9fW)z*3eEdKOjedPA&MBDYB&T^j2a)fYDC zdFRMfX8dkvjgTwR zjcvclBwOYWT}cgzB<2JahMf}g+y(2oEEj3ZR4A8h;!`|DYD2f*w#{cB7E|#z?%J8s z$Agp58gUt5wcmg9aPIfdym4=MqDaF(uIc&S>gLq+kKPtXuwI&bRZvV}B~F~1@uG)$_OK?rc~nTV?;BD5a)m}J;{`!C z@2sC;SF~?3UH6u}q3O-wAZ&0bS`t!xJ?P0>Oc;6mK;0*H(fA?#o%a5YuOqWsd!L{0 zaB&q>y|!4DcFv_wy2|FJg;^wJ=k_XLDRGyTH!jP>jGh2Zl}a~-7G znt_kJcStX#?~U#^2+8*n5){$bS4fQfS<6uwNtqxo953EdDD^OELT07zN{%gevAc(7 z45s#qWNzq!(OgVZuKX3plxt3hx2$)0w=Q_J@4i$DGtNoDNxSy0#;B&q1P{$k1=ZI- zKPWSKlK#E}$|#~()MJMUkEOT#i_Ck{_UD`4$*~+xayZu1u=)d=+=*Wi$7OalXiA}6 z8;+VfZEF~E~^F%~_;IzOl*( z#u%ZQvS9;h$?m{M8Mn*KY1`soB5CvjfjzLtFJ<9cC$lu<|SwWBOOaaoSX z#+nyQ7d5^%B^ilZ_^`T&2c1i{dY#2O?I5$2BD{;E>DiA%!68pB7@f-Vd`Zb?F!!Xn z;x8ueGJ!I7rg{A<*iF6gM*R7Oe7l_8idUG?CvytCWL&t^;0sEAtE=g!=-j$li`lgs z0$Gk6zn>Q*nC893qQOl?5QLBq5y%i8j~GY9 zVvy&8@FX0NL^!a?a1@af zC=*#U4mkmcB_bw3M1YYgsV7jzC?bhWq9klh5yDY2eNbF5VowkWOT;0R z3&aw@Z?bGG`q$skc;H7=7#TcV+B^=z1C9Up-ZzBc$0zZYO+IN@U9PmL4YZdbAf;25n9~}oB;xKi#ho} zd=bbcAY2zPB8KXa7%~BeSRcXw&p~J$1IAH>BZf>S{rjkiH0k4N{#LkHJ%8SZXa02viXX;fY8yfrZKFKO3YxK8<36F@OL2 zk845%EHdygpsqlsD1iMBr4T{-KqvrFFJPzbu zYK(du9?A4*z$Qd8GFtH@EMe0cK>rv}V^WnScoK<<&j3cHR*>#C3k32&MTyLx7yVHX)1fi);0x+sjCqYCi z{{T6aDvUP@cck4x^^G7)K!PM3j*8p>hC`Aduo5x{g4&ZR6#&-9BP*qiOn^-K7?22v zBqRv}kc#j?xsMbGp@}4<6GCVb2-?lg3NWft7($c5pMS>vNyr-@(zyTz%3Fj$km!&# zGl*A+s&m1B1dp&g7zez1vpjeML{Kfxh@})WN@dYA_H- zLfQ`WN>nPup+R+q5D1)_s+YxqvIS{6fZ>p9z&PMaR0Bc1jInIj ze_&Mp0a|2aTeERbg5TKmhW`Iu7)MPipwA>BRS0@KBn3l&^pJfL!2TAy|E@tG{dXw- z$Ns?0G02t!VAMA>pjkoYd@v4=ycGZ#nd&M7-1s0HVQ>os<2RKP{OAo3=K)HtWevqM& z1vR)KfHs-QYvaU#xFDpB!Bqm4(*O)dwFszqsWwd{QxOulasa<@D{=w!T~vxBk*F9O z{A@R}cn1yV24ioI0nmhEk@863jtQx=jl0NyjPSSQfJkT}6}142D(8W`k8A=VaOFpJ zMiNL|R11TCYBM{)Xb99W$lhrKLzW2OZU*FU#EAh@QTaBgb&wSw1Zo{*vIQ6(3n5C5 z4UmdjKsKVH5kRF>+(!aDviWr2aG*dy#sz3%{<_`Yk^_L$0*P2^Er9w589*d(gGG(u zsP5PRg(L5cc0vF|*aYkv)H;;WFqFzMhhv~1hag867iVw@>EuEnIyg8wqa6qipb&E) qkyV9N{{JDitW2t^tW19X4k!HsPddA>GJzGqy(ue`xVVm~?*9QJ>qid& diff --git a/doc/invargent.tm b/doc/invargent.tm index 895ce6b..6586af1 100644 --- a/doc/invargent.tm +++ b/doc/invargent.tm @@ -484,7 +484,10 @@ In fact, when performing unification, we check more than |\>|\>>.A|)>> requires. We also ensure that the use of parameters will not cause problems - in the phase of the main algorithm. + in the phase of the main algorithm. To this effect, we + forbid substitution of a variable from |\>> with + a term containing a universally quantified variable that is not in + |\>>. In implementing p. 13, we follow top-down approach where bigger subterms are abstracted first -- replaced by fresh @@ -1762,7 +1765,7 @@ > > > - > + > > > > diff --git a/examples/non_pointwise_avl.gadti.target b/examples/non_pointwise_avl.gadti.target index 0aa023a..90d6786 100644 --- a/examples/non_pointwise_avl.gadti.target +++ b/examples/non_pointwise_avl.gadti.target @@ -1,18 +1,30 @@ (** Normally we would use [num], but this is a stress test for [type]. *) newtype Z -Newtype S : type + +newtype S : type + newtype Balance : type * type * type + newcons Less : ∀a. Balance (a, S a, S a) -newcons Same : ∀a. Balance (a, a, a) + +newcons Same : ∀b. Balance (b, b, b) + newcons More : ∀a. Balance (S a, a, S a) + newtype AVL : type + newcons Leaf : AVL Z -newcons Node : - ∀a, b, c. Balance (a, b, c) * AVL a * Int * AVL b ⟶ AVL (S c) + +newcons Node : ∀a, b, c.Balance (a, b, c) * AVL a * Int * AVL b ⟶ + AVL (S c) newtype Choice : type * type -newcons Left : ∀a, b. a ⟶ Choice (a, b) -newcons Right : ∀a, b. b ⟶ Choice (a, b) + +newcons Left : ∀a, b.a ⟶ Choice (a, b) + +newcons Right : ∀a, b.b ⟶ Choice (a, b) val rotr : - ∀a. Int → AVL a → AVL (S (S a)) → Choice (AVL (S (S a)), AVL (S (S (S a)))) + ∀a. + Int → AVL a → AVL (S (S a)) → + Choice (AVL (S (S a)), AVL (S (S (S a)))) diff --git a/src/InvarGenTTest.ml b/src/InvarGenTTest.ml index df2482e..241677f 100644 --- a/src/InvarGenTTest.ml +++ b/src/InvarGenTTest.ml @@ -152,7 +152,7 @@ let tests = "InvarGenT" >::: [ test_case ~richer_answers:true "non_pointwise_avl_small" ()); "non_pointwise_avl" >:: (fun () -> - todo "harder test"; + skip_if !debug "debug"; test_case ~richer_answers:true "non_pointwise_avl" ()); "non_pointwise_vary" >:: (fun () -> diff --git a/src/Invariants.ml b/src/Invariants.ml index d581b4e..7ab174e 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -611,6 +611,7 @@ let solve q_ops new_ex_types exty_res_chi brs = brs) in more @ prem, concl) neg_brs in + (*[* Format.printf "solve: pos_brs=@ %a@\n%!" Infer.pr_rbrs pos_brs; *]*) (*[* Format.printf "solve: neg_brs=@ %a@\n%!" Infer.pr_rbrs neg_brs; *]*) let neg_cns = List.map (fun (prem, concl) -> diff --git a/src/InvariantsTest.ml b/src/InvariantsTest.ml index 3fb4bff..2c37f5d 100644 --- a/src/InvariantsTest.ml +++ b/src/InvariantsTest.ml @@ -772,6 +772,7 @@ let rec walk = fun x -> "existential with param" >:: (fun () -> skip_if !debug "debug"; + todo "make no abduction for postconditions & not in bvs on iter=0"; test_case "existential with param" "newtype Place : type newtype Nearby : type * type diff --git a/src/NumS.ml b/src/NumS.ml index 1cfb0bc..ccb14f0 100644 --- a/src/NumS.ml +++ b/src/NumS.ml @@ -238,6 +238,8 @@ let eqineq_loc_union (eqn, ineqn) = let un_ans (eqs, ineqs) = unsubst eqs, unsolve ineqs (* Assumption: [v] is downstream of all [vars] *) +(* TODO: understand why the equivalent of [Terms.quant_viol] utterly + fails here. *) let quant_viol uni_v bvs v vars = let res = uni_v v && not (VarSet.mem v bvs) in (*[* if res then diff --git a/src/Terms.ml b/src/Terms.ml index 54d414d..dc2a70a 100644 --- a/src/Terms.ml +++ b/src/Terms.ml @@ -1218,37 +1218,31 @@ let connected ?(validate=fun _ -> ()) target (vs, phi) = let var_not_left_of q v t = VarSet.for_all (fun w -> q.cmp_v v w <> Left_of) (fvs_typ t) -(* If there are no [bvs] parameters, the LHS variable has to be +(* If [v] is not a [bvs] parameter, the LHS variable has to be existential and not upstream (i.e. left of) of any RHS variable that is not in [pms]. - If [v] is a [bvs] parameter, every universal variable must be - left of some [bv] parameter. (Note that a [bv] parameter that - is sufficiently downstream is a "savior".) Existential variables - are not constrained: do not need to be same as or to the left of [v]. *) + If [v] is a [bvs] parameter, the RHS must not contain a universal + non-[bvs] variable. Existential variables are not constrained: do not + need to be same as or to the left of [v]. *) let quant_viol q bvs pms v t = - let uv = q.uni_v v in - let pvs, npvs = List.partition (fun v->VarSet.mem v bvs) + let uv = q.uni_v v and bv = VarSet.mem v bvs in + let npvs = List.filter (fun v-> not (VarSet.mem v bvs)) (VarSet.elements (fvs_typ t)) in - let pvs = if VarSet.mem v bvs then v::pvs else pvs in let uni_vs = - List.filter q.uni_v (if VarSet.mem v bvs then npvs else v::npvs) in + List.filter q.uni_v (if bv then npvs else v::npvs) in (*[* Format.printf "quant_viol: vrels %!"; *]*) let res = - if not (VarSet.mem v bvs) then uv || + if not bv then + uv || List.exists (fun v2 -> (*[* Format.printf "%s %s %s; " (var_str v) (var_scope_str (q.cmp_v v v2)) (var_str v2); *]*) not (VarSet.mem v2 pms) && q.cmp_v v v2 = Left_of) npvs - else - not - (List.for_all - (fun uv -> q.cmp_v v uv = Same_quant || - List.exists (fun pv -> q.cmp_v uv pv = Left_of) pvs) - uni_vs) in + else uni_vs <> [] in (*[* Format.printf - "@\nquant_viol: %b; v=%s; uv=%b;@ t=%a;@ bvs=%a;@ pms=%a;@ pvs=%a;@ + "@\nquant_viol: %b; v=%s; uv=%b;@ t=%a;@ bvs=%a;@ pms=%a;@ \ uni_vs=%a; npvs=%a@\n%!" res (var_str v) uv (pr_ty false) t pr_vars bvs pr_vars pms pr_vars (vars_of_list pvs)