From 140e4e42c542885441f36b7f0d86a4c0ed956155 Mon Sep 17 00:00:00 2001 From: MarkusEllyton Date: Wed, 20 Nov 2024 02:07:41 +0100 Subject: [PATCH] Add polymorphic code lenses type argument memory Fix debug example button in QuickCheck panel --- CHANGELOG.md | 2 + .../annotations-4.7.0-SNAPSHOT.jar | Bin 45475 -> 45475 bytes .../jars/vdmj/libs/stdlib-4.7.0-SNAPSHOT.jar | Bin 58394 -> 58394 bytes resources/jars/vdmj/lsp-4.7.0-SNAPSHOT.jar | Bin 327074 -> 327149 bytes .../plugins/quickcheck-4.7.0-SNAPSHOT.jar | Bin 114443 -> 115014 bytes src/handlers/AddRunConfigurationHandler.ts | 64 ++++++++++++++---- src/slsp/views/ProofObligationPanel.ts | 25 ++++--- .../proof_obligations/QuickCheckPanel.tsx | 7 +- 8 files changed, 70 insertions(+), 28 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 256f2e1..f7a0d9b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,7 @@ ### 1.5.1 - Add support for PO code lenses. +- Subsequent launches of polymorphic code lenses now prefill type arguments. +- Fix "Debug example" in QuickCheck panel of PO view in workspaces with multiple modules. ### 1.5.0 - Update VDMJ JARs to stable 4.6.0 release. diff --git a/resources/jars/vdmj/annotations/annotations-4.7.0-SNAPSHOT.jar b/resources/jars/vdmj/annotations/annotations-4.7.0-SNAPSHOT.jar index 86bc0b82a9a070a909e376a8ab4fb9587ae2b2a0..6761e4c1aac5c53ecc29740a3a0b266957a19ec7 100644 GIT binary patch delta 950 zcmY+DT}V@L7{<>zTXR|`7qu9b*dqEGeb6?=Rt8b57>!xE9H?2DSri6AAJ~TtLdi7c zUxVWo?VPjeKHba<3&o49o9IF?h=PJJyy&K=h%SO^?{g5k`aS1)pZER0=YKfrtf0;c zqR*q#mvEes<4hA5`^B}o0vsKLvGs(Hn}9NAh11AQ4>T){%HsD)A&*mxKiphGo@867E%cguT|L5^_dtJ5l;- zcNUSe!F3m6Y)?DF&i&1p9PxxO*?Dj&9FK1X?bd)9PE~yni%m9dH_*WEE$=aB=3GND zIrd8yguPd{p#A183%Ukwx8n#)XD5Wxbp@jAP6tG^`#Qwxo@)?~dR1QhcP#P!+0K%$!L8zNl~^j zDisX&BI+Rij_xK_%az1!%1XxM@_9Y2>2I=2^LEVFx)kJ6$^r6zDz!wfx|jGsJw*Jh zHWEFt!$djeBmRgTC)UM}5+BEFh=xHw@tDRZgP0=@9U;G2S1S(6FS^NkGpUT2Woob?wMzT7GE+uBMt zoi;N$i`)5-Mba^hjkQmBYq;Ic)YRhdyf_zf6NhDUVx!ldq=@Dn`!#1tg1S AlK=n! delta 950 zcmY+DOK1~e6oqFdF-faqD;f!EsS)uNd|;B68m%Bolwe5J#s*rgT5A<0u6$4*H6SV0 z)|Oub(?rZKLIQB)vdSW<5y;a;If*lTSqCuh{Q9i^{! zr;(g>uGJ=|Bj=%~B9w?nWVcBkyoYXQVacFgEy$w(N`AVLXq?WOUr0q$pb- zmsEqjh&zbC<2#A7_ljJnD{W&Kr{^biAOa)8p0fL_z?MR8YhO4uSjFw@igj>)5tH( zV9u!wauXT&m09f3uJK70=P%76AIvq;IWKc~pH=w)JzvYC?{yxzjRk+1`sGfV-!|5= zshpX~1>DYu0+NmqY}7M?iL=`Cjv_YhFJiM#Mf6!q_+?r&N+sO-n^H4vP&0b&FB4o$ AKL7v# diff --git a/resources/jars/vdmj/libs/stdlib-4.7.0-SNAPSHOT.jar b/resources/jars/vdmj/libs/stdlib-4.7.0-SNAPSHOT.jar index cb618ca2375c9f5f26623a9c1cc15b84fd6342a2..5a6c94cc2bec77787b5cd1c20d1949f085b5c983 100644 GIT binary patch delta 637 zcmXYuODIHf6vpSeqmeKg6UGozR%p@~@+wLeUST8_QskMG%mxctSScC)*{Go`)MV!_ zEJ&if#%>m5?)zGqjR>1j-0#flch33F`Tk$`?%nZwcYJnV7jMn9STZb@-1Fdeb~$gt zzXqI^0WTFMn2l=y+qhP+=ej@$b5Y)Ggt_$1OiYvcF2R{Ar(yc#uyZJE&JUU-^M9!L zcHKK5T~#e)nZ?d!vC!Y(g&lkEEf)5h&vLLa(zR_x@!tDHlZVl2+WQ?#KuL^GlI_4` zH|-wIDwJ$}{ucgBjTH)0D@!D6t9CmsKQ}9@QFtyyWIeg;q{E(ToeJOW1s#1x-)z`b zVQ#Jr6Sx}Kx{<6C3b*uu@Cf0HQ4lgd>y+8ho6vg>PwO?}Iu?$2W;D z=WPzGtIEYpQ|yO}guVt3Z)*15TO=GcUt}RM(zTZg@!tDHox9O0%KePR;l#%$Y3;yd zH)W4!6-0#1`3Uwi^|3&hT3aDoTesUWnb@hQf^c7oxb-aDNrOGtI*IDYB@HF+->k^0 zkACVbKL_wG%Z>R>hn>W{pcHEXOGIpE{bD2PU9kg%Ue&l0sA{h5i{=X_s50JKcth yt!hqW4>a2KpjD&h^g1vpyV#&k?|J_2^XmoZpXzk8p*Nv+8#F&`452Lx1`|fk9|9+q6@tk$m_^!3r9?s^^m{cS4;2*%-Y6xe02b&m4e-;GNjVB;YUB45rV4&OVNwoK&z&p;(*vC}pEFM<^mc`X4HU z)TLt-!i3n16k!$LK@sW+os-lc=th!ayZ&6MCk|&OcKTpO~%847#b80YtewR2wnzbrwD_g z9c42v3EOIc3_E)1_gxZAQsZ%&do}h{UAa9cJE1JV)&C!lkjJL!Vl2UjQ;xnoZNIUs z{vV~irs}5ZtLvw3lyHD`Q#a>p?6BXJFXLJcw0m|g+`Ewd$-B<#$~CQSjiJ3Jt8W@a zHCyf8(H1=1`n6zq=C9t?UVozb#Dns>1E)f7hR-wQ-*M?yS_6CGT)p@9Zn+Ar_TM5c zwz%uvl}%qKHEFoF^N#Cb3#QXvp(k78Mfn1EoSY+Ov)IOQuF2w%oEc^%FJ|xvNqM%1 zI2IdfY5BSx?rl6{^62y8+pFN268Dz4$0sk&v)?Y%^1rc<@9W>zQLEvWcJ0#AT!H8057aj8nbtv{+}OPMr}r~9jeVb){5mZC?c zzVgf7%6-4QqOVJlUv^-;C9RNe*5j~hbDn~f@^jbsx^F5!!n3%<{^H>+d0I6~c7#+b zM!c%db1%{T8hFxv*RGTeCBaOw2178O{j9*}LsrG{Sr_@&jCNIwxm&UiMAqfI>qYju z6UMCdJr?de5A=zxcQp0Q|1!=%56%S z9+nm>&-%L8?v%9u=rVBGx^~$VsYfNd=M*REDwP<9JRhETIv~1lRrQ+BZ@$)4F7976 zXzr>X-_w!#VA-lob~Bdn76e7JS65YtO9svRc6~&Fx)bZj8Ltrqw;@rL)#8HY{Z2nfHvBNSSw*v@w|ZT)Ii(dCaB zCCu0~$5q`&Eu$9&NX}+fYqmP|X8nu~-?OB><77>Nwuf(SYm~EJvON%<7-o>pzOkS! zGVO5(ATt}iLT2ij)(NDhte^HX!)LDr^Go*{%m=5k%%NrD@ zg}Rl-MW*t_y*s>iZg!qd_P&3dChyvvOGLeU zR=Q`}zOyK|DauYc7;|-LL-ITGZS`~fn+_(fQe_K_>u>#aUCm`+X-HqcK_$^QaW!xM z`w4|X%^IIW9CYVg$Ynifd+U3kV4KzRK&dNfV?x?X*>`=5^nPR{>fe-DIb>VtyW*{H z#N-nZBTDUyT=hCm^mp=x)L1QA7H7GWH27ZUbmM_T*RE=t^CiiN%Lg}q8L3O#eWP1> zcS^yN^|_-~eN9h^(!G{jY88UI2V8b56?8wH78!YBr}wv4FyoG~e!JL({gM}NMy&i) zOeAeR>Kvz@#Ln6mJ%5*HupM)kd*u(&%%{~(uYQS%3%)Dwnl}61!5g8{hZaqJyfjML ze#6YiYd+VsTF*GzWv#o9B)@-3Ge7I=Xj;=b|GJLY$@K*?uj0#ZEt)dxsf1|a;6Cfv z^*&SRe6bwlh(Gf3x1WWX@ngWVHQiy#@J-ydJr;^~Y55j+|BnaqpUn zMAz;1zJH)|H^0`vjCorX6Yn0g96xq#!2i-i_V-Z!m0sBi+6!%EuDOUy>1ScjRm z4O=E>`9XZY{qCHjCXHY8%5vP#4*LB#+?p3V>xcA%*%HC`s?sh#AJ{8Wq;_+FciE{r z1NEQ?nOj#>uJ~kyezCP#R(!y=P2TeJ4}_FwS~ zDYzN)-Nz1jFzx%8bn)Ocjd2mqnNSj) z3Hcak`_8QsAcXNApW88!uomR(?YSB(A{UP0z~`@A>8(VhIChf~O0cQ4bPo~P zl$(wyf;ukdZjL5&Dd`1BToS_;(^G%*)};~qcyTz=YR%U`X9iz^!$7Ui%I>E0s`!ZLNSWcU3v_7v*401@i+HXi*h&59Oe`i77#KY3EC( zFaCzeb?IU{;S+W4J;;>dm*9-mz9w%q+X<*qgcuA31_SoJ1&Zw0 zB^#GYEM@ICv}dvG8nutQ8n{Bym<{QEb>To#Xo1kG;=prWJ}T#rnM5&Khg(05ea?$d zXU+_I8P_m*=Cxm`GlTn`9M$HCTvMJh{OLOl!Dq{p*9K|Heq)EdF$r22nY6=C_soDo!-ep&MUrBLh8#;h zA8%cKK|br%v7u$t8*ZhW=H5$j@w&E>oH`}tUdn0JyBA_k3Hdf3HxP7K7C)^aC_Lmu zTJ~$U%BI#zqgxZUFIjLrGj{81nHJMcGH0c<{5+Bpq@8_^gvQFnNq$_mB-Lb-U;U+U zL5rP-E#fMcA2yI}4anPm-=`ul=93v3EN8o6?S`P^`my88=~r#YE4H5f$RUgOQ9w>pwxo}R#K%)Fdk$=~h2`_w3Zo~V1B zUBshpTTQ}B9#v$?jRq|2+Fm%1H8tag98bUui_Vuzy1Z6x*t%iWVfnaF8*ziv6`9X{ z&dqnxS?^~0!1~dp21U2{`2oYs_%7jG!HiWvM(Vil-LURdyJ+@~qeG`XGUv;PIJrLH z{|Ya9ox045Ex)V%QiMt6To1IgOoeEv%B`fY-IC5A{<(Y$xlh8WZ4_{71 zkFGR%=K3;wN2Hbo&&6!^go!yvvtf3YWX7n##`+nR?fti+yfi{L4i;|;3bjz*bHnG= z)S<==s)mQ=KA5)IwZ^PWZ+KXHcC@{)`R4~0ZX}sh2fDUTtgyOrR+gC&*O`5{M!#Qv zZ`1R$+H(BP)7J40ITla2v+H%cY=`O6Vn30*{JZM<&z$lte5H_%!#S z_o<6RE01|4fAy5!737-VyDj|fuAzTCB;0wdj6UwWryad;1*;(Cr~4wkZ|d4{s-_de zwI-Z!e{)N{+%PZWz%jcC!6rlf()&`91MKdm2g~YLNhgF^NZ*>})$d)JJdndMV84nf z_pjeoAo=OC|Ix;sXCCs&-Hd-N#M^%KqDrQqp`~@rZHn;syKi7Jv6bI zqLTVnpmCl(Y<4@g>`0_RVqxj*=nKLL(nmD6m{0a7b&t5~E4I|2ebo5KcV^j2xkHPc zMhu^~*>pODY3HRaP}{I4j~S{wF)7jE1A8QDoPVf!@`ev;GpiRg&$LebEc5(O3lx<$ zydUATt4?x@jQJ{m{xLXErFL@K)6caoypNg(%QxF@R4d4zAMgB`PeS7IMbU*4M_7Gv zS9iHvRS34TCfIK~u#>l^QsIo{#jERA&yBk_!2Eu${?rP_*DBZPB&1JvJR8|xa72Q!DA}rY_^HLbPFbsh$Shx&Kf z`>q^OvRc)`<~pq1i6tAT{cAf(+Ee?|174Eezn%$@Td5stzA%|dQKMqyYicKJks*yJ z3t0R)ZF?pS~Fe5ip`{wsq zq(8pn%Js7+r6}n^M>2pq4h*}ICnzjOJjjRCj_l}3#!}QrFLECh&Ci?6mByR9=1%fD zg}FY6G^Gv({2`<$rKfO^JVn`NhLLY5>g-`Mh&o<~#gP0|T*X*2N&@@Kx=AWfyMBEE znMh&TT};MNF=WfgQp$7tW3r!$R$ohMP!```l4q#X@yTv-I;B_HLjrt*nfp{6bW{Ec zSYUv{k|76DDc&*_u!-_lF$r9wc-!^C5LF>xBe0V~&}j@NkI0I1keYr<0 z!F^n3Xg3dh#tB*4fi}vWk`oxG43wQgFuv-`jb93KsSqBXU>^LCx5GTMFDrpoh1ZoC~4wF;7TPlk_hHd z2VJY%AefgFM&BwA@_+@lfIshnaL#ox48IRd|6Fv#vio2LCmw8l0OX-kA&|sxNJ$>L z6arcN7F>khjuZkV{HDy&EGY!4_^rDTnEhs3{wCz%o(Hr%_5r}x)0_a4v0S7Gm}8=s z<92Nkkiu^$$aG9#B#lKh5~O5=aVr%gq?`mii-A2Rt`!3(Y%yF6956BGA()Mc@P}Xy zCZ0Z|MM@>W1#<#Q&}efq&M%>Lh*DHm4#%SuEW$*3DX_-GKq>8T>LV}a+3OdBj3fjD) zf)*)O(%{!s(%{o8fekhvtOT~0nEHek1wWy|m;5I9tAG{OSx`j}`_U>?Oiu2NRbUw= zjH~G^!mEGRuo}$8BH0?+p?3{k`OF%+ygzE_1l?+Z2mU1bd-DzRYr%YF6vU%k@7#uZ z^hL0jU@%nC^Y>3uNElSD14dZsPX4>TpA#93{qpF_{I>>rCWS=9t#x1;hH||Q$TOQ| zpx9F&0bkYu8Em>Lcfytqq-u}+YjT;Mfuc`=sR{?gy-6F-8!{OTCp6Iwxs-C`DSx}3 z0v)WnM@*q;7^wszf0MXWjg%~Mm7LJtlub9{Wci6zJ^>YbLsmj!A z<%neUI3h`?*GMl5j*W=BNuPq*rca2$)@FeB1em}P^%zjT&}D@%Y-^-NpE#lDJUX1g(Ex^N20=)`k6qvx^Tw|qqz`J>`#a8gwij6hW2ny zbN4($QG87)uIzK5iMck<5jWk8imf!2kj2%)qDvgn;8e;0WiNxn;){(VGYfe{V;X@J zGh{j?@1Oqvu!OhvE)qkKGXK*v4Kv`%Cb|g^ee0>?falBv?k3l^qyRl>0{HKM@KY1Q zvU(;bmLyberc<(MM%VhF0moB0*Fw(!iF$T6h4RS@ zpojzZz5w#XJ;?hK=-_D(zTnHY9v%k67TpwZPqP^4{1TX9|5ML2nm<4aEOeK^J#9<= zfi5jT0T#UkDp=JyOTfAS&5dC6mt8dk>Gw}kNX@#K7GQ*x{$3^hTdBgAYrd9U(28hR#$c!d&hFbe(Ycj7C6Z+oE1 zDJoY)Cvx>F9kDUD;*;PF-f^J+8Me7Qov&}&S9Uw{W}J_=z`|2X+KV{k<5w7 zdy!c@MZ`^$xnWX@2$GL8TliFyX7HvqT#QJ~P zjy4)%1V`qqOw0V2BcFflUT|c$jhQfklj@(WblVZT!-O_*F=Yxv{Wc(oN9WcdLFY&` zI@{3bsB?{u>TKEoUF?bdt#<{-+2C9{r#~@dI}p2SJ`)n0RR5se$YGl}(}=o%*EyfV zW-R}kgy`P@0&kEkVg)U;;Jk5`DGv^@{50+9Pk`$jcKoH^P&pm*M>filoxM&&+2LlbcbrOiD9ddp}(csMw@;VF3ADcbcmQeJ_kp(0m}STMU2=wl^zcZQS$+L?7^ zP^)t(@xWi5KpiVhJoKyh4e}(8JV|pYg+QAwdgtx7hie`27I~RFh-!^4EMd`GdPn}(rR5(#Ng>{__bt%FwzBV# zZ3}~pPA6rd%R3sEH{uev;NEv&65c4%AFfSqf!4i1iuehO-T{4V+mE!E5)+|dH!#GE zncc|jF!bmKCip!Py)(_l;f-!E71zdVcf9QoN=yL#8-eN{K%B&6StRV0A=O}9DGh(4 zclM4usQ69)X>~{F@*YgV4#y`mPQE}&oPw)yIkZ(Kp`=R?u{c5iDH$Op?qg56CJE1Lk}B9CUUntiOo>|5nW{)%g)6wQ4m{OE7p1rd z6+vDPzU~22u-RhuNp_cz$yGGE+-BB>(C7ngw(0pUQX1*wcA;)E03=?{(4`5i0Y?)?@;fG$Jg{@cz_NhjqDx5&Wz#Z}tH2Mg%aKvRF zf&9d9Px4Rmo-U<7$SxrXQ+GMc`v}yq>TARxQsL-FppE@ky4BAQKt0fpW~&kxs@2e@ z4;WyhfIj3!bT2&FM|YYV|LLzU5vnRqb8uPNg^*A-gj9gXI_Yi~{e&VegZiJ)=NV`1 z@<#7uUl<7=gprz1_A#w?i=$Q#t3LrV3~bi9wdc#w7&^=T``qIURr~3~y=Oo2?69fjZ3iO84)e?#Qn! zH0E#7m~-oXhc%ypF|Pc2pP-5@$e}lCC+^%oLZvVCcfHFOG}PzdrZ04RT|)0nUM-mS zo6&<9|g`^_B!@)&gCl-5ihl-Y6gi_VOHev(42z`-GUDOdiAKzBfkuk;GCiSzyl9{mdN z-_qcH^v*mq53U?WA8!L+>CHpv8_Fce4nRjc8XcYk%QCjbqdfGRFAW~Xu3%bfw7 z>w^#oz zWIN0p2FAES4~md80jfyEf2yLoI%WjuV#Ed`2(kAXTv1gxj(P>N_j1_F*P=w$0*$}< zRUtN0-52(Z&})IhccgcJ3xJVZ{$Fo1ht0nez}io!JU716M~~*ZD*@JMOiR)DbFa}S zVcU10h6nRSsYp7fN$Qaj_q_TARYvJ0+I|!T*c=L=RVW%Q&dC77K91PLN|-WAFTU;x zCT4l49mdfw_c7)N{4`1*V_2IKRiscrW7KKfO5M)97et{O2r?z6Q}qMU}R z7AKT`0s08y4i*d_AS+dL;pZ`-@`Cp;n#vIfkz2H zhhu5?lwqQdI&ww=wu)^(Lyvt|GTfBy{V+4}l@!ht6Oe>q62wymlO>+! zm?H5!fToq_O&$7*cqc zvY8CQmvMq*n0Y>(6bvr*l7dX;d(wvGY9ATm^NmchDf!kdvIuJnEd>bjsn2UjV%wTm zkxiMcs-)1|ewCyV)>BUwVdMK0QusK;MFP$abC5QypOY2_hYx`e^j5)s9JJ!_m$@L-KUEn9*S}{6nl<-iKWaHN~`wNBP7QyYu`C_wn zbrw9)=usSYl)vV1vg<@x{hF(FJ(fvHKmHa`l6yZUNx9*Db7x#rEXD+^- zu5nEC-V6;@{R0B8?$yS-zCX?RDI}cFVcc+mUuC_Mj!dofuD07868w!DR{f(Mm$ldL zrYEzXpYvA#ZpHLxp~Yc#=N`G1bG}@1i9bI-pdsFehqcmA#k+P%*o6nhL64%tSAFL4 zQQMST6rw&q?vi*n_jTl3ia(Ror$hJx_P_Jz>Xu@Vz+Gw9kV@`t+qM_9h;-bpF>ovhXS?SI2-7mE5Lzd>b52!5lTB~Lk+xoyS`?5vc zxXws{Kh&CPeuAClSlR*Q9Y zUhm#RMqj7Bs+N`9owkA*I@57NDK9T}?B=#AXxvccez~Bg`TkeAJqv$?)f`^1#rm@; zM}v7+c%lz~&Bex1!)@(}#ao&`dxe@xpAw;qbo-cWDRqF4SGs+)t2KvDb9+q(3m1xa z?cfb{b?+Z4ty(2jd^EsE&?q6>t^Krd!bvUql)q}N){$-zc#(?eoh{RbJ|O zoiMn~P0jO^BKxqH?ajHmOIjY9Y&V{#8`KBprtA+N8V#OPY2MWK%_X@DWWk=47_2OL zPjmc*^Sb#kRC#EBRoE~+SVwKKv+E#iZy7ZxOlEd9yM)Rr)#| z5-U=NPg!U^Ua-I4sfP#qS8ryr{ovyOrk~UKP2UzO=w;kj`jFogU>=!%ox5YHwz^2Z zwOReH@SO5!Esqa=d~mSE`ud0EneQy?-Hev4csuR!0}HqNEZ^1pbHh%TBljIM3Ub*c zdS8b&J{7Eh@POLIrk1_dY9CpnU!A*~f6aWb@>5UYDNS?jPT#nIHfhh7Eq=`G3Cpcj zgg=-V7VYW^G_pAN@S&g?Q@Fr`Fne)@L(c9!agJT#Zu;B(`em)Fx=ucmu5!1*nnRVp z&8a%f>814d#zAN!2IaFZ5MhCM)_zCc|zn4|+L+9cF%zoNS)<-fX5o zZGvOZi*z&9%ZfaQcxbi36PtX#?z!f!`d#ecT`^yP$K#pi3G z6_eMl-PmynG)M~`5^MQ+VQFaAyP7=$vfEYP1(t3MabNEq!uP9heWaWAb+?KZ`jrAx zn+BHl=4-F5?M_5{(i+_6)Vx+p*k_k03902L2Yv|?k`Fev=qhhIUDYGFYcgoj`kD`6 z*Bnkodlk2@IIYifJUqMkth-%$)r#h`v+I_h_db0pAVKbg2Ql2e|dj zpU79e_;-Aw<$O=#13bX5w=2H}=tcc{`{3$(_10RC-1G?x@#r)YxA0`02X-rO=@}|= zTU*(-@I`&v0bGxtIS`n8h>!Kt%Y=*X1%6!aid8xM{IU9nl+Vhwi3!Y3`GPiX&(`_G z+6=i2brPsE(2vxVhjGh)a8B&J6xTnKVJqUcw^SvRgRNE4Ba}1F zp^3#b^1A!wC|e^#Bg3agTec6od}*~;x)~(?x!yJPLi+I%4%6GoUmxa7)~?zav@r8v zU|vz^qVud9Rm8=`y9}K&H+U|Y}i6}#)+Zm zg8)`UoH&Xu3S&~lxuU3C1UpFT^u@82r0$RevSVQ!EpGGovwVeWhL|XP+6)A*_(@}= zNq`KdKuYIiv5Ul!sYp)&TSe-E6|rliv_u)RCZ!-1EEpp|gBB$89)^b{5U6My;DlEt zF!mx%RV|k-E3Km<=gu z>;2Aaw?4w-VB}RX7kA=4jYhM926~tv3}^yOaA-C5izw5G0j5j3DjH%2q~vRaX^~Q< zF(yY!&rPrn4#MNI4W>k#1dAFsW6Z?ytf*%@Hbd5>-3KGj$VD9iSOPcU;T?sAlaz;# zVs|+?8Kmw_N%C#LXtWLt_WB@J8(#wEqPir^jSQ!nf+>+M&JfGsB4B2({?^IoVWGs4 zu_(6?E3hJ3o#^xdI+5>*xy<_&fJPgIZ+$SSqTNjNcH%Tyw4RmzhRi`(kgiGsxJc05 zNtRDF=qhB$F)h0OA_7#^m|jQfewxxdNvUfc-IL6JjTOCy#N%+KA18^YxzQUm316Q? zx&a#@2{*bjQpe5zTF3ZUB$%VMnO6=tbLEtSFWN@lPGe}=|f~R?pk^f zi4xyI=OJsH-A(r)K0k`M`skL#VZ6v=kj_hHd1#d0LE71j(*;bqg`Nw z2WRQB;XTegX1u>RSp1H&t>bNUTAJhZ@AKfi?x-8gCI!7VM>aS5#MIH)p8LOi1qSL~ zt9^a_Wb)dru=|?^u59U<{`t?YhT5C!j}G*A#EjI|U)X#2>E81{<{BOwU>Ow&fvu8R zQr9o@?`N+Qy0BuwW9=SMN51W)2VJ5cVlVFhfI^)6a>G*(C5kxus|k9)xi@m`XR@83 zct){;Kkw20>4TOXGSR^tfnq(EwCox2dDeQWnAf_pM-zoKg@cv~UtB$0; z&)XEgL#Wd)qn_u?7-zJtRmsl03codlre=AbSN~<|$(;xuDf8#B8tjzOShYcZN3B4r z${S_DXB+&VtA~q)ymnGw;wrD^@`hWyyk761ey`i2Z?4lFU&@jyr-wRYcJS^^S7ZKi zFu>Kfg*((lYtB`v&nlnlgKJ#J&eccrhby_N$hq%$j z1;$k#qM0l8Hl36DxGK`)r0T!+_f+EtSE|}NRP72deZX@41CMUXgkto4(JlPO@w@i? zD*T|le|U2d6IxUQBc5&b=kIKFdq9)SJEk1h}_e%Hlg)tAgp6 zQ>dzP@u{tD56YICiYmr>3wCHkuJ`FJ3T0F1Vi9p>f$`Qx%_!*Um!imeUz zu}w}s;rrlbuceqvYD>IkO>5S0esyQ#?o3XWx(avAyI^n3cFR@v`|1n-RnrVR6W6Gb zz;xEz;61N`>(Vy!jL>*a9U&>U(!ytlq*lnkyhc+_+_T}rdCm!L@wIcNr+oY!uFuX4 z@3>l^$u9q^gJ!#rpGh81+!#J3Es~ts{@&CuhQs?}`ipIP5@${%<#+ufFlcV#>7-zXhQ8fq2YAyzdV3j3>$J{|BZ7F;bi(lV+dzV76PM_%DYcMe#k zxos)F#(A-7oXOvN#-={{*3OqHL7NXWIr4j~ITD!Iwm2lME9v9d&|n(;BFXbc^3d4eE86hteF9Dg zEhbfk{guTm9FI5OVcWlN!q0foxu#Qcx;o-Jw+cC~8QpWVq&0rQwRc>%k0&28;d>~S zwI%EEU017t7-^B6sz)kQWzh6zuwdM*N;{{ zj9L97Y9`Gkf%|m$ykpV50lbCWEuP@`dU6+FWyY!9LXr*NjT0N=wAJU5 z-8eckK@Clu7vAkh2c~LHJeb@qOu6ybY-ESW zkzAS`@iKBxgwFVRQd;4PQ^%+KTks-&VvpT@0KZOh77M|bk^8e=7xy!qx;w)s`o#*i+9s=*@ZCsSxcg2eF%OscbQv3oL!?O~vAd!`yg>0#1?pCJ#SUH!NYX~#E&1LFFzNR$WklXwe+z-N-nH(_v%)a6J5KN62u9$X=H zPgKApPVD3SXZLdJFpf40A(s%~g*PVwZ_$7{FeYiKYJ5k#+$wqY_07NEyBt^(n&NWQos1Nj zDkz%`6{wgDO?CzNhY)5ez#2kW^^5|Hddz6#h8O>))1f)Msr0~^w-8f+j0f#+0o-{%x^>2u1Rw}xukSwoR8sG-Qu)Br=m zUGD`jB812nR8#c}iacj6CD_#h1HvY?mg?u0T2xF%?hGyq3p4*z$94VfCjIs(AD5s2XBtQgE>#iZfsMnEhd@FGLq z%0{SpVI>>J2NN0qyCmY}n0W6>Mg*Nk+lP+zqG&Gv{$)oB2*Q8b0S}aG0>o`RG-v`M z^d@0ai$4D(34r1y-e*-2fF)W_RDXM;XLjV22*Xquj)-9V@J$m%W{iOnAWoue5l39Y zIw>x#9CaVU5Y!a}B{2``x&&!|P6FeE5zQ1-LNkK$lqQ?dx3(-nNYJ%$q7Ql7qt8Oc zc_^7Oq$%;~D$)Xozwbc(7KBnOOE&Fl0n)?=_n>)&%``M<1AKIU1+vXe0exUH$P%?4 zWVq!kl1-8;FlLyoh?41U0qhct!s3#8m0XCzHS|w*9*xb=qZMcoToy=(Hj2dv#Ll-3DX{?P-QqLX*^%v;hes zZ2S3d{!=Ji!2jd6M~gJ&ZU+)X8l3Sz&wodzk;qhO9>Z(Ux}925V%t%a5pB}7xE&}E zQ9!8t4Re%O80t=id9La!NK;fc0T|Ii<)z<&P)c;jrrSCg&wot`j3(|?WYg0QAVmZ? z_I0q4kwysOHb1})J<`-c4+T&~T|$AV`dy)MFz;-^r2VY{)PWhW=eZj9?Jog<_pIBHf;J zQ4D$++7{#gVNh+1I-D_-q!>f#r$)C-76*-1D@LOU&nx726AX5lpub=SbW=GV?nZOH z%?5)7*Xca)RyU9&AeNtLUHKG22%1jXlqUS z&xIMHn;d5N<0X|F+bd+?p7OuWCa)+O&WyG=NVOr-%y837z)f6|DD-IO!^N)vKdy4^ ze+?#IQqJEP&W?Gg?LFE={}5XL8mT)A(bdvhAWFay!!AeR`^!8uuAiYLQ+i%^#L}VR zTXY5@@?xM9_J1yt(BHJ@+aF|t8odY_-7PW0fF5cY-0RiYnvMFZ72Qcn&chF3CGm;7 z9!7cuzRuYXT;mI9v|o$<#&;F`W4{G1&Anny%5uZhG0XMM( z7#-Y!kD0QaE9 zVLqt4F=;>f7Kjn1wLBJP>Buw+nIiN*zwAi$wT$|y6ISOXw94gC6)I8X=3B9?hmpvN z$R%p(&5>AS!6N>5*gdeZ7ibbQIC#(LHVat#67XRLQ0g7fAY9YSf`yYbQHI_$n$#Z> zjE$}a2EL>4y9{10#?XE83ct6+_yZY2wXtd2de{aj}u(1!Q5>D6$G*^uK=uoPU zE(j&iSR>Y*%!{7Cy3w~H)55=flLqN9aF8wuBg&{9^VXJtM^}*TMbwLYf2cAFd>!8U z0A!UIYvE9#=IBTCKSKhzXf*zLMn}i#G*6G+YU};I_d%{6AWRVW@5=J;^UZ}>It-nq zixFgrM3-N^vicILRw}9%>c2m~?8wtF;v>@GM4e%eMxW51?qH0F zAzP?DLiNa&5#$vNL(n@BidR2!sXtn;7-tXkH=jSh>_`JxIs#+}=+XSA>n)K%B^q$^ zjo!FGFiNGNIEvD6+XB_b03UQ71;iCU+>Nxj-~k*)9Ka>ujZv!F#SHbcU>q(D!4;wZ zIJKPHvLsG*BRaJx8d}l+{IVl|L@_HopD6(Dh$C6R%T*&zuXcK@=CX0N%QGbYY{ym$YJwj<0Z&=U#%@BP z37|prk>vz>&xGC+)J#riyj#Me39ytHmxo6%gI$agqrRB`4OF}Yf=RHH;H_)pk@666 z9zwHezSVYUJxLWPauPwi!t;|<=qB_|Z(j!gK~KmsMV);lrx0%k9RQ!|0I~mg`!Lk0 zx&Z#v1(JlC2;BGOxOzC6jXh}jo!_0ouw{zs&j0R({@&koq3lI_o1Zv}AmHmZ(9e~QO8_>~~aLWur+>b#zep5TQEp6Ktn>%USPrdLvb?lCkC!cYqH z3(W0>=z9U#|57y)H!yTUwk*h2dR|#Ny#ZX~^S>p`bYRJ2Lz{3sD$9J_J^lc8`~NTQ z68d#D15}n0WRJ%EpI>(5ll_3P=19TmZ`APNoJG|!hDx*4ifP4ozYBe5sdazuMD3$e z#PK%j=J}htG`u|vWQjhj8$T~-TnrqCV z0aN%dfQ!peN9jKV3t`Y48U^SM&T(7#_Zodvcg8>UKlNv<#-EERhmgl;*mTT+#S4&x GO#To2eU@zi diff --git a/resources/jars/vdmj/plugins/quickcheck-4.7.0-SNAPSHOT.jar b/resources/jars/vdmj/plugins/quickcheck-4.7.0-SNAPSHOT.jar index 229c7b4e9af0be99f46cd722b8255ad74e95d26b..8d9adf1092ea3d4ebc6b7299328b60505f3b2b78 100644 GIT binary patch delta 28716 zcmY(qV{m3|(}o+{#vR+XZQHi(+_5p4*qYe3Z9AFR=ESp~cfMV)%XuHUViRjazU zo0<$TCtQ#If?XTr_%OS`zukLo0&{G0{EyS!Rwq7r$8Y(bf=D1#JUN8K%23?$&LQw5 zemce$1?`+DwKRDx-a5c~+K4?oe7H!{LlpJz`AGz4u?SE?bk+g!alHkcN?pSicI}q# zS9c%!Bq<1``a+ULWi%TEHqacBnnw9Eqz!$Hcn%2Dfh=X_$(_`TZ#=WY&4Wc{c1}s# zlZ+p996Kw8*2XRl^}2#5ne*_zY+M?0WDCYPCfYU{ziPc@4jX~W^qbnpquP*{*KoO(5df_aM+E2cltk2&#y2UmaE< zo-wBP)p0h(POCWl&a`oC#@(>!#-yTuRv&(D3a40&Xrlpbe!z<2YV$eP*BQ8 z(D09D8QZ(oS8~pyR5M10`S9XZJ;5lB8!Z=_&{jn3p=Hh^6uv4&@PcA_9yO@dBOW&IQ!q^;Pg z3)${oITPqLA+kR78oqNVEZ1P&I=`BI6bG$J>}{u;UEVC`yL~qu9iRrG-u3IH+B|6`&`)Wz}HnIFT1009Z@BGV`oETxf2lP zA=M=Tvl8?4K_|a+(J{{br2rN=8q3_~X|+`N0Hqqu6e62OY zvZMvM5)96bBu>_DNxP)djv9=BF7P~d-8KZU$`3o2aaY|=;YAIo!l+6iES)&!LH`Ds zV>@Z2ha9l{<-*8g+#egFz|^wj+ZD;ewm4WpWXQ6w@k)lTU_d-t`J3<)eZEz>^uPoC zH;N7KAb;w^J_Gvi2rq3FQ56UL5KsUg(CUYoL1U$E*7$ zMing*<)wJ+X-adeF?B%xb&XiEa=W*rkIygOvxvUN&XLL((fxgo;CElkY^rmz*Y%*j z=uKdVvwY;LD$Ba@en4iRBsT>^vsd9c&iRcR`Zs8PgOsJyBsT^+WR(DaH>Ft^6AIiC zBC7@?+oayHX}=cC_fT5~2GGPFftgeqLOXl&JKNnDEou~v(zGoHU5C)T?2*HtuHmuI zTpAwPDH5#4Xb|{o!V5;i2B9Q5uUYH6Fg{zxCBxAr;{z8~mDtyU8t>pPZpBg|z*&`A zUm*2ww8J&}=LY~O>khq{nA@k(c7s8y%%n7T{U^B^g`rIVV5tRG0w|Bu4fSvye5SgJ zg$!opd}fTCBuFgpjX6tz!&^+K&U-5|B+g~&9LF%PpJ%I_Y5-X{l)#&MgLBTlB#z$Y z!uyL4b3r$AJZwm=9SI6?rUWev!x*nyE!kR^5hq%B|#s7|s`*kKq3`iJu zpDIt?VELrn80cM}>n~QgN(A3Lv9~K~FeZTSu52hI!AY1gdABIs+*DSl5@QqK{?Q}_ z7{>bD(%TM7NH^ZXm5;gc?Dy>S7M>lg#8S;Iwv%}AwYrW6^f@!@SeWF} zBdw@XaO|n1DQxo9{XFt@va8J@hyyFZo$tDtvo|ydKxVweiDB7tc4tC8$80bzM&UC( z!g~hGS&9N<+)+IIK^a_EF@5ucOmD2JtB1WTxafJ`W}Vc1CHcPqB)|J@&ZiFHET*)x z8#eH&r5ft=(0PO_Dw5|2Zm^N?Im5vr7-95VGFc+OUj4$r4YMc zcb+uWKsJ^*RLV2rItBgk zs*Twz_Zl(Zyr>>;%ULm;JVo#eaF#r6y8ebzYb-T87!7EFcBoqS!|uOUxRmIj?oe{V4f_4=e^xl=e_wdvxYBUXe1iF4a{U? zHZ;?a2LOKm*q7q!Zm(aguW<=SBw0y^XRzuX8_ICV1nHaAU~(zJCG5>cTUyf=vCRFN zEY7#~uwTgFoz^ojRC-TRC&|_-0^SO##{EzsN7>^-)SZ%q&E^B)zO#?>9!m#$&ioM> zI9d(KhV0nCi{niv^*!$6t+JM4rR!kMa_R}jeLnO{F*_~^$%*S8$z)h(#Kc|<%5k_0 zp?hoC@6NDw^9jjZ6SAvF@`lyS(P!d`hN4Wtgr0Cdx~+jO(d96}o-PdrE?^>}Xy!ot zmg^q$9!iqn(4>I!Y&4Sl_cSPSHO9~u(EecP6{ZOnjwzZsPyTYcgQD~DfHVfdyDECi zy!mFsYPvFqyTTo=ETnyB*m8S7?C4wu!E1h>7t^X6)+_V1JSdDidxHk)Hju`DaCk@c zY=4l|u3YscC0gl_jsH`lP@9|ja?S<|fj7b_+c`1XZ-hPkH-A-)|95Eg+|(%{@U!Dr zJe|v7EPq3^k2J!@1LCStBJ)#YblqN6BhOFwbZ#~FKO8jP2F6a7Sx@>$Z>7;r(fkH# zRI}8%tQ+wN%>n2Hy1Se1r=vnH2+J~%eRT{Uf$-nIhx%|{d!vcQLlmUet*L0B-iId* zZK$guzYC*@_Q&*5Y!6!^i87b4fU@}+uU;FHt}#OvR1e5u-_Zm0PiC5T+Upn3{9xPp z*{_g+G}$7WaY<2|5x*81UI7iNg?axf(NsitXqY>~D6nUYTHd6mB@rU&%|} z5~Fvc4J{?M=mT+I#X3EhvdQ?~TG9gV{I;p6c^2b^SOMe`DDdpoxDX{tK+Tf)$?jUKp*)@JFiT!~$Ki%}Ke+*~?+hc0z zejgPfB=h?YkzwTGBXXvUFPb|*bui~Mq;_VeP?YS5F3?o@xbk%EyZ^k7YE-x&@id># zRN=H(-R9v3rr4<}Ra~F+154=ZEnSppUsx;J)ZNn*^qFm9)E~3lF`g~d%Vmm0sgguK zP)~wj>2_Y5v$?@9PvFA?f;V-IG>9kfQ4x;>-MJ4+&A5fo$qYy@$3*g9`W*45HJt)n zmR$773L!#^(<=O&$@I@bg%H^)gyp%|urlc`l_|DCi{UX@I_I5bfH{_>q1apma}C}h zl?>SNB*U@-f&yx4`C#8X2=v0bGe1pZw3cTT;{0J`WXusom z!IY94Is2l?cz9Dmxd)Q-@MFX8Y0T<%Fbk6JmDp{5{vzyn=KuXNu5e|UyDEs+E2Xxv zZjCn>!j8~tv?$x;1zZUiR%Ew{kYSTZHm@jV;49iJp-i1%kICEkO%L7K0ET)h9_pce z*fx}h@zKTxx)60w*s#tfUx~tsgp^zqi;SIl(%I<*!uIxOShD&COI;1hl4%E3n-Vaqp0MDTpcR z?Hsk9ZsQ&w@NsZ3PffLk)YXDFKi*J~+xUS$G&Pi@VZz0b{MA!0=)PB|TggT}O~W9u zN#DG6Mmt*1>|y-kH34E1E`#_JJ(C}_2@fs1LY~!9wHPXQga+q2f@_;RDO!B2*SBZ! za3GjHm5iBp7x)W4$_-hG-U8El+{6v`gL{OsbNyHT0);%k#W9$PIq#)SQ#*^F=H)>| z%b;Ys%ZW@*AprQx0Z}*Ik>?nt2B9bI%Gn51KKH|Fq@9Bz;9Or)X4ov4XP10Sz?hEHx+c{^egH|@VO*pJO-45fp zhm>#PmY~|P`%g|n$zN6w;4P{fVqS|oq91ur%}ex8kL2u`?nGa+hWL#L)LDW9(riyd zVPrYR^FZ*Y0ukiQC%?_Gy=&#ZK{(XoVHpm-zyOR&pzm)gy<`4DSyJgR{Z7Z4T@`Sa~QHNF^3oRSR`ET<|;u+-c5_e;-`$3Bd4ilK}|PP zDji!7>tQcA@r)wbFinAP=yx+) zR8z|V831t()AP?fo%ehJ*P;XG=B9mz)>hDNQ5&M~SeUDCdZy69g!uZ8K$~WVs+5ge zQK010UkW#AT!7d{{*s7JNQTA=W#+(7?c2gX=is5=wu_NZD!j0s5QvvQL@yZwH`}`f zG+l(8Es@LzWRbt3zZt3j& zpQuN}nAX*FjU`1rNwZqnpH=Q8Q=n-jGRd5(H<4hYo}AZ0-jTr4DaYd~^;@0tQ5{Hl z-?F1Q9(+@+^h&6XSIH-O`*Kam5n*e=r)vS)^q4ovqETC|%0m_}FMi^PnqFa8dQtN} z&QsuPXH;1(M>S)AVHP&5B3k6sm6i+j9G&Lq!5(6&V63?eg8p6L?>fp#5IsbXe+N_N zuF&oYHl7a{*9=wAu8kPiS5nMZF9-UoA*P}SL?}|&4moNB{kVO^jPEP3wyAIZz4l%< zj%|RabKHa+`1WhLCI)5HWg!MWM$=Fk!%;2UYPpRTL+_%>45k`>8SDM(D?)VlK$uau zYhZSdtB3b<2XABeQD@Lz7w#zM^KQ_0DTsm!q1Em-+xtyZuaG99+fUw&&4;NZ)Ebo zzs3&`*synBnpHrlOBH=Zi%E03;P$YTLzht_E6<^GI#5KyGcUHxEn7&j%5`Ubl6HuzIMJ-hbgVQS_PQT&u6T2rEH5;>Irf;LYf-m@ zBeGI4-^*M0QuyV$&wzJilEMb}&SS0}2mL9sHi_%5xkcKaqD8nM;w=T2;%Q#@f6@B6)x` z*Km|(RVLpn!vIV9EIr6i7e+l@=D1u&g{S;9)8}?Pt_zT>!s*$oo563)I#C?iCdUIa zwJR}goVyM?w+$pUE(bCW6V<`!KS%3lyK|mV1z@jm$lE<5s{I1BkgM-Au%Xk%hXwE^ zROB7Hg3=}bbP^M0mdN~#t+=U`THq~%Y3lN2thP%gxdUESH=VG~RGM4in@wj8?9;4a zw;2({X|fD1OV}N81yqGkAL=u$nYjLeKyx)F-9Hm^+9H!+|4EdR%j3%9EJPbsO5sZM@84LOx4 zzO5}s&Iz!LWIlS0|NgFWE!e=uOIEjUlSApcI`O>Zfc+G6v+me-xeBTFWTCDc4q%E} zx8&i4sz}TLM`RjpR6ly);^_DGiJayw0fhlar2Dp2mo&+=c9iW|LG?+5C64Pu`f_Wz zRJ~B9Q*DB)eK8zEg^q&Q_->J+kYmKt;C_<=7Y3vuaNir>m#ps};NXVS&|sabh1yE! z$vwGa-S|*u;S*X_&>g*n^Nw6_h>*!EKHO{2*9mY)h zmJFn6Zv7AiWA+$uo~CMW=*7z5sCN;B&F6UxP%5K~w#-`mppX73ZRXHYX9m>&)S_wi zPU@!Qs7N_TZ09~6(<_1(qzhUb0UjDFsv13Qe8dd}SiH<09T?kdFyp+$-%Y%OuYGkr zgLf~_i!QxF$1+-!V|mET+Es%`i};DiX#v0Wk&MU^pX6TN8Z9P6o00Pks5gcUo)Z=8Ek{}jt)-)<@>^|4~z}A+!&&N#k4G{nrVlG zoxxoyZz1Y<5se_#OFktlM+ zdi^3DpaG?=!7K=EB3vC$Kjh{jJ%EpFuf7;uVBFAvdJtA)67vDln*;eXa8Qi_ic$&b z85Os;ga>@Hu4I`{N{gKc2gpNCW`M$;GV%j-32c|U33IqKS8P<}GFj;~?6x72$>x*f zhI|+MPz}JhIV#O1`Iu%{A2wl`pZ+*Yet;$K()^(eJK{P-5WaOth4tjf42Ud;0_k$5 zM@a280do+UyuJ8n7+1xVD=TU=FAUO#;D8# ziRqGYAmxri$(p$@5VL#;@6$Wozp66$WOlsdWr(Po-@5V0X|;^(T4a)cut@NI)VvdKTBg^UIm-@;A*b54S^V_72fZRS({q_~ z>QFVqd|Tr&=hLNxP&5abwIRuj5vL>IHv}0&@Y*x%z7QCL<@RN@;knqt9h@QgC!FdA zIqnGc;f?wcolzXc!EdaP0^=#^B$?KO1OtVj97hJ6@v(-kz2W*2!}(kQ+u=?7j{4)b zRs%iWNZXMnuLQLbK)SXm9I;q4~tH4?s!nRjS zF8d*wZ}G{RV59BNsPv#SM5GVZjz}&2#s^jq z9!%Y277Q8)uE?>+o|m!#vayq38@yort7aU>LfE|*wCZj5?G&%xQ3%jNbQZKsv;Y<^ ztjTBKV!(tC)F7KS2tYgOHA6J-EnHyHq*t%<(kZOjeuQ_}$ur1vi-!c0u#dr4VRY-+CANjQaU=O8+4akOkFyHy=1i56ojMzSD*@lTot0HB;B zNA57>!>o*Xul8-c^QiVDM#s}Pd%Q4| zv980QZ*xMHO8tf(g&%<;raFRc&Z!@bKYr7It>-{k!td`&gIbiu-=zVH<;{I{Nd-31 zeg6CqHcODl-<}WLqXz!?1e&uqcDwlR?fky)z1jE~AEOpEsfZJar!2y>^$TX>kB) zAmAC~R}B@Dv#6A^mXjAn0C~NL56`(D+iuvvCv-T-_t0WqB)<+h1-y6PTvaow?s?GR zTN>NlsZVpJz&g}M#Uv^}<}0o10q002ryzSDph6$Hq@^~QUuVU!Bj08}<;(F4 zzji;c6)8;6%I)iCes6@x9irY$8#CrNVygY<=^(N)*sNu0vav!Q>ua=!YZCv_}y(e{Gz|zT1d7uGhubfs8q8=o+L92?ZcxBsz}&cdNUxsdWSS{nwv zL0T>VM~*vP;gPi^?K}rY&{IKZ4dayZXi|yP1AYa8*eHC!px_f?BO+mf)7|{P;{xn) zgiHZQR}mqe5ph(%h$TFK`nT#v5>dJAyO#PFbq@Z_X~M?$ME(Zsgx4GMsb)$$gPY%o zj?~T009=cz{Iyj80)de@T$aGM+@axaW~%%7saw_JcuW2Za;|Ka_tirUS0T!CSMt(k zu_Zj8#_j|mHf(6VmcMtFG2lr$1BY2I8SQ9K*$I~P50+To1ftgveHE`gunCV|ODjD) z=9_oq0uG(!$C|)2e($EdyDYu?qaHxbL%=j4HwpF_kE*ZfyJ0f!%`p&(^DvBC@jeSd zl6%PRL3pbB#L~u#*K64U+BWJkIrec2)jFg_wHw6*I&a2o`oVJJRhdqS)6@Nr=cDIt zFlfk*_VL{8NI}(1RL_P>brK1avu_vthG<2vddS7^@EV4aP1n(S`tOsO-@z?0W|wJ~ z4{?aAIG5-NzU*TST*pAuW?cO2z!(bE&|jaKTzcQ_qxm}H`g?COH}Z8I*rlfjkkLtS zLS6MSnERwODVx~0gHu@E23z;18v>cv+=eaqb(p{Dbq(1jvaOX(@=RoW_zaokwMAd7 zN&GmQEVg012EG8@lV3WTb00jSKR%l3wRRcYKVcLtj|FkJ&mw_0fa;ggduMjVATt+I zj05u4HZ+{byeZHdfA1gQJ7aHO zH2M&84_}bq->i%ge;V+tWdYWUp-75$V8vB4>u)sLMNrZnVFlTFKybg$UgV?|aYeC{6{i-ejqV3hun$S(SHK zx)GNZgk07`@nT5)KQQmncL#eowhN`&?rYY*+6 z_td8s(lp5cX0911ek!33TCpB|NKsg{hV2?KI$?b)`BNGdDGNn&kvjlD8t9 zO;#srzR4Al6jh~BMK+E;<)ZZ43|;Y(I;|>~Tjy;lEmWEj8xvvt7obUpzd|pAY6n~> zNkXgUG!w(!E~FcLeye{HYu26B9i%II7vWVO%*cPPKX@FpYB`Dc4?8noMRDlS22_{u zOVB0OgAmZ`&jC1d1|4CL<7TvaEc!rYz@EvjNhR$1VCZGH(jQP7+Z4ldo?w)t=kt-Nk+kSh|=z> z;azZb_QTRhc--oj{?8C8XF0$jY7v$ofP<3r3BIQw|ACnOlA*py9ae*sm%L?&GsEF_f6Zfc z=&VEV#WS#O^rd?0q?tp_y@F>}BR{Mirv|0Pn>$pFQSR!u<7ceS7?6L87b5sFrak|i`+LdLjj+S>6 zmhXFQu0Ewu(r@`p{yx}}@#eOGVl$P+Zp@n_651Oi!dv$21T$ZzzVO%#I(eS(#{Qnd z#kDSSdsPrn%$9AO!evKi@pAUtANnb^CuX|^0lu=R z>R9$o1u&Xy-FjsX}#RmOM$1U?^5zCJ-B}Tr!!GYHhdL1sl?edK21JHzKVpWG%KIKFlRpX zvsUuxI4yX4iZV~4@Yt6=!@{1u*<}>0dM!N)pY@4vW#n#QI0IA%M(qlMB!E-95DVGH zWxJ_zRvvpH3MYUW$hF)4@Oz#Ls@XA8+3&qYQH!2P|bFR zj2BVh=2czKKNJ&S(iX7-c4ZPL39z~UaQB7Y9^dfhFNNOfm$-W6-gYYA%%h)laJsm% z61ARvXws+hrF9T4-|`w3_W_5HNEh@@%ZOQA`kk% z1fA|#YKI_;;SdFyM(plUd4mX1P<@9s-mxWY2$uD}LOzc%@pyj3MC`R4jon%UZp;F9 zl}fyWW=He2(*$UwedrYmEX0?EkvfBN+-Y##5q-`GCyNx8b1im~Titqc{dZ^nlvQx` zh#UGQzb`_&vj>QOodebIgpGbC_Lc-c2_O~`oomm2MNo4cSKYA7KbMNG}vh&K!{7TlKcv~UGs|sOPWGKF;m87smRM1RcK=6P}tt3z{%`0$y z#>lOGQ4N2OJ1GY)>OT`mg?`xNg<1!bg<|nEp3{#>^KQAoM8<4& z585+q0d_W-hqAgi?f-pM^p!*%!d7}+6=Eh}mk-?2N)X)6(~bq|UW@A|IA~ZQZ>)KL5}1asWm+sH4nWJ>|B2a-*_CW zBwtc@&T;$*JjE0J(*<`9x+d*A@4+f?geTSKrBI|$tGaohtGK04M|~5c(qzYR?VLNe z>v-&h|F$LYdF}OiE#f=a67AW+xnx$G`_z8vvdO^0M+h9*4B*JAJ#^%%jj;8g8{2_m z2*u4g|BKbQtbE4wR{;EIUg{3p1Aj}DGXUggy{UtCqhDdFTy%dW8;^aqYqUyyiuX@X5`fENl6{6%j3N>@$Rcfehusz%ksA zrIt*ev{u=W198s*B~4EfrJu#hrZ$VV6Ffm`t{~emRL%YJ&g7&n7JE?6c?-n)Pkh5v}1*!73(@rRON20J_ z(9?Tm;Csh*@ZKbs^$M?WN2PYJPOH!}Gz)X8{~gl?=1vs>ooLPp%5yDeU1Q*bZ+Q;@t6>mYMj%vm{dcjT{YLl0or zMU$~;vE>pI9w?D(Nphe)zxjHtp{;s(dC|vQh9E(BySO_8)JHed!1Cc8r`arcgXvo66({GA=!k8}t&+KJj`j9s9}! z)oz1Z*ftju9X`QN++U>?AIm`VYJIT9JjAsC01GX?BGGia?Wuu1v5p3NGwX_N6lwV{ z>@E5eNk5#x%`s?d`IXwyD{DUEWbcO5a|g#50=1G*mX|#ja(&&m&KW83%lv@Zy4ij@)X4s^Ma#KM1@=gVc&7QWwc>5vLY3(g8R%sc!QL`Ss^=d#K0 z4|T#%!{^}iWtF>#3;5mgz`NXsfy4`(8ro<2Gr57Pl|k^TJ#9>_EfVmPhIjTRT^waN zt8xO_R&k~9pv@9OixMC3cUE9B*JE3{@ekiPz41g=B+8XjW3aL}nQnvzxPX$LI9W%^ zbHkOxy@g6vd{(4Emk_H)YB$+S(n-HnuFyco`D1IRfCLL>Cp|`CF-x$<&m;5ji)f!T z(fz;^b}_7bqQVcN!kIt)k2B3RIc`z8fza={X@Vz0$9TxCdFt-_)hktjj zqAR$B{$@S%5ZHk(TwaV0_%Wp>)D7v|%$xZqDEB~%qH%1%+RgF+0)cbGx1M6l&6ZE9 zv4J}Cj5!8qR;R?r4f?Tq8MV~MF>R*M*EMi9wz$SrY|xltQoeA*@0AyO&zv4u?}d*r zv6thMBXhH*kg)?~Q~U^5XZ$+iTJ7AR>drb{Wakv!)ra)-njMZo3)q6#am753cMP=A zd2&WW8Wr)%TX*xx!WIK+AWFo|7po)6Ysum6q_JQu5896I!N0w+Y9OzbL$yoQgell^ z!~zvu7cGZi@!ocr;byhwT%FIu&XtQ_?zpg1225MD2DyQri))wRh68U56Ea&x;2cNi zJJorISQE*moA!7Vg8iYqu6Pa-iplp><9kejty4+hdft-N!qp(?5%zxJLU%_B zvhsxdbCrzzaZL4VP@Qs;bpYN(Ci~H6mn=ihYUWz~V+p@&(L~0S)1utCxc<7D5CA#f z?1gCSk60jyk^$7$vaV#42eY^VDA@{=aZV>^N8f6qT;7^AXVhg+e+X(Mk04FLeHyoF z7_*=R%#O%0L0DkX@ZK(TX3b&p?!qQ9M~DpG=a(o_AU~wbN_?@-cDI}b!+LGwl=jjj z{BVoChQP}>l863tvuC(&TfdU5eelvppq7b>{xNWd?!TL=NxnK}t>-2~3j>kobf@ar zV+Dpe+n7KpH97QHN8?LSP`MdLb4w@F&-QSN<~&qC@WgM;7qqqk^@InxmE1TYd|aU$ z(~%DRG`9#8O@->fKXwxnBpDUV+TTXV1iJt&Q6}~Dx!>-S+hD};iEkqx< z1E4@Vfxpzw7L9}ExU_P0t$kh~t{mg}SpztK;d&jN=4VfI(DWzpoHdjdynMm1i1h^#SkVLqmwA2VkyCe}y@K zVR>!;-M70pVR=pEombaLX;lj-yVc-NfTeY~NjQ7H=F1(aVX>&l5q>R3u(td_vX*NL zy=#WXZmG>)>X|w^BqOniTDLi}^hONrmYgC*^-J8YsTV{Z%ezygBAWC@a{2 zl6(M++q!8+Y%BvHmM`0~-+>@B6K3qLJ(>5`{@(M;D6=721F9MAuC94KKhM3tV+VW* z8woA1B|bl+2Yjg;2`#NLJw4L}d`XfU^{uP{FE72`-$QK|Xon|?LIFs3-$MW6Ofdcf zR$xH>$BFa}Km8vA(mJLF`w#0tSRna7tb=(4^Z$(W2LJydB$3;_|5qb@LP7Aq;x=b+ z&|JcQ4uur7{U34CHpK$kiSjQNB?=1ruSHvmBxuRM9&P-xpsWATk~U0L(2@Vk?r4Hm z{$DJ{5R?N9^?xkM$|ybZ7&r*X#eZZCXYxHLUix+?C{Y`%3Frd&zXH)QLZv_m5RicX z=o_;1nLtq7bfGR#L}04szACyFjsO>ISQsR|bUjw3dN?^T-H0t+%BE_)Ee18GW^>Kd zKL};U5hox_P&5Dvh>=?%#3?1jK#WB0%twzRB{QM`k|-{}p^)PVBE_H2kIm~o3`>RDk5 zom*p_z(Dtunl6Us>SX7nmGGZno6>@7~ZTj;)Fm|>%MQ=G=J4T z8N%cA3l<$v<8KFA596+X^*&%WdCQ$(*Eka_bR($So|_`T$83!CYXcA-7y>V&zw8Wa z23E|#sX;%-CYx3!r7^n0n|ciAgczXR6i_va*ECL%w8k7P6MXMAZFawsb^WR^x#mxp zX6YsY%U2>YhRLZQ;RtKK6(;DY=EV}P#F9L$ftU~6$HQL&h+g`0fuL~b&a@25e$R3E zli119em5o$Uy-EQnkGp*GQ{IY!T(yl`f2w1j3R`t(#1bzgm}W4WH5*6 zqZ$KL?0kFhWbXyvIC)Fm&pdpZtBORc<&5m>k&Rw6usymGdisu1H!eNCGeEdfAzDIp z&lPbDx&za3GBHdaG5v@UB@w&xbnV&+chyoA1 z{Gw>d1y*jm+F^=$?v$sRyKN1#$Uday{&@rz1();@Skrb7kvp#C=pZ?5KV|9FWv>2Y zfWL{ibeAPHPVq91)A9q@_~5#wr(qZUw~HdWCwF6(A;t8k`|<5FhKg5fpoQ!&l&Mkp z_ED1>!O0y*zAj3TQ++>2xKjfTg=sp zW_X7AkdW<0s?-3EO?8^P9~$gKMVHt*X-C_1(p9gDbw+ci@Vjg53AzSdJGwdx4z!&0 zv9UsF3b7-)T&e0+aJq(B_aScS1iKwrpbn(|?>%Vys1QDhJWzZnrT%o7XT}{831R?(Upi`VbhN=)*$nZGrMeKEjANlhUDC3x3d;X6P zD_4Gv?NjjTD85*a5eBbBT>Mz|U)KFf(+KM7V&D(5BieqL0jeYU8G`-Kn#i2M3bR?jO z{~KF?^y`0POB>!BV+Hfusd2)d6P=h&M2o#vokheriFP?Y1ShKWgd$p`0FNqLhIQg< z+R~CULYJ~pH@*OME62vw5s`h0PTezJkKhz8tf8fIb4XA;p9F`Va}>Z@6d=ErPx{tQ zWNdabmn&*GLe}=^A+4%165SwXc|-z(8wGcOQ#G*D$PZ8MO4Q|;+RDz*Gl{=uYjoX0 z$jS#gXt7LD&B)u_?7P}pw%Fg<&ne&iOcZ{Mcp4p0FH+JPV2gmsVdRvV(iqYy^H89q zmHjzKGRRy2Xq`3-zp&G`3-85EATtEY4c0c_x&2kCz_D?KpH8)#@&=ny}(!$uQJkSzASk%7!iq*H9BGb*3Dv%=-*L zA5R5icSdyXOL2DwF>pMMZbB{QXEz-hVmvZy$=DE0Oow(>X$8&;d$1q!v$G1Wxy{QC9zqLcHIGAO#J#J zX?K38&5TyRM#`30MI~69Cl1=$RAP>ym7W#fx-^a+EQT7o_5>fk2^I>W&iNWr$Rdrf z6Ryiz{!6JbiaxQF`i-h0u~vyhE3#(!8^7i9m=)xkU$XS|}5s>m^~2 zmS~C7;X#30O2)4rWvw#|xAaC(qEhGp}A$ zR3G9Ey)TF1hm?`Rhj>`jd;r(=&5%rpv{rqcW%2Tki>bx zkW)P;{#ozDZ?k9mU59w-!Vvgt49zDq_OKcV@tNv6w58sSetVEaz;3R=*8?)!;%Ps5 zHa)m?PY8Ld;Swnx-Z55C;t;VlTYau$v6;qr-L5wBQ9^*WIEMHdBz&L^gklEMZL1ig zVl%hEkT{Dk()M+wyU}pYk3l{Vo1Qtuz|0(Nl?PA^1$mch6#QuP6bf>H6RbWE$%K0> zolw}&tlK}-ko4jgI~~Zl7VBI}U6qV$w)FIQ3Z_%K9-kFMAH5xT{{Qwu~`E&_rtjH`8XKNK_b z`>8Oml<&h*d^Q`RqE&LMvb#33G5Bff+0Up?nWq)l(R1T0fvh87I<`V3rWjot&*Q3F zlSoHVaOzIku2ep+nEaUj-c+16b~D$+Rk{#-4O*=(`B>WO=rC+R5qpHT5GxpY$YiS` zC;Ma_wgoQ1_%GKsD@aW!<)&drBJ=}m<{Ph_ z{0i})=IoWdJ}tt)5pUe{l#j4`hmfo0+GHCSjgQJHb7YsdtkPEI-Z}nkNlYV*HL0kn zJVTI!aYLs+^N4H|S0|liNU-FM?Tvd`xmjl8K7lMp&-k^~)MH&t^I1P+lGr2n((vq8 zS$$AL{#tPolv$AZX{ZTTq$#>SVQj4$epO?ld;A_jk zb#j%*Yu&k`ykp$`3<;HDHzD{+2nb+gA-(ool{rU@$Wd2RC>{Bk=kcYw_2Rv?z&g{p z=JcoC1Yr3F%#lto*AELv(O%7Qk~x_5<{e(@Jh3Fenlb$E)u5*p{m;9HR-#u^)|BYp zBUWNMKM#!wl76>n0>K2~O?EIyvAtS^SXN8NSOTx6itkr*4C+A3 z3hG1{4RvZ$C>P;rb2-6t=pj7H`J+POH5E>48bcy)U`v-3?er0>8)19SEQxadiuqRP zhP(ktHY22o@PN$laEn{LLY0>Z!x~c|hcZU{HcFJ20 z*=VLcw3vNYtP5>#aC}Zcaucb4?BlI`=Gg0>9h%46d!un8`qxiTEyvO@(q3#vZZEDF z>?=_n;QgZY2({(!*p4@yRH3T%*yJ@Svo02|UG(o>p(D17OJ`6Qe;$rbl+z+4p@Yes z9QjWiA<)kSr2vA!(R=x*A#!?EVvIBt=geceGR6B?4DMvP?2bP+3$N5C*HQ|PgDUja zNt^s?jS6QYQ=+Z_-A?G(^zc@)9Qx={PkOu&V57NA^%0FedA$aGda)ejOEHNK9^Fp( zRF&wK_%k8<#Kfk-8DIpz)l5@0nx=Suv;dqB!s^o&AYA2NhHPw8{iK87Ai=NMNhCJm zOy3QEqpAL$FXi%u^IN=E`<&WQo_4E2yw*uD2(IHnvqP02-~*|{`;z*14@cX#V22?d zu*XhHo+k+3bQ0$V>em^IJ?P6`UT!;32bV)ZQdH^STiYB1nPSSz^h1&V8|FmeSzdJ~ zHuuu(|LN*0fZ}Mjwpj=o2=4Cg?m-h=gS!TIm&F3XNsz_e$>Q!#a9AX`LvUDvLK z?|*N--&A$g*=L^fbk9uh)@=7V-G>aGCqvn*1PUo<12aeFn>u%n#|q_~ym({-)?aZy zSgNZJ#O=had>j;8pEC4zMDOGYubTRNQYEI1OVp<=SSU;wVLQv^{1f<#t(;rTFkiDi z$|Gi6sK%)C7vs4|%7qUyQ+3pVYJ7{1)P(FsW5NRpixs&aS=I8mj)GiPQo|QWOk2 z)ip$(tBy|$EQ}2^G>8ya+vYl~#{>=A>!Ot}@Up zC}ncOPW?db~c6Cm9kqDfpg@*%XWGMSgaAuaqea2p>l z6mf3c`LiG?50lILgIHOGKi=JB!k^2o+UEDF2?g>lUrQyAf&Y4w)g^s;deD1*f5pcI zjRXQXfI7(jICF%5x=0@QM#Ibn@g)#<-#0fFgL@Gq-ou7DzR`(8P|dVA`YLB-oszbQ z;j89g2c9bz9U!wse@?f4Zyu71R8$1+usiEp19zNB+2*ZhELKwr1MatnCffPeZ#vFy zfkUI*)^Q|o&a4@j63Fs`BREOa{Tyvo)HB#BK>f5BD^CIFT(Q-$hkMDyx(O0^N@>+_ zn4^JdvEa(aMT)y^i}A<&c;(U|*ffmrc_u8H>az(+M1C&THX&VHu_c37ZTKmdCOneu zw>7o)Va_j`BfXvlrk~lybsW5Qxq97+?`Nov4pW9PEt_qFXg!&|41)AAa8)55mW<7mPZjcTB^#~GOZar)whhYzDKfwr3TSdI7YmhCb zLAWkS9j-wfGXY(!D#Tp|R882cJMQ_4b;#MUK*TmKgxLkxXYogHFt6*Fd2{~T_2U3t zyG25fS69au7<5Ga_$Flc4w9ZKWJBEXIyx>SqZE@ ze4ro72cwxIOUc2^l3@neE3LzMssLUxe=%tbXR-yRjQG#jX6Q12#cBB*-72L2cJ}OP3KJ zW(Jq9u?Z64d>atzjX!WuDMN8rr|w%(m~MbQ;-n9uNf$`BY}XGVKpw5k#w2?@{>Ey6 zTwG2ej-Wa}!p+CD5QgJ3Pz_n@0Veqktc35!)5`$4RHQQXtCP($LbUT^B{~S;Bt*?U zc2IlGco@K67xGL>SQNKOH|L|3S*@GL^<mhttcl6th|L}X3?6uD*9zVigCQ4mUnUmg*63v=`-6%oqE|JexCHr2 z2nW~P+%+{D-Bk6I_FY)GJ1OTN$Ds+-UPgJ>UVRHv61AVC;^Ix%jRv5$@Krr_q4~n{ zP6z`Hk2-W78Zm=`Vk2s{(!d9tb~1i$#mSEyA2G>Qz|^|0wm{Vf7M`4jsgwJ)z|aiG{~1f zDVN>15v1Ujb#^R}N?a>|*9$g`j-TgRD@H5D{9^8xYJHrv5>(csZ(Q1qdk`%a+m2!D zcPLin)V>R85vMQ~a+9f^=emd6llB?iVn{to8c}rHo`kEuMs8q22@k*&34wH;BayGo6-%Rk@PnR%2 z1tEg^eE$gVK2rKenZNDXR^R*f8dD?O0qnGtEbofSIs0l3uS-z~N;e|aF|5y%8qn&H z=6d@@=@J?KopTZb^P;q+HWJefA!`P%XL}?Wq)$^f8>N!v=Nq8C161W#^gcy)%B}E3 zbs!6sfx2qEx z_U!W`v?jiZ6og{E)<#x2-S{{nq3k0*vvc-c4%lR!F;&j~A9{YAdl0>S$}wXn7Ug9K z_W`6Ac9c3*Cb9zU>*kop^aL5iD>gE2@k}dJxLxy$+%y}A!);U#Sb91cJgYY{YP*(I;OVJK5ZE+3;}{T`V@e!eMhXjJSL;EYI3{us|qkT z%Db+v?6jjIIdPII9<|=e6u}yBB>+a*sq<=%W-WwE(_yNy&bKKw9CC1=?hR_&b{44Hcw*!)Q#+B;M+Ki0>L%~3 zT{6*_#LR)W;R|K&?2qv1D7!CD6TT!R*UgxL**1ACad=Wj7`_JEv5XeIj!kjEa%`I0 z4AT|t<5jwAdEXELS7H^mxAT3@wxpQYw#2f+vB^1XNm*1K?@!oBZ_G^D53pv3E$t6n z)Yli=%6ai}Z;}fu6lpcpD>W_zDthfnf-4r)vkY2+`mFu2JIY8kBS^%Pbk2NV)YFvm zFAQPw9Iw^D->vJ!Nx^fFSFc*9R)uTTcaQ_5ek7uoVofUPX*sbGt1=ClU8VhPoFRng99d`-qBQ$LMY527~Q>oz8*HnE3CWpXnf6YLW+Je#SR&42` z;w=CSl;=pB7bmHC!py&LJyGMj8+vp9n-i=&-5QfUiqA#_tB;Yp}keh{1}~0Q#WGfkCdYn zX1*!mpG|rR?<@OeLm>hhOMS~Hs2L^hyjS?=L+c?@XW}~D5B8E~$8IzqoE2qfxb(c- zPZX_RsB);H9Hi?KOP6+5Q?&TagdHV?e;-L88X5^5#LdNK*m#f|Zj%*12lpfr=K|SP zdTFb#w{=?sMBhFCYj4^hZ^kWgA!hC){f6aLE7%-8x8dl?dTKg)kW!sy)*d_P6Nm>q+Uo^$vYd97i-I~s5>r^h{xC~lXeVglk#bb;}()gr1q+%4d!YSd3B z={i7T8Kv$aI+V8XI@Kqgh6`bYP+SgwCUKaD&2Lu0>R>&g=~u3G#ujk=NPDCmm)Vr7 zz)C&$K=>C>YRzfkA(q4Erf}9YaZ!_xwC4W|s_J6vVq+mYpuxb95y8N){T)js0Oi^M zkU?4P01VLRXTTdECpI zjQWGxLj8{rUWXZ9WVtWA zA`84Yjq%7ZgUOLgU0VII+ImAZ*jxjmNaC@j>{ugd5+Fk8#m}Ir`3^lT)QZNG&W}3F zQ7HS^q4EHNsh+y4WU=B+1+g435GIurL=`k?4XJ7^t{_3-MjPw3cTBAaCpreHb_z7#jJRtUS2GB!zn<<*XkcEmMxxiUpttq#qhpU_ zdXJgTafa;-mX#@uqgeu}>#>D}pY>4OadX@}GTlTRLQR^Mvc581&l&jAZ77zq9o>Pd z&lADm>PemcbE=vyq_Wx~Ds@`!ogXUcLYX-z7`VEhnLw8TvH8UyO2Uz4&&9&(v$KQx zrG1GS%bihE3xB+EDJCejIb=w=Z+w5gX0khQC7;85i!OT)?mCwiI;X{br8yj;kLC~4 z^o8FvLo`d*dWaRp|HG9j~3h z70_1OE;(_XyPxNfyP6QHKEWO=I9&#iPJ8$=#c4u;oRO=Ag{rTAQfN+J>OECsU{xz) zep_)9iSS#%o`SWVa>7IR0Itz|xY~|_nuAX?rFzU=|4ndze-p6)tYp-BBzc{P!?MLK zKPm}+-GeWyw(IXu1TmV?ka|VqidA!XC=gTDpl^^OP$6$jp^rk0Nh%`r*5Lp#^fv4g zb)u~>9udlTkT#h^7smU!=Zy2bEo6O{QEy;%P)V{GJ!cx~hY(19!#u_o5<#QnP{b%T zq9}|vJlgG(f%K>ghrS^JTVi)6SM<%j;y|@SaE@1lQ1TYe-)Kk*p)-gba$N7R12oxF zUGd<;tg0+LUi&@~r;IL-G#zS1W$wX2r3Dfa^_97{;ymp`=wvB9;P&(F{T3*N@PrYM zQGhrW7=0R>cDmNQOdsbtUO37PN){;#qboU2jT=G}2^OdNp{a(Iw&o3qJifg5r#VP@ z`w*4_M8eaw#6q_I3W85JK=*t zf}9UqdeRlGo57H=%Sm#TU`D)7O^g?yCCKTuYT!FcAzV#){L7QXJO{25$^m%)AKf>v zutr1@N57+^KE}q}vSzcxiSwK{tzk*T7REeg1#9=4?ba_87rM12&qHr`oO`fk9DieG zzuqE`oYmdHDfpcj3>>sW6#%xxolMXuBohi|ddEKnqflARW=*T>`8&x{dk`qJ300`sNTwrF z(ObOiVmyj>o{dY3WaB2q7vkUdde{nUTiO>6K>Uu3?5IS4F{J}+OB-=0Dyf6gXkW@< z%9{HG4KZ2lCUDT4@xALDwF&E%!GaFI3yVA5P zOsqu83Z;(_$!phnR{+yWana=!B;lWvM$dV#_^e2V2sx?HB>N^A;dQ0AK1RO!>D|Je zZSiXQF|42hemfPTiQ0kmju0iQezhY&OZ@`kM@P^SOuS_SnzIxNw*2)4$EhK%Nz8ew zj=t%vp8FuRftIZk%z}%;yz|z#ZJ^O`xLLDp_j*xOSruBw0|Z8#Xr+B%S%qdZ6&vvx zXOwHIvKFP?(158K=UekpHpf{@PBo$tORNwymEO;l3mMMU`Boqds`bc1cXC&qcGcjL~`ear-k-M z;$A#@|4%RMqY7q6TMEqvoxO$v1A2`fc_4&z|ud|}Vsk5LX+sW)&J=Xoz-Gg>v zCmOkRQ1()*+O6$mUb`R8jIz1xCbz-ux6-W8yONsRc`qQ*4`*-A2vFuAWT`}LTOZev zKw_s(C$(VSclOfl}{o*J(1&fd+#7%+zdKN@rA%&?b>(gRL9IQU!z3163h*&3p!OYQd}1+`NEe?b)26 zF}IJWmA`;<6>9BX3lCxuHy$9-&=g1G+wciTptr(LhQ`>f!OiwuZjsY*_hl^<-vWBY z51vEq9L%2$AI}18a1?&^Ur3B^(L2fOs*RMFu{O+4MDq?vn=f!iWh@;9SXXQJ8NFcz zllMFnkq7%=&Db9G&LjCo1ego-rx1m1FISg7p&|frJ4@59q9-;|!>dd!6OHXyDlX$U z;xrbcmzowr?9uEe&yPzM-Ys^GJxN@PTm2z;&|aip=o)-VJO=hYHDB)^VYxMF-uICg zzgF4$TvcO_WCQ6sm<|ZcLr)OfoaP51cVt`+iTLWj-N%EF-|Ty|PF1{LKbW4A$iq*3 zDtrf=%-Q7}+v{Fk3lfVa!L^K!VnS&l&tm;*N4(fr-B71%Z*1acfQoO#AF^Hs)-dA} zALlD9u2Dc^{DYiR&Z=XNdJ~xBA`+G}d^=OhpcuQcLm=jbV4SZKelDqz%i)1%3>Z9T zAgyzJ4AT?WFhxSQzDc7TcT4D^AM#j73MU4_VaGYnGQ&PC6NTdTp!`-yWf#Hi;e2$t zp2C*kbw6mJJZ5rrR-M;$9q+ialp_aL-NqkLtZpk)&UG` z{IEQsJ-|0tLE6V%uJZfS5AiCW`uUPowhsP3$T8l(AfqCFPT8V~it4Ahd*ap6J{=jK z=OgWE5P27(k80wPYRJ!eSass{YtRs9#|26iFU!S9)R8ZliRE^?wL;%l6gbZsI?t{8 zx2=YnAL589+Qe&IpqKwVr@RtTE`99}Z0`CTUv~DZ=LzdnQ+&uUojeC(wLPPU`(WAp zuA;}fzCobOVW4mJ0>BzIX=8ZX?nz7rx<@Z#?ffq%nJrc_N@}L*8RPyN7(jhH7`S zEq6k>QXT+b(lAtZ!2i)YIKiBQVF-3tBk)x{Mx~Y|QxL_Zae;dvJi~yx)+UTQFk5@v zW0#=>hm}b>2>BxOfFuJ!T&3*X>i0tK6=NugSWl{pGi2gtw@oo$d2yZCM_Yu5*vIee zZq6R`l^qPgAMJNkGJe=Dl4a=!zsJ%$U9BiM&ftWI@Rj{uS0t-DnQT_&8d71Uygn>X z+rd8n@U@5;KH?pl879z}D(L>T0x$@Vbn-I}Ki>4({BQb$`jmU#>>h^G= z-?&*cGV}A%DJAE=>ixqp_Gg8Y2KZs`p{7}}^Q|D;`H^tawT%29L&=Ss=0ilq2v91D zI1NeXmQ8*55}Wl$3tqiZoU5{yY)4j~RlSQ=FgwJdve`|k2X}m{pB!4AyQiixK2smr zk+d1~@&2${+eT(2C}O$_4;Og&_UUg30&mXx)`EQFCzf^H0&Uu+SRSbDRCo}Mv>MQMAxZ+&qN;8?+|EG-~Yc3Fqc_*_NH{fZ`r7!Dx=pJ_LH zDV>#rzNbR(xP@KQkZ{wiCvDwHq-L?F%ZU8x7!B85K*-joNX=eR6;<8U=7A;0IXbYW zpF?zpa^cdE75MdA3?4ODjg30U$uhh-Kia#?f*5bOZwP9^oCuP1gJzkzTMK9+Kh{zj zzNP`qCmd{7&4yN5b%}qMVtrgTL!d({Mx)@NN%U+>Hpq0G^ju=}T8v9w-KEP+BFBbr z`(gFXQ<#WwgSxiNYMPgq)U)=eR*84HvTQL>Nh!+M(ZX~v&T?YgIwYrZ*9v)TO*2tV zb;phFcdz(8)AFKi33mg~#?{i=wvFXS!wjQ3vROOVz)pd>^{RBO zCuxx@L_)C_$1?x(+p6q_%Ki6GL*1xMW(h@zs3iUFipX1s(ACBr7yBXBm{0vBN45!SlkJ&WdvK+n^2iOjDEWNN%X0#G)#Y zN`%M3OK91_vM*e>Pvyh6N&XrbYd0rI%@(VmA)P&!NaMXuwiQ@|IG^sYS`}lznrjqd zL!Sk8mx;)YSJrc+{pu<5yn3(s*8j>N}UDU(Y8<(zzs`Fy=}qRdLrC=}I~^8RD7|E81&* z3}mV(Sc_Z^G#IHa)7=@`4WXKZ{%)33a`;v7A$Ixq=Zfj80;O1FaiQ7oNJ~@+KqAY~ z!bs(0Sy;oE4_@$*uQqc>yZNwfrYOu2;4Pw-nr3$LM&+&TL#PYCA`Cds_j?*JGPq3yXRhmghrYe(NefAjPRhTG-?{4+6 ze=t|^h$Pc#$mj8=-{xD3PJGi?sTj^kZf`;=4-eNg8uvixq)FxC=o(Rw8qIPq;Y~nI zE_ULETKdbhWZD(2#%%e&>a$1X96IAV=k2-dK^#0GRnl!LbBIhVibfx)2YPY&YU>U2 zk&WooUzDXny_iqAT$*Z~65g~zCQ98&Lc$G4md`k$O35hl1h3u&h<^5ivclb@-6B2~ zY|LW!AKM}b!3EMs)-zL$U~mdeWgbc*ur((am1jJytrW&RHAW(ylL`ry?M^A%&-xp2 zoKJ=~?5lH@ZsLEg|B#fs8HQAFopuuJ*CU5QLx(C0EfYcSTkv15Wrr*3{Z~nvC$f z>siVo85VKB8QttyY%IAb_ZL3AI^l19e+%gIU~I4)5!uKtf%b97leY1o5)_amVO179%{J59$SIyTr$RBRQN5Qay{j| zZe{0HZ+I@Uz&->2uIc+u5 zHLo+adYuwuWnM@pIeF|{RX?X+gh>}7txuJ5W1DlRb8s3Pne-fRF|Pw2;g^h69+R)E zgCN8Iqz`a>7xLs|yIsoGui3#a*IExl%HQZwG?!dbP*NwNf6H3{?Z1(SOt+F?*(nHT zJ$l}W0vn*OersphQq8pQOxTmiNXgjCRrA}iZ0H-jUU> z`Q0Q>sNC!fuD(wGN0&Ov;h(56xYO=p##PYSnmpujAQi@-3 zdDk;yA}|#Z4ZjY-3x`YY5&JfG{tC#HPrKyLZ2$>X=-fs=MSxC4d+g4!P+@-*N80wq zPlzq|l<)3qqO zYZ)%^Wa#AG;`1&I5XLg}$s>e*5cOFLXNb7;=#qU<>)vR2R^*fZ=j1@Nukw z)vqE7wh2fY>~hP`rishSppKKhN)2eZ5-%Nvh&{?zBa)X_{lSU4bFF8&^jk+iUnhRv zYoOqkTz(l6&Hr6S7kw=*#ZP4A6S+dYWWM>E4Gy^d)&11-RI_onM;UvoO3DwIG`fc|x z=IoH1Fj^9_UpS&Zit&nvvOGj65d_In+SWVT^fE(l4A1>uZ`Q*-W1FdT^G55?v^jsNOQghUpz4xMq{=uJ|B`)!|321RtqYf(b0V-rJevQ?c#HM-5ASzC znmjtgbL)0q7bjjYon`$ig?&znw7s!c;=`m>HcPrdN8d zr7%^=nkaON^tFI$f>ru67ip5)u85{;EnMyUi6MfKhkBM2T80t?qvX0mGRyLGQr57? z3lz%7&d6HLlo~~?Tglo?;}}fiw`?0AbovMXT1g_Hj#kNin9{Y(*j(Kex*BclWozkE z>o*#sx55lAy0l72wkji*5ElHzpHj8yUHE-Tcw_<@v#!?Q193ZtKe|WF=>?5=fDf5v z$un_NN^mV(_8XTg;^cV;B*7}GOgU7;GK@EYO!6u>`1tYb_9l;E-PWa+*|!APVz7p0 zC?oHHxdn7GA97I|0*~lZyKgWL1qC1oCXvBad>9U6Lk#z*zfeU!=EnbF!grJEHaLEe zKJj}(s?_*1pqn87hir?`doke(L5#zhK!A7ZRsQ{$C7@HLUo)?4Q8$kSpt@rIedsu-I zzX3#FkeP1)i5CMO{0~PL43K<5*ee0VpcXKI>E+WN81S;473dk3c|p7?pFRFo*is1) zdNHmm0dg;fWEDX3g_BkV;D0e@s{WD3tp;elAdc1lX*sCB`X4fJ%|D1s4M6vWGhXu# znXVR~{elG50(4%C<^PZH)&bOBkjT1!INNpqc!|^lwEw*e7AUtKAo9XquLlsrX7+1^ITy5cN7L6 zO#P+PfY=)WFS~Vt4*rUu&Ao_#NE!jOBEY~f{m&n!Fqjr((g+ZI zsXw#v+0|m@uPZ)isu4i{g5Li{Y4`pk$l3&;ei209_@b{x1_Q%r00YDFFF_@cQxib= z#TDEHAci}k1b}K90C*riDgZ7>sTqL!B2diN&h3c-17pwsEb=dbQV?Y`K;T8dp!r$A zQu0Lr7Zl$NpribIH9SJ7{94bq1L=9bpXXn`F0%h{kD382FA_v8&k}_40MLonb4Y+{ z3xN3r4*UyWsQm+rsy{bvxCMavBA=V_YE&B$2FCcgc>@2EZ`FEn5Cl0rb6<4CTAy{S zjb31GP<$%@=SAXQ8LR)2$T0zclq#Pyy*63_^e^0hC9nRA+iC#-O$I(cjOS!l!k6mw z+n%fQv3Y^<{suVUGpi~9U~%C7o5id9ucWen$Tb^b4M_y6AgbKr|O6A0Y? z&+YgdTJhh=ihl`yiTYndULq|>Uc~=9!1vrgnE&MeW7ho;}m306}^#5uL zWA@*xJ!>93m*<}H-=i@2bvXdW#hlH}-PP3H(%Q!I|BCAp;PyZL{i1O_m*-ya-=i=% zq8vog33$nK21#^2KaJIL0LY{Yzyyly1Yp1X2<7~R-N66AzzV<{&{Zb@0|BiP@GSKI E0DVhrRR910 delta 28086 zcmY(qQ+Oub_XL_Zw(U&pOl(e)iEZ09-#D4rwr$(CZQIF&=ljk7T%2=N)m2Zg-Z#B_ z^?G&<2S7!9K_bXYfq}zOU*OKm+O@ zIWbR!`$v48o524Ob`Le!e53)e-~*4aUOslf`^*#Z|}}9hKd=#6}x3`zT}x0-mGH9msKY3?M|S z@B2lizKvh4q1r&E+)(+*>p_iYUrVWu|_@)!E`;gRX;%z9$?JJ3)q#a(Z#H)InhlG{5ep*We=*Pr^}M>b4thw zBg?*vjs|Oh-5<+fG^bn~vVRh4ICl&zPDc({Lx){%?#VWHD>*5r*+!3EbU9+g3(sBk zLq!u4q!zXvF~oG>Bs5IUmx10t?uvrh+1P5CWKu!UP&}JbQkI~Mcxi#d`{oJK z$o&#qQn_7y*d*$v{bZ?=MwM_wl);wgfiijP_2xk(1#Mz6yN~^F?X1$2OX!+(3mWOm zzb9PFVHWhcV^}b|=?X&yw!l~nk^x5)%DvV>2Qk0FNqA5-xw3WwQPLKbxNi;MXbLW; zMQ%%Q^g2wFvei^gF6y9Y^2UKdT+9v{yy6K%R7U-7O)w9K6)4d%w&sx+>2T8OR6CQ$ z>ZhAa3BnP9Q%?@mt+PQ9yN1=1^9^J>4*WKAa9dI`(EUG_E7Hx$2;s%uyJ2BjBF*!Z ztJz4%l2mG&Rktss)qmVn7t4z{i&EtPEX!afatZVFMC>)fj#SYiXW)P%DdsScqz)87 zRY-Eqdd<}wUS$7LKokWXRCZ`WN4|uQ6G2RFqvB4{ggIZ#*6ge*(V4075@c=vI}f#z zC@X((U#;tXdAfW-t}s7wWo%#7VRcOY$TKCFDk;3}w>C^lK)$%v@5yB;6p0wo!kR zJpr7lXl*watCvFwz(n5AOYm>5ei>j#{MI!0%Ac)vISB99!{%M-5(N={?T?&0*I+!~ zAbU*-4&cYann`fr)80gD+;?HB0L&F3(k6Th_N@_`ZE#MlM=@{>*-B7^Ns$(Fk$;0$ zSSDh1j~LxFwMcqclb*t<1IDd4D-v#>8zq`HGigqtp5!o43i3gzdeOGE-+_}WK)z}O zLBOn)=S{z@9D9C?ViWA8o}|t|rm{vLz)I7+*N3+;+fxzA8ad@JaU=F^EKHAI=o*rX z#pa-{z$UVxixCiMZWVo>_5hz&nP(cKp8u(E3;XO+0gVuiest-y%0NQ@cdEfoGc_6< z&g)D-RP9jEhym?|QkM`b24?J9vwU*yRYpq5Ksfl-nA@oaYZ;RJp)|=a32Wb*rR7p z57Ez5>0)`M%(Kap9^#?sq@8#EXolT>6tVO>Je@C;x`Bp_M|h_xtQIJlx!76rsn=C1NEp zh?EpJAS!B-U2dLeHwN-UV(|+t2(7&_IXsU7?q=eNrGE`4uM0|MFEA1s6|h{=^39Bv3T|{) z_-B>=e&ZDcl_$#9OlAc@fH#P<(a*m`9lF{avb=gjO<3Wuj0TA38z$Bhg2wR zn0aDPQBKU`+sGwT7o*cn`$AXPZ?uhd#@82WeD*ypa}oP{Zx97%DST8#ZsN? zZ=AqlGqmtjR(FKMg@8KpN_s-@>D}2r!XHk8sgE?7JWS5Ryrs_DfgyivC-V&dpRXMKP|>1`h4h+ z6^K7~lt~mde3hOqRrANE)-NuS&s?Q6+bA9QMi^fB&L966(<{ae_bGiDli7021eYJ2 z)K{zzCStkp9UI5$10(ihuGJQ&fte>{2c3r#1Pa%^^G~3?{Ya*b3mu`QzW)j<2V3xu zJ1*%SUTr<1=rd#U5U5c5=P;4Aey?RLj$Sl!59hW!Ih70t~zXd43BkOM< z4CRvNYJq;YnnfjBv{f}%b{j@MQ zMaL|m2v=2B#gS1hPEwui`?%mL`|v+X4!AEE2eZ{}W0-|4wN5(86f4;V`_h?1myR|< z(du4Hjcm9&P5pyw>SL>zXk@=fn&U=bS(kn!KFCz|b4k~TEjJ3w4dd|Nieg z$5zG0qyil(qfG;_a%HZ`!O^4#2D?ca1pYyZtncGsAK@WCY(6=U^FsT{$WbQ|Am}8) zG@KS;!fb0?-+djM8^pq`ZLlw?J>+UyVx=?xV0<~m;)K&5CXG9b9r-Y*35aGBZAjBp zYGps{TdG}-QnP>KV?&QqVFY9k?WyERgDPng^jPgLxkojb{y3$-a7haUE^?+wy3;hR z4(YATMU~`-P|t7tgAg;s8> z6E;m|OktBlqWgk~c9ZA=ytQWkmfzH5df4^+DDxLM7$xFDVmwQ`m#&Io*x!@|p>#@J zv`P3mzqduPO&ZB*#TjWc-jCp(A#BG=hqGw~E3xVXmEaCP#N*o53!M zZsKC<$72nfqX#JpU^iWk*TYFYV)bBD&HW(72?>|+1cy41uYdM}qTAnY{P_2{&OZFy zW=qj7fqxec&b(9Hi5JC}`lxt|O z9_=q}f9|2a`kMo-JDu%|Cn4ZkPUZt%AZ3b}cKElL4W-#^-85m+6CF|g-3v?2`&YjomV^JIm}D|R0RIl^ z;v($|J5ZM81in8yFn}?t{&^(H%+U9)7!BorfT+KgvmPPR8XWM02d7Wo(Hu-9PhNh+(_ zC?}_9ImT0}*}S(V@i@ATCG;>$jTfPbS%Z&OG{de$Fh$&rD1{E){nXrj(*T*O_O$OC zu+W-oh?3NLzIsZdnr+5A1?#SQyu_)j`%qSQ|vRFUvB z^c3Z>LzvX9#7!fUcv@-AG7degBB2&M;I<1|3GEsx>pR{PXe?CdEGy#VDQrS@VTC)x zfklJ}B@x?Dt(=B+VTDY4NVUnn1spDPiAjAnq7`9M!^R44WiZDZA!T7BR(DA!Y zqGevrSctkY-U&YFW06^r<|ek>;0a%r#{i&|uE@xkxO_v0ap7 zc5kuOWQ;bw8kIYd$@~Yma>+jMdb)AP#%mW{g4Q#)<5X9u8X=9q;RHOnLAw2$>Ia_y zdS%KuVS5ZA`Z|4@g_-*IiNtF#Py%Uz^f^AxM6hnsLp&sph+J~7Gmx-A54UlyP^J;5 zZ>7jL34?1~C{fe(<1J`0cd}Eie%wQtsH6(ghJ~7h6^gKonO5zo@LsCi)T1=X6}vGZ zL3Z6`a8!&vircy=8ULsKsj^R`^JAez#~HO1Wp8qs&-!tsZT!l5Y&6~_a8yezJMpbB zYS$tmJI@R!@PG}Jb}N-`W-hZ{nxevj*KS_dvyYiG`iU#$S_oGjMKdiMW>)I4Ua023 z2CZwE&)In*l)rUpZ%`JJu>F$F^{@{Nn9CvUsq}mg@5MNi+kzq)LEk72sEO4x1pet zLTxBtCu>kg6?mGxIWr3U(w`?flS?C8#bB*$fV;|g$2qv4Rv-H84gMPoN6Xt7^F>27 zk^nsVmaEf?F&?@d3;doeoH>KDlCEzsAvonO$`~4(ex-)-4HWtY?qY5+7kNoRnAyHj zZZMXhoxC!}u0}tsP2HkRH=bD~bmx6*^7x;nJxipypXCeLa`ysC$!O}2-|~ZsLS^2P zIc=u?h*u>4%GghSZO?T4eM|w1lNtVLTf`Z8u(+a^stJSb8aGnKDMQ|dN8rZa|5LV3 z6;f^FBO>sL8%|LJSbSe~EGhV1nMes^bU%q@ee##_HN!6R(vC8}OC~;&Wn*)Nq^C2;R58EU zZ+LXn5jV><8~GgTGu1#8bSuz?{E*b!cw8EBMwU3vaZAt`pna89zYLn-*P%!@_fU{Y zx%{!G;&Guc0*6W*{v(SsjRKKF1!|CRPml43n`Cm(Io{_LQ1YXWd@jlNoi|laa;qHO z03VC~TXrn`Ch-^d;xW!s4g5&TD;_o|Ucl3kuNPkaY7Z4Q+{&xQSJae43+`APF-O?@ z2>YNgTb+Xiko6aNYr63*f+twg#MZfUGEz#&r;!o27s1LlF>aZj%^i*&YO)Oe+Qx&{ z(&jmQg@H7#rpHvPu?THkon}#dcE2debZ|)9QW`XAt7^Fharu-xK8Lk&&u)wE=bd?Z zl~&eN`0feWC3sKM0`A42iIGxc2m!VmPIz!D;R6Q+aH;T@-U3-%CBY-dm}{s&`>LfQ zVn22du(HdVpFs(28jRe_h#})+8HH~8`H&8k)?X_srHFtw;-SUP2YfJqGW}dz#gu@l zzCyW(Kxu|?(ta~nQHFg9Jqs!#&d5tb~qUaqzU&52glER?*b@d z3W4&oO!(_Oc8~P&ic=(0e@*yi!Nc1qbV3=4uU@-KlG0V7fMJ(rsWYqMY}kj#ZhGPb zXs}cXiAqyk;m-p@QD29$w2p>$v$l5WSvut5;)%i61%;6qSgY{{lJ^7_zc1||<|aU5 zu;!#ROcI2_$J1jl)Rr}4@BCM2?5Dk8)LbMjZyI9EtsfV^*=KYiMah5!7NMNcBDaSL ztJoD$XQp$|m@GT`-S#IiMbI>!Podrjh?>NrTktRhzab{hjkP|9yCAbP=1v99lGV+f zY-DNV)ryhH>zRAR*D*43=jr+tx+IK=tGWt!f#HL0!7(w$lc8G*XKmf0=DTL7DE{o6 zEE}N#VEQ`!GSi(NF3kpag-6xq8CdSBEjd|rpNtTWDA*^ATBIs=*6y9i_2NSY#!Sw) zeMgjC7m3gDmp~`+@i8nnj3K|eu&Xc97=!* z3s(QEAE%tI$>y}WKBNg6({bKi-4mDqlD_=U6KjLAyVjcwgX9lqBd;hJUKh=WW-^g|daI46<70_778GP< zGzc!0n_Po{KT5+bb^;iM5KcJ|a-Qzkb_{tLZ1sojK?b?4~ zeW-%eM0`*7Wfpdyw!GkozfN3bjfv*Hj>}W+6P=|zK~=x2UATDw&+>wc@2DdfY)Ua* zB&IJaox(}HgrwBIw5N?pV;*lVA510^p)7L5WeANHH7C&zIZ0byLo=z>8`tfKeB`-2*Dr}f9f(zK;ptcy%;lRQi8 zf0(DK%2zFFB~lki>1=Ht^HTTZt&jK&m+U!FAPL%Nw2D-4Lj3T;lzb>(mASfMN@-rB z7OlV15sG;y{kXn*+{Svla}r2yN7L3;9I|@=zVh5}ad`9W+BYFY?zJK~ z9?okq_^@9bJH2}1bAYyjysSzLu?KO&k_Y#GNhzplBiT2-w_;@jJQ&s+-D>n z!SBEh>*#Z8_T~{DAxWaSp7qP)#^FbVrPqi{uc5VeWllAoMb)RdT7+zHJ({D?A5l!q zhqcAymqBm>BdnMqM%=3trgC&~y5Zg!R}n|XQk7!5=!MY9^#$9!>9!FAY41au`~Lt! zXX?O0NWnAtPY^jV3rp~1EJ)o3FTu=xk>$TAxQkFZq8cQ^ey%%PZAbaoH|T||A>U<~|J&41rGaj{&j!%XSG z9&16QxKLv=LhzFU)EfJjc=o(>Xy7GPTlq!KT4oZRQOPnl6=HezhNq*}eV0H-lCUnm zd}qsm_AGK1naZRkP)yl*76 zpdka2*f14&sMY%Kt*Ga_G}TW!t+>_x|IMg3r_r1Ho^Dxtx?lu?eC*M@Aq7GP>}hdt znVjsQ(kroj4EWyueuBT^WP`gIP;W+=J-n*}Td_v^eAHoH4upMspa}=1c1a?88SOE6 z15yTzS`pdzeQIHd0;gJGnpsw24pdh|yomi7MJiNp5Uh6|^b<5o89)NtI>mKL84NSS z`m@drRln$t-J{xn>A(^mm&Cx9i|R8`-YXBt9q1DaEZr}VTQ`$5rIslh=9L?bwWbCF z`R{3E*xO0m6EypMP-a$eF^(xANbhKx5_9k;RrHGM)uoa2>SScHlPw<0PEs7C2lg9C zhRlNgE;_5QN~Gjiw|^YgnwN?dlTh7~j#>qRw8Got$tOO$kqP2~DY&kHf`LM28udzN zCrbKtW*)5Tvtr}WGK=9LXV~@9e7XGv7C}~Wfs7Dz43Dm?NpH_u9-7r5g;>xGhvx_Rc%i}=(jXG8qRkR%hxQpOMDvn;Q~o{zzw`p} zBtRxhK5~LnYh#2v%lhFbL#^M8{I$g@@460cH&&PSXL9s+p_|zcBEq=QaP&BC!U%V; z9FSJ~0c`$?-&EIr9pLyJMc~O5z|c<=v`+%Bk(~>~H_a#;h1AP9)#67D?iIb&3Pa74 zibYE;w0ZH_k_Tx1Gj32@*R=M{{Y+b9a>s`f$*bV_>fLd{iY#^Ii!G&WecLskrT<@YY%!GJIk+mXiTlt|N6X43O2cH z*0PeKKyY3!EcA1pm$nyvY%28dM<{U{P~BYyHVf=sC&{R+TS+WrU~ZukC{^IRf(B=Tr+qsV~6SgT?$I>wmE5wur%dGhmR}9^bbJXz4X}NqS@8oP#SlRSfjX z$j@7*ZpaRpl~m<|Sw1|oMCiG9j_R#Z9q4{esaR?nWA>M~sZt^V-Y{jBqu3i$cB4onoY3Zf*$Jg0PAzcVDJGWR6wGn_j z91moCq0VUoV$68@7pQc{tihFdIb@PnQ5N5@r0sQI%hSsK-Zjn{(+^tkp+IWfG_#F& zJ#i4{;*l581~N|H{K|!>PS_8I=D9T_G^%D?84mUIsIMzXVH{bpf`Wv3)|Vlki6Bu6 zMR~tRRi_lu-F3< zme~wbDG#(n1Y6%J#?)#=%)+LfjJoBFjaIv5PN#WltIUT<$$IWgK+?}6SZa6%>hq0 zf^pB~m8QDy#h(5P&yEc0E4KdD^gO0z7Ww0+Os`fMs9nLsEn;~ej|FvgftYp;0tevl zEmg-W9+&%6-w>13r{E{@edY2h^EjV=i z0AEPe7Kh@5BCyq{57XWf)YpA}uux(sV5OpXz-F4htCBd>SQ2E1;Ip3<=DmPh&Af;` zsv0ji*ZQBuaJ0Vk&s~EZgL0VF;lPV-xfc>@91rAtRp`GgPfl>8Q+Ax*R};wZomfCa z%84t^Aqsmh+Ug4ZtnP{aX$7rYUB+fkp2fx0=Ljs~iHMkHKWavvyA%+Ws#XUl;LpG% z-Bi6s2qHQC{NK80txDH&6!tBfIkLMCqN%-DZQ)pYKe^|UF(ZlRb1nU?ICu14882eNJTQ0s%IPLpLH8q~LMf*`-LGt8SjFE{WczFQtY`57 zXWhoY0Zga zBBJ3AvHsqt1u+5{ACpRUfR}|rAkwQ+foYa-(saww7m=Vd+?*;cXneC@>^oAvI!>k4 zYco=m=PLwN<^Y(1pOnM1z@UMdZ+y+q*9#s0%Ryk z+jie{TA991v?F2N6A<2B-wJUbCD^ELF$&pkJ#sAlKf<54C9&_=10^VxVv}Q~c3$kY zYlB=*-w8d%u3LNmmOl`C)4Q!KWs>1LXEFXqs;!O?ee|<|R(K^;4|@(iJK+t7(MQ$v zZ#v>Ok7lcVjn^Uk?nI9xQ2NCDqd5P)jj;UiX8WW}p*Ih=3aK-`x2T)o5e_WB?BObV zNA@H)VORFqquo$z|J=kJxL%t;UH0qX*YN=u4-#(KuR~t$s9y>Ar%IpbUcT{9x@Yo{ z^ac&^LuF2Y?{wY}6L&6^{T%jy?t!~?FL%=J7><8`9{tl<(dm`kn87s8F3G_7_H%?DJ$XDp_o-fS+7%Lpo+|VoiL_Jb) zsb3LHV`7+UTwpZ`rH&lrmL#EPkfR0OlcB~-9%UPFo3Q)l=v`_tW}AfQGX!#$(wX-& z333jLHT6rv_bnu3mISvvR#ur;k0u3H1%RM7qEyEnCst~pTrPR0>;jop49Y4gvlmvC zIjx-JoZKD@O7q)ji5a&9*P^pMa(wZ>CcUcY>|C5xicj?D+@oBcao*#ctz1!W9{-7L zN(Bm7whmyO*(-*K)^+wTVAMI}j9_q$ERn)jI#nF8hUI1`j6IOlynH2G;>xP z)w#)(u*y<#4s-%+op#3h9>UMlPZvEJok#-P7d-H)oT^KnroGNerlHQvrp3=rrs<$3k$gQv12=%9 zJI%97)i#Y0S6>nD~rH8n2AIgfzAp9cP(K@Z?1w0*o%TI6{S%p<#$ zv?H;UW6D%*f)-7O(!JDaAhv!B8~Tu(@prAv_I#WOo5Ttoo{8U%o!8gO*XKZaTM#b9 zeh8?%XVzEDw^cw_&=(e7t7hm|z2P<_mXz46ECt^^2Q-3X9vMhr$-@E(_T&ottHj0+~_c^7+WT>PE=j&M%yZpL6=)penB5x<3uhH zB(#i*e*ND`%B^LjE55P&{H|NiI7Gnmz=NnI6#Wl(T+j=BjW|~Y4Dzv}#rQ?buz{0X z#VAC}k(A3^Wa0XFfvR{FMY;$qHczCviz04UogrP=jhuBtbAL&;Yj>a(tpk`e4Yw{! zEmTF7Y%-T-nE@0V^{NO;m#p-Zr$q3Cs)hwPIGy1NwY7y6{dFU@)J$F6RWPV0O2|Ad zQ>1R-!YKl0=yrg`Bck%G7gNl3sOTerE)R)BwkLSvl(aRPKjdbCXczJg+}2EKM=+pfRjzSWNuq21^0^1~0% zb#Q^RsKZt9p>q#ndLdH~=sPtnBeZ~x0RiSmgUZ9}2~#^rH^6=p*UOf6cOD&Gg~p`r z1}y&L4Y!wm+&1#l_Qv2Rbw`7&ZpMXs)+!w+thY=r^Qvv^T)Y?IHe8$25%AC7%zPb3 z<{tC@(^3AF@t_CXh|!~(s{7+DHbpKSr_~VMl~>MkjwqIPQX87lK_3?+6~7#gJo>Zb zZBERT0fd$o2dm2zs`J&%OOeTf?>Gxc!UEjz zf!Hq73eX8j0UF~lPOGiQWpwIg^?SG`{cvaz`S#6TM~gO&P>Ie0g23G$~)#kn#bU0W}2p=LN67s-U5{()Oy4L>HxEP zRwvhY#c}?N451wkbNY3>TqB%Go@BV$*tDQZ5C?hU@2a9Ad3QgqsraG~`o~ku^?Q)c zP00;fPGG3}kKJCsh53@zOVPFmKx~ zoLm9BA}qAWH$qP{xN6V{d1u9J09 z4C*7#``4Ikw4;fW70+i;=jzvMncvh7PV**4CNNG7ed0?9vlF^zHs$S0%<@|whvp-dO z0;B!&8Lbs&D!Meawq-3QHmGepHs&#_P?UPNASpNSRz35}mU5BcJ>}$H3{p+b27Pbu z7h}u=x36SPiE5QT>ZM(|v27S+vjh7uwU7vB9x@lk;;gA8$hjl;_0}pD5oLS7j-1F& z1#pk+YEOQsx*mCYct^-TXWJfFc=+j8`o$`0!)9nGl&0gqtF%E0jW^L5XS( zehyg~KK&UG3^GPw@V7Me9ZnQ0NvC@Bu?H%MU0YL(HdxlOeSMs#Lug*qat}YS3oY}0 z(T6CMBNqQuOsOb>hj^-$Wb4KF@TM=gM^ZuK%~kCcYYHFg;byZ)vTqmj<%kTJ04~Ad zYjYdmE|y{a&43#>i1U=_=X9NKIX%+t`#YkP@Z5^H7+d0&;F+dXDEzY`Qsk%Aghk>j z2-5keMI#26OurpTL=X5XgB;%cFpD9Cp=c_r@dj;Ye*yOd)FPC)wXN%%RlDzyorw8(eqb8Ygm+WYE2L_7UiE6oRjGL5QQ7TR=p zNHvMhDe>ioM6jb17r%m`2}~c&w)x|!)79trWypL`+s%n|^$T>j;-J8l|0#-^OD z>$Kwr-HCfRGiDeG1ly@=v7q%x23K>0+L;y4!p{0>UBZo%>w~70ldOc-C!e8sBG~F0 zUZDL{jL&*V&2)?Klx!V74tzCM>Pan|I6Oqc!JmJeaea0(y)?k{0yh4Vv}+YD5B1Js z%kzz|l<@yBbDd8~@bbuD;gLd7btJI(YphU#JN&?)rczl$`uL>m!zZIBes*E*!zZN& z_QuU#b;a3@C|3$Y5OWG|Es#G@&TLVVKK`5+($wfP=~A-R_mWB$m4+E*!B_zeMaA^(FGP$_OeR-37aiXRQQVka)E#GLH+zsa4PC|!lrGBO{~wMpJ0<} z0ZFKS*i-LEcLn7GUokxLo(1>l)6U8Y($f>i+nbipXI8gwC3g*QaYgR&iSg}?!{<|4 zuV;3J@#%@y=QE}IOI)vKZsikkktPVykrSWc_EX@0ffn@t0xi)03$!$p4L<%~MkIGc z3Fcpp?`Oq=r7&}(^IC$>hv1YYRvkYm)$(_I{qTk;r4dt%>(bvLw8#! z@caFO2!!KS3KE8lywLbDFULT!A!A(EYv*yZ*|BwFQ%y6f*+8?po?@9CxZ!veGCkX) zuUXtO8cUaaZUIkBPeMuxmuB!Gv9XBQIMVK#i>#~E!hLp^y_@X|ig+w8s{8)=Yf zfXzf-HMhN_6T-6O^CYjbp1metUVNeAt}QE;T_6?O-eA<>iCIAP8$02SaQY{FmUJHH zf{tx-XNmAWW{j`iFhnF8Fu_zSTT=9AB&JV!h$YVW`E+-+M-u8-dzcg|g|T^R(vp@H1gG4>Y zeL-yZF{>=RgKGj0|H|I~Rf~;IU=bd}S9I3+1@P9fpxe_1u@~wDC^C}pl_ZId)+ilv zs8i4pw&9<91B3gp@@I|8VHM~zbN9)?XeniB8s8{3DNgMiDE*?tus;f<2CIk<7)-pe zv|fI@ZB3Aw9tC0dAi*!yUax`pQHf`}rTKEiXTZwzguV;eCggL?pnE*Sr${`aOf&Ni zFxgCqbLRBk#Omz_o{?%x?5*tUpLINR=x-k8G5f*&%F)`qn5 zbFlDKa2N@9G$C!_0zbWithxw!e-O~fv|!%l;-6C`Ky9EP)gKBGs)0R+2K63{fO}=* zo~CGL1EcBJa%IzhIUwiZq6G_Iy65q$pjHaH@RRBAFK|ORali&pQ>MD>P1Lci{dx@g zN^&4QP(t4N1?8J~9hTG22-GzP+)KQ>>=h}M>jh2lsa6MoPQKh1sr z|8__X!3%J1V>l3yb}SGOIuMYSWD7tB9OD1taFb5}9witM5HHje0T%#0P|eF5Uj^gK zwmxIcx`b8ZO}{MBf;yJJ1)Zw)Y#_c{F}}Fb!b+=7mV+Zh!qkkNrNQDHEJBsO)GuF9 zp$=A)C>O#~Q_&{E5W`#Gu8N9=|LzWJH0EtRhs8Wy5#f=)*o^XS+>9}az%Gb|XE~mF8?Tm0 z@FO9K&(_ya;NisWG$==i+4jFvhB$@Fv@j-eXr(rxwfh zO}#?{M9V>38hf5xPMko8{tr!rm9yUkbw6BbwMHMR1U*f6f%A!f5Q?BNK__I{Qck0c zYM~?8=;rP;=`emLHb9%}6!(ZdE9tomMAA#9T=J3U7m(9%=>M%J}6-9}mRAocj01QYAtl~@lnUm zGMqbw*vcNfap)4VO#2X*Q@P6aq6V*O2cf;K2V4noYPE*Wd@CMRs&cYZ=3!u(r(_8< zoMEKL)A;JgT+G)fXixVgAsB9FbOXraVYOPK30HaBfg-NusyJ_)Es6w1AzaET3_MM6 zPn_J^hi9(C^re%dzAPzf2Ia9qdFb=|e#m62opZ28S(E6zJLd_cfRzYAae(#mQ=4$F zsnredkocv|p8_HtwoZwW3>D>x1kZE;sOK)G(YzrSbD!%vPKg}Hg?ol#E(^WPpr3|4 zv(ES$P|LYfhpXbM7Buv);$(+Qr_#@rI1i;bZS=6cEzmQA_b5cQw~zx!v6MARgavn( zK}GT`CxmUF^{dpPf6I9*!i~Y$v--Jehj}9Z%5pag_C z?9wxJ%Z_MeUvI$?opGe4`B41VSiy5?L?*CfpsN<{0JKKDAO<&DscPJ2#5=3E`iS_g zg5d*QN_aqBgTLu`nC*UI~_DSGFv-R{_=+yj9nspekj5ekt4L zzviElfzk9%VXU4iD_t=A*NJ4A6mV092rcWZ5%>Q!A9yRGU23Yg^q5%3j)t9NJYYV? zuFomL9aWH*yQ63cG{7#QsdLY3rnN2u`c4p9+p+RVT}ci8o;CSfK9*?{RLFsnL34(9 zmwjfz_CSsi@U5gZ?HHltEi4s$T@`RR22YtbPOgy$q>hu0#$dO5{9F0smG_Swe12Hood>x0;yvgN;JT@)*u@!U=xPzOJAGYEBD-Xv**tgVDK<;)V_|IuN8b4<|J)+tBWB|(9!aNJsXF8EO0R=Buq6wF%R7h+ zxdAN|cl(qwcq?vb6lL`qES>Tbm_A) z34Bw|28Zl!H)E0%>J==z)(fr1V{~x?FIA^ z^k`Df7H_wqrRG$6fOdHqkXc0+a1clhBlhn^yxl&4xWez#CrT~D19z(|Yy^&}->T8D zE2wVd6RH2W5y%hnfw|vo|M>h2*G+ic^)GYC`=%h)8@45>760W>Q95ArY12@c_JAmdVu!UTueX@`eOGr+?w2OCi+LJHc$&W7y@D-6rbp|LN*0 zfZ}SFwprZW2_D>nyM+XIcX!v|Y>?m4*fSkC9ART83KT4@udAP#1tT5) z6ttSDpYMAgV1Wh(KeXG~uy|+ICu(0lS#UF&a*JdNBrn|UJUqWV{5g4w_B=m*mH_C6 zb}J=hsfr~>JFCJo5+2JO0Yhn)Rfk;fA3btRz%4$*4nxfFs=B7U>W*QZkNZ8SF7uI# z`RwQ?hyud|mW2zLqMx!{TRH^7Y0WKvyN&eFLDm!uAtpRnEh0h}N7zm)*OWObb=&&a zTnsbSGr`HWOb`v^=3;Tgyf@>k)RhpEH5?p^OnfJeI<%?yCzT`ws2X6f|U=^CfJ8o8g+<64b^ zQHoBxXQ`3e@74;vgQTh~$UyCA&&nOGZGEy#9uMfgR`&mPr!x7one@bR+#dTgG4t;# zL_AELy0)F>r=zxdPDA=RAAfD_LHxc4cK*`N@gA}8{AK@J>k%-KNWmcdiQZT+A1OcLt|ym14AiZ1N+mh;6M^sY$wG|FT%D)t6_)OaSn zll1;}eDx(=uHh_!Zq+Lz^P;KAafIdMdgp`^W-o3_CF8RFbDUplr47s)!X2>ZvNdp; zOf{XIA=8~L#N#-_DEO<==*V)T{VMf8KbUqD`~I9^h`<1{Wq=ef_1!n=prcVwr9X+7{xrLd+1LwB6abCTv%>97lhP``Ww$HS~@SH4O|1Z~Nd z5i5zZz*!iGw}nqM5yht;l?siUJ3=mHS8Y;)gM1F6SMvw1Te}3Yk?7~VI?;)}i-_!H z<`KqSOwyZIBWV<}Jh+L9Mo@pUHll_s(s7Ez9y!_NofW@baS=C^R9esJ_=`2utu^d6 ziXn{WpUxgStCI)t!|Y#tXS>(kBZ?-%58STgklg@k+V{A4mvhWF%>SIFpIRxG1%`C) zLr!@kuF-CHRNw3IeKA3^nT*YAzR$MWw|U6dvyzfsiMp}$sEEEPs&>D3GDV2pa%VO5 zjjBJ8gy|FH`%}@WSZ0Fx4Gpm;CIk|}<{CUXKr;=-hqjMgr<^ZY%i$9W_8tuTC_|kp zva%C4N;!g`bO|r?%ZO@;Ec~HT;n#}@ zJdhkbrIDESDaLrp_qH}#Nuba?tMjtDEWn7MKPWiF^{^kn)%H@*S-9PmP3tIcL>6eO z>B`MnRNXX4948-0I7TvYMoU7;(Vd_E{pbm(!e)z^V!WpvKx9JOYoR*kr!ERs{uDW8 zcWm9-s%5xsitC_6Gck=a8Ws)TPOGT#!IgjknP8o{KnkXqyUBOSEUB1w!N@XxJ=~hi zmi`)ds%F~7Ug;F*v<|(26~%-E%VeuQ$VL?6w)-%zD=T(-$uh} zsib#N{aiU9cNHsU0^YJs{^7T+63yCQ;8r?sSgRJLshFumC4iJVfwH~dL?oREQk(8PmM;FLhskO~n zxr#JYyr0}PTiA5+Ya^$)#ZqXy#iV4!*uP_e+}YwYY_Fw532Y(iBD4AtzFFVF70|(Y zZCAc#5f>;fgt_Fd4)cuBD|}WO3@nm;;BHaNpiE*PQ5~bwsW&R;jz?y)cw7cb&^XI~ zIM{_XHk1Kcb-9JG?NMA=@%2`sVTa=#RD9Fnm^flaor`RKo$kJQc%b%Rv6063R}b$3 z(t^YwA#DuNgjG0Cnnx`m8!=Oio4=yHKr^rmfEH{|&8cK0*b2UO}=d9>J4Z z(Wz{I^}c}*FR@j>Q%wCV!h=(;sGvuCs5D2FQawAYWb~FTFX`+wk#WM{mqw8s`zfan zF+9+hk^@L>eJ01J65!zE29P#bHGd4x%poscTNG&t&Qn74gIgH|-m5zEql7|Gu==~0 z)R}1B@$74R0<{*ySxd`VO6a}eA4^v#af=NOph^0J@6U_Rm27h}`vg6VAT+EjchqnPY8A2te}D48`OO)f+JDyUs}}S$dmrAWS)kvsM`m7}$X$}y>=-{e zuhYx(r(U7WZwLPv9G}>zBQ-K63p(iD8%;Rfx1@4DhQ@ig=L-sRzqoEX5b0v{gU2#Fu|{lQ8L}Ne zRWq#%jt2LIw>iU$*KGrFTVt>R^qiC7(U$IVNa}666CNxt_;N!(`t%bLnoBrMHu4^P z#%qXt@U6hG3aV2(Q#X?_bIAOZV~J+yVh>ECSZQB6`L}v@Fv1Agw{{8jldij4AwP(y zb3(sR(lc-%ko2M=)j^}u^a)y+igPeps`zY9<(A-SsyFYJ*H5%~6a&SBup_r1+!aqu zI1+|%pQCi5@*2jkS0f1eappT`)Kung$GT?$KBDe2}oN&^SrRy>Mu_yj*!Bn?^Ki zn|KV+voy*G?tvfG?D|Dr1|q3PRSjwvN8c;^GPw!zeMEF=4J%ER6!$LuVPo;JFo+y( zMD=uL_Dc1mQN2HJVw2?UT_q37CAS}DB|3AX^_SMB zR;q}$s;!ObMK4%z&S8HpTv%*8i|+GdNdD8%aQ2%xO3a-j|8{G()V=gajejPBUvqvc z6~@BiE_@=ZUdhP^D`&g`^F{uCBE62b5^9G7pk=VKmOO`Db9tha69_%!{r)UN(1tmm z*HivcdJ?5`*p8UxFIWUn6ykw3|2fi^No3q^<8jy2BvvF!C#=B3ER%w4?l10k!%+v8 zsix~omguQgTajC)@sI8Pe#gypK@B;2rj6eL8Z8Y=2o&ZajC-n@Tyi7PbQ0dkdh_Kb zz!3lR-HZh4R5pT(4}$MLr0cRVvUqP!BY$rNQ(<1xs?H^i)GtJS{m~fEKi0{#J5$x) zsoyGQG`lG$Fba1>F0)?JW`AE42h(A(n%~mKVggK9~1o9G3L4~rR zkrkQz7D40^En~#5uUnw&msdW^GHDtyjp#d_JH|kPbsP{8_Yg}vsA7At>&FyphOIWV zen{`JODa%lK}I9ud0ptf(keH-Jc2!rH51)mSuyV~BlF92nrUPW6;>=fjbjQG2FCpq z6J4TvQbY$b3W}Y!P0|GL&ellEoq--h~opIIP+ z62FRs!`87SklUHRi`e`u(xM0b{KNmjG4ga5+%jp!FlElC>R@lT>>7+N6urUsywpi^ zDn$swjUpK!k!_Uc+Ew!3*2?%+CE1<&_SWWbKQ@4 z2#gTAcXbw=5m20E@fuEqu}&?gJ3jQLmnS=WZgZL`(B}+VobeLVpa=wo407rvnAWp= zcg|jHYe#2krXo+5)q{@n?xD-%K80a{+$|)j`id+>&-IW^Hk2zn+*16xAGpD&+Iwb4 z;$vUM9%zoy)2m|w+vlVmFvZDUP6;;XY4YwGDZt_zqtn&%GF&1&9%|Nu(>`L1|C#$y z;8*T3M?9Pdt;+NW2t9wx#AB!vL?!+a`P`@e+t0P2++hR4TL#fk0$I>?STpj;&iReB z{7apG$1j&iU*>^)K|Hy^BVcuM>4uH2_ulZxwh=?pRXM@;U4c)Qu^BHMa{M?3OkoBxTIjIq?P?BKu+%448rX&mlig7Y6U zGuOwju*_cBJ!LFwMP$#(9%+FRtl$p(TMWOEukkW-W46V*Kk2aM_<+xHMr)g?y59C7 z2~EOQd$;b{r<-@jn$+K!OAV{*-1Nuy1$E&*W{<+=?df$+b#Fv;HJ5f^cr0H0GO&}o8GjW}d*o-KvTG`d~{_Wa`?DJTi1@>T06`l=I=<&$5r z8ZMKAqrsq$sxT{20u9)n{HHS#i-%G?SJd*h zX^SjEa!HB$7q9-F?0W*y+7D~H*3Zz??+-1#HH?Bk7TCJGcO=HOUXnnG`>o!8>f3rS zqxLtua7=O6=+`0TSzU-4Uf%BAXRhNYYY>73YGc5!Fgc_|zS6 zjNakcB}k$yK&cD4Im7ry(4k3Kdl*=$4YQ0$H782HXR^==u|qSRGAj?pGf8Nqt$AGM zKAvO(kC;~TuW7p$Ok_x(Q&-fEe@;ILdY z8$@ZGVnsi~A(aGY#yx8xJh?FTu*mGX+4`8pKeNO1!z zw>ePa9u$0CWw3C{Xr3u1oP&6S!}HI zzIvynrG-`gz-7WOE|#9%_}5axuow8|pZ2?F@$bcb3!Gw^jutC(*O2iQ(JULd73tV`FiG-EEdqV?kSEN4qB)g56^GKa!r&mo6R)$9F-aPu7_&rgR2 zM!=RY=Xk;<9SvYop^rDj-IWzZ#?SUVcifD3f2xPoA9ZmH~e1NUdy5 z9Jv0Ri)~-bu?hUhLiHpRqyM4bq%jie;UULyQv|C(K<3cxMj^d?)LKq~(+j~P z%oA%s1t(m%ip3e3BO#^hP;(d-g z5=oA3j>c6E&~Bs8ryyxujt45!41tIW+4UT1$_iqKeBtPexb1^|yNNnPs$bk7poI z?_K+D3s(m6w#8e{Mln<&xy?t-%!|3sM>H6d#!skncPl?Qiu8V0eBvpD{ZMF|s|p*U zic8?e-R6khy&uR^Dt>A&?bYIiFEJhO(;^&kQ@C@h_yT*Z%yRDkY}cyrgeigWffV@L zd|eD|d@bV?Q~&P9y2L4SHW;pG?Fp>@ZtlxE7MTB3ifIg6b|YweRmu8B%MPEWj?yDE zMId`QipBEASd~B87Yya0`|wWQ%3zyPA!~yRKf#2Yg})S08zLex-v|Euv2JL*0wPbd zoc=cNqE)*bDJxF778C3jKsLU1B>{w4+o4nYQ%cIDomu=oM4{3QGT}B6DsKU7Lf_Mz zRYdTP3z4#8sC!yT*Hi!bb&JSTwRrBg0=!yHTP82N#waTEc87|@R5n4yhIZa`iRLAd zC0^*)#DMxCvdpjLamad9w-584jB6)I(DFbhgx|#*hg|X_-Z(gd&176K%#6U(&P9cs zkrWXbpPQRgKsEPa!l~n%GuWhgt~r!eLb&2a2Sji^4gr@`Tp4bIA4t zyvjPV)n;zY(^T6PqlZ6*iZ8%{TBMgL+83Ap*vHWy-bqRQJ9PbXcUO>kzTYQ-@uxRT z<@cy6Yb}~FCm4vpRjb-0aJix7CP%aUvvURWjjIjQ?yUB2JKr$-i=K3wh;mB|n)V)s zfD{=yPK7D+Yh^#E>^(GzHbe$xSOK4BB`JSYY^njsrI(cj}5<(LVRDyNl{HBqzr4g&#YY--rr|PY*EF4gB3OgyJpij9K=ru2gt| zI@zu2iu%lC&irRZy&sFH_7SgLq*!*^HM}}1&ixF^_ScpNR0Fk()PLT)|9euFA<2lK ziv|G!-~t)_0EhzTL?CnE1HT4IL>j~Ji=snHa>Pn{z!&YBZBrAlB_puALu%@}`Pv*c zmzQ*b?Pl~ga&U*h=!OR-b8b3yCCAo!CCm1{szo}kOm<~B3oGsx1A(&dU+f0jb}~-* zSMJ8#{}^~YM?fh+{-BY9N-+c{$udr2ST#@*bAC6qC`bf`=G!nUnYdY(GV^bSz`?*G z%Hf|P7E5YPr7XO2nM_VOw%plHDfh@{N|Kyol-4{u+SBA~kXPgpP738kg2qupNiDN4 zp|+<2Tc@O}GES)To0OqJc7##um@&o z?oV9R`W_bW+HR?KA)2R-oy$Xs?sxqs|F@V!%%trD%O^W3ctopR;$ZWH5FJRig zFtl+bO6O0Om+zuqP9O}IYA!_wr=SG1V{5ZDS^=YttNGE!5xr z9Ff)O=D@4G(*wSnz&5;3$dcS_@69f`y& z{oc$f(|&6MB7F#~y!>b#Y&-c6jt}jVa$Li4Me;UeTXb^3sUCw>)Gf{EMCVEAa}4Af z@=jU5*O>;UEJ3T$^q<)uPJ}vmH0-XMqIZ`S1UU?)9t_-OJz7mc!?Z0ZH$NIRfD3a9 zaC$}sYLh4;-7`ZoFMU0}^s5oO`&VI-0$6I_?;39F{ZD>0lA^)qXTE3CU`->KT^!7n zV^s>5j-f?Q?U+Yo0;;OZ$uVY&7BslC z7+62cbt!>fFOEpDnj;>L*zgz25#=kX4^EAnPTo4Bafd!-XydDy$d5H)Knt941Osu| z<#N61_4935mW&N|3$~On_WtM4CQi(T$vp^HT|I~!i;>YGYGKwhhy6;bVs~p2Re!Iu z>M)Jd6Z)kEG)=~P`T@APmHQ>0nu!vR(M|=q)^ZP+;P}&4**k_KyXb7+?w;{e>XOd^ zP&D~de!!6++vE7p%`cs``zG&;=vj07ja&R0`> zU#+vlVIAt7auKi2{4S)YF@u51`s@Rm+#{M_Jc>NG;N(zL&V{4bNtU+2Z}{m=#%kZh z^s%0Fj=J;jhJ7EBl)P2)%cwOPLA0iccAxF)twPj>-S9Ji+?MUn01=lCtykUeoafM) zWf~T~&s53xZoofh5tb^b5jlS6JHYVCMt!8g%G@Z-n#S>7hEJj8A z3)5sQskuDW)@iT2A3&`Yw_Z!0Pwu8bvb_9+BIgaaI4uYIxUZ3{rloW^Ll?n|?}gnn zR?3FUYQIIYo3&P##X#9Yu@3fRTz{=kFe0mk z>?R+Lsq3_<5gJj1*7Z^FR$LcGCm#PnmziG>GOw$Xx)aYLC#YJtDN~hQYZ8r_BFO>D zJK)dMfr@W>20^%48{&NGntHrKUi95<-wafU z3}7$rS)t@u76K)iSg*}dJbfZugdRM$2Z)&O;v?h8n!_+h_y)s82cv8vRk_5{vbI^I zs18BmpcK_ms+yU$!ybLHy57M=^@5>O+u)iqayVj=UOB8TB4wqqJR&ToYhbm1l&9Dq z?&;_F&75sQ77_~=?t9eGkcirvF5pBJeaQXsb@|3K|51?2`1sT^ zOX1PYP^)WGZT7$ziTL%Fr?+SsxlQo%gr#W>VYR(vxz2KiwEZYa_e$DGF2!~AkB{^r zz01kg7;>#V$*$Nh%c6v474jM}cndYDlrml-`w_TCHc zD!(o!{sOMz`>i+@a4C%>O3l~?8;2>rkC%3$exLUZ^NPJk2gPcGN#5fsna?prGn;?G zXeS}LZJw!S+Q4X6;|BFu(K%>=l5uBm{fn2i7~8`4y<%ef#P7KDqyu6?=cFdEHHA40 zTs5C2*3Eq>ei7B|^V?|`2KK#6EDZkOB=_j7%;yM9!jJbPxU5XSTE$K#D-boMV3niB z$P|DVPQRT7yc2~s183c_^HA?QM87LqAE>iUSzEx?IPdM%>;w|m! z4M#Ixx)*UImG|9$$elBTT>)t1Yh$naNH?O_R7#pV=dul}m=D@EAY?Mllp|Z5w_rO* z2BiQ2tRCdBAvUzZ4AJh~h^$EkX&&fUvnSm>IJ}K)aNQYIKLjd7GHu@VV57<+dCx?~ z)uLG(b{|%<>`vX}h<7(bk33C$U-q1|7bvh+~XJ`S;~D=IS4Ui<}`eDU^{n>%mREG`2hqx!LnBy-Snf zli_i2N~|r}wP@TH+|BK(UeQm@aKj-$%^KG)vG0kWR0RtWK`=6jUiK>pe#D&yBzOgU znqFy=C%cQ-(yU9X>H_E8!Ef3HOJOCF=( zj+P(y9#<}$_`h@}R?}Esufy>>f%V_bM--3-aG$aW(!xI;0Jf}{Kb!fVls~Kji6VA* zm9#!oh&XvT72Hlwf(nP%pKj59(q!Y5xSMfM!_n4d*T8WCawh&&y|YSXQiPl&ETO=B zl4yw5wI=eRGxQxFKPNXoxq$g@&|Ervv}f_o4~grnPhW;3&N2I}P_!fJF&ci#*w5Pc zq&r8no^+wr+QZb9f!z?BFWgtT-1S8{6?Vt4_KB|WE*rM6VbtWOR%X%6fEQ&FD(EDM zrfrd&TFVMltTgC;`xIGjvzUdsCTN`HCjh7aG?{|;c*Wu7CW z;3lVU$da?S2wnC^Z9;Ntf|FYK%-a#cRGr#T*fvkkvQD4j+|n9QG3-50PP(dn7t4H( zQ68`0nDdCrZS}cPEA^{R9gyHQ_zSZUQ+pB9>L8J0!)(AqQMz{>L#51OOJISnlKjn0n2{`?A?#R~twqY0(VK)4O0=Tjb-yg}?6)N2a zr5wSQahNp%x=1qN&C^yEpz*;EG#E3kA-w{ERtonfT z&|`LKoVZ`|WDkl(oX(dDnfn{u%oZmU&;{+bh2KCxc{O2qy_VhGS=7 zqwx)mGLCINY$mX^&ywWfL${l#YM#;J12VrWgJhQ5t=nwL1io2ObgAd}`WkGvv$(G$ z_3)hR%$bMDK>m7x`rkzSZ{*V)_D<(J2++GifWY5CERaqi0Q@HK6akjs1pH!v=bMmF z3{d$iH0&1x;@={uKwrxM$$!JJK<~-{9B+b3IY9VLNG$))^+TYsa)96)f?5F(eG`-` z{^2B406xAU)|CJv&}9YS?P4Mjc_l#n|KQJWLUrXo8kdy-zBh!m3Ly0+_*MZ_-k-YP^&4-#A6p|7khsrTUfpx4r5$ugG7av<9H{CcxMJLpG`fXuKgUwE)dG z0k`fS#IX*b^oI2OA3{?9kCuBqKm+A(#KwOwFaj;szuNR~9fS=4BFO5Vc+myi_^}=m zkYghN`7OiiZ$?r7-waS$1AyeM`D1^KrsA^$q!O$`p53kO#mV&6DUBu{}K)e2nE0gbu<8w$^X`5 z!Pdg&^17yT`&teCzx1If{_=4_WE21#&_dHcy%%YIEvlXMKShCA|H*nQN-`|CxbwBU znaF?l?EjZ?{k=c_hdwY}Q%aKbet-GgZ>9eG{KWrgx&FY=|F(kajrxD9dR!#`{|KT@`Y#m$#L)pD zcpK`99j^u&%>&tW00`fJ@V@|7KB%ArKuq)3PL|iqqqVPf4g(+{Q2$r=YnM**0T8Yx zOpXqqiVgq{*n{xes7l6n*Uq{<33ncU^K*|<^bUOce;e7t) nWETQJv1I^e&_E~PEyffC{tNSzyum!655EBDu#+XP&4BoSy`!_4 diff --git a/src/handlers/AddRunConfigurationHandler.ts b/src/handlers/AddRunConfigurationHandler.ts index 0febdc2..2f4d4be 100644 --- a/src/handlers/AddRunConfigurationHandler.ts +++ b/src/handlers/AddRunConfigurationHandler.ts @@ -6,7 +6,7 @@ import { VdmDebugConfiguration } from "../dap/VdmDapSupport"; import { guessDialect, VdmDialect } from "../util/DialectUtil"; import AutoDisposable from "../helper/AutoDisposable"; -type VdmType = string; +type VdmTypeParameter = string; interface VdmArgument { name: string; @@ -32,7 +32,10 @@ interface VdmLaunchLensConfiguration { constructors?: [VdmArgument[]]; applyName: string; applyArgs: VdmArgument[][]; - applyTypes?: VdmType[]; + applyTypes?: VdmTypeParameter[]; + settings: any; + properties: any; + params: any; } export class AddRunConfigurationHandler extends AutoDisposable { @@ -42,6 +45,7 @@ export class AddRunConfigurationHandler extends AutoDisposable { // Argument storage, map from workspacefolder name to arguments private lastConfigCtorArgs: Map = new Map(); private lastConfigApplyArgs: Map = new Map(); + private lastConfigApplyTypes: Map> = new Map(); constructor() { super(); @@ -142,6 +146,18 @@ export class AddRunConfigurationHandler extends AutoDisposable { // Add remote control if (input.remoteControl) runConfig.remoteControl = input.remoteControl; + if (input.settings) { + runConfig.settings = input.settings; + } + + if (input.properties) { + runConfig.properties = input.properties; + } + + if (input.params) { + runConfig.params = input.params; + } + // Add command if (input.applyName) { // Warn user that types might be unresolved for projects with unsaved files @@ -181,7 +197,7 @@ export class AddRunConfigurationHandler extends AutoDisposable { // Add class initialisation // A constructor cannot be polymorphic, so no type params are ever available - await this.requestArguments([input.constructors[cIndex]], [], input.defaultName, "constructor").then( + await this.requestArguments([input.constructors[cIndex]], [], input.defaultName, wsFolder.name).then( () => { command += `new ${this.getCommandString(input.defaultName, [input.constructors[cIndex]], [])}.`; this.lastConfigCtorArgs.set(wsFolder.name, input.constructors[cIndex]); @@ -193,10 +209,17 @@ export class AddRunConfigurationHandler extends AutoDisposable { } // Add function/operation call to command - await this.requestArguments(input.applyArgs, input.applyTypes ?? [], input.applyName, "operation/function").then( + await this.requestArguments(input.applyArgs, input.applyTypes ?? [], input.applyName, wsFolder.name).then( (types) => { command += this.getCommandString(input.applyName, input.applyArgs, Array.from(types.values())); this.lastConfigApplyArgs.set(wsFolder.name, input.applyArgs); + + const lastWsConfigApplyTypes = + this.lastConfigApplyTypes.get(wsFolder.name) ?? new Map(); + Array.from(types.entries()).forEach(([typeParam, resolvedType]) => + lastWsConfigApplyTypes.set(typeParam, resolvedType) + ); + this.lastConfigApplyTypes.set(wsFolder.name, lastWsConfigApplyTypes); }, () => { throw new Error("Operation/function arguments missing"); @@ -249,19 +272,25 @@ export class AddRunConfigurationHandler extends AutoDisposable { return runConf.name.startsWith(AddRunConfigurationHandler.lensNameBegin); } - private async requestConcreteTypes(types: VdmType[], outlineString: string, requestType: string): Promise> { - const concreteTypes: Map = new Map(); + private async requestConcreteTypes( + types: VdmTypeParameter[], + outlineString: string, + wsName: string + ): Promise> { + const concreteTypes: Map = new Map(); for (const [idx, t] of types.entries()) { // concrete types don't need to be resolved if (!t.startsWith("@")) { concreteTypes.set(idx.toString(), t); continue; } + const concreteType = await window.showInputBox({ - prompt: `Input type for ${requestType}`, + prompt: `Enter type for ${t}`, title: outlineString, ignoreFocusOut: true, placeHolder: t, + value: this.lastConfigApplyTypes.get(wsName)?.get(t), }); if (concreteType === undefined) { @@ -274,12 +303,12 @@ export class AddRunConfigurationHandler extends AutoDisposable { return Promise.resolve(concreteTypes); } - private async requestArgumentValues(args: VdmArgument[][], outlineString: string, requestType: string): Promise { + private async requestArgumentValues(args: VdmArgument[][], outlineString: string): Promise { const flattenedArgs = args.flat(); for await (let a of flattenedArgs) { let value = await window.showInputBox({ - prompt: `Input argument for ${requestType}`, + prompt: `Enter value for [${a.name}: ${a.type}]`, title: outlineString, ignoreFocusOut: true, placeHolder: `${a.name}: ${a.type}`, @@ -294,7 +323,7 @@ export class AddRunConfigurationHandler extends AutoDisposable { } } - private applyTypesToArgs(argLists: VdmArgument[][], types: Map): VdmArgument[][] { + private applyTypesToArgs(argLists: VdmArgument[][], types: Map): VdmArgument[][] { return argLists.map((args) => { return args.map((a) => { const concreteType = types.get(a.type); @@ -307,17 +336,22 @@ export class AddRunConfigurationHandler extends AutoDisposable { }); } - private async requestArguments(args: VdmArgument[][], types: VdmType[], name: string, type: string): Promise> { + private async requestArguments( + args: VdmArgument[][], + types: VdmTypeParameter[], + name: string, + wsName: string + ): Promise> { const commandString = this.getCommandOutlineString(name, args, types); // Request type arguments from user - const concreteTypes = await this.requestConcreteTypes(types, commandString, type); + const concreteTypes = await this.requestConcreteTypes(types, commandString, wsName); // Request argument values from user - requestArgumentValues modifies args, changing the .value property. const typedArgs = this.applyTypesToArgs(args, concreteTypes); const commandStringConcrete = this.getCommandOutlineString(name, typedArgs); - await this.requestArgumentValues(typedArgs, commandStringConcrete, type); + await this.requestArgumentValues(typedArgs, commandStringConcrete); return Promise.resolve(concreteTypes); } @@ -365,14 +399,14 @@ export class AddRunConfigurationHandler extends AutoDisposable { }); } - private getCommandOutlineString(name: string, args: VdmArgument[][], typeParameters: VdmType[] = []): string { + private getCommandOutlineString(name: string, args: VdmArgument[][], typeParameters: VdmTypeParameter[] = []): string { const typeParametersOutline = typeParameters.length === 0 ? "" : `[${typeParameters.join(", ")}]`; const argumentLists = args.map((a) => `(${a.map((x) => `${x.name}: ${x.type}`).join(", ")})`).join(""); let command = `${name}${typeParametersOutline}${argumentLists}`; return command; } - private getCommandString(name: string, args: VdmArgument[][], types: VdmType[]): string { + private getCommandString(name: string, args: VdmArgument[][], types: VdmTypeParameter[]): string { const typeArguments = types.length === 0 ? "" : `[${types.join(", ")}]`; const argumentLists = args.map((a) => `(${a.map((x) => x.value).join(", ")})`).join(""); let command = `${name}${typeArguments}${argumentLists}`; diff --git a/src/slsp/views/ProofObligationPanel.ts b/src/slsp/views/ProofObligationPanel.ts index 6527c35..0f7a89c 100644 --- a/src/slsp/views/ProofObligationPanel.ts +++ b/src/slsp/views/ProofObligationPanel.ts @@ -14,15 +14,15 @@ import { ExtensionContext, commands, DocumentSelector, - debug, ProgressLocation, Progress, TabInputWebview, + debug, } from "vscode"; import { ClientManager } from "../../ClientManager"; import * as util from "../../util/Util"; import { isSameUri, isSameWorkspaceFolder } from "../../util/WorkspaceFoldersUtil"; -import { VdmDapSupport } from "../../dap/VdmDapSupport"; +// import { VdmDapSupport } from "../../dap/VdmDapSupport"; import { ProofObligationCounterExample, ProofObligationWitness, QuickCheckInfo } from "../protocol/ProofObligationGeneration"; import { CancellationToken } from "vscode-languageclient"; @@ -343,14 +343,19 @@ export class ProofObligationPanel implements Disposable { window.showTextDocument(doc.uri, { selection: po.location.range, viewColumn: 1 }); break; case "debugQCRun": - const requestBody = { - expression: message.data, - context: "repl", - }; - - VdmDapSupport.getAdHocVdmDebugger(this._lastWsFolder, false).then((ds) => { - setTimeout(() => ds.customRequest("evaluate", requestBody).then(() => debug.stopDebugging(ds)), 100); - }); + // const requestBody = { + // expression: message.data, + // context: "repl", + // }; + + console.log("debugging with", message.data, message); + // VdmDapSupport.startDebuggerWithCommand(message.data, this._lastWsFolder, true, false); + debug.startDebugging(this._lastWsFolder, message.data); + + // VdmDapSupport.getAdHocVdmDebugger(this._lastWsFolder, false).then((ds) => { + // ds.customRequest("evaluate", requestBody); + // // setTimeout(() => ds.customRequest("evaluate", requestBody).then(() => debug.stopDebugging(ds)), 100); + // }); break; case "runQC": window.withProgress( diff --git a/src/webviews/proof_obligations/QuickCheckPanel.tsx b/src/webviews/proof_obligations/QuickCheckPanel.tsx index f812a06..0ca1943 100644 --- a/src/webviews/proof_obligations/QuickCheckPanel.tsx +++ b/src/webviews/proof_obligations/QuickCheckPanel.tsx @@ -3,6 +3,7 @@ import { TableHeader } from "./ProofObligationsTableHeader"; import { FormattedProofObligation } from "./ProofObligationsView"; import { VSCodeAPI } from "../shared.types"; import { MouseEvent } from "react"; +import { VdmLaunchConfiguration } from "../../handlers/AddRunConfigurationHandler"; interface QuickCheckExampleTableProps { variables: Array<[string, string]>; @@ -48,12 +49,12 @@ export const QuickCheckPanel = ({ proofObligation, vscodeApi, onClose }: QuickCh // There will never be both a counterexample and a witness, so the following array is either equal to counterExampleVariables or witnessVariables or [] const allVariables = [...counterExampleVariables, ...witnessVariables]; - let launchCommand: string | null = null; + let launchCommand: VdmLaunchConfiguration | null = null; if (proofObligation.counterexample) { - launchCommand = proofObligation.counterexample.launch?.command ?? null; + launchCommand = proofObligation.counterexample.launch ?? null; } else if (proofObligation.witness) { - launchCommand = proofObligation.witness.launch?.command ?? null; + launchCommand = proofObligation.witness.launch ?? null; } return (