From 92c7145d7f0810e2e857ebce4c27dcfc13bbed0a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 2 Jan 2014 20:03:42 -0800 Subject: [PATCH] feat(kernel/expr): maximize sharing before serializing Signed-off-by: Leonardo de Moura --- src/builtin/obj/Int.olean | Bin 1664 -> 1477 bytes src/builtin/obj/Nat.olean | Bin 20087 -> 13027 bytes src/builtin/obj/Real.olean | Bin 1139 -> 1029 bytes src/builtin/obj/cast.olean | Bin 902 -> 739 bytes src/builtin/obj/kernel.olean | Bin 22239 -> 16442 bytes src/builtin/obj/specialfn.olean | Bin 1101 -> 768 bytes src/kernel/CMakeLists.txt | 2 +- src/kernel/expr.cpp | 26 +++++++++++++++--------- src/{library => kernel}/max_sharing.cpp | 2 +- src/{library => kernel}/max_sharing.h | 0 src/library/CMakeLists.txt | 2 +- src/tests/kernel/expr.cpp | 2 +- src/tests/kernel/threads.cpp | 2 +- src/tests/library/max_sharing.cpp | 2 +- 14 files changed, 22 insertions(+), 16 deletions(-) rename src/{library => kernel}/max_sharing.cpp (98%) rename src/{library => kernel}/max_sharing.h (100%) diff --git a/src/builtin/obj/Int.olean b/src/builtin/obj/Int.olean index a8d2cb76b5f94fb80b7346a52fafead258f2d675..0f9ddad3e99e980e616004005f9a21ff927f0df0 100644 GIT binary patch delta 554 zcmZvYO-chn5QV#|r$76=}l(Q{k^JwHC6St_T@evbytN?r}B(jX_33KoG4|X8VnH~(ZB1#EvPvd zj#L6#oy>5lhLtCRwu@SAk!cySdx$r2WH_Af%3%+*%!Bwk9V@`fF_+_e$k-?qTic4* zBGS#~GNLu(=}h&`kPLs{H2DT-yY3ij*Ow;02JO`GdJ>jtBUx1hI!04Qsr`>RJqInB zt0OXeMJ~)h-w}{o&HPJp*@uiB?VIrkk?Jv5aRN<;V=EnM|C@aF3!vsUE`SA*HH-h= c=@8_yh|Yi8oa?(<%v{9MH(?_!|BxR10rI>k3IG5A literal 1664 zcma)7O>fgc5FKyQBz#DGly89o3PlhU2~g7_XoFfHQq`y&kT~=b*?1Ey9J?eNPCatz z|0sVfzl5D2Jy-M91Jz8!DUSo_H!iZ$hrcQ86h$A*6DaiU|&vm@WoH-Aj( zATd<+NCl~(y*TnGq-KB4NoA||r%`O8gi48T`X=p17X2~RLqIL@#?Yz9ZlmUXcN#bL)RQ=82w&?@(61NxZ;4V6|RDvUGgmS z4cD!@Q?s*kG51Lis0@dOnkvelyHZgBucew&`)L|mb(~$s5W*`6pYq#!Yaf1jE>$O2 z0jDo5Nt~Vi&2;3mP{M_3v00^L9k{ERkn0Rwhmacx8%ibicnN}TLJL&6f_4PsH7Xc~ zD;evO@ix=c!FUH@gWq=x1H2V{9l>`?@J*({sx3A_n0tMn>o-C803oQ#*c!q$G-K;E zIF`(9WgUom_XKgGhmu(GJz|or|ESEkL#%u#Dv#1oR-X4yM^ZfIr5$YP2|}>7#g^b9 zMk^Ra?w%nNanUX+*M$W8fkdI6tdh|KIBy=*??J`}%jj(=rGIfm^Z}EH;DrJlv*OFa ze)q1DQ*pWtp~DXx4bp)Z%yImz6b(3_W3W{njs-Pgc=v(@N}ZDZRqgt1)P7E1PJAkJ z!5Vj#SEPL2B4zJHIyX!Vv38N#OF?Az!xWkQXuRzD;G1^Q(uy;C1_A4#A9D9w7=iI` z5n}u8Z2Q9P3tRS-Z0L63^`_I%+w-+<+GSzkf diff --git a/src/builtin/obj/Nat.olean b/src/builtin/obj/Nat.olean index 677e5c5a99e974afd22d3220c049561ebf7a8c5c..16e56518f9ac8053a7f38193f6dc2f7b45332a1b 100644 GIT binary patch literal 13027 zcmb7LYm8l072bQFduQfO4E~Ttg*a2^K?xOYYXNBsN#Pb+EwoUIra*Bzy)9R!Gi4rh z&^FOBKrqD@0*Rsq1+X4pPtN6- zBstP;QzH@SStPv#q@^6GH#jeJ*#*XWszo3z=TXP+d@#UOYgU6|TH$8<#o9>4P;wc-?70WqB;llaSYl^dp% z8>aL-H|jlZsPq&N(TGZ3=`xW@ou?R;yS24ki2AT>rIpkR1F0Vgq}Dg9&%i6r`4~YA zIpdt$Y5aeke*HY!_ffNa+LS=oxo&EBc-81vR9Y5+4!6<_I#;_1bY24uO#pT?zZQx^ zxWWMS3KlGs&1dhSTUz##oA2q+L5V=4Ylzx)f}*^E=s1PN{$tFD{E$SQyC1` zT#>1gC5SMsCzE{H)JS`qN}yMpT*x^~lPIEKlCDyEcP4ms4Y^c2AOp_Tw`_qq#?0}P z+H`$lazf^|?1l;1rvB&yE>g2q)dMGWr65IG zKO)Xt=*?^;Z!Ysj?GEY-lmnD;n$)p-5p`jD>#IVNO} zI;H6@C26R=jBzOjdj^*mn6jJ3oX5*tQE?MDjO{qPHobkkHZg$;+1ztv)?p1KRLTvP zl;I%!x#CRNJv7<~#{d@T9P;+cJX&Q+^nkK=fMk7u(^KRHuAAC4A+%%!EqjUZio}z3op|ZzkhYG^UEV)T0#y&%n5@ouO)D zMV-QU^_&UjFJTA@5LMDg1y|CGMD_IZuesngy_B;NAa4zlO@%fAHHJY7#V|mU_MYK= zf6KOQSV)(q0Ch9HcM!~{z#!J74gzBRyQ#1d-6=hmMji}_pdtdzkDjJ@IwkZMMBN&b z?#8N$x}ErIu_&0xPj>=yTj-}ypuq4_33S{-Uk1gF{3bA!NWpDbyraDWknF*rveSgd zqDJcW_Qx2+qK+B46LUuR4r0_3Rm|z5=xE?rTs-DeAuDmsjt02ri)#Q%q2&(0fVmuv z)dY)21ItSz=Dr|zfS2?G#2TL>Nq6V?1`N@N}FVb;`*r1lsA60Os z=?9QGSB+VLp`#A~x<88e3>Np(A8Fmf!o3*cjG>T9w7r9%JRl|VV!#qAnx<6@p;|sM zG1ja}=s5Z9n8r`H&(xEgpy|9LC6rgd1_7@mSd6O5VKyAm`95%T2OdCue-uaxv_%mouU=5N6KC3H+|KwvSeO%)tX3(X6_#CdrPi-8rg zpU4Wj=3px;)EP`ST0sMJXbb6%)eqWR6v?Du4y{_M4}x@vm|29@L#Ydh{M3dQscwMjL1pWuip&FV zqtODm5d*FUD_kw&r6T*lK#}ukToxHA3v`+6Eb})%YGarrw4hUM(>7*T*IiiDsdRNHNE02tE9A#;uTM0 z&yuYd#u6k@7R4w8U)Zw)vkFqM@EJdt84RRfG%I@68PYFqM?V0u3>LMhePlhiIjd)} z=YbKvv*$M_qU2J8N*qY~CBWDY#gKm^<~&?zJnVVx4%c0v?Za?aX1|m!nGXX+S!^XL zgANNkX<~O3b7_iI@8|rQJ*S1 z%#8O;E9)U(l^@LO7~&@dLGhpqN*#Ev)WXk$E$yhHaDCPz?81{Oz6S!3RB=0J7e{+! zaHRLq;P4H>{8n1BERdaOZ1lvMeKdfSy1hk_({Zfr0uV`piY*b*r-43Ot!6FY$>ILA z+w^ZRaRh1*kjfRVbr31G2UV{upeRN~%BV5dwby=H##g@oM|oZN^xEQl&nH%Yws zh|1!4&A^OSuOU<*&khB|$L2N&kh>?l9KAE~QYd@OYU)o(V{(@mE&m6V&l+~J#-^sU|!mYZQHXnjBMkAae< zcuhV)?7(d)3J`^ws4o{y`W7o z(H|0pP*8+J`dNvdL;m!P(4T$VZkwTuF!>ts` z#yp?nmayAYp3FkQY=^deIK1optM{=QLGawHApPLG_Vjk1;CKOWAPeYQPYd4X1jKf)TJKEJ4 zX=Y%H{MJ_m$4-dV-a4IUPIO-dI(iZBru>?lmcw>42-px92rS%{Es8VDU^5p!GVokQ z*A11~XDB*55cuuMe^WEBT?xbI8{4*z)N9^-gJ92^Ln#(ZqeXTeayGsJayc8j6}**T z;cUQx?%qh)KF~hgg^_2l+kbuGOYiUvL*rX(1$#DtZY`-(E2Pf2pXQT9WRW`jK`Ya8 zJ)jNwTfuO#568-&@QDn1`d9h0Asg`&?nj{O$Clg!(Z&vfO7cb8;0Rv@y04tt|I3P7 zy)gHs2heYb43$I|ku&~vJtd`33ZNA!6Tfur-lB zD#$A%(jRI=56yS^|J~tyz}%C-yaB(m50!wiNsC^y3i}gf(8pI!daM$3wj>B%-_g_Y z?eio&$F5GQ1HUy344^w{MO+OIct&?HvRAy%?Pph{EYV)r9Z<_e zYNU$W>G7GiD3@uJl0Xy)+*A3v*(2rabP%{dV)zrlivJenvbDJrs*HQ!&5mFWwx?i@ z78mzC7qJGtX|E7hu6BhB-+lQ%?mmqD^wzfkN7+A(7m%yghu5lAk>K zWy@a&TUx9ENy%w^KZcY{Z14ry>e{N&$?z+}Vz-!DY?jeAw3vJEBX~EIi1FW7@E!&4 z1-Q&Re#K32J%ub$G@GTyw^vw}ECd8C?tMK!9h_tMuQZ2edAPCHCT}Q1RgKTp^6qmd zC;-Os^FQ$gr6L)U5hw>N!xq?FZAWQw~At!P{zyp)sSs=(VTdSJ(KZTlNB3wefC|i}V4A zu<}J9Jdz#Xzze~j zoa&>oNFY_sd=sxf1f00~VFiD#;4eIwoJuqI5}en_9EKl+DgRFh4q}wfgbLw*_Y@ZC zB&bf#lyi#+1g#t1-0q;&UZ7hkV6p%|wI}#l<>YEmsi-C`j@%#5h@r8*$5(@%nLk_EXAJkm!lexd06s&A2GvVpnwYj@#tiS;6c90ur=G3+tWNIE^P;C_H}XgTgyV}qFbDQix$9zI}*!cy*20vr+{07)VNl3n`+ z2`IP45*#*?8BuZ#c)MkutqLoPo$yCtyEdTAKq-!(Pd2uphrS~q`ZDY_@<@vL5Qb~9 zSq3~XKYFYe_Uq}kxEqqRJPJ|rG^|k`f~C^;a8uopD%oz7Ti1CWv!|#k+qEd9z$$2? x_gV?lG)t>TJ%z8WYqk%`&qAI486lYYe>f4${6BXHX7$a+t{B~X3I1Wr{{SYleZ2qx literal 20087 zcmbVUTaa8u89wLCnVp$^P{Dg4DlQv>B$!PUEDKPOOHzhQL4swpgiSJ$h0QMPC4i_< z1)@GF0t!^XpoxfRNvU{!u%d`5i)Zgvs!$QURD4h$6ifU2{_gYt=XB4^u3OOQ)BRt* z|I&Z=IWuSGXZzE0duC?)ng7eT?7e<|VJW+=zcAOI&90nY$cjs*m$FWt6+7pbvU6u= zrWdo~nLF;y3Sl{Kd1iKLX6}mqQr4Ptlp8WX!pp0sckj+FnO~Y-nwg&iLtdOl&U10m zs*&zpo^6o6k)#)bw5*Xjz;&T#ot@>5Y9mP7^{Hn*anQ`2-`|s!H0cBVY^<0LW{ed( z!Rv;K^XBJgofKU4IK=KayCRavbNV z`^D%U$L>qmohXVq7mbW?UII8dG1cLmW%Ru$Q+*#u>U#|&cc|oL=)Q*Cm$N&8_GM~( zO4~U`+e?kMncdbp2wFqQuVOcXT@)Y6+ol^5c6 z+E}qUn=Fd{4Ovz&zT%t~ox{wWG9!|!Q`scsu0wMg2n$lXHGq-q1dimD`pagQ7kBg* z=B<7eu%7OrzOWK#T#X$TSoQ$_yri7GDKeO#;}QvPU#05e<=Ig{OM)ZghJe@d4?_Cx zCQ=F-j#NmfkPfc&Z0#c}6U(rFa#76e+2b>u3r;L`4#x+XA& zf)SOqT4~)fw|jXP3({C|nbjWFzRRVZ*@Sh_STVENQO*UW$Tkv)e0EzVDn1~_G9jVN zkY7^{cb;#%#%DJoc1i!zxjyoE4vCDv^)^IPF1NQW%ui0*jnR9Rw^uA)Gk@dy{!P~}^cNRV+VhCT;;u4`ili<%ZIwIQ zaPJ@qs&*}`pPqBE$DdztUQg_N8IjglpR*rU5`}3BM@1UC zU*)Dm_f4!;CWl>WKK<;2Z<_hP{L z%>AE(FV6!SUX09c)lztCfWVt#COPUUhPbljNt83VLPl&0ku5ZVq{gcf5)~~50x@r} z(ha|-wyHpW>dAEUgo#^#Pf`;+E10mse>|z8DUM?P)p2y2#3kr9f`hR;L*{XfzkDsP ztC;6!a%LDVDzEtwBMA?#02??7YmH)Iyxe7$zo~)k)Rk0YwNC;ML06hV?b47Pvi!F| zVOX|JdoXo@@F{o84dx4&dRGWC`8bRo_hQ|`G*jqCC|h1MyP?UMut zh5T%c<_AX>id8~Qq?~|IL+Qe>;-X2jXj{e^0Q;>bajlAg!tH7>Yl5DV*=W_kAem}H z8niaR!9yfh#gobgUHSKTt&8=?AkRz~Li#8lDY$cach#rzqmXb^Y`IXP?gsLsRT^Y+?mQHVllLakGgI185g6lR*aT`dh+L4e`+!lGGN#%ng!)DTkdyq$zocUS;)A@9y&PaLY zwR+^D)g2@%zZ7?gU=>hjAbHpU5)}fK( zLrL$+CLV6`=)@h4qL?a0xl$Vj`#9gs<`R^@

_p8IY(X`y$j$2@&q8T;l$f|oA925f!5nboqnw|34V&}-h)BYv2TcYZJaD_>w z&&cLf(||$sQRS47b2sGJqYeh|QzEmFN&iVsRRy&50QlXrWwe(^3ur({n#K)DQAr8G z!`9d-qjUtC)&P?u=@h}W&87tJ$5a?hX?=v(YUjsSuq#K3n&yiRwnNMqTKPnzf{px> zUJx+p@3kly0Q4X!7|bX->S59ANXs4vhkBeE#Mg>fJuV)Od?pM80!Yhb)i~TL>*it> zY*3ZG2rpTTeX8AhPez-x5Q&q1dCKZ-6X=SX+T3N;|yjXl!b?&#InP}#dl%T^n%I|>I@qP%vhs2A>{JCCq%Cn%uFkN<; z65abLhfU?M@;>{~5Xrs(3dk(KsOa2fR?25+)dDLY0i_)3ssp_XCq4%?&xE6hkjt1R z;kyZ}l}L_{GbIc+CoRli@VuNP8Ps`BSl z#4-Y=Qf}8YqCc-i6eJAh??C$p1?euc@;P2>M4ttD9MJ)f`P7y10#8Yb9`lP*`ltr0MBl`I{NJRhLqBXX~$ z3o|>HmumIMKVN9i`ltNu*<^(>$92XcI(E}mc@Czs` z-{b{7D%eWMyPbhDSsB@&vLnshQOBvgZj4p=d_Ee*^dIp^4|0Pgy=Q8m15Cec8|vyFs}MViGJ73qd~ z5ctAKfu_I;e)XD8iNBn{vCirRrmU6lLE!Nt1x6+h7kJ`GfofM%v?;raaP1I*BFZ?9 z+10#;ottX=MU#Rm4m&!#4G#O5Ylsc3{I$xY4l@Q)f;fP-Hm}VpHd9r-7&{B54ty*m z$*GEY%`_6nHVyVb8VpfGtk?!#@{e(9s42z; zlC+~tQ57aM8gh}RsoaTD`ELOA*IE%H%o?Ey(tu6VdsghG#b^k`?#JFfMGdOXi_sd> zWkF!(74?9uoNrW^P(V7T3*5TY7Q)myeL$Fu`885qX~@FB*wm6{hyH zHSYt@CNvwGVd|U??jmt-ve7;)@i!-(?f&MZvwhOB)gFi$Xb{N=2r3g7hSTJkP|;H# zbWEM??B1f?53$Qw*vC}=moly)zjaao3q=}|(Fg?BibCb0EXhks5!oQUA;~I4P1vCK z54GpKuNV$>pk(hN#fwhPHIq{@cubJ|X^;-Q9jJ7e@W`@Jl+8$q@G8p`J2g?~U}XND z6jYCmM8?W(?qV%6je<~77zY*E4U*{YH3Im+{dFFza@;)&9P}N#&Ql@5pNbM3l1#)+ zf;V>xlhq%A>Zh31*z$e%Hg;u+)*cg^hfK!zOi}L)HNKe+c750zXXb`Q>nGK19={nE z@j?n<`PxmgQBkWq0@l&nuebzGi20{U7m$sF zkGkhTePcM8_yLYmisK@YO_rauQDZk=mP<@q}x@e_H zxOeW{lipp|OfR?>gB6m$j}H$e$t6-u{mm#xs&L!A83+YGsMe%dB@4GEhr$dQ*nSiV z$I-F-l!=@3Gc+K1lItw)4GZ#R>UaQKM++EoD5&}sXV?SA;9TlM;q*} zU`!dL!EyHtyUhZ5`iL<08c*W_hcUpq5gf-ED~ygbM+u5oq&bXzMh7`g7|8+V;B)AB zy-CyHU8BH~3sQrZlMr%hxCbPs4in8`M`0xg?IH;5XON=}y4r4oVG}SA^d?k4^G#}b zRW5szQWxbbEG0P3sDZN{gZ#w4BY7-(47o?5`mu<6c*mo+t)@bUBl}}8SfM0A({AW0MbZi4bE;<((Sg}Hwz&ARL|w)t zx4$tJ&+B$oE2N(Ab3ndGE|!8Z+TRk}TknA1-q1zI2O&F95VbPu9ABunm-@spRzm=PJ*0=Vz%q`V_5y3xv=!JVTbcXqj3dMOE9(nrt86c3`vCnGvKJDJ0^wUp3 za0JayUD{l50}_W`!?#1S>*)6l?D|jKU?Y=8j3=$ZVv8Dnm!fwR&2MCFoMs%B_!5cg zT|fBk`i6dh=5HK`Z-LZ%0Ut}&-p1>e0gj*$u1WM|9K>Lm2XC#pvkTl>vl-4MyFkp8_BdgP1X^B*%H zLgB|1FnoGAw(-KqmY+T_u>DFK-{dP4I-C6sE7Mn;;RZLR{YxSyzO1(|LFFbQd{nz% z*6w3s4+h?h<}IZCijJO%(YKxw5}2vxhFsE;^7HIYqFu)>IT=dK_x_8($vuw2CY9+S z#(-$0inWUy-S1&QjN4p_&F&&Cn8`rFr;z%qV#vk&;rO@MHdFyR(}) zia895O(|aa#UPxt#y5FfO2)4qOM>YjO_x2XI%$pH3f#=sYO{I7jWkME`p19952Y#> z7KP6a>TaGZWJ%C|(aQ||1`IjG?l-mjgh;>um+m7Z!1pS~A6->am5xP{N)CV{LD}3_ zthr0IU>s6EooHrD3yG#tVBVUOfkcVfV-iQ`n_Q$yPI1$Sq#A*6*{_T|?FuXA?JtH5 zrkCP|`9F$v(T^1v=L&HWGIC`6Z#MbGH5{&zKb*s=H1)?lQ2mF4Oo`}@qq(4sZ=?R=RH1anDN3mHQzxbLD)d80kI$ diff --git a/src/builtin/obj/Real.olean b/src/builtin/obj/Real.olean index eb1548a6ce0e9dcc247aeacbb354eddcb46e1147..c095bf86a42146cea5a0b79c69ed8aa64f001b9d 100644 GIT binary patch delta 422 zcmey&(aJGlCMyFFFiu=h$jCEUh*6u7cd{LjSnDa|r_@ zkZA_w} zfW##bRzh_!GwXSPWDsr!^T4i@K`>>(Ot5Yq5K|b;B19>RZYYRHgAfu6DzS|m;zXkwyP7y%b=eI+ zqC5Cw`6bLfGa;TdNR1-rj(vQ;<0DU;(aLrbqpA2rm-jzi>gk70tu|CVT`NBkhG1qvaV^ z#4NC3muXQ>$q?6NDqba3nLNl0CytY zDlfieZ}Yxy#7ZV zAu-uQS=qwxBJ-(ph6veJWNr~<73HRk3rJ3esLVPlY#__IF^_|Xr`$-f3M1|usd>&!O0IRry%@B&w5Lx%xziAKckMB;WxToueVi0@G12Ca_*h$irk z0^Zwz*Xy??9q|CbBI}w^4gh?Q5~vD}hO(Mp$lZNF#?sx*FCiMP1!SwcAvpxD3+4EK zT8r=sTR#M?Rjc<}Yh-n?6(=3pN*8%*!xsv{VSujjPms*NDf`Z5TfYFiLEmhv4i z$nG|2$krd5RO;ha+kCe#>+(+Gru5(jF)XAF7m=&#TJ)@%nlS^fYtt&J+GX4j0?b8*k6EUV zKIH^Vk5OazO7;}ynCt~vzyRPTz&_v#z@(}-xM$50j?9Ui9jy6bw_RnQ)>MKR%--Gt z7#q1YJQz6#j2gX>IS0Mxko`jsuK{Nmb1;shG^4+vIPP%D-;A0f71OQX0lmvEE^Yx_ V?F<$cDThaJZ4UcgWbco7*uRfHHd+7x literal 902 zcmcIj!A^uQ5S#Lo2YC-PVW7n^31AeL1rtgLk-kZTTE%?)&8R5wcfY0W01dSEs3hSPR`!jgP@05uYTlcN z-M!h}8VS(36674ka_)`&Lyr9qIU)MA5T6qE%~^)AsTt#`3yI|dd~x~CeE4yw63)3? Uh&cH?|3DXnND52)a?AhT4{5?Y82|tP diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index ea7dea49c22971091be04ae1084ee7e2e15dd895..df1b25d15005c756dea9b1d329cbd21fb7130d2c 100644 GIT binary patch literal 16442 zcmbVU3zVHzb^gzP?}UjnmBfZ7T6`s$5FmmiNW}%@A7HYQc0w#BVOd!9-em5OA;a9{ z&Lo6D6i@`(T2}>e)kjNLQP5>Y#QJDyLD~Q+RisucSRN6psEf9gmL=%2`}@B0`0t-P zgZ8e)$v$WAv(J8=eO~|2o@_Oz#wR9Qng6*hQxkhzo#|GVZ_J#_vOIHHzO6lzCB&A9 zV5hCkPL`k9Zck=M7`^@6nR_NCXC|hy+DvCpD~q-9=A`kB)rs+J!^OL@-2O!;cXn$$ z%Qs)TtF^@#ffEap;0WORB6?#$qglwD$cc-0O-{6?vw3;b#I|3}z-<7seinTda6aoR zP}T^RMzy*-r#;i0nP^V|=kn9fAl1vs`iQI>dFYz=2@Bc<5@(!>WiRP7dGPD+3(`=W z0kjQvvpKD6kio+Sxgia*h=WX-XYiXJ2Pvro#2^ZaTv6wqPXd#zByM3wZtV`+dPuw+ zhy}|~E=JKy_{%S+bgv@EMHSgEI8jJ+KDt}!L)YF~!cmas)EEeR*-kP@9*_(qp(@5) zv4U)uQJz;+#IA;Ds4Ri0Z)ILb5L?ldPSEu4mB%RU3&%s@kb+PD;AuSMfBM%z+= z%ZVH8%lDxs+bP^z`zEGmrrElp&zR%4tj}2Ex7@2r`Cr4PfyhHRmhuJVZ0)9upk0P( zfZt%41f=VySjPb&36CcYTUP-j)k4fn{EoH%TqSZ&x0H}&t0~s83Y;k$7{51^l<=d6 zpfC9;azDYkRJk9z?xqs|6SCobmWqcS=_THP#p|cMiPH zo|xXgquIHz72VgxGPcqV1BrhD{sV#G8xzB`nwHfN4*1QdRCEiY!cm~)raXA1e;JHe zL!Uv2b#7~1@r9P;J4Ftu!q8`0O{%p_nThF3FOD3$!b7^O zrP)$!P);&FF9>@<;yGOL5*(Oi7ePk+cFxN$jKY>2fLM<0qx8{U(61s`0F2=X-RUFP zX8l_(y%^#Tg9NtFfH9~B!W1%KJ!uw_rL+hNOc*Ay+}vqSVP!p>=ULok{Cp)7-({%xuV9zcvk)m{b^}n?$6^rtIO53UL|2Tg z2aQ&T0Wy6%>PoloAc`yVja}R+1Gy6#0Cx+QJ)N;6aWtQj8(1wNKaO%0K#lTFfP-v( z7r-S_2)WN@HVP`Jk%F7Av}PH6WcTc87M&NO7$*C71Jt0`B=A~*3*$5|R-*nk6tv_h zpaR8*QFM!OwYAt3g#IR3h&J!D5K=Z16;euL;Ib};)Vees6<3t>4?!eJ|0sd)N#Gv? zTu0jX5**4)O9Wan&n{mtahmkwUq%e|8c2gPkGyw55@{*m3kl9wp;?Uee1 z;3@e<4y=T0er;{V|Hx%^@@>d-~xZFbxz^6j1cTpIRm8advypwn@t&NWk)LfB!O2 zbCdf@K$=j00kFTv4E`<bqMM*%*<5e_C1IMWBTg}n(Bl{FFS zE2K7VPCAq(j8DBVm?Zb+=5ogaBBiT4sb0AJ^^sa5K0CQVSI>%)BUXW)J&(jtF3bzsJa$hG-PYj+%Abw$02LU24e&WFdj|k#1(kUkAZ6vn5a9N1aL=H^MggCR@KUkgr>=JNn0 z%@-2*MFZWD5&>am)bsP{9qmhA*V?zM)0&>f$=D@^&n0V9Q$&aiE6mf$i85{vZW!{Y z#7A^77mR8_gRbQ?HHfOr(Sv0a&>fZN0L6rWp!P16@m9}bJfm|*qU(}Aly{?$*}jy( zdkl0(CLJhPvc&)~aHBh_hqP=@ovQ}GFwzu+M~BpWm(|jAx~RAK@+JOwKHE^YzuwU&||d#1L}%ofNT zn!-nW_-Oto@RbH%OW@ZHbZeEXn8mV!^3+IzLXHCDP{iNZSN*GOl$XZG*sd#^{Y{mwLqgXLGTsFENrb>6SD`KR8XTIqL(z{ z+!gqv)cRus-85-`0&s>PbKM>cu6Q3ELJ#_uY~oJhDI&PSHG8MVtho$*2WG)Gv_2f7 z+2(<=fnu}=Ir%I$q&q<4|C}JGo0^V@0YkC{MS)_lR}rG-2Zjv$O1sV3Gt+g$grmG> z1$UM7uCm1cfT?WxzXrKK(e((}dAFB0f!s=4Dh~5haS^LaXy<-(El{iq(miVx&6Mix zfTW^oSJ7cFprbAae+JN!!Z!TNQ3)(uiGSXPg7HxRk~W(G>b8O`M;UcIS|!pL$Ilya zuvs_`4TD4J3M`}*YI+?c5y1)0j&IeS-+G;M*^^??BJK!`ME^RlcXu%04x&|5idvY$=umK2DTeCx-iHn$ zEg#zG8*JO$jzNVJF=(^F5(nDqC1};~Qb)sGfM!3^5I{~yjT|k<>h%fjwF(JtIV>8}SU(HSv2HOY~wvuq0rcFE2MSfJQT`;sr~4zb{v{6L=*jM{%1j92FTAPP(H^q zXc{yo=S_oiig6ADIhsE$T8_0Z>L`s45QWnN<>*^3f*o8B6IJNl}kk z@eUy0%05pcGnDed02gM5Nn&#!mUU+lB;8_`6r7WaMO6L_BeZbZw9CGHnD9p+)u!wN z0YUb-F9470g8Z{KbIGR8S#3TW$vEi}j_#bGf;{MGPE)?$fqaUfQG%RIe{Z0hup%Fm zaZ)|_b7CdhZm@!rhuO(-OOj5Yg*M_i;+4$=0<8&tmVT221xkvR&KLQZwehqCWImP# zRp37ug zE5QTykd~aVvPXlMG^Dy41d07$d@xaW906dkDsy>9C;Z4-cW0TMX5GRJgS|7vBrC0^Bb^ z+?gn(6n0vd9w1>6sX0B!IDgn0-P#bq4?}|dQ4kg=l-eF6h@wED$@K(44pIQ3*USos z=Ypg)RoA?_6n#qbiZ^K`u~ZLYJq<(TX+*CZc)&WEGf&4klawH#s7Z&3V?zFt%imJO zO-A_(Kw{M0XtpzqPF!;3+d(Su9R#CSbKINcFGR2UdeHLuB=;x?f10#LU9W1ig5v=~ z;-pRmh)Nz)Cu^%^iv=^ju#ltGH93J}cdO09MU&vbA|BF;K14 zQ0m6;VvIbakYP(C#F8$MSb9s#Sh%$-eJP^nyo|d)j?T}@ zw3I1pVNsTqvh)R58Z&>G1||dAR^KZaDU*6u8mso|NLu68g7l@O9+?G$9NzQf)RTFv z+7lhQp);$P%GLYrZNSGzz1lgETlO3fd=z&dA`K(s!wLL|fwgleS^Btz`Kvaj*~)!E zR-g-`A>Jx}&|3UWiHWtTGq)pjPF)H%B}e=@>T<+Q1cQzCp;oqTK1Qv`;6)sfAB?2G zq9gJtiEP=NeSZi1Oz%yX&YWd;MK-|j@H(PV^!^rMl zen8hZVLvM4D_egYbs7H?1bZ8w-I!bk2-5octnRR2CV^H3fHFV(zUVw)*Bo;2rKCpt zSGxioCc?<>x$W;2<`mEtl$(Dk{Aq9!cssy1RZO4lx5nD7GX1Tf=w1ypVXYK1)VQz2uM7i}h-X2}5@$r^G~_ zNlaL;GJ%Z2J!Xx${Zlqdfu71!Uj!(l{7nM?)r&qQJFt~JILLeOE`WS()%VOK(9JsonMDC2`g<{;m^tsXikHYg6zuN4 z6736rwP0@rzl*Nf8pszO$O^RV(?R}tz@y>F$w{-3Uh0A16}$Tqdh{^?-2+h9r~d$O z4O{=wpxR?At<3XzXyzH3tdp9xr+|T)wZ~B$B9R8=jXU2l&?$%Vp2(nNhP%=3zq|E! z?Z2EI(C;ywPuCdCje6~IXr1ngYlo=Imw}hEUjZm(zY0*wK44H#79iBB{RqY5D5zG6 z>rcX?>ixia;jvdqe}`m!iOFLR0C6djRzlDD~F>O6sozTs}V^Jt=c@ z@S^n@Wv?^(I(M#_c7UuK1N-xv!x$8X%)_5E87vVC3UMFmg%~IHd-Z655YFm@C>H8^ z{BE>x{&Dd7f)JAhX00A_5H9s2LARG2pCrggV?FJ=YENj$WVaOKQJ8!)(8)VF?`0uW z%tC&C=}!WNfhqaM&-uEpOc+Xb*{H2YVU+ck(h%QfFM|IHP%-o!5b%*II|%UCP#mLN zgxi>&x#(NgoN|$Z-lla`u#%so9b%*Q3ot#Aa(ow{0_5KSh5#|JzB<|`dp*sU!eDh* z7*s7>pf{XVKb0tWr+#Wr?>wWvain~!(X#NHM8C=J@r0J9Mle5a3G1g)uO|%jdL05N zQ-9B(`f5m)`Aur_dtr?VxKm~OM?ltV9eCWDz3sP5jkhPqBwW|$5N}4`%(8BiKzN9% zZ=fNMwnlef8ass~(MyNW=?oO?&Oj_s-ALuW4^Zz`{|->f{Q#i$CqFc(zJU*zd^HQ1 z4b2MezWfr9BjNj(_>J(7yMaTW3RD9Hb4hyVs-K_a|8bJPL9v*~8x;+7$3qREi+d2R z=DDeUzKyNFDy*N6Ve_2~gNA`w6VmYeqx3AVCo`^%?f}^w0FkCCp(v3%;HRHEP?4wf zP~WgV^)VA-s>Q1wSsbliZ3?vmR2QMxuKYy5P^$U_XqlGsM`<|V$^u(8cOa6GA?H8I zc0S6LBdF_Bl3o!+T@XCwbe}R!MOFW_1#-G^uK~4Z=&Jujqax_P04jo>0jLQ2Z-eSr zC?pJY$l>+PR@6u|7{bQg$9Xv z8#N$*EAUER2%-AbR)D1<7%#|#>eoe4YoGT*@v$>z5}^@&M<+2?bTRQgM~V%6yib%HX7cM6gCyy5(-a!Y@y>_(=>*5Usb@PB30rvLx| literal 22239 zcmcIs36xz`m3{C1seV<7gg7xYLXrxI#*i?zGG=7Z5Fm-5Ez%XJKxw5asj7r262x9I z*op&5)aNTYqu9MpNxoQ<1*_ndgP;m2uQ^)9h^1SOBdWk{r;7P6Q zoF3b`BMh2OJ9i=}3uP_s3?>&0nmm~*CsN!Fh0duT9HaBe^VT->(%L0M!@UCoX7CKf zpDM#r}A3WE=!?Gr%GVge@=IZmbYlr?CLwMe`FLBWUFN}J?2sNZjf`7 z!-e{Hk^Eed`X*8-wbG%!<&6q^Wf9VaoUto!hmL=xx_5x=B{>D;;%Hi+Zs5-z_BSmg z>VcH1;O^lj!D}&LPY52Q-f19*NKOa2Ob)g%WUBQR4SDkXt0GgTCNoa6nyN@Tm;H?S zXf-=*S`y_N!L!Ec6p-OI^FHs5n>2;A+5ICYp3*yfav#&9AoN@tpQnxLY0yBCsTcXK zAaYi(m1v)EPGTIiwHN#W4oAcF1f zI>`nzy8!fI3r=4O-=o}`Y5hq$(c^9N$`wZFi)u|E^IEX9LG;4m-oZj~m+WcPY!;Om zp`hAil@cRPWcnCk*i(m!gWXS$@7cxt%GHmU&?@Flnl3!W_HM)dEBku~peacwF}Aal zOj|=WifcvRk$rQy7u1?LF6rP9Trv(@m4I{3yf{gi0n?aRD#Ii>8P2wW>AcAtdJxw= zh}yaJ2&cgPLm^N`gXRqM7ZUR@NV4p;OG;fI2lXM6|HiJO+RssBES`g*!_soaaA7ZE zpmPA>4vt9()tn2BA0c@j$N`e)ix&+`Wy0QyBaPy4>h)Rp32-t@bC$PUh0-%a1}K+l z5`@tGjA}m#F=vwe_dtFML9B&E9B{27P zx_N0JFAL-sgY(}&>o>{!C6IUa;JOB$75v{QM=uE2FeTEh@&5}Z&ig-S`B-`JsQ2H9 z7UeAXt2_z!QA%717apZgR|WFRfm{RfS7f+4K=C+QpJ?m<^Rc5%@fR%Z;(vvS_WsWv zTCsS*3aBkoR?AstN=b)`K`0-ZSv2ul*!6d5kBVcPA+B!4& z+tH32Vm367_Zbm)a896iC#?ZIu^wGT!T+%eB z&%REtV>74vtf9ft;ofCKtxhzuS>|NZBZG_$o<&Zoe19F%XVHh719?kuayDA$$frmS zd{5{fPYIYFyrkwXACt19<>ET|n|mkly?0-Oc*RbOVRJq$_DRhs5*wqYC&3z`CVy^+ zyc6gTN>Qdq$8Un{W$U*z3=NC5B{_!%W)0Dy7F_ZiyUl3XX-6<-{j^qzwh}Rr0wEaW zfRc&d2DOsL+!@Hb;$dh$6_?Xw;&n2yo{gL`bn2A8)0PeQjf~(F%EdE+q8KSfCJ)NF z-pyd2R^k@2i!2fiN8I9#D8R}K73te(WhiC5Rk&M7kNpiY8v)DFzXNJw_@}pme_ea{ z1461pKY+k>48jisxiK~h&8z`81;=3?XS7oM_J0JL-w7D}KVb6{YXb}wVpcXj+zPJy z3loZZ8T5leMmx0sg0TCE){g`E6Oa$E^`{^o6i!jv1l031G{z)*!sC|fNgL{67)K+N z{ob>CAt89SV(`S#mXq-%WJ7RAi3o+7hWCSdiPk?5$Okn54S&Mr&$9FmnNX;D5T@eP zSk&%AbEAc=^0icMXQ6WR=O(69riBj&@)x;CyGIg85&sGSBU6haF-UDUG8ip;ADojTUnpyAlmo4K>l9IfCijEm5wFD z9~5geyx&jk!rUoYXEb-@SA!qVfgyw(2a&BdKBc8@iw~l~Bgv#k9)Hy|YuYOh37d4G z?JvUWr6m6t$d>~7r{MA+T6G@$XOJTt_CFw3#?!LYV@>f4koRt9SUM*zhvgPUAGnki z>NdRd z-4&ySBWO*5pc)E%GJ|~8{+6yMe4DFi_`7(~d;{(?ogloR=^Z+6hApX{4OWA(bTcKALMjZ*F%Y2UpS(?Ab`N4Dv@LaVgzR60Vl+^@k%c zgPG`Nx!oqmvXPJIbiE|=XX^%?3XZcrMSb^y@TUUN*;m~5$!?IpC;2*%FUAflPw5Cad<`%@?^C&2m79U}REc6X9Bz+hLo6y>VezKf zt((h0DGs}Uay%fkev2d!L~(#ar4*}5AM-5m`pi0Dd?r?T&DAXj-9;c7fb z4OR4iDth0crAc+D88>Gq23^*G+pcJ8z-`O01&|aDx^KhuiYDC?3ZneHDaud1-@u;R zz1ASWc+JuHT7%%rW0Fb@BJ&Pdyq4q?kT;N=N-Xz8!#ZMlBgmWBH!bvim3=tyaD8}q zF5f~n=K8H9@jAEs4U+qSykid*lo7pD;wmjfNy^uV#K7{;w-Oitf!H&ujLm1r(MXK*Dunk3DiG@zs? zopzyaA8Sn=7iFkQh}M2alwT!@@=#IhyRlniG%LWd!iT1Ge~=XlPqz`WN?$=FUv&(q z1=#qx98_LU+$KRSN`VTl%=7hNUu$+7S2^p~hAn#QOIDoQF#=H$JWift*P4 z5T@GViIcp*R=UabOZ~b?1w0=hoD(1)p9@s> z(bn-eqm#$6l>CC}@AYKZcOK6rXW%e3+`RwQ{(J`vALhaL?iA zEL)dbGqs#^p|4C8V>hsj?6rrE@^?DM(Hq$JWD` zh3`k-2XOfpwjNF}k3hrmB;UiBeFzOF;L=<{rh`u5J&_K~|BPNiVh@1?P z8TwY*t@RI$^i&50DX>c_!?>JQ$$E9C{m44`t8tKC?y-wK#84A1_)}T!9%3rzXilI* z6E&y&>)~{k_4&Q2Lba7MBVR0C5TqcESrm+;VAjP1_-K%ql3W1tGLj34@)yzYCHXWd z%iLF1imcDT>%f^zqRZ5P+i?C@`HGK0;85~tw(Lu3Ji$rdX9Fv@M)JyNxPdt0l7loK zH)%S5S+9Kw>5dh2hfnuJ*>`p#@FkllXFoT4^M_{*@uLD0VbUxO+?$Zfh7M#)52c!D1e6@LNr1IO?0x~Gpxdl(h z7O0P6@%S-+c*e-c(20g{6WE*G!9-=VL%pRLQDY#L;0(aYFmW?U>{uPyPtu1)1HzWZs^$;7aCu3F0Ea=MuDeQG0S{tFFxZ`7ZB4lE~gMeU@%N>uD^Zt>@e&G{4z6_>Q>vB+dXBme} zDjVz}ThR*%W)}q(Ll7Impf%uk9>#?A#=cr}A#m^JT!{!iO9VA(DjweOElpJGSUYs# zOj==@s_qL6RJf#iEiP*{CBnU#px)Sb0vs-RDXZS-oo3;x-o)D=axLY0k!wBv;8M&; z$&+JF8POL}QC*4sfmMu(cDZLl^mlzZz|H!C^7Ux+HL|+C!5{0Ausn5G7^`c8*Hq+thi8D_YE>AKOkU2Lf|`UwtZS#NwA8 zj|Q%T)u(uTlAeKv>NB}53-P0bW}Lw#Ku9rfK8}$uoz73W3ZCY+WZN-t)(r{2+T!WC_zRaFHvj}8VV=Bud}tx_82o-U_sg1 zyaY8wf;<&7>vWdv|dLT zS7Pi-Z4ee;$i+?2giRv;t!;{fPWPBUp{#Jtt8H@pVIL8|jz$G2+nG=096^d$UTtJY zy$zN!C&#h_uYt4gqIz!7nWBj$j+EH%c6iREQ^Bk8pztd1)N3h98^_F4{FCG zfvT?s-7|s<#o=Q92{a_^Wcyu(MW)0-sI zc=vTkBrcF?ka0SkO&VpOMX1Ntu{Fr>dpu&WN_cHqY?P(WX^73n77L(w<|BBU--IrP zkdD1mQ2B~m2W z`OT;V8A_x^8Kx#qBqxKd!O*Qqq-L>EB1K}OxV91-C(``kc6s!0A&Y5DvWvFf z+;g~VAxdnZAK!tkFO&Q($q;kp&CanTrA#DA4PlJ(pgXfzj;TQZ+Cb+oeHqS!s!8q)LV0C#Ju? znrQwskUxtG!FFgq8<$oKO7SOLj9DlF^$V3HKMGlLVMCVu*aU|x;RhS7^5k;lc$@4F z;gC!B!`92`(gT5f5ad?MmRd4zW_>I5yTj7j-_XL zfG&Ls4KE7%KZ1UV(El0aUmBp_o%*ajnIAzPwOWs$-)vN;`#P-$13I@I3wpfctZNKZ zSXbGkUjP6 zz4nvb_GA4`QS}8) z&UBm;3%z>1tvupGXL?^W)Acy}nDKRynI}%??y*_c zm;M0^-;WJL!&EKd&$1xWRLv=0qyK75VF}l_B(}Vb1za?N3v=wD0%`?NAB&8W74+=y zu=75UOvTOzo9aYC&C`(@C(;HdlLBOUX>z}xhz1akWHtu)qz_2u<2FSj8tR1f1x-FB zy4+TmOTe1{u|~E%`aVLe2S6_6b|#%g z`N}V{gyo`ZDGkCIM%PFX$Iq>^9njifF&b9jvJ#h5aXC{4+b@4X*f!9`ejF39=xU0w(!O2;+5?uPc8?0StXyUJS zMxZIuWER_htku#!on}8GfArmk{L%kaqz{;>40^N^sM2P35s~7ys_M2pUEeF(u5X#? zVI;%M8|;&LOqd8hnWt}jDpz1&RnU-Z5)Z!#jec7|sLr4!xuz`&cDYFx9u2!5g`7S1O0Yxl)55SwG|tEF zZgz{E*zIcLx_CI2O#t~fwgStpS4j2{SDtluy^7||XsBZk(#>;O{tpW+OacQI-EO8m zf6voh_0uC**-$l%UE(Gbqgkdn21qX89wF@>N8iIdr0=N@E;{w=Ts~83mPAF!51vj; z3uy7P^etDfxav?>wg(KGTl4{VcJnMuzYU;Ihk#3ZHFh^}9Z4t2u#GcO1*dF|p4t?D zCbSBY269Y{0cT2^8LN5qP%-0~ey*%Qp3>26?y_C1rA4xHf5*KR{_n9da=pjKCrj;b z{6v*!_*o%AHZqcw0Z;oxX!r~6AmZ^*GUBp zZR?7O$@YQdh9ZrIHMm?I;fVXSxLoe7xm(ukvUS$@{F!1h+y~U|TqT_|c+y<_r?&qG DRUL+( diff --git a/src/builtin/obj/specialfn.olean b/src/builtin/obj/specialfn.olean index 5b301b289b47b779184a348b991002a09b32d75b..4862612d78045efc3e3336abb8e4f49f06037e5e 100644 GIT binary patch literal 768 zcmah{Jx{|x40W83stf9X$^Z*W#70&650C(fg@J)JI+`n-xL&H<6?Nnv@|URXBuFI{ z87x2h`Pq3%ZMAYMV>Pr-^tj&CO@I&GIBlUtPbzfjvsM;fR0F7Y8^}-rBG*KKJGOpf z6fxQuY28|*JmB{iAQci(@x}@FPOku$wHK7)juXh4oI!z!?D5-IfQXt!-0Y7jEAz=z z%n_XmWvEN41H^j-3t-`(+BLm!K|@(iF{Y5prV-_kw$}tk(ZLWEClpSY=Jk>Q9MV{O z#8=!fVIr!2m`;=_g;v$LcS3(;`S64~Q#rYJV!gGH$Hx77Kme{6M23_HFDM=JY3Dhz z%-Cu9Uj1wPBb&u=RaGP+$6iu))p&lhE7;7e3WNO0aOH{N^`T*5oAfQi)tb{Gf7>>e;g zFglavjLv8;JX#b!@?I8P1N;4iTHq^N~I1;<}4VlG-vo7_kmX z(#sEk7M_jTRjqrH7vJbXFJ(+|Gcn}^_W|0q2V<~R3`YSg8`$^F*)sdM*B{|};EP#2 zIRmQYq?$D(!GxhD9HE(n1eesnS%MZ>jBp$h&_1- { typedef object_serializer super; -public: - void write(optional const & a) { + max_sharing_fn m_max_sharing_fn; + + void write_core(optional const & a) { serializer & s = get_owner(); if (a) { s << true; - write(*a); + write_core(*a); } else { s << false; } } - void write(expr const & a) { + void write_core(expr const & a) { auto k = a.kind(); char kc; if (k == expr_kind::App && num_args(a) < g_small_app_num_args) { @@ -369,27 +371,31 @@ public: if (kc >= static_cast(g_first_app_size_kind)) { // compressed application for (unsigned i = 0; i < num_args(a); i++) - write(arg(a, i)); + write_core(arg(a, i)); return; } switch (k) { case expr_kind::Var: s << var_idx(a); break; - case expr_kind::Constant: s << const_name(a); write(const_type(a)); break; + case expr_kind::Constant: s << const_name(a); write_core(const_type(a)); break; case expr_kind::Type: s << ty_level(a); break; case expr_kind::Value: to_value(a).write(s); break; case expr_kind::App: s << num_args(a); for (unsigned i = 0; i < num_args(a); i++) - write(arg(a, i)); + write_core(arg(a, i)); break; - case expr_kind::Eq: write(eq_lhs(a)); write(eq_rhs(a)); break; + case expr_kind::Eq: write_core(eq_lhs(a)); write_core(eq_rhs(a)); break; case expr_kind::Lambda: - case expr_kind::Pi: s << abst_name(a); write(abst_domain(a)); write(abst_body(a)); break; - case expr_kind::Let: s << let_name(a); write(let_type(a)); write(let_value(a)); write(let_body(a)); break; + case expr_kind::Pi: s << abst_name(a); write_core(abst_domain(a)); write_core(abst_body(a)); break; + case expr_kind::Let: s << let_name(a); write_core(let_type(a)); write_core(let_value(a)); write_core(let_body(a)); break; case expr_kind::MetaVar: s << metavar_name(a) << metavar_lctx(a); break; } }); } +public: + void write(expr const & a) { + write_core(m_max_sharing_fn(a)); + } }; class expr_deserializer : public object_deserializer { diff --git a/src/library/max_sharing.cpp b/src/kernel/max_sharing.cpp similarity index 98% rename from src/library/max_sharing.cpp rename to src/kernel/max_sharing.cpp index a09546a9a..0e7f3e74a 100644 --- a/src/library/max_sharing.cpp +++ b/src/kernel/max_sharing.cpp @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include #include #include "util/buffer.h" -#include "library/max_sharing.h" +#include "kernel/max_sharing.h" namespace lean { /** diff --git a/src/library/max_sharing.h b/src/kernel/max_sharing.h similarity index 100% rename from src/library/max_sharing.h rename to src/kernel/max_sharing.h diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 15c95b271..629eec3df 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -1,4 +1,4 @@ -add_library(library kernel_bindings.cpp deep_copy.cpp max_sharing.cpp +add_library(library kernel_bindings.cpp deep_copy.cpp context_to_lambda.cpp placeholder.cpp expr_lt.cpp substitution.cpp fo_unify.cpp bin_op.cpp eq_heq.cpp io_state_stream.cpp printer.cpp) diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index b3e14504e..6a9d5f7ed 100644 --- a/src/tests/kernel/expr.cpp +++ b/src/tests/kernel/expr.cpp @@ -14,8 +14,8 @@ Author: Leonardo de Moura #include "kernel/free_vars.h" #include "kernel/abstract.h" #include "kernel/instantiate.h" +#include "kernel/max_sharing.h" #include "library/printer.h" -#include "library/max_sharing.h" #include "library/bin_op.h" #include "library/arith/arith.h" using namespace lean; diff --git a/src/tests/kernel/threads.cpp b/src/tests/kernel/threads.cpp index 749f819c3..208dc4de2 100644 --- a/src/tests/kernel/threads.cpp +++ b/src/tests/kernel/threads.cpp @@ -11,8 +11,8 @@ Author: Leonardo de Moura #include "kernel/free_vars.h" #include "kernel/abstract.h" #include "kernel/normalizer.h" +#include "kernel/max_sharing.h" #include "library/io_state_stream.h" -#include "library/max_sharing.h" #include "library/deep_copy.h" #include "library/arith/arith.h" #include "frontends/lean/frontend.h" diff --git a/src/tests/library/max_sharing.cpp b/src/tests/library/max_sharing.cpp index 3ba0f8762..11fc67302 100644 --- a/src/tests/library/max_sharing.cpp +++ b/src/tests/library/max_sharing.cpp @@ -7,8 +7,8 @@ Author: Leonardo de Moura #include #include "util/test.h" #include "kernel/abstract.h" +#include "kernel/max_sharing.h" #include "library/printer.h" -#include "library/max_sharing.h" using namespace lean; static void tst1() {