From 5c76a43a2f7111074e1632b9300ac0be4a6ac521 Mon Sep 17 00:00:00 2001 From: lukstafi Date: Tue, 18 Feb 2014 17:17:09 +0100 Subject: [PATCH] Timing information. --- doc/invargent-manual.pdf | Bin 129620 -> 129672 bytes doc/invargent-manual.tm | 3 +++ src/Infer.ml | 20 ++++++++++++++++++++ src/Infer.mli | 1 + src/InvarGenT.ml | 2 ++ 5 files changed, 26 insertions(+) diff --git a/doc/invargent-manual.pdf b/doc/invargent-manual.pdf index 43f77df9b81096cecc22d6d9d260bb3acc338d71..8e74ed6c394790f876809d15e73af384f0eda25e 100644 GIT binary patch delta 17447 zcmajFby(HkwmnRDcXx}h6E@u-(g@Ps(j5XDP$Z-qK>;ZxrKOSX?(S{`q+h=0-h1vn z_GF6;tEjoW_QL`?s-aoDiM4=yw+Ep25Wsu;et zebBZmDfJKLT~N!8ed9wnFgtNR!S4tUw=5hKy*@cO*A$)`=^}t@ z4I6D@TQqt3dHRtKSi4hMR!Cz&>*t2+>RI>yEL@IohsQAhA95<{L-q=rhaAQa_US9? zo3E|l2eE2JUXIgS`FTF$2M2aMYp~Gebin6@Th+=A*~_|ve)3ctm(+aqeur=$n=k9$ z1i>~r>-(DnH=bLsK>RuV*}~=N;goP1wiEik?FHSnSQ`dr!XbyG>nw@_x-Z`Wn9K09 zA7g$-lZ8>CX$uhiKgk&7uw+hdFDJrZ!ekD5%1?e#nKW-R6UBy*pS# zfsOGsW=Ru2gp=`IO!d(R{47PX+>*DxB3Mj$`&kkzmZ_}nV{Sj$qLFVKI0WGfsFp%) zrph0ikWDLE_WMgeGUUgfZ<$sU|L#-UKI3qk<)-sdx5UCBu<5hZ(o!lzIZ5Fq`KGLh zfnrD^uPAB%!6UF$1td4~Rfp*)3nPaCvrH|=CIEXszzBj-JH6P7})`qjld;N>RY*Vz*I7~bkFLNO;R1hJ(-L> zeue@gIJ>F40H0&*`5}RfM1R3fok`nig0r|TM?ZV)S$@Xe=~)Ap*os;f7D@ALvAbrY zV8)c|VhVB^G1VXD7z*tC1EoOeu2>8d>OXlLdt;q`#}3Dl`O3#%V(e4lA~`pkO+_Cs z`nu*)%LM;19qsO=B~SRdQ8m?Cd_S_ssJ&j$$Z{(OuFItFt2Hh{4lEUsKh`6o9-~dOICmb~ zM&(AMy;);+)~%!N)%@WQc>3>70jHVDG;CirWSt{yePo za2m&%$~DbMDu6%6Q*W?56j- zosU6hu#GK2urW+u_9h(65;ya;l{KU*uPNZrTo;Bf)d*lWB)}ir@d_0`xGi8zV`&~u zmZqXqQl~@NIw~GrYI#o{L#q^TfUMo=OS^%WkVpYUyfgY_1lJ@|0g>4iC{)s_xS%1v zRP!aw;|}K#ziJ@uvyk7!Ng+}HgnD`Gw=Oy5`bURly)rv17ilx%3ecTGp6~-8$gqt%9O|=rxP}(O^!~{{q88?b#o>}QEe<3eq)zfsVHYy z@<#Bn0Tmftn>;!A6q&=H4o+Y%xX64>O7#^Za|lq2z@@X6MH)L>&(7FU$My2tMVQ=pn+2Z2ny+7YK z4EuafM*IS&L&xl@p+A>(JRGqNrmEN3vqay_*MFw)idQ4xYs$XA0mH=0y4K*C*JhrC z-cpttyA+Fwn!(XbNbb#Ep@y~lCc(8g9#Xa@}ArrM;(tI02>e;)p z!MM(B0jlwLn#csLFSDthp$lbxEtuNoA*yT%+LKQLDH?djz5AXeB8Zi%o@eG797J6; zVakrF@`9(*l$MovBYh)7$`i4G^u$dFgxjXjItaOtF0$}4$#SUjFtAf!{n25#v3<&h zP_Y)I0B4<_+r;xg+S9J+d^JOB5jQ)?mTK|NgVSs!T)7#Ld@@ZbM&z-?(4*5C@b!(y zG&wrlBHWt{p*=U9fh;l*Q+weT)?9GrVA4m{U514HOcpCwOS&$UZK`!XS>A^w=eZ*Z zR4xcxeezc^Ul^^^;D>k7GF2hu$9H}V?tw2&SKy?4yV^}Ntf(_NHRQbb1gm~d$IER4 z3&|pr(S|EWjUuA+UsRknwHDaTPeK&Lryv|$Jeh(wj)Z=2#F3pdLXm}J?*+(2Xu&CL zsn6?3@i(BNSqq(XL=T_rI=IKV_<}Ub@XN*TEwOpWK;MZT$4>(vHdA>v8?DJY@^tru zN8ufT)c0(ZycYr^849a|yo>_Rul7$WC*W?F<}fq6Tm++;mk!^ORRu3u=t(2LrTxeV zCkjCuPz{%D3gF$p2|d$Dq3>_Jy%hAMWsHPjM1A(={v)*!l{@o>E&bw6D=g;dK>sG- zT{Y!vTVFDP<9kMu6~7st`r3O*7*mz^W*K~3=#OA4KL}k=70>Xy%ka4zCNL^I2mPL~ z#L~mHNQ3~bZ|P?a!V!loUwz))`x;anjPh*!4>HCqWEF`&Uu}w#+v|*LWaVJhyFx1P z7t+n<-0oUQ9I7oL+Z-1P3dR|-nFmHYfL&`xOs*JNp?mXY6wj5RnS$)&Qd4W;3cCbvw z5#sH6L+$e&e?DS!%LM!5DoS?dETHA_rC9T!qVgj1S;}!u!1K2Q=qY1A2$bv&+JoPi zR+*^?koJkrH~0-%amCh4_A#uP>=(nijJYq|voe#I&Z|*vXw{O4vI;*S#%Muwu!=|U zXuT;IRCkoN`ft0hQ_9fF{m;geY>N$X?6pMW`l6r>m?=@6-BI1t03!~Vb|mB^oM|iI zoBP_vy7ue7{2b(7RDGdJnBpr{|90U@2$Xg_=wJG1#nU|au(E~ggXB4uKSTD9-LDFl8-(D~b=NAV!8=}6A+@LZf8ipE- zsF`ItZwydyF5U0w5zoBJpFIr2mS$#`)t6r_fHl`eZA>G79bqORzHq~-)iHI&&|>5w z4@^dO(P{~3UdAq~0t`9uT3^G%02fr|C(d7Qs`u}A&>UP7qsWUC!TCHqY3&D+_S zIg>cgKmLMFL9ltsQ2A!xr)lS%iaX2N?Rzr#+g7KWGQQS(0FpVRJ*gbqBv|1ph>8lOa z941@qX#30~$_OZ{xX&gHcvE-!1uc;%CJDJHMD9ce!b$VTA`wBaI;7t-yFn--hX{)2 z8Equ^CX785*AJb~^;FcVi=BvzqmK7>X5i}unYPD{pv|F%@r`9GTuu2a*i*r7nz;%K zT{bmQdZxu|*1)h_?O>t$WN{XfaMEI2OZ!9Y$B#vT@jxy`bi8(<#D^kL1*WShz{ zk%AV$)V9aWEnwdA&7-0213$h%lZQoV{n+;msjzaP89OJ?j~CSQ4J|?OIL%ZSrkMl8 z;UN|QKLIb{pMpLlb6*bUqimaDqu~3GDww6hRglBY8xGeHNB#U`)#CA;_dYz6 z#m0+d`|})I{Y#G}k6Lvt6COtEmA#+>9(?vsJf*fwj1f#@SiI$SRgq&^F;HXWZP?`Y zoh2`@SsyGGKnc&on6M&r20VmFK(OCc-Ob(y|JtVTZ0RD?+hq8+ ziz%(<7T#q!&72;tkMVBM@hL4aBO~_aXDXpc4lYH|kq2t`<`;%+<%hE3gUDNX> z@Kz&^+YbDiDXpH~#m@@0FN4(!=NcQ2Jdjmxhv-lEV<8Vk4v&9@>-lMW-YsO!EEL^4 zy5DR$Avb#%Q0Dt1I@gK2U1e7o@16ecd01R3npFSBF;<9gAhyb$D#O%s(pqx3n?+;m zszSKKt%9OYN56|oJ$eN%0%RN1Ql|A~@P=Oz!y|Iv?4c4Fu)q99dTZ2ZLUiNti&Ooo ziks>A{RFpZ7z42ge155g<~`Ri&2Q?>V-5TP4@6m#-HcJDf^vgQI@WiuJ`?I2CEipA zk-DeLI)8mtS?ykBED_sJSAEofBAsL2`Jpk1E3EuGvK?8d9$AGI{GPqWGgkbkAMt(E zP5tI^DFvZpapxFQIaaBd*u}e%ODcVUx~^{f&8hWa9}#-coIhYGg4u*uSPU}JhNRhf z)!=&THP7qi!)3V;^~B(^GTnX)b|N{VA(G!I3lsl8h%{*XyIRY!v(oaD|*emVJS!9ib219 z&f>#Ok;+^!zmlAJp~|{UIUbSqXyl$9H;Q;nO#e18Z=uYQ`r^9>)_^$%QtH`dARGDA z>DUkuSU@(06BMdBPQBBZx|-)MvEwjkhq}CNS;#WZIM~gw6csyVNQkSK;6QR0_UDke zyg9WbBd2~aJS;PTaG|RG_4{V*`R@>gM ztfy^0G)Hgh_fzm5!0~HE#uZ*=luzh)ZMrRIc&b1WPzoLe}o}vEb5GFN5 ztv2QOCVmg$i#PzBg)xO3KWeTnVN>-QwIvEQ|KUn142~LGCKBaNDvV1gs_C4AjpSwI zSQM|XOxUzjki~;t55VUOMHq5kCdJkYk5;cUh%WWMn9Q^`%>u zzJQ^i1bF)D-OiXiY0-|VB55E=rZ3eDZCVjMp8|X7oaK^R<&Sas9P8w{tfe&GI^WG4 zkCN*{0AB7dH)1$TaPEL}rZsZkDRNo~Wm-8jI>rts#PVUwDq5t&mxNErGT9q(tb2uq!63qrI}3v22lbVKb%NMjXW+&31jM=>o*{zOTMCyX++CWc%NE zn*y;@kF3$(YJb5w?kLmGKxdw>8{sBdw^QbOg*v^m+dWMaD2H}g`_+jBYFU{TH%;|n zvtVh7IR=_^GKMPgEw-S){KYYO2(9@5?FM|btj$Lu#+|=Ezd3!ev>&d;CjBDQ4j7?`M@OHsa%@r3#CM0E z_mFrn>G=J@RNU31A%L$Q z-PX08J`&$efiFq?gvk$V!qrbjMuJA)H=}-d6sL+sUcRHX?xiqEop1kKk*3^Neo-ZgE-r z#`LA;Vv}H=!GN~THGb@97e3)xag1;?05aGXt*+B#l`b(?MBRbP_8^mlEzS@w%vwp@ zjoUG<%+Ta?IwPS?VXV|`h_9etB|NaCI3a#>Q-A933IQGs=Dxu|yK|P8A%izswo~U` z!llaX74uYcu-CAt-r;Bgoa|gNe5WmUr4E1c4Kke zx?`zIF+TffrVy1+(Q?o#Ho^r@I3@AfRa}YFc6J{2It)>n*Y%23X2b)Rp@D0@)SH_q2#GDO{)-j&^HTme?Vk;%=}3t)TjZREm)B#X_fSbi|P3 zald$}m*3khhK|FIOuJ3#V<6der@Af4UA|J+wW|Rw<#~b=I&vsD`V=m6)Dv%a!KCR{ za_>WPy`Xy7>@o2B6Z0&C^UkPO(51U1A{0XWU6vn7B7tJO{2C?K9yR3LcZVHIwAUSF zX5&4RY>Rl|6${&8#Cs8ujibirDZw%3{()AhC}F1Z+x1A*j6E+B+ztAh`nSX`5ew@E z<5xAC6H}eKjn6EoDT&}cbjXKD*mU2H;Uk#Ab|E73IG8AGhsePFzH>Iq;;9PskCK== z$9io-7IWhZvP+Ilm3^~6pX-3Xsmu>oSd9=nTPIIjBl?_Q z>qT6(>tfwJZ(`fYO__tQ;I(}zRV?Ox7ewy5$tP}3i8t^{DO@2>2RN;`dffg7y%oal zTI3NV+L??=M=H?8#)J~2;8ONj#^2f5vaBGOM@CHMAtL(`4vJvh-?S2`*R`XNz< zc<@zDm{C63AAkW|#T>d_Z7JQ9Isl54)J1hruoenw@-t=G`W}N2(QhcNd_|d0iL?yB z$L7yM6>8tPh#98AV}9OG(s6Z1SQBVu6-YVIppG5iYTi3@%L05?#DcklV;;vj^9|ii zPw%`Cc9MXy25OU7ni1wYH~e@f)q4Va*u8e3)usRCOMwB`h?)3=1R5~NBB9Dau}f_W zIsT)s9Mt$}Yrjv0#62N|vCoS<>eFlz!8i2smxr-*0|o>IIt1F|DQ}6W`{p)Z*|Wwr z2!|e}e$5loGgjD=urj4(`I@Ms>h&5A=j0D{>|({rkmQOPoMObr7YV)GFyQ@Z<8?9} zX4S>)+8R_54t~QDBd_q@K-c>Q*Iug&Z^P+!#Fx6Cy4Yvr5^Y;rQCS)5D_1;=B?#@ls71k@ve<$Qrd%4*T5uxWVQR*U4tcBWbV~G(oGd zV{2}sw%%TE-=8htS#pV^S8O#mL$oA;rb{nl`pRfD;jsdwO3BU?ls~;!Rim;-hvk{V zQWVRJzS*)h!SVuThssVqgm~s`c~zRnVFY26pOcaQhz#gmAW~+~BX!zMU~xtGLBzk3 zA1Z=)7+tqB4I*6_{^@pcWmZW`A4^i|0pPZ01id7M! zEsgI*5{4mwG_76GpPk^&IqsGfk8?rd;h+<* zqU`LoAFj`f!Vd;Y0-rj9mO3O=of%Nv9ohwyuTJ1AC^4dq(5o+wICA!5;I3xh=8jte zA~p#!Z zD@iSAXBLk^mVd&_&~1L_JxJM?=DTJIV$dfIkfEI zN3R;a{BXX+|0K8{-WPwy?3m2?qWL(Iw!zdeyNp=3_DIGVF;}(ZJq8-PgPjq~ZY=}+ zg?5we+?W6%b?Q&058lp*$fYUq61`mOjUEeibX!^BQ7`Iq9$MK4$4^?*u`I7{%Cqb1 zW_4~_DIbmvdYAYvSj#?%7%bGOONEaU!&PX10gyY!3$T`YgbtsBzvc&yM-;~VRQIu$ zd0TnCf=x(e9$IRL+%lY;E+5w{uJT38wA0H-Z=Jje-fV-%JkHFFDAIMIwMAYQ;>hc= zg%$K{?WNxA6+&p(z676t;LX+d&v8nGZ< zWSzvQUWWg;?owx47KjqmIGv<9xc(&e4<{&Lr^~OfIrmj7s7+MelW4g}r z;=dvu_M>6>nfwiyv`Wtnt@-j@Z`=m%$DcRouKSUN#hgJVes8E6 zbH05(CnM{QBG>k(WG~ZTs{)gQJpT2)E*Ve9L+SmMW$<&k!bJA8fHm!Ja2u2z6@P)} zo>SjLkVaCTLC%`2p)Rs9sL+#*QrPZgN?-<@In;9bxfWyUG{f35u=hBU^i~f~alwHT zy@z&aH-9=f^eowj8Ef(lt8+?i*;w5PHaXa_CawyvT43|LdF#cp5V80L+ziPi8b3nj zhhB;x(YtpZ(m}bOKiXLR?q?o~KhpT@D*1+!>IDKD^2PKE+d7n9cWYK_Y6 zZc6z0BHN;rZ(*rJ$BI%iwQ%^-n;8^Gy3Ld&j@=;55AWi)Hq73>g0*xcP$n2$9QWQV z$4#CV-UmdIMM++)bmyn@Su}Zcoa!fM?EX@vMZ4iumihg5;B;0jo7fFCZ1{c9eB&FJ zfS`=RR|kS`@1ggt_k>^K*w+_~n9FpN%G%=P%a9YxZDlTQMiV=3oU<^`rhf1l4eG<`%qu!$&H3TdK~Q}2I`P|bNCUq*6gWNHT-n^{Umy4^zQaa_LckUK?}`xN zIPz29;Dv3;hSnlA{JmJ-{zdm>K;U~PtrN`zuPblSdbwii=smqSX&Y*1XW;d zJ4otE(saDplt2m;JpFUpSHykq;ZKGZs~x;4cHfsLDt3eGj{w*7CMq5UynOxn@%QuF zqF-Ah1@$6gH!E$tBfHgGau0Vax7>zsk!3Nd8?^g@Tk%x-TQ6^avf|?d#a>OO1YLv4 zKZ_e=vbWJ011d;14@EqVgG2XL=avij26OYfhi|41(#mVKJ4_f>C(`CVPCS(GJO~?( zP4Tb>r!J(gdJQgbNU_(_>(E8tYE8du(k|8{LpL$4R>QGh7>gH9iuLB3Cw=D)Pbg&g z=$hJ^omM@!90CeGk-916=$1)H<^SYYT<`KqW7C@mT|U%k@m;&=x1Sv23+Usw%D8U+FX@U1S0{8%2^e7gJX4_8DmL2w_b5J!3L7#^tJ;>1lyE)r-bz0 zeC0qjO>gzi!^ExhFHtSW-)niZ@XL)xN<&$bm{!-bQz?P@Mt%9%n5%{nk?qwAa4l+5 zQhQI42=|Z5DhwG6m&BcU*=maicpcYXVF_(`mfIq-ssGh@YD81~!!2QTg(F|5Vha-y zDS9VWKU!ZNKxJvBOGli~J)i%_1_yyTf5t$x1&Q|Cu?)#nyO#?%jdw3m;Ogd+{*HCk zhQ@|ET(>;qCp=&2y^a;H$=BA%;fAJbXK}Z`EejpP{VW355HY{E*OlM8tyI>K1&9(4 z-Fd$Ug2*MJD5^hO%gD$Fn9}TYh~gvP_{_`=nc0R4Eg)7;_}DHId~ZwGV?R@;qS7R- zH<%JlatCgQ)6Zdw2V$wV!M(P1gXI~B+B;VUSJgOZjS=c7`d=c++fGI|U`RIB`)PVR zM|&w>I5h(R85QxA4V{=1q>_BiG0vm-aHaqIMOvNPRIhk#BQMqmsqP{&8V+Eov@zRkT_j$`f%`^@Kza!ym9o$|BVRW`B)eOQ> zoGwZ3HM_fbDD(LB5@P1K2sLN!qE@^lv~W`$BL_9zva^z}Z`9DTu)ZcpcK@<6sBN6! zmYi+PS8YcxUEwiNpo}!&dw1wFP|d;cK3u+ETLF=&|5$CLGP6IblcAQ5_fLEKjU~r3 zAqlb^o%KlN@ZsP}VktQ80iAdc79@mRO-p6gTGpI0#KUls6ERH!+155r^>FGVskGrN z5xQwYfhSEL7E=vm&yb5yqE~i7B$nR7aP@%B8v|i8g{nKi&Zk+*5J6S^wT)i~PT-u3 zUZC+=6bIhhIU6_xyGE?26qBDD`qE`<27OI0H6u=aW_#&E1{MAuNraFI)xo#$xpfRV z7is&e^Y0uln5{6j-(eYtwZHWa*=7Z|mm7?bR?!WAXwjl1Jn!_iM|b<_JSD3A>{PLk z=M%e&sLanT7Fp!-76O(WbCGvVNipbPHm4BtD4~QO&-MEzR3~R$(alI7yyjQfF=WXQ z$GSNeg5INmSw2s}+ZBk7GuG3I6Cz%<`tnlWP>6q$rRdVcOzFW(o^Gjo{XJyzQt1J~ z*n*T6Rr)MYa1Ir=oQH~8WBJaTBy$Y%MOUP>clIUZoGKvGn5ZSdcZ{aN9>BW+yR)7n zNVcJt2?7{Dh-R2*KNi(-ENee6_)B%{m(aQQyIa ziCdX#On#4rCSS3yy}?AzX_{J?8-pRvzvCOcQg@F0#vY##OIsP_$cl&Fi9Lvy>UVHpl|4}AYnZ0E;PiGAyEHPk1+DOW zBJ7#Nmh1_1JSp0}hk|WIE$)n(cVc z4@I-0Ow2;pPE$KKJ!STqtrZ*-2_h)$?Q7AFpLKE&uhPmR=q5+UN@IplXHLzE%F7xyE!4kfJxQ3B zD(4K1F+uRxChzxK=W&D?F{&5U1kB5TDfA+6h2s(pkpz$nnVY>%Wn!J)=x3NTZ?`g? zl4)d)z!hGm(`;ibgV%j)-a7fasF6=zAYYLdx1u2+{!E2c+b{Bq6}W*JSP=#wkijmD)GbBLXzL1`;OuOYQaFPYrT~Vxzjco;3-T(~2OTZxov49c zRrx4-+FYzLpHDiRJ*RcgsNyM7S{O&$Q(;xWeIY%6_l6k68Tp{>RA{K*oJFJyqp60WvsGEQ%qjq-C`r8txS2eXdesqoX58$ zhS^Y7-oz~oTHr0yvJPb^7h-2`T(V{7)5gI!{iy6V&8~xQd}WmDO{FAVB0#8YU(8_5LH<^7D4$p4(@~v?E>o*A4ka&U{#wBw?t&|AW zvr#EM5(;&0<}^CK;5(XVpN4v)H}W7ck)}A@a~B&k3jn%!F{JbX3?q-y`VV z@>CI0N@@Fp%YhZ&zF}!>v-OK*3*#<4nhaL?{EAdhsd+4Iw8+QoDwJsqK+J2h9Hwq$ zz6_1Ye0GPi{*s@-QU4^z=c-}pX!=x4@8yj_fr5iipo~>d!_B>EqU9HJPu46EIE)iK z8#o{1Bqesp(Unm438Z>PMx{M)X2nzFJpw|`miG+cIOHAyg}0Ylw|351sc?LJi_P*| zO>cHrmP#-|S|R@Go4(5eKCR|7aWbjmq-pJEEZ44(ye_uUZVpjlNNg(8W`L6wmJ~}* zdF`)q<`$O30=5lAPQ_!xQ$AkGM%#`UxbGEhO*tzGcqqy&QVQC`+@QCAeh#* z^$OFV*Pke)ci$sGD!dpx2pXM_|LMup{lFvo4nMcV(66#Htcdr=@1YI{#SkKTkGyyB z-k45mlaV!!6)cv?L!m1P(((ob&nf1j3J|9NA*lJIo%LGJF@Ad9jZgFg2UD0NWOaxAC%N2NSr+Vc!zX|_jyXe|`W#aFzTDzN{jDvZKhHEE-G-~6 z^+vIoAR`svzoR^0Bn2_6;|9LMJD!*4W+@6|_V%s&mf(XnqZs)s5p6)%K9G@-$R!N@ zbFZccFsEP|Tz8KtTPW|bb`1}8;ru0MJ0+l1Rfk_!nZ zr@NMfZMk!+6a*_2sE2mjWfus(M}8iH5gTQC{Y=n7^vIAPSWnv6wFo}Mx;wH%1=w+W zQ`6P@K_kQdXN&qbH{fz!alu7kRHYdkPO{r3nd=M7EgAO>yn~%-6So|b*YhK_QoGLe zc4QpP{acBI^JIEsQfI4}r`E5r(UiFap$Vd|X?x4ZYHkWzh`Yu`Xn!#lDq4=MW##?w zBjYvnj~fV=6XV&@iampumpLI^$qW9ncJ*DyF_pw%Cd^@GiBm^ijJgf%E&)i+S z+b`Yl;8Hcgkrd$iKbkcnKLy3D;coKM>#vsz5jz-_{u0nWegN@dj4z zB2CZ;b)i zi4EDzE&$e-3NeW$B1?LFdV7B|8{wlh4W4>7X5#{N9we#>kw0+~(%cfal#ZwaNECL!oW>jT3pS(yDtH*zN} zRuHoM&4iGs9V}rC1GV^e@x!np~pkjRKcMexRZSs3ny#Px3bYji%-)ui!ws-Z$1GoA(^*7@0F;><$ zQ1?^9KfkHIiQ3Txxfm{GG7BXA5u8T#SSV||xHujoGYiL@ZBRd^sC|_yXMcq~esvdw zUh^g(D!32@uF}Ao;{n{Q?(M>DSZdLFpDw2I{de3NiGYf05NgmJlCx1nsccD;$;YIZ*Tmh67hKeTa>@t&ts}oq(V;94NpL0zvgaI?a(rTM37+oS zMxr*6dXpo*cx-AEx?W^Fm6y5}KFeXK{|a+!;p=+CXZYt5uL-ucP|Ro{ zbHi8UFx7-i{y)x%VL?Bn8A{_lq~Nn`W$|CVy}0~sI}Vi z$a)u+Z)ki7t6MO2{o(>$X7%>@GGNR5jhrT1w&(T=Mt66-V}fJ+Lil7#=nb+)|L;S0 z{#KDhMQ3nAAoQ3R2d?tNpwvt4N; zI=gLW>cSDaL5&poQs_$2w~HGq&lifUAeWuQkwbh5|;1i{j;Ty=kO56yfGo}LzCS4 zpAV@v@Q(IL<0Ygjdv@p`vHXeDoL^ImziG1UiUNWENI6w;jZb~%i@P}9Ny3DbLD$27El5MDQ{ zNMPq`TxwJnBc^DqCYJQ`7w|Pf9mNKH+mK>j+IU~gSvhvi@oqX zYBB28eEE~X`SzKek1n*3OsGP7uzAyj=3t<)@&wi36%+NPK-&5A=fjXjv8LSFV-B1a z>%QIr-YX`wt8&>f%{Y{>tN1#@da`!9)cr+^TKz@Mu$@@%Gp#?hm6c}gaH6vtensB6 z%}-!OIa{J!H9UvY_=ARx^vkuNeJ(t?>2z9NxCC=Yv(cA~yX3ov2SiTEip76EK*ELa zF#s4GP2b>RLHI!Lc#~^*lM&;kp(x=_0+l+vNQts2p452qs;JVjTpG|9m89ytxC-Ur z#n;j2ogWw4c|6jmQ;QDTqiC_~sjZVQ=MW+A3SJe(FZE86)^dx#LO6X@bL(ub~k<9a0_2aAjZNzY-{ERnq*yzs{aCJKUk5WC1 zZ*6uF5bQv&W@dqhw+tAib*Ls@Ocde0i#pM*^l5bKDiM*9I45mEfX?U}))}GaXn*9@ z;3qHq)yin-;XJT|!~_obevX`)WGSs!NkM_$?~nxv?~C(ajE3i2boWIhN$a7IwhSyZ zl6(6R-V@r_hZ5LCP-T%gWoxEw`~l9meibw;7J=pXR+F7~0we6bE~L z%hUU`g_Ec@d>tZBw{Igv2EYF5usO3O2k+w1Eu;!CCbecjKON`m&~?v^QkUO#Jm&c` zD?2wh_jN!poN}2zVt*i6wO^-D${@NmrSCQ0<1 zxw1`IRMBHtY18ayZUMk2l^J(*+uxTG+KoHv6^FC51dlFriAO}PtvR;xLGQ$9f^Tt? zhofqn^nF)1<*ZFN*z7k@&o%qr&!qTkeby8@uxd~)@5u88fIj2$U4!R&X-7EEE4gP7 zL+}J%JVv@_Y6kc$_8~<$#c^!m?Xa2Sz3GSu?}tT|4&E;>KL&(P=s-3yS;U2i61uOYGJ1#`xnbB0grs)-MpA&dMk{w| zl{Rpg z{@!vFkvb>kgSM1ns7KdiiQ9^plctvczG8&UrV<4huUJUMWw7xweSOmq!U1mR=(XU4Lp7lPFrKS0wk;2u}JNNf1Iy z$JO`Ke0|grn;To_f-~%Zz?kAHKJ*|b0Va%R{2z1OS!+8qqV*x;^+2-~#gQbO;-$Bb@k2HK z?WW2ZvzU5Fc~L>Ru!dariqm_fNn@hX>!^0s0~cxHAu zP4K4Du#m186ScQ=CyjjbiuPgs{sQOId4~`JY#!6CE!Ewd$iRu<$Z5V=@RIzfVPp{( z%fi9j)y>7i#6G!x4G|}~ehU#B5m3{$g&2Se=La$X{&_Jt;9~vj2Pi-Q2zrXa0Q`U_ z7(X8$4EzLxf(7^<{rW%lgF&Hyrx=7E%>Q4{;{Q7^5CDMyV965)h%6|401zzs?f_9x zoe%P4I{_dc1ood85bzk4{|N@<;}d}XCkEhy06>tMutP*7M9Zi306`D|@RNFgKoD5q zDHjl+0N-EhAYky58i7C2*w9{S{O(G0Djtw$6fjU9~kUuVPFX0 zY3=~8FBh5!3(L13`I`UwTVU{3@MfC3*I`XmSx2n9Z6 z5DF9kJY^6Hgu(u^xJUk>Akg0j{jqufx$tov1Oj;~I4A`A^u#@`69E2|Gz9k7iGxBx zd;;*NmB0Xh^%Dx?`^zPuFn;h~2?_xJ(h*bu2zc5ir~vfQ)BZ~{@c*&4$MgSh@PDyK ze|nN2AA}G3bVEKU@GtuL9((uqy1&{42RwQu^eJ8Z{Eue&Brrce-(NxaVW7Xn^@#nC zxc;pzei-bpLST=b12Oz_{{D}_KQaw{8u(F`{7)-^Jv!+B1N(2|{$Edl@dN)lijOW0 z`nQ1L|2Dp#03XlT z)4-1y4EXP?|10T7?9l}NvrWLqLGsi^|CvEgPt&7dfd2^nU;O`1pB_Q*QxAB=`2W)~ z0f2w7r?V9J_9tm;SuBGf65jR4&nbh2=uRW{8-x~vrni7K7M)NucRNR{r^_?-^K9*0e`LI|F2W> z5C8v5KR@5oQ3(X{^8x_rwKle4an2#Kz~oqM-Bcp zBmQ-F`j>q_*8gw%L137`(>{S72lrDJ9&clRwFCqO{r8RL|Lg|^KfR~`K~R3s|7C{u zvH$;oPiH<5#0P{zldG-}h0FzDkERHH6oMHDV#)VtN)RYN*b)LV1Dk=&9t~KOLHPfF ki2*K_s3Hq)$ delta 17430 zcmajFby$>Nw?0m%fFRx7F~bbZ5Q2cTv`9&}(y7#gbayv`ASof;EiEA3NOwrrm(P37 zdCz(AcU`~vYv#W8-fOLUt#z+GGf&Vd`maCeWh(}NR^%+4z{@u4-WN6%XhS<8!|1$b z9Xs7?hX2IO+zo`6Dw$P1UCm#yIx?bocS~FpLg@KDX6lEYBZ74@eW-!*x;1St2)CSI9=dM=#4l>G_4Bb>0YHj0w!K=|Lq)9V@4AvqK)yy|jrR*}Hc0 zz9z2AW}vGiNy!b_=rwsdHZwXh^a=MdG^l|A-!8^GW0+gbM6C(=51G!&)GuDF0fm9) z?5~h67KL}6786ek8J5jpgUEMGKAc0QSjY>%B5Nw48v-F`Riy`ZK~FvpJek_J6~J79 zc9hT8lNBkTSLh(MyjI zNZ&_-q)!_u`g$Q4R<;fdd<&(`k3a1(sx0|)qOx_u>NLSg?Z#_{ML|1~Fj!ieVuZO3 z)@KE!Cn;kzvc@FE%{|&hK)%+F z&sh!YyM~LmSjl83k`o@Z$u{-@tXM|;3X?b#6Zv7t72<{>!D*tm+KDt9>X(R#Sn639 z<2EHl+g+FL&o{yatQ^~s02F-V<>Dqbh?g561kpp+e==KQv$zP8XnOLd>lldzv~xl6995?V@&Yj;%53;8M|e4{`ctiZ zmM}FNThrStItx&#$+~j!{rB-8C0;zZOpP_BqAzj|^vCqELU_*0EQ}1dppnmCwsJkI z$gcK&if+{AMoZ*RkNCy!>{<{4mT8}1-U0jki!YM#`qMREkk=#aS!sk1e) z!#D<^+X3SjIyAQ%kkGX|ty#8LL*imh>C{=v)vL8VYYZfVOw@8c{# zhs^T#C#%m=3)!k)?(=TS(4riY3T^1!kwlSRI-3yChx*1kIuB%!{**P;6D)nBpmVkp zp8Q%&S!Icf;wA~Dv7=tBL*l}5g^52Kha>1WR7Su+{}XXP6Y~euuTSf#65uUJbWCi< zCYTpf+eS4LTxPbdc%jdefGk1;P>9bF;L=$nqbS{2et!MA8z-|tj?y$%Wf4|PGehGS zZxfnPjq@tur0kQbIV`&0V$n|OrGpN%*5rfLHukDwUi=B@7k1?e>W3u7-*g03Cq)5P zsyA}_K2YA2IAM&TOr0;8%YGz5R0^TG$XeYVRBI7&@j*$gcRYjN0QO)O7_n8Md@+^M z{u2Z_{ALU_Vo4O`yM>Uo3Px8nMJ%?#821Yiho7fhE1U!lfBsCepmeZs? z+LBpexmjvS2?9{jr;(4;8g=eP2tlnXQKe(nKx?gM*==?)Zm738dTd=?h<$~5()^Q= ztka?jku)j4;d4$LpvqE*6W+`5+nO>C{DVP1jrgDkZR5vV>8!5}RLslpS3W;oJ%Kn` z5Rcu{Rc&%)Y+GDL&izE>91)Dwkh4G}rmYmqM z^}IHK4a$du1j?$JL<*d7Z_zKmCE6@YJdoK2^6-8+%7xgf0L8jK9V)!(2F!fU`=1LA zLHnH%^@dfW>BtjMXQ%oXXc(q)FEY7Awdsd(dH5&Yx5{wy;PRs>vHd zYhiO?a`OSMrs~T%KiXcM{EY3CLv2Kk6RjSn!W^#Dp{qlP!G~ziS1XjDzg5b`{bYsc zB&g@Q<4|t)Y&Nf8$0{J^7$R0*o-)twJ>^k85sLR!8DM3y=m4?>#Z8R+W86uz9KApj zTB9$aIbzQ>A>OoB(86+uLuB?sxA0~9Hmu^>3@5gZU(PIKuflgn@Z;o?BL<0(VDE~$ z6rW|pP<}U}VtTgbvz960idaN+Y4L0NA&7L>KyGZ>9CDfHHzt*4jLFu0pIOuG~&CUq7k;!)_Q2TZ66gDyOly3ZKw! zs6=B$rw1`Y`f!%#vNGs^<4>*#|sN1#ex%mCjA|_!amn3WbNx zc^4>rsn>T8y2K>^%;flc89KZz@)XNT%xAcr<=L-!(QL7%F=!^Sk&Jti!53X9?8p;qb^%dd}}V&>ov5(X2pwL zj*K$5iND8s#s z21H0;f?CFR&77O9RVXBRu+&m?$r@3@XLkgBjNXo*e_Ae$%`r2yn)6+uva0{QfM6xw zyg*O&)|EfooYkPkl*(@6ix(Mty~~P@rWSaftro(r>nc(?7e8&JAU!oqYL)CHlFmR% zAjLNC>(|sF<>pG_p_+o|?PE?K2(H!$;V8BZmTk&!mDpf|&nKeW%ezW#otw5NzrHb? z-q4{1o-5hN*Xs{r^4i9E9)1x}loB%@Sh58?r<2nfS=P&!zJ1a;OCbRj8PcUp%>-kQ zcWU>PI$-rL%r|=Vzh{qb5bp>5HrxeD*rzmiXT`<1B-gF6D+DVznZz}4kmfZdf{{1W*xTB&;OYuC?ZHp@?!f|pBTA%m z2=9?$2R0J=1e+WdSnZ3H*HRKL!mxOKqByGDZl==6a^v&z4Gbjr87$J_B7@TMw;l3G z^?4kE?@-7!7Q$pMuap)kOq9|s8(6rXh6{nWa=vl~2-!Mn0QAH$7K!UE9= z7u$6iJ&}@a%2&IdV%Eh}-71x7$C6MW3`$d>=%M<$SkINO+4^n=%T{H1-Hi-=7nd}o zypXNYQ@GRc)aK6}D#B8-&+hdCF*?p5eVC2*EG1^I+*uhr}o)0i7>-P6zWC zf{i8}FL34)Vg9jsF%+?AIE~bL!?W0)4h|KwCr&W~y7!TGFQziS;2E36>6#P_25at_ z4*y)EFn9`9B#3D>ePO`Zvp@wKer4+@{5&gFB%1G@MDBQrZJIVx$TBMo@2RVWNNhYN zn)P80MY<1qRAp}e=g~ZNY~WQ?IsT@Ar}9j>e%M6TLM>GG1KZ zEUME|(|ocHH(u@jGZ7E@N!v69B1Y(9?vEUqwy4aqT@cyqg7>K!V;lo9zHSKPE_vJS z692bsf$9Z;&-2V1%p!nQl1_Jm&r`cjxxM${=SY&K=7ps(L1}F0Y0O(lF<3X^R&$IW zHkD76E@(}OS6IZSF8CO)cBQmL=Gn#)_5Bg4l$Z@}?Xgq$ITZsEhGyz58XdQgO;c#p zMBGQ?;p=-ZcnNYSr2D3CWIsS(G$w+@m(xP!OQUbo<=oe2$~FMf0ixs0G7;-kx2`T} z!Lv~=w>gLTZT4fs#ujvyb?rzu6%eCTI~W}TiI<^=JJ>nV_0rqSu9xRtgY$S-E{q#N z4&gO&VK_38~Teb}%6ASkq78&9p zTW2VHXrhH-s{o^fP+^n09uX#G8XejXe`58>`)}L@vt+ul7d)iix5neIEE{Bdz5?+L zFRQPRwg&0xkwj|xR$OIxD~UMqeGHo{Zrk?u@O!FE6x@&B{`T|j1O{Cvqj;Ffb(oY6 zYhD++?b$GGOMSg;o+)1U0-<*VIJ08iy?|p^DA`wg@-^@|cJ`N%(1#79%^)x4-A+`h z)_SD)9pkmq^2^D|%y%YjcCJkb2WGA$aUaa|-)(>0J-%McPRx(NlYF7)mW9>z9!9)tPZ2Mq3GT>fioVfoM^AF zcAwY>hE2l&wtSm`;hl9)jnX?3g-g#4EXei>Hu0#|ctd*FV1^psjt2Ih#eIiL6yK2`148EOp_$}k$so{6` zDY7Jp4(%&8_X0~K&(6GaSd&ml5_*jU;-@S>>!&}xvwq#45B2pGvj;Ik#WYLylF>1d zRB8rdS(KPBW>3{AnT&{1?=J%1xq6;b+#q_rmP{$GfXiw~czT}hoT{6DV<}o*zS`~) zy^ATPKJ(bJ1sa=2fg+OY_hGJ6nFBO&mmNwqlN!B!3+eK8a{j7Cv*}F-F33tZ=b3~0 z^uhOUYG!we?zKF%U2o@0o3w5Zw$Fx_FIrqRqvh^B>~C&1kEQedfeK--gRjAXz*#k0g$pXP>BGx@5gPt`WFyIP|%Y{SD>UgmetOpN;= zO7b>LHFvB9%k+lfxO1r!n5v;qaZcH24U}He%q>VFO<|qs4a{5{x=!wrXu790Csvss z?V`=kJW~n-5qPXBSai{yirW zE2^)I0BIUN+gt(_gX%6mX1YqQR$MnKInO|o*H`pwVJaeU#PRF>^9!wL*{LRKKvm@x z?Hg_}AkK*TTdU0e)!zK)=jvO+9=3S8eEgmybnuS-D3(RH0IVG@EL)qy?2Xj;033QL zHC%-{lMwpM8a9WU2Hh6#mzy6%hIAOpFVdt1$kYssc)33(mEGP^=>3?tA!D$tM>o1e z?Ga}5QI&FBvxh<0#8@D&RU*--_xC@b8Y?rHiTc6-rQ#n zc3Kaa)5pKfII`rUQMfQjFp)oLE88W$(2My}IcB@#%E&h2s1akNqx;n>ta#Pvs1Wg;2~c#Om!>pX$=A;7 z71n&&c^Jd<-W4m|_`v607~*Qg{SZfZg!DO=0#$nh&e?VIyAPGLo3kIApuZVJuvrDV zu7Br`sT|4%&c4Q%LF~(qP6t8!qlp}_+)b?as)vMGk{(o> z@wN&LhMmj*DHXQsI7pejLw!@}J;``-Xjroq{{}g=+T`1JMRSeURo&T9!zTVGq$mJ! zvZEgPQ?qys^S&qa+Ci*zO82Mb)tTx;@ETLo@aMynhV-Jb{!Uizt`?Kj0KzzP1RuW= z*YO3tWA9q&&CG6J^=-gp7YeFQ?pj7RS)HNMxn=!??I3DWJfjBB(Rt?)A8w9lR>K#N zb*fw^ci`fAgPWDh9}7GI9_IW}FFXLW#%?r3XElLv-LG>A{WWa%`@4a(=P4%Ssh5<{ z6lALxfrhgG)Dpz2))VXRmp0hTtL{xT6!CK%LzuUAn8}}k%2?_dyKIS}Md{Ui6JkX- zyH`CeMwf297BS}C(jh`|9RoL&P;m{CY{GF8N?MyqrklaYc?n-dt^pIODn1Z~xc(%X!m8`WV}laz|2$l-L+>y}@*9O?4lI3qS+ zVWK|^9B=sB25g$VZ{;Fm$LQJ9^0g?O_QiwE@xia47RO6VSF1Q?s^iAGo^73qj73T< z-m>Xcl<+FRQsYn!- zqt|yFsvAqG&FvCvGF20!0)8q969|Gfb^Na+a1*Xj$B4+E;V5>MKSSzXUmlsE+>-vy zFdr*4{M`1%E6G<2(y>^0JWpoN{+R6ZkD2+DS+CwZdGI1~C#GLC2tAJhSd*l~JtJdM zF|SRk6MD#GS=$${SzJ^;z;z-q`-8NWmJ}yR5tVksKbjml7gP6&4EB<-koDoN+Xvig z4%a3jlAOp6Ui(Q4P*7Xb`uQ4zkRk8U>bnhB7AO zU9_)O`j&xOlUnu8<-ckJ8SA#p({@)44aZ)Ntx2vMUsDi$@5&e%LKnZ09!YKAX1=H% zF~O2F|5Tc#5ViaSEg?J+K_|GAR<_%TN_ml;uaS${oS=M=?kvZd9!D&hjw9-DlI;bK ze=%o72|ObO!3O=#Uy80zZLf0?Z>ajf9&LL=Om*md`AgB&*8v4A_d3FI_ zYkirua#2FC7B(b!iHEZEgzt5jSec)G;N9V2(69d2&K9!jc!oCjzg#IOp7ZL7u8@g; zgNrt)MHy}Qu%^~=T~K0s8h_ynxf}azd|OqD8|Efg>yOyEoZ~U-{)e$&FE>PSOH%&`jiQ^s<`>ZJDoP8CcP_vpGXHHF&BYs z8T=O(U5lNa>EQ-SN|)}o&&=o;ll7OhWTIFT{F*ro$Ya7@YEAO(VgvV%G+zsMgxQ9! zN(THS(E1atO=K9|pVVSMsm<@aS7#!e!gYu9W1=wcBZCL}#{p)ulF1_UP;pGHL!EhY z)7fA1RJknJa>bUK12?6?BGpzHY`UMNr+wsf^JbmY-CMo6oaE|QxKoOGm{SXL0)u`~ z&hov%M{u7VhFK(LG$!A^i&9U?c3??3?TCn;dA+X+LvI{Aje-9jZoKGPuU#D&d)xSN z-C5xK;{Gd3v_Rm=W(NV))oUHHpoQ|;!dZrNiqqp2bQwusG zESYj)|IQn)*o|D>*XF%c4y;luPldIp)f!X5e6eOYY;_JGBJjo^l3eW^PBO#r?ht-8 z=SRHzv}X+BvtCAHX^_CGI2`#M=fr*iB%BPX15qWtN*+`SA}fnwjDv*5yfVq54x61R z*6#{VWF$=_!@U|h{`$+kq=1H?$M|mibYAegh|eYH=~wS@Bc$YYZWXL>C8X+sWr(kM81hx@6r}x3gv;8_9JVdld)rglX_i2zlJBKoZGpNQkmj}}oL%c?{d1UsdoJ3db}Nl!n|Bm|B*-`y`wags@rf?HqQ9#O95F%{7~69M9y8E z8vTS(z_kD$wetrSw+M6&=3v?&(yE0OA2x=hj(Gw_(kk|!zk(SZ5z2%jmh*#}5H39` z`y9|$s`okzweO;=ukjpA2I~bdhUms(kc8C(g&aDA5T+++Kuo>5cR-o_d#>p?SABr`F%QBqTO+<9( z;Yx)u6dwv^6W=Lh0hpDFL5o zWa1Pa`S?*=jPUi^@=B#_G2HEpnRT}=;o<&M_C^`;#;}+Z^N$t@+^e3cIBFAQBl3$u zcR5&Fm)CU#mj}P+IK`LfQ`kip;_%!Q|8Lmm&eB?iaqT^K4cK#{Q%`i3aSa7>Ce6}4 z1S2Q4bUM_xTPQJ-en=~$ty(r&M3el%p_c|+lO%`&@8JULR50Ncvg~w@TCT403w59) zH!3zmAP!lVU`vVX73oI_;ExV5UE})5cR6OppYcB0{DBS{3{(PDBor7e)yVRe`k5cg zg}%ixd@G~D`!PuS9Q&of*iG)+bn}qiyqX`Ul)q7@;QNT=DQ>=BhG})Hs+3N*Pr)A) zSHv%jPZ08XkDau9{va<-b#qMckgfEXsYm9CS!4o#7?efu=WV6lVstvd?Le zNZ0s8hB72RI`vddbx!t#FWoNGrO;6*bz~PE^r13wQ%T()^l@0p6RbDyZgPKfnP@KS z5%owszK5MLm8aFGrMAZgD?)p`TrQa*GTg>}8{}bV?xoKW_UI*fPdgbSYK07L06>f^iEQF0U3DWP8RiI#PYGP;8mhRCz z@KK_-pDKdXn4^`SoiSFiy{&vvakv@^zk5#9cep#>#)A=?eD#%Nz}EIn-Fv0)6{$Xq z{RLu-Jamih&Ncz>>et;xazy8*Cb4SkP~H!-pNMBDFfASJd+gW%q{Ykyy3I0-6_tbX zFASTyP%qiKhM~j5lOs5Ec|dW{Y`igfUa-J+|f*03XNB0uoGW$+%7Q47# zrnQK`Vhr{Q7;z!6Y8{x@n$d*|ht`fksIi_LvlX5Q1kq%X`RT+(t0qbV>UuOY+=7Ks zbGk0+jg*q`@%IbGX+YqaD#r){ViI&JRs7u{6T&WS-9h8sO+j$`H_ap)IwLF>MVTZ7 zoiD%|&YMklw`$MXGoEUWw~}Jk+eX-moj0=u2gYsF#i+LO4r6n8TGgH!ISQ#}(lxhv zkj&-eln{se=J5*L1>x1CMYe4p^?>l${PUiPyjRF1@@7#k(?A!;fv>z=zxiz&p*9?A zI*{V|S}p6zf?$ulu2%tioZ!=Io;>=i9Jh~qlba~&Vgyh+I@fP0yL8JNyRRGiGJx=w zGW~Wnhrq^beggMCUY8HNvM#i0E?<6lY1DsDQd#$3aEl4vxm)t=CYAp(Hkdt&V%wdH zw#>Fhc0J#4z78PTZ#JNtV-2B`Om+5v7w`G|(hbuEU~|jVqw($i`ad+V7s)#rRo05F ze;4J~@zg46I&ABw!wUxIrb1c(SBd1rh9H?HuL|29{)3EVu5Z*c)Oi3}!%_Voe6>>A zg(w9%B@*Gu3uLjBWhZ?V5U}o=4mZ}nSP%H{n<9AuUDi{vX|8G0JvmO#^2CAdxu_1J zy6j*}SY{^Aha5e>MR+ug=ru_YJ5JO&qZ~oUrX~Ph^RhPjwH;gUaRD?mHD7Vu-2(+R zWy1gb=oIVei;c_=g;j?779#@kj&o8m%@CjaY*!;Zqhbu?ukG@%kHR@4VLjl6^#Hsg zOtdLo1tWj78HAKbKr}f%S^b4;8sSe*e+Vs_V3VvzvcX8IU0zx_@@Fn~EnY6*{X&eLEa@QfUGly||~Cfo&>X z_;%AYHwlV{68~{2{Y4*MrT5l)v#E$E>|%rFF!9ASK&-KIQhBe_Soc=__CB?K=B?|V zGVXX6J*F>QtI;y`&gf{kYh1sl=xU~GmHoJ~JFpUshenX==Et_(>Vbh!gPFi%(mm4vbpLjm1XnXmod_RI%j+e`UGZlG;Qe5}@|XTTsDy1x2r|(I zzMT1dRchh^U0>zYfjG@R{go8ja6AAO@Hh%23k_0|KORes*Gg<~Yc28hb4tna{*{lN z-_#FR3h6Q>9EI0r%y&DDR}?QZsCSCt=dqTKzvK{^xZl)z0*<|lS*50lz$qaA_^?BkO z#W_6nJmBNf`hg%YW~-xBqM8lq%U(OOq@y1cDWhjYTKMHI^qD~6)OUL3K$TEsd`fhO z_IFKx0Ljvs4mWxROEzD^sr9US$9#9Q7Rs5S=^7!LK+CU*a~B@_1XL)P4s(AcsZ35t zlX%n5WlV!3=FLiDQL#>p*jHax2C{u%LcK_bfqs?C1M4?na=PP=RUvgwUj6$n2)jnq z#)cH;)-cfi@oeGZ&3aGnYrgdjT`dg>$qbBWAO2=uV(1ih6>dzyl@no^?B}drbiP)C z(DUtxpYm&drn40sFf&>TBz>ZnQ2Cn~+)caRrJiMPfH*WVc|$dRrCpB{`(fEIbiz;g zGOSE)Xr6-@m5K0m)7;-`bJ;%DBif~b?~H|AUld*3+6Nxck!qm~(C0g06JQNQIXAOm z%BT@B?xsD9d&S%B!9#IP`XWV|v_~B^i48Y#rq!(gf>&~odWYEB$1X^ps9n=wW=gW; zok~L30Pr!a+j|dHn7li!V1Lgs^6NcF2)EJRx1L} z>@o3@X;;J3g6O*TFstT)!OP8m`cUS6K$h^o->eZe%)MJF8!<}rqdX!a5?>_ zhsoX;&8M7{pBr2W3s-;p%IXq>9+)78!wd0N@-V?8~0H8-Ix{q53J!h>3qNPcJ~<8AfJ{?Apz1RJY?73W0h5c zyr~Q8&2;TS#Wb|kNExDEWPn| zKKbL#jcbn*t#_KCw(9aDrx^Kc{*ZD*oqG}%F~8DF=Sr^FbO6~+6oyAMqQ;w?gq$!3 z3V?r-oi)u;U5L1U4Sm<}X+A{5@JJMG>J`;=_xVwNJ^ds?(NJiPEswm6_M4Y<#wC=CYVI>)%kHqI5Lo9nKIQ{U&lelM%1|f_I z2%OKf((v#LS^WyA%gl(nBf=eOeNdRXn~WGaMW=d7J4{XD_dIuXI{zV!1P5y^~Jdp=jyFe}uJf0;`@WCB2-gz-Y^^ z_jgT6F^o71q~IeL>C0@G;nO@tmTj$Szb#4Dfj~6w zbd`I{wd2qe5U(^=1?N6v|BAtAb-OKg5Y)qzRJJVqL4cH3oxF&NqY@v>)#UJiphe{^6$IPpToh{|ITcEp0 zbmN@Vt`Vv+x%Is`;^Hj}AINMdTbJZ`62>x*^qI4KV80NlK!3z99H_|%+qnESd%zWS zC~a*TN};u>9K)$Vl=H4vLDcE3fs*bUkXGoLiy$W@O-e=zYn)02VD{NzaNyGt?v6NT zZ=sgjIKDv)hkEQbLfMaB{^4ke8q>a|IV_a1IM0ZF`ahdJ2|?BC3UTsR*5U0^jarqX z;d;wh_hixDptb$$;U6Go8R>;-7;zaIw`tNbTy;_WGl4k5%IFUEOI+!M@_pztHxBFr$LHsD!`-&0wvw?U>1Kb zDT|jn%2o8c4RR-DLQLM#m~+Phh=v&NV8xnd`iraXtF(51sTE+w81bVSHQN5>z&g>A zh6701SvZ*Vsj?^OlPc-g7}BfcKDm@jb+MX1G-F?GAKIzBzkO0+7~ZCiW?xd>8pVrQ z_t{Z#537Mt)p>&q=xqiO@-N;R$Nzq61}Y%lo@I z)uO!;Or6=wE~6VKq2MkcEPVS!v&MN|AL;B8;|&g(Pl;Lio+$;b*)e22K4yDlNIW<1`^DdgBtBrj+;FgJ!z8PfM! z*{!y1WzBf!Pp+QV2iWiLF1g1Hx3UKdgQOH( zCvklov?Y0rd@PDbq&)g*A2voNw_ccktJ$-+ozft^>PX)j;PDga3Hv?HulkWu6+vM_DdnC7V8_)$4oy}%(J;iTi3=t zvIvAzi{&jr;fFE?QGNK#+LYwFDiB$zF8b?Mg;j^vskJ}u*MWyUPcFL;Da&GD64HUp zpcY%2F934ph-OTRBeh^2$04ngqyjOrMs-B`n;F%u)!O4Kt|rUC_wK7E4R@vKU%t6Q zeoWX-iO5fU1giX79LP#4Eo*V_&LRW!Ki?;{)!m3bm+kVW*DxKJjm}BBQyMYwQcTV#Un-UuHx0A%Y5y zK4gH;Es}j^?10qKmPemEOwXORD?`?8E*efsz?-9qZ?yV61 zAT_V{Vv~8*Ojz1B^C?d6o7gsN?fB#gTf_-asZXS`@Qi&x#{IR+43e36yX9gED&};r z^RTbq;c5j%!4XoOy-M7Xc8JPCp_PETfzep$R{^C4^20RYrXNc0d8P*7QsJXx8^4|Y zFysefdefbBX71PGC}WQ`z~(W|odmm@-f_X$z5B4MR#RoCj<&VY%Qalyprrju@cQ@> zSYug}RF`ik=$v%#FU&J0`Y{)Jv=$9_F3*KXoPR$LyZ91AJgXoZz(?*sq@mZC%F3qL zx1C5ku_gOSKvZ5B(UkgS$$+epZ4>^q%S8OE(7L^e)60!!oZ)l?wNBIqJBeY|S1)5# z=MS(H^`i|X_4Cad>%rTGZDY6-2|S7AGy*2`IVfOIce5<+%dzKX1iZtY;X+E z+vin5;6RK5nJ*a_%k$KbGFk@L%|2&|UTSyaBtN-dQqRUfE7K3p|m* z{jju?>AF_9v-ffNNa?`ZlD=*KJy3rx$#57*@+*RNUioCmcJ6!6u<)@4^5lBSywN^S zDXKeObAAK*Gp&x6wb`b?wKf@aJQ3Z-bd2wpPT)YcNP%Je?AxBSawW)34lmm|KaB72 zKIQJ9SifnCJBKl2;qE>NH}v6;H(nl>7VwS7A$~9MK^?TVlrt=%=2)Fu4WK$t);GQy zgpeR-q+dtwnMs(B;FjL~-~)yxwUwk1ejBqYh2K=O!na3m_catF|9WrQI77`I|FC znJVlvA*DV0PO#mZBd*B+X+s35R1F)iUJ}f+ta7PJ$rLoUyVyFt2I5X?Lzjb!w`>R7 zgzhE_H^^QZ2`*t5N+G~48nb1o0J4zw7;7k&UF?DNM#*X;jk$>isVuyG{l@MRLe6&Q z!x_bh zo=O%fkJFC4k!gZ*_Oe%Ri%wARxIAl^vNtlXsD38o!fD0-B9U_r5el5}D8ACGb&|7? zUTBwQ^&nhAq*&j*nC9M(tUN1Z;tI6(PHDV0rrB^Po68h*y-z20-Lwl;%ilx{K{Cgy z-uohv@FjrLxaHhQ2y{p2jDWzOTwt|F>gx5>FLB-nB#i$=()6HMdRgfe-f@0+w^YD| zp&04!p4*t+bYkS2+^=FE7+bz-MntweO*@m5ixah<$zjdbP|SF(KF)R3v7aS;y}k7G zn;Q`xpob;z@G@n27zG*YK5sMe0+-`F3pH3!Dv@>`kqBrK7-8viQ1(Qz;$8}uanSrD zd*I#?La5yMd6*>4x&t2>^5(P6da`kjabk%&&WkcEXcY3tcd14t^{PDujHj><6du+& z)+E*=W>j5I4k@J0*0EXFi^sD|r40v6z1liIE35C6t#8{-WPh?D-K@q1Sx+6wZ?dq= z7*f+P3vB|-CvZDD5(P)-VqRnCCt7w+OvH=GNEj^lbz22YZbS@xG$i^s(jtSUZ zNX2Dqui47u-VSj)u5%ZRmcKT`&ogkaE>AH#;-1chk?>ZodxyvnRLdlvfcGD#jo09c;BVmuOq-bgwY1p)nPxk!%rYG(R5M zl0Mt+^Qm3X`$9@r?agv(egf*0BS|+o+q3rAhC1UyYAmGKO^w7`c67N~x31|IMLQ z+o{LF)W0LSmy<}dh)B*nw*H<5vMN)Ty0b;jru@3!-rK!t+}QHlm$~JHj-!LQbG)_C z-u^`JBqDK*^CF@H8t_K${a~m6@dw?cI8DQ^!6?RIottv?QRxl%`dEgfc4kq({0V5q zAzR)!s;?x9>6l+O7{Ax3KcuNGkq(SopYi>F<58KjDV1q zna=7ur1CWRJFw0oD1=UmG5yXlXZU2YUAV;~U-@lpWf2(>Po4yvJhCU@kaxJpo?dCy zN;}FA$YW3tNlO1Mn!Tkb&rMgs01MK$8`wQ1^*3q+Nmn>gX_ zbF7#U4L{+wo&&&7Vo1OMk#c#eUWXuGP77iRMW- zsM$`!lvXx`UKZIDPWdF@hwWLFDHOYM3ZAiTEUOe*^IeBDm&y1JN550K;iP|Ga2zaIpUMh7Sbi6L^flL15S;493q7 zd3aRwKlefez>r56oDa(P7=ywfy#KWq@85>OASi^7FA;Mekr9PY0LGsP-bWNv1%n?Q zCjjOX;QLPu3=-f6Lmy#aetszLe_|khhyV;+)3lF>ga|y22h0nF!yg#~gLxs4$6P?c z0^mn+gTYW<_@fxXU^xF{M?t($$OF^=P?jiih)4(gMGP;TANH7NUV(>wk0OCUV0@1g z_kh74M+||2|4I_%!Lk2x0{A!iAP5}xm_iUl0L1^-fdcTq4;0|#f0)YuQ3()%2d@9Z z_#pp*0S{Xs0)Iyg5fFeqHVg&B;g5|#c^}L?G6Lo0`)`W>H@JuF{D16)^8#R+@4djko9?0ZK#%kJ(1?&nl@8(q zL--yQ-vb8adu)Uc4Ci~y-~-0{pTRxw&&SLAw*o-m@c&%+unzhFKBAfr3jM3X`JizA zznp%c;V)w^PBM;sF zS8>7M;QuMEf7cca4*M&R2T^{gg@5|*|0qA4|Dhcp(FNy!5XQeS{=cdp&d>kfivGWC z_aG^Mwc>+(!~R{sz<-Y%0p17ke`G}9p)em8&4bSTB|Z-r=y7`rJgDrW)crGE9#uaG z41k~lk0lfQ&`*yIKVUHae|!C3PXB{J9vKFM_@R$g^kF#hJ?~IJt{&l7{dFwg8#w( zo_r8K=p)tpXBs}fK|EmmypP!e0}uCrM|lT>`TpwTf3U|I@PI+!e>u(1|JPUt!$5q0 zt%Lnnm;A&3|I+_3Q6J|R{LprPdHv8$|4ZS2Gx#7#f3X06m}37~)Zl-v4*$oQf93xH zgg(~le=y!ha{GY69%}%Y7sU5iF&{7i-bZZ=en=eTv4gx|0P@$3hxcK?JofrQsRbUj zBAAz#AO6?6zo+Lz4gNJF9>Print type schemes of toplevel definitions as they are inferred. + >Print the time it took to infer type schemes of + toplevel definitions. + >Do not generate the file. >Do not generate the file. diff --git a/src/Infer.ml b/src/Infer.ml index 131c581..3370a4d 100644 --- a/src/Infer.ml +++ b/src/Infer.ml @@ -9,6 +9,7 @@ let annotating_fun = ref true let annotating_letin = ref false let inform_toplevel = ref false +let time_toplevel = ref false let merge_rec_nonrec = ref true open Defs @@ -744,6 +745,8 @@ let prepare_scheme phi res = VarSet.union vs rvs, phi let infer_prog solver prog = + let ntime = ref (Sys.time ()) in + let start_time = !ntime in let gamma = ref [] in let update_new_ex_types q new_ex_types sb sb_chi = let more_items = ref [] in @@ -851,6 +854,11 @@ let infer_prog solver prog = if !inform_toplevel then Format.printf "@[<2>val@ %s :@ %a@]@\n%!" x pr_typscheme typ_sch; + if !inform_toplevel && !time_toplevel + then ( + let time = Sys.time () in + Format.printf "(t=%.3fs)@\n" (time -. !ntime); + ntime := time); (match pat_loc with | Some lc -> ex_items @ @@ -931,6 +939,11 @@ let infer_prog solver prog = if !inform_toplevel then Format.printf "@[<2>val@ %s :@ %a@]@\n%!" x pr_typscheme typ_sch; + if !inform_toplevel && !time_toplevel + then ( + let time = Sys.time () in + Format.printf "(t=%.3fs)@\n" (time -. !ntime); + ntime := time); x, typ_sch else fun (x, res) -> let res = subst_typ exsb res in @@ -970,12 +983,19 @@ let infer_prog solver prog = if !inform_toplevel then Format.printf "@[<2>val@ %s :@ %a@]@\n%!" x pr_typscheme typ_sch; + if !inform_toplevel && !time_toplevel + then ( + let time = Sys.time () in + Format.printf "(t=%.3fs)@\n" (time -. !ntime); + ntime := time); x, typ_sch in let typ_schs = List.map typ_sch_ex env in gamma := typ_schs @ !gamma; ex_items @ List.rev !more_items @ [ILetVal (docu, p, e, top_sch, typ_schs, tests, elim_extypes, loc)] ) prog in + if !time_toplevel + then Format.printf "@\nTotal time %.3fs@\n" (Sys.time () -. start_time); List.rev !gamma, items diff --git a/src/Infer.mli b/src/Infer.mli index 6a7f022..43df001 100644 --- a/src/Infer.mli +++ b/src/Infer.mli @@ -9,6 +9,7 @@ val annotating_fun : bool ref val annotating_letin : bool ref val inform_toplevel : bool ref +val time_toplevel : bool ref (** Each disjunct stores a trigger to be called when other disjuncts are eliminated during normalization-simplification. *) diff --git a/src/InvarGenT.ml b/src/InvarGenT.ml index b8fd864..eff45f9 100644 --- a/src/InvarGenT.ml +++ b/src/InvarGenT.ml @@ -73,6 +73,8 @@ let main () = let cli = [ "-inform", Arg.Set Infer.inform_toplevel, "Print type schemes of toplevel definitions as they are inferred"; + "-time", Arg.Set Infer.time_toplevel, + "Print the time it took to infer type schemes of toplevel definitions"; "-no_sig", Arg.Clear do_sig, "Do not generate the `.gadti` file"; "-no_ml", Arg.Clear do_ml,