From 69176aef2b0b24a1d63f036083498157667475ea Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Tue, 24 Sep 2024 11:56:08 +0200 Subject: [PATCH] add summary & traits/wrappers --- beamer/lc-beamer/example.tex | 107 +++++++++++++++++++------ beamer/lc-beamer/solution-traits.dot | 15 ++++ beamer/lc-beamer/solution-traits.png | Bin 0 -> 9614 bytes beamer/lc-beamer/solution-wrappers.dot | 15 ++++ beamer/lc-beamer/solution-wrappers.png | Bin 0 -> 8738 bytes 5 files changed, 113 insertions(+), 24 deletions(-) create mode 100644 beamer/lc-beamer/solution-traits.dot create mode 100644 beamer/lc-beamer/solution-traits.png create mode 100644 beamer/lc-beamer/solution-wrappers.dot create mode 100644 beamer/lc-beamer/solution-wrappers.png diff --git a/beamer/lc-beamer/example.tex b/beamer/lc-beamer/example.tex index f1dfc9c..463277e 100644 --- a/beamer/lc-beamer/example.tex +++ b/beamer/lc-beamer/example.tex @@ -255,19 +255,41 @@ image-write "out.png" im3 \begin{frame}{Solutions (I): Traits / Typeclasses / Interfaces} +\centering + \includegraphics[width=0.5\textwidth]{solution-traits.png} + \vskip1cm \begin{itemize} - \item todo + \item \texttt{impl Angle for Degrees \{ \dots \}} + \item \texttt{impl Angle for Turns \{ \dots \}} + \item \texttt{impl Angle for Radians \{ \dots \}} \end{itemize} \end{frame} \begin{frame}{Solutions (II): Wrapper structs / newtype} +\centering + \includegraphics[width=0.5\textwidth]{solution-wrappers.png} + + \vskip1cm \begin{itemize} - \item todo + \item \texttt{struct Degrees\{ value: f32 \}} + \item \texttt{struct Turns\{ value: f32 \}} + \item \texttt{struct Radians\{ value: f32 \}} \end{itemize} \end{frame} +\begin{frame}{Solutions (II): Wrapper structs / newtype} +\centering + \includegraphics[width=0.5\textwidth]{solution-wrappers.png} + + \vskip1cm + \begin{itemize} + \item \texttt{struct Degrees\{ value: T \}} + \item \texttt{struct Turns\{ value: T \}} + \item \texttt{struct Radians\{ value: T \}} + \end{itemize} +\end{frame} \begin{frame}{Coercions: (In-)Coherence with Transitivity} \begin{itemize} @@ -461,6 +483,22 @@ $$\\$$ + +\begin{frame}{Typing} +\begin{definition}[Typing Relation] +\begin{mathpar} + \inferrule[T-App]{ + \Gamma \vdash \metavariable{f} : \metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau}\\ + \Gamma \vdash \metavariable{a} : \metavariable{\sigma'}\\ + \Gamma \vdash \metavariable{\sigma'} \leadsto \metavariable{\sigma} + }{ + \Gamma \vdash (\metavariable{f} \quad \metavariable{a}) : \metavariable{\tau} + } +\end{mathpar} +\end{definition} +\end{frame} + + \begin{frame}{Morphism Graph} \begin{definition}[Morphism Paths] @@ -607,24 +645,6 @@ Then .. \end{frame} - - -\begin{frame}{Typing} -\begin{definition}[Typing Relation] -\begin{mathpar} - \inferrule[T-App]{ - \Gamma \vdash \metavariable{f} : \metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau}\\ - \Gamma \vdash \metavariable{a} : \metavariable{\sigma'}\\ - \Gamma \vdash \metavariable{\sigma'} \leadsto \metavariable{\sigma} - }{ - \Gamma \vdash (\metavariable{f} \quad \metavariable{a}) : \metavariable{\tau} - } -\end{mathpar} -\end{definition} -\end{frame} - - - \begin{frame}{Translation} \begin{definition}[Expression Translation] Translates a type-derivation tree into a fully expanded expression @@ -693,13 +713,52 @@ D :: \Gamma \vdash \metavariable{e} : \metavariable{\tau}\\ \end{frame} - - \begin{frame}[t, fragile]{Summary} -%\begin{tabular*}[h]{p{0.5\textwidth}|p{0.5\textwidth}} -%\end{tabular*} +\begin{tabular*}{\textwidth}{p{0.5\textwidth}|p{0.5\textwidth}} + \textbf{Problem} + \small + \begin{itemize} + \item fixed memory representation derived from type + (loss of low level control) + + \item weak type interpretations + (loss of safety) + \end{itemize} + + & + + \textbf{Goal} + \small + \begin{itemize} + \item handle data transformations in type-safe way + \item allow low-level optimizations + with strong, unambiguous types + \end{itemize} + + \\ + + \hline + + \textbf{Ladder-Types} + \small + \begin{itemize} + \item connect low-level representation \& + high-level concept via structure of type terms + \end{itemize} + + & + + \textbf{Result} + \small + \begin{itemize} + \item extended SystemF with ladder types \& morphisms + \item formalized in Coq + \item proved basic lemmas about correctness of translation + \end{itemize} + +\end{tabular*} \end{frame} diff --git a/beamer/lc-beamer/solution-traits.dot b/beamer/lc-beamer/solution-traits.dot new file mode 100644 index 0000000..34e9b8d --- /dev/null +++ b/beamer/lc-beamer/solution-traits.dot @@ -0,0 +1,15 @@ + +digraph SeaOfTypes { + + Degrees [label="Degrees", fontsize=20, shape=plaintext]; + Turns [label="Turns", fontsize=20, shape=plaintext]; + Radians [label="Radians", fontsize=20, shape=plaintext]; + + Angle [label="Angle", fontsize=24, shape=plaintext, color=brown]; + + Angle -> Degrees + Angle -> Turns + Angle -> Radians +} + + diff --git a/beamer/lc-beamer/solution-traits.png b/beamer/lc-beamer/solution-traits.png new file mode 100644 index 0000000000000000000000000000000000000000..42d6483fb8f0a645493da970a25824df67e84d28 GIT binary patch literal 9614 zcmbt)byQSu)b#*L#{d%2-L29&AOa#F-6$;}?T`{minNMI35bA7BO#@LA|MJ<(p{26 z$k6ZM_x}B@^{wx_uB9$!xc7O^bIv|{?{j1IbZ(FlGY}&X2r^9#HGKpErwIO^L5K@~ z*J-|FgMaXCZ{AQtoSpx9-Bg&0K(HY+)l>}qGuJ2XDN_%RBBoO#kQY?Y7gUt(Q*WV> z$a3N*CHH9tTvkyQw<$jkM7op_my`_E44IebS%0u~xNSH-%t!pEl7ufNjE{~h>^p~r z#`cNyR8|HLJsA}b`{s_Tw2$NBEuH`wnWZ13ksWjF2t*REVI>{{5tfS|OMzhXW5eJe z=E=Df5npG_P)U#1GskZjIpS&`%8w)YR1Xt}Tv2lCYo8rl;z2|GVnmR99aW6pR~qji3)c|3pw!wB_MZO?bG{LGB%f-XP zrp_~WtK-M#&#ymyIy8#b(bi@Xw~g2`e*5P zB!YYA%@%h=n(LW5$%2xKJ6tlrx}Q&ZE=&(F?o z4l~zr>(;H34)i1SQ0yKYH6Ve53pDyHxqfspFgI)K~I#q6orLLIucoT%3PeCKbOcb#19P& zaFyS6b$y?m%`*9~VY8Xq^k{9QO5E<-mK5(rff$WoH_5S|Kgr7`nu2OSkN*3I&SMYw zw`SH?Moy~K+d+Ul^tizy{x%$$r(YaLC;F`$PC-US#-lRFq5B2p3RVB$;2s8}Lg*!( zd3+oken><_L`FtN$ZlZJzqdL}@?o&QKQ1fva(r1Vqz*0uF=P> zs!YYj#r}7HX37u~6St22%vQ*VQ4wk3J6fe_phzFc~RilGjJ&e3=a?cVYlw?{+g=4 zkXH^j{H1gjygq4YWE4q4LqmhXP3)Kx^>BCJ*x2~ijgOCCHo8=FJKs9U66aTr5^u`d z?n*y@nVz+E!m6R6VN4JqTR$77vtf64*XdWbnYp>ntE-y+>u_YTjXOLhUNL)B)lE%V zrW<~;BvBo~Uw;n`@fe@Heamyc9CM{60p-$ZUt??Q)6vZ585tIOdeh6x(x%ai9xUhw z51QUFWc1Mb{c>?}Y4Wd8DrKQnX(`KvUA-EI|zRq}3QBfgL7By~^x8uLuL0(xK9UVaN*UIw|moLWZhFCTFSJc!D z4Gvxt6VvnUDK8hZva)KFud8*i{^ZNw?0sHZ4d`_$(<2D(`dBUXKEb8##(*8DawN*Z z!J)6Oua$;@k&cKRGynMa^yH|isVP1_J~lSi+S;0hg~iy|7-AK#F6T8HQBxy{;^X0Q zgq*AOm~!{<*!=r9aCf=SqvZrj+E`yduekVNwXB7Fs2fMZE=D9C@3)%2N9(*eCtrNILs;e@MvogU9k}b<(r-3CF<~Y|>vdcB?BgfgS~p6? ztN)h!I4LRaT)A>ZkdKePx|ZfUxibc5`{6OB;~bKVOC+vbG0@isRPpxnJKGz!fpUQK zSJie}k&1uf=;-(&EiElG6G9}9UNeRMg8%rgz5VV+!zPQY?=oz5%Tnt=ZRW&BLILqx z-NXdo6OP1a{9Y%bk+>QgW@uMo3c(;`pCu1OG%9EWE5C#1&P3kpf1AumM6Uy&l~Q6+ zn}Eti>WVL!n3zO61Fueo22qA9#gEXRIoMgEq@-+JAjO|6%n5n4$U<)^_KrkjXk;W{>1WpJ zaM=_98Z@wqii(nw`vXO{VT*vIRu#69xw-5k;*VzV|F=i8{vSGZc*uDha^Cn8a%~g$_*0)hUZ=EwM{e@Q?e-M(9(X5&=;n7~ctSN6`>CM2vAbEe(-pNVoswlCB z(s}RIH!xskVglePwP`u+yTO{w{PT5Re?PQ{48@0m&_c)SeV|2tPasSprD9bk%zgFh zRajUU>@PYZ;t~zb!Qo*Fb01rOZ||R$&`>R{F33M-X67=h26ePrn069&o;k52E-|sT zs_N)h=xJ(JR#WI%$n2M=ZMqs78u#uMzklzltgLKmN`FS(6K)ya&O6Ma6vBi=B3W3P zy%)Lwwxy(`Dmhc6nVGW&1_tKm=g&LN$cRe6uA<6pszF_@6ZBFWo1Ev*KiYL9;EeyV zLPthKK-;gYt5g2pFWnd%9E9KcO4iiaC=Z8Q$;lC3TDlQS%?st-|NHma`g)m7iw;`t z&a(1ss;HW3;#XS-C#P-;RbBdxJs)rHSCaS5O-)U2+#ndC49`Wx>LvhyHtqbBoB8jm zudf#o5wX9)MdSP6fo`^ZY(@wgjfS#iljC6Xf*9bsFUv?vU%hq>`WPKUV5?_Y4nXlh zu|e*N)SAjH z4MXN+DMGiutPpz2B()1i&`GW}I%BOwKoIRW89?wVq>YBF`R@D5%HLB{p@Z*?pt!m^ zJH5QUIpjFfa|;Xo{tocxt@!OM-m2upeN0Ltjt95fQJo-+r@+_nK##D>az29$&ii)6tF3rzN%gUxOCzCQN1Ok{9rlzLq zW=iASYMHq}HMP|@JY4Iuq{GY0OB|V!lhbm4Oj0&W2d&qJv$0oIRrUDoR5?zp$4fq8 z;jF9oe%IU|%gfIPgeWN~=}d4orF1@=`1BxdE#|WYWW|oB>aURzGZmHG*RSu)eT%=! z5Wn_1ig$d~$<>wQmXaBOe+>;CT~J`4`i=8zs`=qqSJ#uZm?)Wt4^OT*{p8~2p2?_j zw6{-Urlcp-2(BcS+O@Q_g!tv=O0|2IO#!z$J~?S?ZIzXi>r5bwA)w09{^Ylr-Ov!^ z>+7qnt*x#eRZze^LfOd-cii3e9pA00tp%%UhwCK_~fbdLV51OIJ!usVdr%)wn7DXFPb-d7P_JK6QawU_nZ*H3a0hxexUuVS>CD@lxVW3pxuD|C;B=orX#u+fO8N5TOJ!9Lf40CA zI2U<&`8Sk*siMqNv1P?#HxOfFJHFt$qfen+K=)4@yC{_CA z%>{kMX*S!ouh^&vT_lM1^7g`Te_? zloSBfR7>cYUXC+<2k>;DiAdDyPzk4a<6R=E95uN3`1sf&_%3yU z77CEJ1_j1aN=8IC6h{>JbV5ey4}C^v5qr-eIuii(o!C|&og*$t4J$vB(mJfl&+|%O7*t`DH`3D zt`vGY*%Sna*GZ!6 z4Gp=Z8fS3urSJ{>{PuwyV>U14CAH14MbL^`lbR(?FD^Q|xoIC47Zue(NWTaE0qpru zQc`Rvki3UPxk(ybYZk(@DO=Fc z8I%r}IlbqSS(bj~=xS@XpNSsq?d`2kHd*YdX>3JJ7jC@P)Y78DtQYjJ0Oe>oJ3Z2i z;_B(@>VjutDhmo6%*-y=V>DuihKz6C?Edym{dAEfT&v(+Q4t(O`m0yu58c{`sX-2dcox$VeQCD(t5dwbn*U|F#7=3^J?CCBd_P9Dxw*Oh zSN{95va+StOZq%b(SJ=UtL^Xfw0I1 z-0hOb7RwRR3Y+^LV=>LmiV;Zn*4=;q1o-&_{Qb3a6eqg7yC)`^rd(;}$3ay9u20v? zpUiqn19}dF6A*mh4KU#0A^P|WoBN!0uAWY|{J~5#YYO9=wMXsyHLwZ@sf=o5WONS=)X%>B z8x+j4TpPwx9+S_Mg|@jxMK`-eTY?A8i6f!K$c7waU%!4`Y*47hhfhL660B<*8X6j* z=jmCl9H|;jo+absxU<*;dNlPmUcIIY9PzDNWQUtUR|B@^mzSL*^mKJ~?d9N6{u}c++bav@=HW@Wd?kv{?f(6f>BkgE)MnGZwY@!8=n1nN z+Oj$Lvb#6tALQ4QCr^+lXfwhB0ziS~d=^P7YCe9vcIAo>Fb5#8&CSjH{QQ83DJ1wx zisxVtJc@(ZrqMsQpy2C*H%L0DBM;yL%Z)v%0T`CWAL*QWKNq|cndRP=mL?!y$@#gv zx~`5fT_lb7XgknF;BBJR&iS(}L7)MbQahhHYlP+0)=F8|1s`npvOWa60|-FdV(w;2)=!Yg zv(wXI$S3jfUnd?ZyIf{uJUTdtrx%|kTeSd>>)=3Bf@6yUO4mQPrsl=CMifr0u9I1% zeJ7nwaNpQiMp6>n7T-;gw2bWR5U6(W0X^$2@$m3iS#tm<92^!x{ETdDLa|#jakg1o{5```lYBq{)+$){VWJK2}}b z-C(oW+`fI=!lHY@8$h#AJ6*!*XQs)-NJ~S5oVYj!>K}YKP+b6|By=Kcet*=k_C$uu zfB$|0s}i6J?rCS24_|ovxb56(^pUu}`J|fqP?9;qpQ80K<1zRJqLw}V{i!XD)zt&v zzC~#jh*;DJDg1YFa6Hl}T>bkOtO-qjB}jQtB3BuNfmSIfoUa)4&EetUSgl9L(b;~> zS&zNM`}glAA~e; zb&y=(!L&9A2n#byxig`Fuz(S;0*n%fHIxh|i~ldBI(ARm3+M;yqt}iF*~P@R5|vKt zd{^|{+}5Cz7a9I-Io%Tt@A~b7;?Bm7j*WSJglwUTggo;9;RmeY_&KPgaHPJT-uE9r z=0%+((yua*vHPz55uZ6U_42CtoC_%siv-pA3Zh+GyASy#YTbwhUj(QI2PT#=)^yKI z=*7Et0?)M`9%IEr7pk0o%~Cvx*}tXLD2bumDq;GZ>I7qEFILF(?bbb5r9E@Us8zMMtDUw&Z9;$uLp=(f z#I$!fR)H|1M1i(JVx=+u@{Eib;F3Rk@nV~fMGj5MZtvnU3dd+O2~IQEKr@#N%+0lq zi7Dv^7cf~u;oAcPh7rBsARUkZC0$=%r$n`!{L9#KO^%`#z_fSFVPd|aO-$%SU}&I1 zC?hLNZ1QbFy{4u{jVP`AtBpXoBxlqT)f0_iKyKC$EISa*E>#pNrk&TAYj)^tE>Q`I zvitUwveeDa4#pXwIAHHZMqW2CpuWw*$S9bJMWTTD$ek@(ikPUX;;~n|PsrvaEo;%f zOlzCNw6?W5T*Z8>t`6SrQzPs~FX@_pMLmBuEFhk4N zr%_~#_%E<53V~dD3DMaPe0@RQ98S>G^ZN3Y4svH7jSLP(B0+lBgG59*Z;aQsKA#HO zREW?6j~$Jc6sdo(Y8((CgDRSGbv|6DoQ4R8o*p;}?1h%?Mze-|W)7ZJ=Wss(7c)W+ znmo`XBVeG4_n(uH{0XY#t#)0 z6+zIq&0vp?z&Vnb|CYE|qRDkZJ$BKVFLaQz4Uow!lco*7;HI z=;#x=Z216=^4`rOIq!LmKAf1BFL~S{6>Dp1CZQV7+ui6W1GFz@=Jn-e>}1d;*iy=~ zoO;EE;2#Vd+lkTF<)pE)OwD7gByZ&RC9o6E0vjSb$I%;2LAfZbtNiH%*CBQ<4jusJ#c~ zA|Bz(9!Hor%`En007$}$n8>3;h0pp9l7r46Dn{@q#z(W-%H)G7dtQ_JamVt?$`_Io z@*gc|b#9ER#ml*o` z+pl|37N^c~1F93{pGDlh*7R0~S|CFD{{iZ=)c=p$g#>SoD)tgCy8eMU;rn&YisY77SC zc=_EnSfiGf7Vt)pr_lbbZr`T7bm>`Y>SNx)Zsf&_k@v@HgiXuCdK@=LKe_^SJa!E| z*&EIYIV58D1v4*PM|LJ?Ddto%HmDN3H5sVDPoHGz=+dA*OnNQ{2R#l!agS|#I6G_T z=%^EpjEzyNQn%~+o|Y0&#+XEot>b1x$C}>yuXK)`ufA$&Ict7+1nKzbs1O>)K~R7kceY?S)WDi@#o4v zUR*+gleDx1148wI4keQ-5)u)Rm_>MEVdrcBh*ek^LL{x*<_1uD-C^Zm=GScqmKQXq zN?h`J!nc8(hJ=IwM>vkW%5WcgY~7Nz`jn5r^G|?~5qc&j!?0hh37|7uL`1YRB?>4H zE;r0crT6!a?o;i*Fu?YnuvlSx@i=p-1&Z5Y=CwcKlmiB;AU{8B`svwXWWIVl@H!F{ zpNxzdc1kB8-~a|;|hxWjF11Y0XJ8Mo7>^D$`i)ex;seh4QyP+k&TKW5XI6fI_wEMM0GZt_}&$6jLm>cr>gvFMav)#oyS|%}prO z{7dYIcMsX=9wQJJrOw|4ct^O0NY>~ddz`&l&vAkQ0A zX<3=*M#o@p@8=mJOMA&_jmgFkGqaJyy;ZN_r+^c1Ptc25I_C=GJUvBul2J-0yQ%PN z;!*i!Wr}%&vI_RzC z<)Y$Z8IMW%;3k3!)zj5Ba5%z5%Yb>I{rupy0*gv}B21|Je{M>%>(GZ8jK84q2c#ki z1lC^(hKv@q?q8XiVJ+Zc0HS{^FK62rkM`RG@xS$EC8Bw-Wa%QTqX;HFuC6=3mi$Yg zbYHz<2u`Gi2=r0=0B_pTKKBpiMiRk7A|)n95e^OvAlr`NXj+@r;HESR57j;ZmQ0O| z9ITC8p^dv7@NA!wQRHFyB@`5eR2{F?tTk4cWemtj(r-4TUJ*QwP6z)`|}k4fz#1_Fa%$z%oG0fmz|>;{&$p`P&Wqozt}m*wl_W zBSS+N`M~=C=@}Vw{as4P52dAwU{S(MYld77&hs=xK_u;HYo-khLEtc)oSd0BSiftI zKj`6ZD>Av@y67*!$MB*7j8}nv=d~okyFHpKXUaGb8sG)(1(e5I_shVGVqe8UOeVQ; zHG|%Vs-^NnbIQYn=ohtRtvmB&FC2t@iW`@rkc7lGD9ZL6a7(KkdtC0_8>zn64?0hi zloY{cVV|D}qc50AZ^Dnj5CcLjE+GLWb3PB0_L>F$5PMk|f!N})=fqHgI|7q*&>@c= zJ&KJb^1=uq5REdIZ^9czTmS5f6Di=GsEhw!?;b6kAynv!D;rKS`r!pDgywY}wNlib GNB;wHD&Um> literal 0 HcmV?d00001 diff --git a/beamer/lc-beamer/solution-wrappers.dot b/beamer/lc-beamer/solution-wrappers.dot new file mode 100644 index 0000000..877c372 --- /dev/null +++ b/beamer/lc-beamer/solution-wrappers.dot @@ -0,0 +1,15 @@ + +digraph SeaOfTypes { + + Real [label="ℝ", fontsize=24, shape=plaintext]; + + Degrees [label="Degrees", fontsize=20, shape=plaintext]; + Turns [label="Turns", fontsize=20, shape=plaintext]; + Radians [label="Radians", fontsize=20, shape=plaintext]; + + Degrees -> Real + Turns -> Real + Radians -> Real +} + + diff --git a/beamer/lc-beamer/solution-wrappers.png b/beamer/lc-beamer/solution-wrappers.png new file mode 100644 index 0000000000000000000000000000000000000000..08103dcd5e5eee81cb5535f59ec41d4b01991495 GIT binary patch literal 8738 zcmb_?WmJ@3)bB{A3?Lxgp&%tncZ-CCQqm>ipd#f^($cLWAff^)ARsVED+ohKNT)O+ zEiv@n{NJzl!+qDfk88=ynwc}tIcM)*oryNk)1)M0B10e$l-gQqh6u#D0(hKBf(QR& zw4ZapA0j&)O*O>n*}vCy`6&nl2SQs-+1U5h>V%&u?a(MoocfCPDM+r zUh(HIzb)S2H$1e@_xA2cNx$%WfvuH(^z#MdOH&~Y1VV}TvI8;P%rl~BDuj}BA`XE_ z#sB~GkfID9fk-SVEW9KsnSpz>HHZE2;|I?VZd6G!uDzo}P*BjZ7mCWt%4%!TpK~7i_++RG_4oDlC8wnPnyQgt(ls*r)!BK|!ong@>;fHKcw{7Z zSaNbQQbq9uH@mw!#w&Pqyf>A=u2@-BmEY^KMXqXV#k+aDGi3eX!Gon7kGCZysC)OK zku(4HDJd!G=;-W!#KJ3PRrj+>O4i$kZyF;R7#NtCmgnZ)78mPXAR~DC<%>jE&v2=I z{>>L$W(}V|f3B}*W4pU?(B9te*@yl4^S+y#z34?@Vd3T)4-XGQLPER{o86TWYHI37 zi$BveDSrO^X(`OW*}r&hY;5fB+?=t20rJ9y?O*zeSZ;(mZ39tl*gKt!8}yZ5zPyrt z^yAw%JWdBk$F#Jx9hr{^vU1dvLYTpW2c-_Ss;c;t9Trvh(>^rZpZGd-bb`3Va-Nv; zZGJw#$>jKWty33M7&1;nHt+~zY2R3L*vcN1D&&6eUK8nqh0Yfb@78>yIQ|_`S-IPu zCiv*lBT3ZctBedux4}<19FEhP9MPYfmj@f9O-@c;YRbaGVrgRX?lc!+N1b;>G( zU_8-_v5k#NVaS|r#V5O;X7Gp096QzCi9xodoammVNj%#Tk_Vt{5hlZ@HAI@*iw*K4N61J+v zxQ~dB$n5Ow=;tWVMXSyJh`TB##^@V@R%j?FC@3%g)!6tuPIB^fuS-!;QSuZ%R1qmH z-+1+-NP*sgfr`>nWfD??r(0WFU%$#EX*JuGI(26s%Op{Js5cc7zH%jCcZD$pD*;2w zdasZ(C|JUcVvFRxS4?McD=RCVZEYNrFBJj~o{QOU{O#=Q+}-s)GFMk`>FT0v2!xXV zm9I~TcTS}Zi!J>8*`U(g$HxbX&e=IXIvR`HoF$Gbf?dI;@N*@#_4M@g_ZzD_`gWT; zmYU+!ot>R?=$h>|%bmMFeE6Wo)!TvYYPN$>bjBN_E7IfMGo^8s1sRcZ+enks>1W?81l1 zUAuO?kclF|3t4$6BP*+Tu*9vatIL=2=l5?LxCcACvY^wGOi9$tysV7OL#bEKpI=nS z>7MqKVu>#<7FKB+8?z9iXP5WyZ)=Ofl|XMF#K z$%%y1#Kff3^i^uAgPWV+eiwRsDap8EZEY<}*2mn`R7zHs`Qk;6u$9%-t5>f&<~@sv z$-M6I60VAhomj@JFuM`=-M)7^_I7p=zW9`dCq$B;3kn2k9j~J%g?0v^0rBwhE1=b{ zU32byZfkF^n*S?bH`9B$zwl%bU?M!I2%av?%}G3%X_kMo>*eD!Yoc}je%qRm_O)x* zp6so){IcZJeJSBKD5R>Y`uOn<)UdIMiMGk@Y}U(r&3oH_j4ZpFo5KVyM5|d;x+{}N zOH0f9Z4odG4i5VJ`*VfK$;;Q&)bKL&jf_OgGC;!`85xC=ySci`$;oYOh^YujO5SlD zsIRY=+6?&DB}u{wH7q%WPU&*e;j3@b5Fb8>p}(R+qOPX4y}gaJJ;dRVjAqz6(M@Vk zRekYI?JLUSo3_MMY|X?^S@|VSsk&-Ht#Iefmu1(Zn=Ah;Py#f}qd>m-mHC6}%b8tva zPmj=n!tPc)?X)Y6jg7s0`Le@MF@>!0S~OKoB}dqjm&^%O%jpq+o<`h<;^OpA<9&T^ zN=g!t2fst9cse#MZ(Pru7#Qz1dYkDVf zKJak0%F45ThE`53~jicywR!r6zU3)L}lsZ_)yK(%xvV}VmGx4TETjE_IOAC5?zQ=W7@{y zdPC6BW-CmYf{2@kXKri01Lpox`jL~T=V#-b3}El0{eRRdtqJTILZ?UnU<9Lly(~#o zwu5w>200lSllvDUA|l{qGc()SQ%=${ zwz8V+>1ka2*J3B8Qczh*X_`qhFMIR#M z#7$Q}T9lEI(aVHNFx($f~Z!Ve$nKbz+?SOr*_GO@CHI63W3 z_)J}sl(eo#??XjNFm<)GIQ|_h61-E);+F7MMqr`fU51enbECXx z8<>sT;9Vo(9G?h2(OxFWwQr5@dM-8_uEP;eR+ue*b9qsH5aFYJ(VZu>C;{0wFc23P zC-1xQ8vu-!hQ`p)@M}#Ckk=3}*fj}>3wxEZ?lTM%EjDc^d*%FJiia!Z2?_^GRa1d6 z2?-4k=WpD(bLYl?m%F>Wo!tz1kWgA&TH3(D&R-C!*(oV0iHS%gl4JkAt!-{hjLxG+ z|GtHj=jG+`=D&`NjMP+9)4I)ubMc@4nM}vRf}U%mrjOa_5NW_29_p-h<&Ktb4d*^Q z-HC~gRwjYvohfw<>v^l4vJrDK+Gxmk^SP)}fStme;D6K67ZnvHAtlwmal`*$`<|K_ z!Aa@yOpFK!ZlVen$B2gcvdCXkL8rPJQd+vY9w0Cwk zi#X^9Tjg#J^GmN9Nb}Xh9OO>#uZ>q9?yd8;v$C>o4tGHnI9A1L@t9*gbLZlYEbrdk z6mqmnH0}dkd(uvQ{(5rLU_wmHqsNb1Qha%;zkZ!z@a>MHz%gLnzE%5hG+N>IjDlNI za_IZ_P)v5Dje~;(G_=I4s(t62fCzo#cT52ohRmhlbYn|PA(J=7#r58+=3&T;4v%~H zlKl68C0UHM)QG>jAKvmFDACZ9H5QK67oyJr>i|mj-8)A>o($o;$ugt~(a|7o18^JD zP^njTMnGDElL7{(Rwa;Nx^nsQGrfGcbS5%ppg+O5l+Z4}=JE?a0Q9X{uTS~lH{VVd zmI!#gvXVdTwmH*6l3QC_3-C@G4lw$5Jaq*qA!GRnFa-1%^?`HXh^K?Qdu$2Q4L!Yd z_XQ#AdKS)pz>JzSlKuVtv%9+clffD-c7GhR*qt+r6%K>KJ3U%d3?;h00I6yTx?EUE$@O z2k8!Gc5`zR=V~`^3>QeU!NG{rPlbg|nY|+;)!oX&10V0?0O`W61LPmgrRc-J8}LC4 z1_Q9;_v8t87#SHE#!Z#qupBj?YbPwrSLe;E@)o`MCR zv9z+%Y@h1O@bSY3Q0cQDrK&B9LqorV;(=udQ?b2&e+`xpI5?iw=-ZQd+N$hUeqvv| zt14Rh`rV_W=4A`{If4F1xJ}S;T9F0MLE?`ZXu$l|s$H$IilfW&_iqA{f zu^mGw6sjTc_-vwXZf-g9Pu{CQ zEz)rGaA$eo;K2XNm7;Ql<=nYRj{UAzk8mlZx9 z?~b9&&CS7;B+C?C7Zq(R(g{&YgyNgZojd$Uk{_{*vr9`D^!`IEvxz_gfE9YX zSF>y$bX%D!BRs7|?~89PCUI+SgrujYdO=6R0NL4Wu%2#ie;qs0Cu)2|u3t|th?Qgw zoS2vh02=|4``Y#EWh3s)%$aF|cV1>@>MT&p%GLl{DF_H??ba@jp&ED(cHo8CnHgU> zDK>HI|zixJzpLLwuHsCwaGm^_@WE&-C|5L!Tym5mK5dw-L;PJTR0ye}}N= z9WYzFy9!=Q$dOwVig+O$TwLFJd&OjAUapu%@M@t;c*VqeTU%Sl#$-7-f_**N5f9Tc zG8R`>(7zi)0uFb9025h%ekO=suUJ}If)M0*vz5KDu<-Wn+YQIN%p=qxNjC*9ut|9~ z_Vy;V*f}~nu8vm3=;f!d_QQuzBtqt21QZp6paf72$KFaxi28YXgsPyT;?&3pqvB;r zY3Uc3DJfsVL|gr z=j(O`EnvTUw((WDV0<8VOm0SUvbe{nL>V^|DZEi^e7ol1JXu0(`Ij#%|I8W@wG?l1 z^WVI|qpZs%jMf*X7cx!E$f$C_CPP6I5)f?fe|AO?85kHSNo*S$8Rh0me&N`}#-yj; z2E??pv-9`=3akY>0p>iNTUE8!7=jP52QKi%ix)jTDa2ant@+i}tc;9E%_sPHcn&$c zaJJjEw$VzR%1ttKIzk=inTWd(+2zD8;}z90Pft&8Zf4eGl8(@p*fzJY0C~>9$cS|i$DVhc3vJGK z0hk4&4~BoF(qrt6dd!E9AF=TyiSIvsqLAFKL`|KilvjV+tcgcS8Q0d<_V(>tP_`}y zw^B@nz+qIDmfrL50GPh-;J_2p!X+y}7SgPFMtyU0bM6ygAA{?LDu+^a&?LB^_9539 zh0^y{gX}ip=JN7#Qc{x7+W4hQmqOmN(;+GA78Vw^x4m4Jk_c(o_bn|g%gW2Ao~+ls ze*Kz|oL(;AAax}w*fKRE;|ZW9F)?bYUY?u#ds9=$N>l+kO^#usZUcPnvu9)gHA_n_ zrKUH%4Q$$AT##EXOPBDq&^MY#Mx?J^O>sGZWFu@Psu3w5A_DAp-}ApqLjwTrYFj*s z(hT^oKTuVMW@e=$~(GTbtHd4~OENQt>Ff z+l6e)2?z;TAR+?fJA}L`tkk|CFfc&&Y{Vo)04%Jmus7T1XmZNz#b4BTuYL_W4TO*m z_FdvQmA*F*bbLm7IuWJ3BT+QU_j5(X+18kzUC%Q!EdctUf=~0y%K9MJmXeYZ5Ljvo zCBEwXlSh_I6sd*&PSm^ocX|2g`%&e`f z0uOgRT$U(Bp!Ed-MaQ?tYJ5sQesr_74EbHQ5P6g9zy&7gjGE#E+|Gh|Lv%i zD2-2}qoce!>AxeaASKDnJcF=1YN0yHnz2VmN0iLh<mKSmbqxUyCxxX+(B_sr`*X=>1qMt2?o%U=yPh86;c2SuCPuaoYEksvY zS$A*WrXQK!o(8Nq3p1J=#9!Rx%hKbw`dCoVYlP;id$G(D!?T|0&F0#vR(w5ZE1P= z<%<^&sx8$c2^5p>Z z=91R|C_g%OLx}j4l!D#;Afy4htplqI;3$vAA@xw27s{@RB<2C2K^&7Ah*roEC@C%; z1mkn-7P#s7nY@EP`8fwGLGZk=sK~@q6qq+6B7!6r(h;3>YmBF|zCH>#4>szyr zI=6wBr3WZn@-$TX@p7uMBzp=LPAYCWP{^_AS59l^^`2p)Y85wI=WJd&bSQ{Ri)B12 zra14NWfKt*k??Q`#B6PBAlKN;p&4p6Z55N;*4N=J5;&w8SX2~5k`!Av1Of|%6XI*ZQeFloh>-0)K;Pj&LN*CId0B`JViM5p z++ojeF2D&%|G)rU`6S$ISa>)knrbL9G4bU~rk3XaK2HO+1gU#YPEL9{y$Xr7AfHJ- zu;$;AhLeBYigdIzF)ikm?u=P_3?u}Cw?7$l-T+y1_%a&03jta z6BFq2+B^I-(Y1ATDapxEDVFpx1HXQKw=0DR9+c-|SLWiv0#WzTdps?4|G?N-W>yxc zo>g!cAjcJhPF`Uh$O!O=iHX?~@`Gm^s;YcehD#y&gvcy??<-Q}OhISMKLLrL#zmc_ z=i}*V`q?G~;*j$4tK)JnTsbz+g&}Fk!WkJEErs_W#s2f>5A2hS*HR+hU=3KS;NW1W zf{rKZ+S+Go5R%9pfV7PbPw?gPvB584fO~i$zbEUS?C$Q8VX8c}wXw{o+TN*S^9Tcf z|AW*^MqZB}&)0E@0zjWh#@J;%ga9!OJ0kcYeD?qO;as2yhmskzEZm2Pk&%f>T9=dl zE2&=S@1M%&f{{E59ExC$Pfkuk52E7Zf1beuM6=*yq}2%#Dp4Ro^t>r-9AK`nA3%=c z*RKb{=?9pe4<;XlgoJ>`A)k_T9~OnP2Z#boO)c--iA28Xb*ZbXgWku1w-dZT2Ho3s zLeM8k9$5)dapf8O8%;pI{r#z}vw$LI z=H~SfqoWm0A=h(gCDh>4LMxe>nwdqn*d19ug1rwj00TFo9Fjyz!)`#2Q+7iuuygiL zPR1h*8?XF1cMV2te*;p9Q{w)(R9Fw_ZfX?}$ULnC8UirZrMbmLs4{?OMkc0+$Vh%Z zzIX^5o1PN>_ifJ`Dca6rW9UuzMy5C?S6B19cZ-UP10nh%lv|)Qpyg3edI}a^CqtMs z3}Q?1t5@~2WCkFyKwiFbMV(|HheN|z3-BP1CaH$77CM*!whH92VL0T8oSd9cuzY-c zZ`BA3@DFeZ(%87TGhZ7N6a;5yZ$5*TlaP=Q7LIRjM5rspP$f2wk015qs*>bJL=b@= zudS71V8{US$$^G|^I$p>0$W>KhgK4e*JiVk@NvO=e|HEan6WUm#Q5pQA0C#p7m# z$=3Ju7+kwn@ja3Xc8P$HQ1`j$G$cxMo4#i&CIk~i!*T$-t%C-E1RoUC1L7%&3~qQ^ z+B83HCQkhZM>%km1}D9cXbzTGD>}Ac5YC7}%@H>yhQjMlv$H3EX32)D*qWMN%+gDU zic;!X!hZ-qClH9CQoz}CJ{JRT-i^hY)uXE+Bmhwe?2nBnk5!U5lax^DGn>9RTh;#p zpIdO2rl|?=R#jXa-(m-=z!CN;D+>bi=mZuSFBgb8+^<_08I?n+=jGuCk#QQEn?o3V zWAGGD<06!Z6~=Onoc&_+v?s<=c#}V;J4fcRtE1yP_bxcKgq6sRLmJTkj~QhD-*)!@ d1_e&2&d(<7B*e7+gWp*owAJ<0idAf${vVko2%!J~ literal 0 HcmV?d00001