From d0fdc3619b9e400504b467e7d90c27280818466c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 29 Dec 2013 19:11:57 -0800 Subject: [PATCH] feat(kernel/expr): compress application serialization Signed-off-by: Leonardo de Moura --- src/builtin/basic.olean | Bin 27839 -> 24779 bytes src/builtin/cast.olean | Bin 1281 -> 1205 bytes src/kernel/expr.cpp | 28 +++++++++++++++++++++++++++- 3 files changed, 27 insertions(+), 1 deletion(-) diff --git a/src/builtin/basic.olean b/src/builtin/basic.olean index 49d0ce6d149e6d6cbdef7be66a0d34b929031632..4ccb80be958e50779ed6b98ce03b8a44ee5689a6 100644 GIT binary patch literal 24779 zcmc&-36v&Pb*}oi-c$slK}FB+EG!X(K_s#b^ei|NmPv-eoFD|dXS!z^n(mqI9vPMp zOb!A{A_x&lNLb7f7ZwwPfMDXVugWGyp6Qg6}BZ>V>myC>#O^nTqO->|fnyfl;{m2nX+7d9qyZjHYid@D# zG{(d$Fl#a9*zxPf$3~`;v?s$+nITm|`oUoTg-Kn&w<$N5poI108K15~E66`On#&IUB4jT3 z*0JDk1j5!7{7r;=LUD_7?iULxtSW>&KNJ!uv49hkGbI5dYyK7l**=|*AH8_IQ@h1> zqeJ7-sWH(&_%w#9EAXpT*PEM7W=2n>(TV*>?nn$a=jqqIjcyl@jKjwC`&?%>= z_U}?TglWk>N9{HX!joryp@0$FZ)jpo7gZL-s=ONlFQ6(a`~ug(G(vysZFngOyu%JE z&Ro?9%u5)%9W@)qlV@IDM2VFeotzpPAE#b}$YcGdf&2TJwrtZr32OhT8TdQsJAit= z2k@elfh-v+n41#C*2h51d1TYr^o*tZmT=w;+zuh<-2ty~Yl_A2zO(U;1aX`>luMt5 zh#lEbX$~n#pvt~sr>$*Xj`l?VF%;?jfImWbFTg`)7_;%ALsQ2sN6A|~COISj-Y5U1 zX)(R_S4Mki42WO_Q75)s)_uV9c*?gg;0eO}0iJX-MMbG3^4@}47Wv7uE(wH&h{@ol zvB~2RIfv#!<(A87wURss2x2WwGj2=9rdO{Unp!)O zMRJ+x$H_FqP-cpjhGLLqT4K4Rz;f}B6v{&SI8*-#jiDuD5Db$6N+J4LV4|_DjS_c0 zkbQN1&274JWVAYgvxxPK1kt3V!U|~&jCT0O;c1&F2933uKch#NsTgTNS8xy);D^nB zfu`DA%T%RURHtT&)6VshkSm3t6qK~E5K&<*rvCq=W#)VsO5Z^ED8M%oJ{s^h2>&tQ zZxa3plWa4ZZer6A;M>w2X~30?cCKR@YP@<_%$jC13kXHv$g-1<6vA~eUzQt7XT+Uw zWWj8UqD+VbV3d7c)IC;}aU$g{sQB(rlZPlJudWuU!i1HAI5;sgHhrQL3&PQPE zt^xm>0o1)rlqyKg%CCi6Nt9y?q6~J*f-N@?G+HZ)38!R6^>QoKq$TaAUXhLKA~my~ ziILTZ%;q4*zH)Jzls-+G%GY8EnB{gp48`G&Q@u|W|wl(;- zYTd}>)QC=7tER?2IyNL*5&1We+WKNe7M$7~p>G^HY~&zaG>b`9{B1=J#lxe`wlk7o z(9%OoF|R?qySZ9dk#p@u*Iu6xO6ei#d=gvkD=skDo^w~_SS4|W2`@i^9}1#!FC8DN z&cS7h-qukmtJYsgQ+hPvzeIPtQl@iFcIU5zNGC9ZV-Bu%t0E8m@M&1n`lp) zLYynD>9K@A4fr_1=h*->jk}BokSJ161jmyN<#aj+U13-(-Oz14lb*x~%;J)MqL&Lx z8OrxpU~m%Q&jj!Vfd7Q;p9OqsK1C2so>JcNtPyQkKp}+|s?$lS^94alaNvO@lN*P} zC4Nz=L}W=nB_lOhY7ywo^&fa~>Kc)MjrVihvW1B3Hd;A!iOEc+E^+Bn1wmm-(!_Tot4b z(@vFp2eVu!D_P214rv~y1-=l#Ukt4DU9|seIuAc?^%#;DacD74YG`ibF+eLV0GvMM zX1UnSgl34Q&?k!pR98r6({2S(^=Tn3KLp8(azaCxov8 z{1V}-gXs9FPljhxn_4LdWS|LC*6YjK7nB~^{mK$h3TC13Wa&`rb2pm?6-fb(rp`YA z?4#KK7{Fh318_Kc`tiu-_KRGdUNPkKy2%rE9oe*gYGitv2cX70vSK+VYC_UeM4exI zdtjbGaB8B48d%yE9bX5dg>>x=0eoZGwR$XYpeL>BfQJZ-W-LYSYFC+2Gx>DHcqUb=~iG)_h3}PX##f` zcv@w-1K{aY_|5>n%S?x+kK=KMtMwI=vouktmD_?V69t~-q`F-it2ODCRu{~oi6zoK zAbtTgxi^5n6=;G*XYE3-^;R5H*X;TV%`o6nc_eK-Iw^Ly^u>zFGUM24_sG^0q!`k{ z1gC!DM#t9`8mjk!_Lr&G{eZ6^`~cu9Jv_sRH2PXeSrxAF=(9@dF)1WOZamA*`nEJi zQ3sXGPl4DK)zCDwb4RMg(6gZXj*zb1L^U1;d^2IJN@}-MsFaNsKo$W&yGO+?ueu(R z&PeRRsj0~mR!!;|b@*8hRKk^4?IDjdQwa!UTy=segHoT_`9x&yqK9K zR&x~|OXpCD4j%ZP4hxq{D@Ud$$3Hq!9azK4=DDmM1_4Di7;@c~O;3R1b5!Tw0{BVh z5I#@Teu&4v6Xyr{5~}tik1?rm#WiGI#w2Y#m_dv=ld3caJT7?UY{H3jmxXhk+N}l? zgRxu;jNnY+UKk;8v(F9M^}dQOBG@+MX|hnKKNG;u2Jmya#dK`lLLb(vw`jfR0rwTE zQQd|`DzI&X-sihIg1KWBB+JSs6A8vaA z4sW=Sh~uOV{Q6uaY$ZowuZF-exD*giVQ74kB_9hm&QyO7k@91%4MbG(ZRKe5#fu=i zA3gCC9%jCjhjV>@jA;A$#8VW_H>DVQkP(~1Fg^?T(rEc@ooM8F7J@O5M@kCEWgCv} zwcy8~6PALG2cSb{MKyvQGupDqj}R^K>_Cxk7N0K*pZbxs%Fh9RnD8$EA4T|o03YL~ zSxJ7LLeeLKYHkdx5peX2Mn}s}9nlyLE6+hcQ;bOO&gZV36@UHbt5oQh5Xa87eg*hs zw*MONDGF0%o^h#R>!-232An@H7|k0Yil&yli^D*G1G-%1E-}={FPD2A$W)10+ zIU;B(7A3v=6DcDbm9w-%ySD-SEuwA<_Xl}GKk1*7H zrNOtPgGVwoKw{Sp9(gM|3pGtWLQA~{hs0+0aG(uI%+qUrDZLs8meb2-)CO}+(w)`G z;}!Xe#U)#5i8Qm5TQZDLbKbk5@jmnd)(MUM3D2X$u%d1(q{DCyB%-N5cL=%{vwKO< zy(8cc5_KoQ%Lwlb_+Y}g`qVfq-I+Ey)$@moIQJIcy!OOzC{B$v7SQ^#)^iX&$67e0 zZ)K`75|d#yx97C25tI@hYqi%a0xuGz1G5w0Fi=>ppn0HFz1xCP{yut;-XhCq&O)5o z1r5t_EAg!?d2MBr-PaNpR^x4in~y@tx)A-l$fI!%;avfrM|d~gK{PP&Ht<2M@fo&b z6V~{wC6`R8W@@Jyo62@9w6#vZn5`R^DXE0nr@IR~*-)F6Hr45SWKg^#qosn$`?Z-0 zY0_cFi>+w>qw1KD8($@iYi5nF5q>|D0N2wR*D?vN1AM&~vRA}M(%`oh1WJAR4j&|A z7Atf36HWganh1+GSsTn}iu{b!(mgZm#x>I4zzJ024&U{x#+b&PBtr*)j4qc1YX{Q8 z)rO>TTQ!yvlnGRgMLb$Z79Rz-Q*sE@c(fGkI5COcw^T1JZc(7iT1NHuxW^`&E${WI zSl9`YmqPrs1jtq>6xSy|;ClhpoY-3$8qd{|24PCj{}-- z5p~c?8!9^)gcic3Gv)LHiXAOq84_ET(dOQ4n@MS1kT^UdM=upQnmf~>s7%dW2rmP? zE8*qpmF9cVw42*QXbO3|^-Eo))=85tO`7|fC(Ul;DFnnRv>UxK=*cSQD3sZy1FG+H zr2LsPG&m2IuI93s0XmxdD;9CfCSM{bl7xqk%&b^Hv_bChi?Cz}5Zs12PxQ`yU z;5vGQqPM!E7QYf5e3x7?wRqC+O^MG`Ud!WQ5ie=}p)6Gp?MZlQD+!)AQ9au?tl}6o z%MpaFM&cS;(mWE6qx1chH^5PFv0!+KwiA|`g>Ar*VzNW#Obn&>R=f8eqEMml3{kgm z%{7krZF5fGC_isgNhwh--O&ZUZAg&PN)k&Is2I?66nwWynh!9<0X|4;*&$f=wJRp& ziehjkB)+92%_o$UM`i3KAjsAmKPoFm&{JV+3~Rm+I1mk$4l+6cxlmw_Aa$TwIy0GA zIvD1zGkdDBTBe&YZ~56mMJ%`iaV)qTWeJ@Xl;T*6g`!hq2^kWx4_fa~A9%EYq6J8H zw3!D8djp-FB09ngk}IZ`moF$r^`GU^pPKf^360iXz7*Cn-@Fnizk|kc4w4A^|B{a(P%lg7D~k#nj4m({`)1P)lR&F|h5T zfXD`Uv<{DzKcXZUX2O=7p$mVV@q5{PHU~BoFm5T6d|~_hRVJcfI<>j z95b!($$1`GZ43-+N0Z7Sv)Mw2m`s3eUN}LZ)&|!MhtSwmG3@Z-hRa%7x-`q0RrB<4 zpeAkkueB-Vr<8O(np!6prCfzyd@N3W?l26oJuE>D))PVK&&+t-G{Hi$^HhCg>61z4 zqfJqp)|P`<>yt#!?{%W_>_|R|sIKynEU4kIQJATGrwG_OzuJbuh_aNV!JrTuhPY-# z+g-=`J}3*x!HzaG)wu@>Nvf=Rqx|!MErSY^*lHN+TxD)d^ov;Qs=!Qx6KlG!KU>%M zswKX#qO90NU2Xk&8W>(fTYijiwjRMNP61kS^HYALw+0P)nq23}yx9p0nw0B#bot$E z_0o?%$vXDkUfBl(WrfRJt?Pn}yrIC#iN>r*+vkgzRn!;TwR0s8%|?kWflr5kKX9Q~ z$)7>nvw^{^p&_hU%bqEyPnq}(3lcttx1I^qf7UrgmiB>y9nDP=DzmJ1Td(A+U4g9- zEM%@wX}7Qvk2`{hauGDj5wt>0;ZFqcCkcnqrAL-Mt=w4NkQuATcaVwcY-^iXy4c6Q zp2%A%s_^gG29IquGhJvCXtVSrJ@^gmo~_(L7Q5XDZjS-{?Pw=xd}VN8BBuc^86sdr zdQS@v$w=wZ7!jLfVs)mHpH+3cc$^(heikQ+%pSq7#Ca)!;qRqn=k`Tg9?;6nw=sjPma zYebZAnN&b!olE2y8j7MMqhIuq6qU6@w^?stNPzrR|MLXynW>!iq9J+YpBz%MY41;! zBBs-xlYQx+zqZqJYROAoS9^h*+MwBH`s2{O=XAG8g_jJO_673U^1$fKFK4@7EEm;? zZAMaFHxdx)IXfRGH1hRc5F6p}SjE{EacWj$Y(mP9^g=McsIwzn)Z7u5>1dLO{Llue z%iIs=CsZ<)vg`80v$MGTFmL<~=wH#n8-5rEx%6KiPKR|Nv4 zyir|oC0t=&>G7LO0#~_Z`V(B@Z`mP%B?W_?Kuw z&N%$p5`;*n!V$|#$5zsJn^RQK-_n2&uH;nKrfalpW%rsqxIF;WIdUliB6xAqz`tG^ zdTn3-^#I16y7xL;ugHB8{M%j~#z_nN8T+#D%X;OpExl8|`Go_5_{+Fm0of3L2*nmh zNH;};ZkIs*Kv019FAO^Yd+&75kusD zi~(JN_C$fY+VmSjviELA_df%+n|a>^d>`94Q~aCIbiajp?*n*yP`%Xq9l#Ig4p97L z7YZtU$)I_o+##KM_o4SO(0EEj)KR#Jl=Qxk--mFe(LNjy2AT~;SJ{_0N@Kln4VKp& zUY|4hyS|X5&u)D&5MI4A^;@<5ohU|P;MBftDxBK4wVOes2E4bca_Vj9u^VK!1Gejb zcLKI6e|OQTccZD-oZ8oiw|;eM-x~nGvFOwVx$O^&oEmn>NXa+Em;0)qOhp$n6EUwG z@LfOY+iBJSI1FewA@AEu$CU#BhY^JUz@j+*%V4h}le6*^WFe0?bOPv;Z~rO*%Yd5& zzwdM(ATPa-8Wua$^tTw2`~Y$Lp;oEMOYf7m#!697KrRU3stbG;_}MfTQ)H+Hw#W_? z?DBjjK_m!=f&V3AyxhuT#rxhIOAfWC#CPpX6*D$c9oMYK1k*(uI zy4hBcvW$lO*-bhKWZn+#zqfhY4G%QAff0Ix2PZaGbkBUSNS%``)B~&JWaY=Z3gqoY z&XZSj0@p12_heD^*qQV7OnDj4EuKtS@*h}Oh5y z!W!a#7$G#d=RC|HHQr2sx5(3BIVtW*)geEZ0sXhpIllmG(H=W8e^T1Nmt7axp zgZZ@JrVYFnWaPkM73S@hkuYZsu`zI%BL{|k}tE~)?k literal 27839 zcmc&-36y13b$##uU%w_NATg-u`qDTML1;vxNCVXac1NI-?j~752v#*!-33KecU84C zLkLM0B1$4CaY#%U%u<|)2|++Gky#m(NsPz>f(#l=;uz651 zug|;p+%unZ@4N5*&&<^L==8+o)Ocop`O5K$$?3`Y$(iXa&$A7uZ5cl%%i98GxR?KM ztH>$lQ86ZNf!T;LCr{ZjH90<)<$XeJR7lD{%V%b$gaKN{lz2-Z`DkUes>BESJ$ zUaBZ!zlqVQImX0rRk|BL17?+mWE4Iw;ptKh)^CH3!2%qc)Dq92K zl3vz2^GwBmnaU%~6I&g(-vS7az4P)4Mr_N`=@WaXv@}-fyu!QV(GWh zbr^Mi4dCTD16;CKFt=y)A9{vk&g0uB=jN>xJR8pYf##9qyg%Tz-lA%4in_PS5D8Sp zZTL8=2)eb_JW{^Em3?D@M`WA>(SHI(d_CZ|5k3g;s2PevW=D^BN}D)wXN zUE&0XnAyno$(d6SO-Gf17OYoRjWbo9)k`y#z^Vg8GPAM!0GgjpY$P%rCism!FF3B8 zoZGm0bavBt5#cH0caU;{QSxNwI#Dck61FQVY*&m*VO6rJ#$JG+E$M=BHeBclzQzz8 z9qkbR1_EV&Q=3XVuN$AJPxK->Lgs>S8jx$H(HU|5wy`;zXhwoJB5U!c$PDj@tZ z`16GS81NSezpYHh8_;|sn@0iPs(t-5>^f!z*GDZiSJM~4K4(V@7DeLdGyskj22C+( zkw>fMC3N7|iYb>@;y|fN@Bnp!|AdLbiC}D{EV`M)`#K;%(NwyP(&&?1is{Jo{N&te zQe?nbL{&K~+_={KUk2F1s$a0|;M2u~7BFVaZ2jM+JZLAy<&Bm|pR z@x0Zr{K$u>XJq@PNMBY9D>kl$I%cM$)tp4f86mHURz$_>^{1U;Hc#RLvg{e$Ava=3 zNFNo6)q!O!0PoV`zC9IS!|dpE{mNpw^4wpUu5hpf2kuyJOd8&7^gXCitVCuGnpLKs zxRrNIxm4n_gp)j0;cvs{@tN6iod!3|PQHC|R33%oZ&=+RxrUpyMc`^zG-TWO(c?$x zg54aaBX$#c6c?8cshpd+fvb*6a-sx?O z&_wA;!R!vRT=k01m@93zUGX14A<;N5LD|C0d%6B2T1(Vnv#&}mq zo^G41U-%;efKL0Z7SC%6p=AkW0@$H27Ydl4MEJdcPbU06HwevBUf#pVKuzEA0w$?< z0mgc{S8eUJmda0Ov=%W;E0mfDImrNC)!Bay2B%Zz_dEClfd7Q;9|U}sDo{*2M3t*d z7q~WvIwqiyLrXBCf{9`mNwd^V7qBa5wvA0mtfS0{*pjYFMryg$Fc4be%o=e~W&TDm z@(aABE0MbxN=mjz>=ttNh+i*dC3t8S3+umwz#pOM{=R+?F#f@-bP?lGrviJd2Md2M zw`9`+G>l6J7eM)^$%oecP!I>*>4f`X4De1mYD3~37Iz?CT?8Kl!Y7(a%P6dvBzaDj zB@6~%A|D~D@TCsEOf?{VG+%?uwZ!{~vm%Zf%2wwsChlKyp*#XTz z(tDe{&!=WwkX3_6uuZsB&rfQfD}k~TAWK>)-jxDaq*!CnhlcsZg@fZ}(Wx%~Cux_V z3jec%uXJirBM^82Fotl6)+iqiY7U68=Qhury6^b*EwkfubKFdJk?26sGs6g!#uFpQ z1x@3{DoAO@igsbP=`I8YSltQ8Xwsa$MXeH=HB=7(dSg%JYFYkCY8oD=fWQ_;S(bNa zUhk5?Pzk9Bq?d-oX9OiK7>o&7gmjIGLl++t70=i#^f@p+l;LrmgRk!%9=hFfI9(+p z#IbUvQdUs41T=p4*W%4}l*TOmEAUoQ*sq0|qM1<&`$;{VG(jiX(z2{fYBn{J#_gdh zbBGsB*c-uWg5J5w!8Zfm#P(YNZ}#p0HKoXh*{1ecbV?T|4LA2S<|>{766N5eV!07! zz$!hWG6K@ap&P(4G1s=~jq|;V-8nw6oq0kULPVS3z6kIf8ske2zFpox0@vL9H4W|o|Hg24x<*ZE!X$|F8VF(uptT?8f{9>e-cL;Y^h|0H$2 z2k@r|-wT-QRx9J6;-lGkX+>w{xrz>@DXgN0c$UGU2d=3@zaouMq(VjWrBkD(8k@$n zw}u>5qzD$MUlsC=8>!XLLAudflAds=siWMa+;nZ;t3Z4vB_!|y>2=LduR?=Xmm-sGKd024* zO(3P7`MM7E%ffZzb2C$KAFmI^Or@r)(fn;( z{*z|-CN+|lYzdmbqxWSM#i(kzQA!=@ung>Nk4FSA%|^U|=<#sTq{bV;#9%C!!CATc ztSo0K7Y<==LeuKk6*HdF(|9C;J;FUfHfp&i9sHDozvZ~28C05e$bZs3tFFlo~A8L#=9O2EpYJ>#{ytmuTIY!!EtRVfKIl5H(p@`P>UP;R(w%sY$m zXJl;iSX%5SfZs~^r+|+m{C|K?@FrVFp3JtOi00Xt3WKeG8DwF=6e)L`(cy=t)%M4V z5$WH3&%L_=c7AW22KYI|v3<&406v55zXW`y!c?1kmTKVU*=$EZHUFZTUozYo zug{D}gbwrZvMn`JWVxC$?52d^w$LR9t+sdr(Y%84Vk@%A zeG(H(9*2Od7w#nJAor-~cZ-^z4f3jdM8){RLeei2wQH(ote!`U6qARtO|!N<7_pU% zNCW|w7s@J0GPk}7_Vsvy2@2S#ma%zQ53x#tng-l$p=6?^sW*k|L%#aAb4*7ofoimX zrM7qusN6tX7Zfekfa5g7V*j8V2tUxQ~8$F<`ER@|OUX zx9IXuz6ag=QZxLFMg!cyg7Q#5@*E(9q57Jg=d5>}t>g8t(vzHpDEhvz!6J20v!zR}N6rs6bY9<#TiCnWAl)W@+PKmvepI8K5}VYKzLuk?<2gQniI5JSTwZo zlDGAK_U#Y&gG5j_3#fOb9O$QJv?sbTwGp~?#nHM<$!5%KG#AScz{%!B{u*hGpIT`_ zw*c8O6C(9`%+wIc<`%OsRkS4+78I>3X&M~IY<-sS>zPzI#@V`>_5pYeF4yY4J-Yl% zd?}6LRE|J-cx-`>vPp|6$YCZ%^M8A@q3DR&fC6pg@5iK?AIQ;|^JsF;{$ zV{tuK)roda@o4l#MYKf^JetaWQWrV^F~fEtr{rR8K{MH84VAmm%n+!p4|T$ThFtC=IQr7zhUg z=AKS|2;isLzDz9wVy*As@?W^ntGT?9k-J=r^mhp#P6Gl7&y_7aCb#%tY|;6>paOg# zPj@P(U}a0>)5jWMK9_9^^eXe~)hb*fWCz#{dNeArDwlKrxM%QLnM8937h9OC6?5HI z?8Cr5F3m@Q(id%Q$eu((O}X0sgbWC~FeVIW;ID7javP?P+c2~`uXH4hKsb4ikiS95 zh`IbjIYa8%RSye|;!(X+EC_=Z^N)pC6ez2p*4_*VJb(4=LwGgdeF?9jz0mSnTv(hn z&bVHOLUL%5r}U}6)LLoMrC8sait*v}i`tcP2tjdV*!ckY5k-#!g{}{hV+a>UEH+Y- z&4DV^TR>%XJyRg`EmLfcNnNy3P$cQskI%2&GP+g1rz46?hVKN$t@xHr)PnDu#4Y%` zNra-`)`(id*Bjh>^tH1qX2SVI@v+Klbz@A#%liJ%mS%8o#w|}`m5F7|RMRGl4IHax zI)*SPSk1;!(5&xRT#ly`1k7)7jqnOWL$DOVrV!ixqL=8IL@;*Byblu0(~aKK_ft^s zV?)+Q=02{$EG)ia&U23B!cH|)iI1n0rNmSzmY6oP=QrpT?;fKilK8Y5iG6HF5})po zO=1grmAer+d}MBJM)sQEidv6fs9hT&QQw8J_hD;i@8AZYCgG6iN)w3SKvtt&NEpYt zg_E|QKp0GlSW)ea?XN@v5TXATOB&*Q!qsH%-jpt`h~;A|iBiUo=_7<~x+%;fK+SuG zKoa9hz8D@3UsPn^B;(iw3K(PIV^!VeBT8WL;~x?nk-$u&-JbL;Avj#JD-i??$({3K zkz3N5;C-~PZG_TrhMSW0>O>0QonF@WsFEcTMM^ym#I9lLv~VDY;2QZ04SnBL z&12_ub+)7FK+y4uMNG_Fk-5cNmEpldX!eF~n=PcdT|7?<{hC+{c?}X(b)+e_Sr_)i z!_{J~E?83O8Fr~Z+b>anhNuKt&it#3ZF8q^QQ|AY1?m{?4_U9BU6USg=7TgSL=zk* z1S?}FOK1BabwN?C(1c}i`(SNn*ttec9k~~*nt-9l{nhNJGgh-@CEVeV!%5Y!|ap`K@I5BK2d>$B<@ zGq~-v#C2vw7VaZG?d?pXn;lC$dDTO|G4s(H+tbVm0jPb2qEoU=-wd~}aAqBuKC$<6 zK>I4c66D!C`pQi}Y^FWzIpAzCzl!$%Gs4d4`W(>4PEp%Vp9{$PWsPN8UZWaVwA>Jw z2)<26mauoQCrn}Jw~VK_w{`6YA{O**9PDgg<0=AWi&+N-&?aV0KJ2e!9redP=sgR0 z^HK{dBDQz!jA!{rR`y>$}^YDgO(?Mv_JUEcje$ttT9Afjt1Y|@s z-%7YG@D$SiS@{$quq#O1+SgF0L4qfgiRuz{;>I-uozx&m1fj0*yBz#(!Wd?1sX=u+ zy`Se!3WJ8m!l1HZasw?=-8wLq8mJaO7MfxG7x&-}pX^Zi^zVwxZkp*qA#@f#KsSD2 zqn~fG;s9L?gFP^qzk=Zzl!QuoREj`Th7~Jgpp<56gQ8RgA*b`a*|8A0>baO=q8(!23emP!fl{Uy^jjeaUr1+jxY=Xrsn$-;^2xyuKJ|tlOhm}=N z2YMAC7t7{lfI50{vYY?V-hY|4oBuA#Xoy()1($Hkf2!l@$M`md!v+FHby+O=Q4gBap# z!T4}gm7odWtS#T@VWxBbr?601m-QVEh{}VEuFBunAyQP5H97n;hB5tLx8;Y~ zsv73b7#eB&r+T5?Svq4nUrOR?!OI8((E=j+KJL<IfS^zz~zLy#lT)YMMz>G5n%^nperkwEzHf3lab+! zP6RaXL=5y~pTvMy6zq2<23BqD5d&|D9l*miEGRh6R8cx~sB1qhat+w&A$(g_V4%kd zpgTJ9qY)7)atYpzx`cpD*xj@Ff(kVZ2@dqce7h#uq7$}`L-0|RLujw(02wMdDc{5C z;gGXqnpK~zwb_TeW z#Py?`p~K%E>Ud80c=olEN#T)BdF@8erl)DKS0zhEw{WqeZd>ES7I*{}(#ZN=huwZ( zP=NPu$`zM^yMj3|);1RLdrRtcGX!W`ka3`1LuCSH-@)4Cj!XP$sOFN`f&vXqu3_6dS$T||III{u1s4LET1*4#E%rO9}kw91K_v@vx_KeM{opU^Y zF9VVc+9_HF&9ig7o|&=Vmt+LH02tiWd9)e;gS!ONXw*TT-5q)q0Joyoj$+>i*p6a< z39uc%zMTPZ2bu<401OVIWr(B!J_ncQ>U|{umX`iGItl>aA)_UK5tqTAPU@g!m+qhx zGfTPQEK)Z3YNfGI&>Rg^ypf~;I=1fgw9Vw)=OmWIKVOzL|8zgfSrccdINbY8XbUBvpMgb&!% zvFsu2SVAOKlRB>jb@yhiM)Q+<6T|lzkCcOwJvEdBC{l$#6To6_#-$Xz2FEDZw>Icy?m9lzNj3m6>YK(#O?+=0iG1lO=RY9ZLT zw6eLG1N6%Hv80TqZisEOxPtMZ!lu#YmwlOQvBrXYmk^mTfxV>ARI{1n#BoNI+9{** z2Ql;$Mh$d;GPtcOOFHly!23)U&+(#x)i#vFj_GdVV~$NEJoRxSYLn~3-vRnSx=WMlvwlb1*k&LmU+ISJX0?x86@s- zBZs1m3rNc`ek6BGGx>ou)mLy*35LqqJ&H?Dr*{rklw4dISgMFf67?!QAWMuAL{GUm zmYe(u8(AHb5KM=DTgDH)D&fYF=wmKgK)WnFW_n^~>O>}@OrtmlW_S2} zLq`2D(gpz3BPv59g+_zBpno|Bf1fb$6xVBut`)ef#AOvOYv?y!51d*^0oRCYLBJ$1 zG_+X!%Nb|fsU4@Zo5$7|2}!9Z9$1d!GJ(scLWRhk{%9arSZLTvT@{=zM|uTS3@l2A zRw~E?dQ<_=szYIwslDfU4bbZ))As}TW%dP?FNXqtc^m=b`r$ooR6Ujk!K2VPK(pPRrSP*wq9dYgB z(~O8BD#|ZHU-x=u%uhZWb(ivl|leV>1KQ zJBF~?H~E&+(~9l)NqotZwe_#4#m&AR`X7j@x+~Nw5nXC)sc+B}E%;dU_|jOn zx1tXHiQo_2O6UF*uq|cqE_w*OptfpX9Wop^K}y0hqFfwHZZU!bq2DnP)q+YrC9 zjv006K3urwit7&*EYd=Dw+d!emO{!nvygMN5&b2IKF=&6u$Jv1 zK3q}POn%{}v<1V7lOd^r04nS7bCp{NS7>YVhOmO_a)%N4q!oaf9p;&mUoa$EV%xL0 z*s~bTLKB7p20nC}6(~6s12Q_{u$B>(B767w8kg>XJR?Nn?NVO`o_!T4gqwooM-RQmI=gx#J!+ zg78OgsLswRwRtC$3Vv|sib`prFy7t|^AwIri-u8L<{0Y&X2aW^>iN?lwl)05k}Qoa zjqzo)Izd7)jdCq@u8eMA6LR>S^>#qlBrYczA&_voOr!5ar^^LimuGfdm+D;F(1|2p MHGSd{_@9>jKN=+0@&Et; diff --git a/src/builtin/cast.olean b/src/builtin/cast.olean index 5751af3a3ca8bc0a93747feaa7a3bd00bba65e2d..380e07a788b46e6406e3d32d8a6d806ebdf67b28 100644 GIT binary patch delta 274 zcmZqV+R8cMA*1TVXPX(7CeLG(0+M?f&4J`kMj3B4Mn(oOU}ObR!eAadqY{{A0|}`> zWJDk$P#LgdO|TF%m}F#Bom{}A$fz{&m+a)tOiggBBAM61*;*_z^$?RGni!y_F)^yb zodL3v6>KC6Bh+z{ATfqE5Yf)a0#sSS09L>X)y@LuF)*@#ROmtVqS^zJ0b4QoE{h5P Dtd1JN delta 284 zcmdnW*~m5FAuBTj0|V>CN1MS6rpdRNrJ$^hjOI|*OGX(5kTNz#Mj#0UjI1D17|dg5 z1W7SXmSvJu0<*xPU(k) && static_cast(k) < g_first_app_size_kind; } +static_assert(is_small(expr_kind::Var) && is_small(expr_kind::Constant) && is_small(expr_kind::Value) && is_small(expr_kind::App) && + is_small(expr_kind::Lambda) && is_small(expr_kind::Pi) && is_small(expr_kind::Type) && is_small(expr_kind::Eq) && + is_small(expr_kind::Let) && is_small(expr_kind::MetaVar), "expr_kind is too big"); + class expr_serializer : public object_serializer { typedef object_serializer super; public: @@ -350,6 +360,13 @@ public: super::write(a, [&]() { serializer & s = get_owner(); auto k = a.kind(); + if (k == expr_kind::App && num_args(a) < g_small_app_num_args) { + // compressed application + s << static_cast(g_first_app_size_kind + num_args(a)); + for (unsigned i = 0; i < num_args(a); i++) + write(arg(a, i)); + return; + } s << static_cast(k); switch (k) { case expr_kind::Var: s << var_idx(a); break; @@ -386,7 +403,16 @@ public: expr read() { return super::read([&]() { deserializer & d = get_owner(); - auto k = static_cast(d.read_char()); + char c = d.read_char(); + if (c >= g_first_app_size_kind) { + // compressed application + unsigned num = c - g_first_app_size_kind; + buffer args; + for (unsigned i = 0; i < num; i++) + args.push_back(read()); + return mk_app(args); + } + auto k = static_cast(c); switch (k) { case expr_kind::Var: return mk_var(d.read_unsigned());