From 6d7ec9d7b6cf39a1c96cbd21401fbfda103d891a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 7 Feb 2014 10:07:08 -0800 Subject: [PATCH] refactor(kernel): add heterogeneous equality back to expr MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The main motivation is that we will be able to move equalities between universes. For example, suppose we have A : (Type i) B : (Type i) H : @eq (Type j) A B where j > i We didn't find any trick for deducing (@eq (Type i) A B) from H. Before this commit, heterogeneous equality as a constant with type heq : {A B : (Type U)} : A -> B -> Bool So, from H, we would only be able to deduce (@heq (Type j) (Type j) A B) Not being able to move the equality back to a smaller universe is problematic in several cases. I list some instances in the end of the commit message. With this commit, Heterogeneous equality is a special kind of expression. It is not a constant anymore. From H, we can deduce H1 : A == B That is, we are essentially "erasing" the universes when we move to heterogeneous equality. Now, since A and B have (Type i), we can deduce (@eq (Type i) A B) from H1. The proof term is (to_eq (Type i) A B (to_heq (Type j) A B H)) : (@eq (Type i) A B) So, it remains to explain why we need this feature. For example, suppose we want to state the Pi extensionality axiom. axiom hpiext {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} : A = A' → (∀ x x', x == x' → B x == B' x') → (∀ x, B x) == (∀ x, B' x) This axiom produces an "inflated" equality at (Type U) when we treat heterogeneous equality as a constant. The conclusion (∀ x, B x) == (∀ x, B' x) is syntax sugar for (@heq (Type U) (Type U) (∀ x : A, B x) (∀ x : A', B' x)) Even if A, A', B, B' live in a much smaller universe. As I described above, it doesn't seem to be a way to move this equality back to a smaller universe. So, if we wanted to keep the heterogeneous equality as a constant, it seems we would have to support axiom schemas. That is, hpiext would be parametrized by the universes where A, A', B and B'. Another possibility would be to have universe polymorphism like Agda. None of the solutions seem attractive. So, we decided to have heterogeneous equality as a special kind of expression. And use the trick above to move equalities back to the right universe. BTW, the parser is not creating the new heterogeneous equalities yet. Moreover, kernel.lean still contains a constant name heq2 that is the heterogeneous equality as a constant. Signed-off-by: Leonardo de Moura --- src/builtin/kernel.lean | 4 +- src/builtin/obj/Int.olean | Bin 1480 -> 1429 bytes src/builtin/obj/Nat.olean | Bin 22862 -> 22847 bytes src/builtin/obj/kernel.olean | Bin 49170 -> 48642 bytes src/builtin/obj/optional.olean | Bin 6841 -> 6798 bytes src/builtin/obj/subtype.olean | Bin 3026 -> 2994 bytes src/builtin/obj/sum.olean | Bin 9146 -> 9131 bytes src/frontends/lean/notation.h | 1 + src/frontends/lean/pp.cpp | 12 ++++++ src/kernel/expr.cpp | 44 ++++++++++++++++++- src/kernel/expr.h | 35 ++++++++++++++- src/kernel/expr_eq.h | 1 + src/kernel/for_each_fn.h | 4 ++ src/kernel/free_vars.cpp | 13 +++++- src/kernel/kernel_decls.cpp | 2 +- src/kernel/kernel_decls.h | 8 ++-- src/kernel/max_sharing.cpp | 3 ++ src/kernel/normalizer.cpp | 6 +++ src/kernel/replace_fn.h | 8 ++++ src/kernel/replace_visitor.cpp | 5 +++ src/kernel/replace_visitor.h | 1 + src/kernel/type_checker.cpp | 59 +++++++++++++++++--------- src/library/deep_copy.cpp | 1 + src/library/elaborator/elaborator.cpp | 6 +++ src/library/expr_lt.cpp | 5 +++ src/library/fo_unify.cpp | 4 ++ src/library/hop_match.cpp | 4 ++ src/library/kernel_bindings.cpp | 5 +++ src/library/printer.cpp | 7 ++- src/library/rewriter/fo_match.cpp | 2 +- src/library/rewriter/rewriter.h | 2 +- src/library/simplifier/ceq.cpp | 4 ++ src/library/simplifier/simplifier.cpp | 8 ++++ src/tests/kernel/expr.cpp | 4 ++ src/tests/kernel/normalizer.cpp | 2 + 35 files changed, 227 insertions(+), 33 deletions(-) diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index a0ef26c56..057dbb82d 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -12,8 +12,8 @@ definition TypeU := (Type U) variable Bool : Type -- Heterogeneous equality -variable heq {A B : (Type U)} (a : A) (b : B) : Bool -infixl 50 == : heq +variable heq2 {A B : (Type U)} (a : A) (b : B) : Bool +infixl 50 == : heq2 -- Reflexivity for heterogeneous equality axiom hrefl {A : (Type U)} (a : A) : a == a diff --git a/src/builtin/obj/Int.olean b/src/builtin/obj/Int.olean index 83995e037c25b804834c635631b8c13c21800122..e1a16bf66c18036fca893e00d26b1b1a6cfa71f8 100644 GIT binary patch delta 152 zcmX@XJ(YVyDT_A)5J)ik7bJoh3^H(*Je;KrXKBD$oNyLDoFy{(C5tYPKFAm=b`WVe pS&7w}M~@*THI0DB!vN{1jwvN@iJRN@_8(P+}4aH$4?u zGN%NYmk#8mq^2>jF!?2xFibwpqQqkka)T8+h_syilf|0Hi~+0yBw#w(fz@2YngQ-O TQ&hK_g5Bzxm*SS0lga=9aS$gQ diff --git a/src/builtin/obj/Nat.olean b/src/builtin/obj/Nat.olean index e351cb21e39ca0e8addb534e56bf4557de375af7..f9391e528daddb09b4a056a613d61c29ce116217 100644 GIT binary patch delta 1136 zcmZ8fT}YEr7(VZIKFu~$*_=AXIoNNN6EHIYk3uMRX1yc#ps$j(KgcjA^gKpl_w3`Zf zX6Jb8*w$2D#A z|6pu)f?-*3{Vc&ePM@jJ@f8dOtDy&P2OXB4Tw~RuK58i@jwIW+s7KA-i<06L!)F1k zNL;TOPj)nvXiYI3=oo`1Sf?m}cvm?ga7?iqlLlQ^qxw{(Vf?1lLlO(F4w+sVsND^q z))Er;V{fR+NmLp&=(^pnyVw@9ij{QI(IZdp|pU%LT}+c4t9EPO_K0PLbXBo=t$ee{JU k0+9Q{jO%>iein{I*sd@>5ZfKbqS=T_E#T^nv~&yUAMHQY2><{9 delta 1115 zcmZuwUr1A76u;;0yPG(PWOCh9CRT-#fXHez+R@*$9f1Stpt z)6Vt~1Qij48H5G(Qf8W#+NSlKNH0N9;qyfL&Mnl92K(LLIltfe&bf#0PESE`3ZB^& z*(LCwL@-3)baPWG~FEDVIVUDaJg5m*=!g~VXfA-I` zZDmU&c}dd!rT_a$Cnr-0R&~==PW3~D-;~71y~p4SMh;op*fJ#&`^j*PKySUu3HwZM z0TV=*u+?XS6&&ww!!tg{Ytug0!8Luf5pLM25}Z{>6{)_2FMMx|vqa}`(BE$Sz^P#d zKXutmY?1go{Mls}d86-sdtG_woma3vV3Rkgvb<{^9t&QCJrOek2iwgHl%`(nBZfT1C#0`G~lyN55T3@~YGH&o}W7U?+=m@nQ zw^e89Fq%?oCbp%^+goQVq%;xGdLSsc@USguP^q;7BCZ z+{Y=4Rd!$nU4IUJZh%E>i@IP515rC@c!6^b$D$38#Ya(9UL&WY@-9d@tnF9ptFu`= z-~SZG&>D+D9&@oH9r=B{T5uAGHDZ>Y0@R2}da@H7q=H#I+o@kL={}ZX9ZU3JmWHs{fBe~N7lPJbxFpY_L55F$= z;_eo@F4CMn(IC+Ulc=Nz^pXW!k3WD397*^cFG;&u!x2uB2s)(?Q+h>k2Y)539#Txn eR7wE#Qc_@gn7yp+4z={|D8sGZT&gF-(|-WJYtxnh diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index f3ac6fb14a6b0a50104294e83dc8d2487722e613..ce394517b6b79456eba540bbcd1751c252363593 100644 GIT binary patch literal 48642 zcmb__3!Gh5b@zGQxsQn$tAMCzLx9B5C7GBafIn1q=Gf}%tX zGz1^Wrws}|Q9%*gT0v_?0bB7=d{%;1B>~$?QG9~7KKR!E|KG2B?wtVrzWjdKv(DaY zueJ7i?S1yy=iCkJ#=BD!lk3Ja_b=Z(HF@s%^vrlxoR#Id)ml-k+^{Jd8=uIEGtb{R zepc4;4eZoGS*%|>Iz2s;6^7Q`ylzu=Zg)B>j^D6honaF#XU*#Ia~5ZztiFGLh z(ajD;k2VS-v!LJ|&tcfw@|>d_Kc|-hx)Hh21o&7KIl;LAJ54XNxL_dopRrY}JePf} zx^Ea6G^A1NlWkg^75#$%xy~Ud_eGJ&PdT1|N{Phw&cVdMm^`wV;PJrB!NqJbI&i4L z2$5k0LXV5r$Ky?GpMStTZ|Vv8kJN z@2;Ednj7D}wgAo)!*%tLW>a8Ck@>U>)e)?`XTI2jktByeA3AqZy9fQDZRL9UWgcxqd)qXcfyc zI_*+Wrvj8(aJh)CdmKQ8$8!NHJe~*e1Pa!Po~zLEG9GIvmiVNYi3#)=q!a}W8Y>hM zqF2+$E_yEO4`Ac-YbLt;;t-32`HcyZBkUAXrS;vSjCd5(- ze-SD~^;Ce8^)!HsrEq|y*YYWL;gkQC$(ctt$2vmY#sMq}9>F@&?7-H{tUf@T(|BVq zB4=8dEz;de)Gj)d!oC!6ru6s}!sK3p^7>6d{gw{d3)$Pm#J^)HARw8Qj=7e+#!xF> z%=rQtLB|r|Y<4rxmAq>Yp)7EPEL+R*%>^h?yy8|_jm0A*TeZQQySs6NGSzmUa$@#2 z(jbr>i|CN#i#1?SF(xR;gPeoYPg=F(A+PUKY+Vgyv=cQzqH{UQ4Pc_NZ;aqM081iF z1Kg=e`W1k)x%8z=0Lp6s1?i^jLJHV0t@y@*t7dZxN+)AX9TZA|$jMVeZ6rglIE4*CGb@ME$*B&OfDf|U~wY0 zD{YOtYJ*K#qpQyLS6>} zRAr3;krs)}T%wUlna$UaZj zpGEUOqPPjgr&;+afH$MK6~!$m$bWi#X2ZI3#}AL%P7H3=iV`TS(D4e2u??WCdr<^0 z26(#}TC>PbT#kAFdc9p(EFx3RY+gBoWV8ebncb?$*1^>+2;)>iFIAqJ4|Lkz616dr zwhODIy_5xr#7=8H>+QhE?H`g2nQsK8?516--)ZzK43 z0HwE&0Tk}v8RK#wkT8|~Z#h41Q40sMwcq_W6M6;}}B=h(KMcaZ_B z`cuJ8(SMtPZp!{b1iuLI)G)Knt&KNon++Xc2W5WVE^J1x-5g)QS#hic>gVhC#yel9 zR%^@0F&kq5$^MOZ@_1izDxDg{NKtg`tJ?i(i8Z#0W)y6XZH_e_dJ16KJOt!)vmTKvSor58%H2jUxMz<;p*6_82IV^`?|-3IOPBiqYDW4Iz{g1x zl-gux0LCaJ#|L!_vLBGr#T_n##6Pr)L}J^b_R~$i( zBq8T>zd)rd|H}wI0ECYQPn;V?tSK@`^KqBJPun5;-TXz#Z`i*any`!uu!6b6gG3Qg|*0MLVR@j~e% zGp&JHnS>{_pO+};qdD^zhm6iC{3sW~qUH!Su{AxUa}ggS}FC1qLI&n_99CI1R_z;KWbh9RPKFbAM? z@ECy7!9E7%cd^@JQTxd5iJ}fTTq**Z56LEP+eH}e_&J;Uw%L>pxxAK8%#4hi{0~6t zh8UzHxK7-TmL)&7ko{J#Xy`?2x$$$9MM65p8Um!U8&PnNT&sGq<+}Ms?bZnoTU1@( z_N^Qiu@Z%M`uy>BA;y+k2MrhlQV!<;dDis*+N|IMnTyj zwurG|YYc+OMh24HuSd@U!z_kG^3|vj39gyLS~uAsAgz}Iab#~I6T`2EizoDonyVE= zbPw@Q05gVdfeI>bb!KNtC#bVTWdTA3pIBt9$-V#dLu9Zz#-S-VYjS0=Z?$AXY%qUQjV5JyE2 z?26Ns1hoj6J6tRqomsu%yv*e;An&wX)Z;aU5y|KG&e)bd$%e{{{*PbjjnB`7!7w-P#d? z{ztx|7VnL)WN?;fFO1+RAU(s|n;dpAZ$Uwa3gC{#2tToZs(3Ngm4QsS_N9}0V}OTKj(O4w;q*aqa4v_Zj6%q z1vw`T$$JKB1yV?XXIf=(5p8`Iz>5iDPRQrQ0j+gYdzRSM?I$2mI3;RxZI4}Mik`Os zE1CPS-iexzKQ_ zh~7hIHOKY$CvvH9xtL1kBuFLu2T%D+jF^H7&)deg%<>rAG8O*eIrvIiGoN4>gq2hp zSwxWJ>?V*V=YDBE2Bs67@ZLFy%*dchsHXVfe3V?C!*JbAc9|8|i4;K;AF1^Zd9JwL zI;~7Q(V;3(p?OCD5xu^~W+j{Lu+OrU6F@9JBDL1ok6l)o_(azNMnTIcn;d-$WfpbX4)q$AHRwg?7Wll6IVJRw@vWO!@FX}6; z%`0Fz80X4vF0#MmhH!}9R#qK*@aeDkAo<5{_&0Omv1lwBRn4 zXsZ)u5@rr}(-V+PYSA{5qHWJVMLT&C`w*$_A=L=Vxs&S%Y7jIW7dkTBnnc)h_d;6i<5NvMwQ|CiIe-c}@2vRq}swylYmdd{x*P0C8PcTjfx7&4jqR*(@&Mn>voT$I+ zaf!u@<_r1uXHgl4i)PIi+Gze1nuE1$C9Vuqo=CHiK^Sqt1QZ#F0vV73xkLuyPX=ls zE5xqdNcd2yt0_EWq<)lxp(V#VYK>8ELow5XHPPs zd%{4gz`-pCh)$MdzTA)RB~eNZB8*f5(x|YNq!e%PBJXk>9OhaxU8%UJms+O0g+WME zIgp{JBl%QdsRgk#0fCkAqz+uhLDhV=oJKRJPaGN@JVjHNRE`Sz1l7iEM_GR>33=^o zjpLyrVgVAxdssMRw}vD^X$_=!#@J-y=4i4V#4$&=RZdxi9-1OQ12B<`%Q@Hq_2nfs zx!5rNJqPiH?hWB z2ph7Q_&DC0_8k9cM93d?TPX1ax>6-Z_)D!moJcQ1n#OLP$5F956$ z_G+suB>|LGVor3zYN($>MR3MV-OZblHx#5_Ae@0he7*$GtrG#BG2e-^1i4VJo({bHGF0onl~MaP)?UY21}~}g?o*q0 zb1v&yoQ2d~udT1*Vrm{h_>-1i-v)#KP0y~EOUV_0wCB|0%z$^Bi zs95++d3PL}d?;KOXM>PN6Fb$d5gf0)H<&2x>G}R3kZ`Tx+ASgjUtX7YgLz`$L3~pr zx<*h~`7`eYvuE(=2+aF(gdc-#;t0Q?7=94Hi9%8@uA`et>W-jR5ZIbZGk6}OG_i-I z`58Lb=98+jx>9m!^86mKw0qW}9xV0bf3v`c4s2+oB|CqRXOt7<@ zgB^XW_$`^}uT+$9ycYJdhM+vc7E>$pUjeMEVSm&~GB9Iy>RCbj9KDhlti7*C3ALb# zN?3s|Qo?@&OqB36HObc1)1ZWmOBmj*Bw2_VU!EKDl`4J8aQjv@B?-qXDNZ_m$040( zR)M{i0NHYb${!@eBFKP{Fa3@km@IxD!G{Pw9TaXLhywbknlN1cAGl6#1$$@mFs1a& zm@(t^Ro5qTpgQmD!yPo81AoAL?yGAPIt7v0`>03tLgAAm3h84%fKgE2d-ZX*C*Obb<&{AlQyJp% zB=UfB7Y~3No(!W(i|Jm^j0Wwoysuu@yYfTzAa@J(1Mp35KZNwv`LHj;AVg?p#}cGZ zxHMpu1#QQyRj@r#9`?Jdv;63eT?q7dTA?`H8OiNLrH&YI@sAs8c|mf&%N(!`m}A!5 z^T3~XJ#3<`(H(f??dV{d)@qb^B&H``<3QCbBZmRp22^dZRR&cgz;>N~;7WmW6847q z%Fo~>G>GLNJs5weKaP^;1d3;%Qc8Pf1TkOaABCFolUN%HiHl2$=$FL>;>hmhbf9bwi;(oK6n`L&OADGBa0>_eLUiYe+~O28X`n9xD7QJ)pz68> zrTwATa=*{H53m4Mp8#Yt=6U$b4M7H8wuPol4izwlKr6{<)n_!2`KYFl5}m`@Ln%)~ z)1LZ(xUA~RiMdIY1oCF{NDuZmJaN6dj01tV6>iI*| zXTB8l$zEAP;uz7r${VNDfj<|MVmrjdH^StRfCK(+c&l!BU<0b!2vUus4v(Ltw^qM1W*pJk1Mtg<(w z&>+jLV|5*hyQ$%>flk9K4Rjh_1(1sb?veWrZVtLm&IQk~SVKWYQsS_*y<12Sv>(Y& zRj;r%|0$ZO)!mhooA}~C{VL1RQ}gTD0CNt2E@E6{9vWhV%Q)XZoU|YncqhhazQDa& zd!ZKpmR_}Va=s;a|0g9vbFF_RNTD6OcXc{|6em1_N5!~T;yKpXH_;8SA&RD7G@i81> zaRQemHG$)1$PM{51~!hMb+!V04#C$Ms3&37t5ADXvp6jt|7{#KT+AGv<ZSbqK-O7=?EV}ew@fb)tB6Z z{KgAHk6jDU@adM7#SSa-rC{YIC5{l;wZQ~H7FfTBIl6IjFrU4+dipZEbk=%{fiA2r z2UbPh<&6Et%TR+1!1<{0GU))7_7IX9ACT+hrFcpyh|UZmh*cve;~?665{&i++s4We zsWne8-iAK(bmb;ohFST|cA*?Jv0=KqZr$i3(w22**M#ZR2^XysK zc5%FB*{J*Kk#42-Wh)Bm31^2#SK^_;ve8wj<-F8*4QJMX%MS(Q^XSI!1Cpkgt0VaS z2!0@fA2hIWA-i1*FnLm}Y5FkWLXgI5=Ub_#d6@f0SE423;!xWF#M++7<#P>J1t{{4 z6^%>KTSHOrc_3ulh|Ek3$b6~qy9eEtqS$w#mF`UzgBov0QJ54OZ>*yjo?6~iZ%Mf+ zqtsr$(edaJsHXqro0e4;*IUszg+=dm{Y+Tn4Tul!4vDH>RnZKbFNN>L4T{E_>@pjH zvKu=A?t$ppZWI*?=B9`CBG=yli#i{nT=BYgR;}@-Ue>OY^=`ba#+2le$tpeHLna^f zOr?=`VZ?FUuJJ}(?ttN^X!*u=Fc@S_W?fpn&)}ee(KkMV;_bb{v(ofdT3f-mkZ&fM z6Y0HZ?qk+hoAnQIP`rlEX1bR-2q28m_((5vEugu7UJd~X17O~DvF*moG^9AO_Qs_s zW(fy0y#WPOC+Ckt(X7Q=y?*CJr^|eBFyiQ>Z?*btJsLl>H#-0U`t6T5t90t$o9!eT zgDEvH$YLao&!M;(6yk84`UYDD_{dm|n^0Vf;zmZt^#;;q8}RVPCw)eKuU&=rRVRH? zPPU34CMmmQ+XeYd_n;xqYI?xVQpnw7#9N%?Jyg&EFvm4si(wW2fJ!B0Zf^?w$5_id zG}UsT47TF4hS2yn^-bT|gOO|35FFB^ya!g5&`cRh$`B#j2GmQ@RrwoJ`>5nzTel@p zk%IPO|Gs33KA60-KC}0vSxWron(38UK;i$OkeAkQ5HZ@(@AvkWH5GI!c)9%HEe8XP z(RvTAm48W!L2-rEHLk32LVD43_Z~FAw-)9S1TFV6hNQ!7ATr3=X9-*Mr(rqR9W@c6 zLaqVgwN_-dinh#2<2H7a8@(YhE>Lk)>i@S{p;?(VhO0t+5m;&%P%rbIT1vEh0R;FgqyMf4@v6_LD0Md#p{?bzG$FJ7+;Fumm~Nu z5xm{N2EJg2g(BdseAlXYFD{gd=(+S4+=rsNu^pw>_I?y!u$nLm9*D9ppgpSPEC^rd zmaK%~8+sOu)pI$@!Ewt<$?h9y7x>Kx{%ZukWuRN4Qau+gw2C2Q6*v`XFv2qWv6 zZ}XE-4U4M?p`{GE0}WyK>1)8U^ZMLA@MC|}vxa++1$i2GxM>3Lx2+g@DhChHjrcne z{I>{xH-g_YaOhd=c9(%R6(G0@cw7JQQHeLAM%@>xcS2JSqXYjUU2&)3_6`4kD*=J@W#wZ`{f5xg&gKZ@Xw4Qy;>xBCg!4b!sP;yQEy8~Syz4wr`o zXIIO1R5FZr($IG2IG=b{G`17uCbV95rOdc-ceh)d?CTCeB$DL4UT}yX8p(d8KB|C# zP`i?~(ilYLHbw*PHgqag@^e&5lRDzV+F!=n2O{{OfekH+)i z?0TU3x@gF_TB^}d(u`Wst&8HSIFowj&6M;^yx@&LGn)O1`(K69X;j5;A*B@by9mbP zG6nM*5lXc8gp!*IV9oweGS^@|XNTUY;5XI~Mu8`U7FPqtpfCwO=uT=L1*(ft@F+)F z0hE9Zf>>7-UuoG6B7hl`SWgUH>?9iEs%S6A3qZWW>kYCYKW#S{eH)1H^yn*bmGO~L zb`6C;1{Infc@5b$H}dF!j!>!{nAC6w5T=`+of|BMwAS7Z2!Xe^a}9`K;Mt(9-hdjF!JZD@4ZXliy-x-l$uT> z%RUYQ3H$>fT*Sq*d+uu$JQq21DWC9`RAc&x#VtX~#~P;FGlkdfR-S=oOvv5~ z>g26?=o41Zk$XH79ajeTbnZyA)5(}{Xuv*CgiQ2V*U2uO&-zjR9Sw&WwEsmHU?ULe zyb3Md0n6Li0x{@v2?xZ28$fhUrA4A+v6`ZLXR~$I!}!|YTF;>yDe@m0=nOh9f(IEm z^tUx%<6BHa`T$hF&6z8B=Y z0U{4^naz;l!``Cyt)`*x1F0tG5KmO=2X-LW5Eij4bf1`?Y}anlO}!}ifb{*^wR&Qh z$@IH`m?*x(QK>tT63T2sycI7DptHyTdeVAn=sZPQoWdlOzY!G_b?7_ZBb^gGj9Vra zm1FTBSP9vkhtha*iKkm-ak@Ozz@gnJexp1{;RpF9(4BAEPpX{5HcWvNNew{8K#Y@#(wA3{wy@3*CO_X&w zDy#V*RgM7GA#I%Nh5mUEGmG7C0>+}=LFF%IWfGzT%|z;Czi7U7XdZxGs4NbJ7m_0e zkg|-7*_%0f5oKM>1E0jzmk2kHCt}_L+I2BsipuoS#y~MO53qj}lm5ZqloChC34tBU zC?=3f7`ox~p414m4UU@V`NWA!2xb_awd=@$usOp{O?5hZ9cpx@F zx8g6w?p*-Nuk6lgJrRHct#BUMJX*O#lMIF$WK$Z}0|7Pkocc||x>g^(x2K`k75kf_ z&-AqQy2gN}V8foa#8d<7rNWRjC*mjF>$4_&hx;w*;aSZ&2$b?9v@20E#5H$vf0Leo z5N$36=JjEb(Lvm~9aqth?!%m-CtaAawS*pt?MysnLcnmE6ap>HW%ZVU^y!}5U&(e` zFD1hgP#RWAmJ$_fFTPkOsAUob#9D^5C{XhV$PyVeUx>@(lu7y&ZXi{PS^HXF^AzPc z-lJvpZ-Pq)O)$C&Malx#+fXpH;{JNJvp0D+mjP)fBx?RS!QOE&*V)1tO?^zFp~xyR z+#uG?WxcGG12F975#}xK_H0GnrjZG~0kPgZxsGI&1-25J>*_6aUDM^58PBYZw6y+Q zP&eU=P5Sb2y*SPFz}Y!i8+A_f6{RMQAv(;ItokP)R=27f#$XnPUU9OoS+zK`SG7%S zNNMk*xfx9A?oY8EnN@+>)CtNsf_1(8WJ+Qlm*km;S(r7Kfb_{2YWX57TxK~ng4l9s zE+MaRfG43iS*x)Vfi`G0c8XQI)tEb*Vs|cM_7iB+lPm3uXxJhLV>@{g&hoU1uU?F* ztdXPve@Ka&bQwdC&Lds$+8!=$VLvr+Byb)bYALy5QM%;)WdkGOfyUc9%_NSl1oBb+JPMWOZq zy7~YDAKnh*FXYrP^#qdn9{id*IzTytc@95K*%O=e8^MxV{X)_|XH9-?U*Gl6-rHBKmhS*49_(0|(=8lVJ9Dg%q@KPpa%f@{iSXKXQq>GaR`*#U z19AG%3&7ZcY2H<9@tbatSITzp*7PcS@99m-X1T`bB!?DRN4>*e-H~}-YkgKjCk~a3 z!8j9~k6MMyD*+}Z;5hI1D!Ok05I+r^kcZqW9jrsKBatWy%p=EIiO_IVy+zM?=n_vG zH-8azuM_l?KY3WZ$Iz?$Xh@nlacgwdNqrzSe{F?6X_IWmDggX=?oY;pE)OIEKNlhX_pT|_$dI~h1=@UZqs^oy* zL)KD#DLN3YTYqSUGeu+-U%j!$>H?7GteDY|*=G|>bcfKbdA)=+3CPA?Y5W2^C!NRx)IRIjlqvGUBJhzcOoe5&)zzi z$KGE87PRZW6@`hX`YEnE_P_NMqog&$gR=-o)~zGi!^ctJpKVF_gB~3weiN+q6svUX zd|KURRW3N}V~BdAv*)eF%uc~C2S2=vu!2Cto|jtKq=7&Tj#e`luAL>QhA zU4mBuY!Jlas&xwF*PAbwMnf>+VagsS$Li7rhUH!tGDx3!&DH>DKM3Jvk81#SrFr+@sX+%@Wc97HP47TxF$GnxiezId zwC3sqJ+E4{6wTOGZQkkGlY*W`(@`7Gw`N;xp`<6oyxXm&&!}|DZ;^68-Ry4n{ zz{>h$imJ=32oEG>6RZ>E1eY<3K`pqD4b-mJUEBu@cFB=e36s^wtlHhh4P57h8-Rhgaq@yeHewyu zHDlx)uA4u`wQd7GVUU}yK8aebY5oDAcH-x;){54ftY{(xT0AWoj~1#0X|j1gm+vKf zSYvIy5!L_Y9fETxd1MlbpEfFGGDfj<16hTJ>*kMraNKBDJrnz+ouqwq>u;)osUy0x z-*iPf%jdW&TCd5URVZ&lgJ$*580d`7yM(%$-bV(=!>x;~pt4(6b5@SJOpvg?64JE; zk!qp_>J=So417KWziYkK3QoSQ_u}%p9-R;U0Ie8bHYS~K11x;pTV&k5%yt8;?0*Y# zwJw6o&$1nM)WK+@c${#NaheaZlCw}JUWe@zi5jyYRU}q_#o!@1^1s@;x2^>_$}VdJ zNBFeW%Mn}v+b^>FR|L~sdA#A7xe&+m0U<0Kc$(k*2BZ1&s8lrH22iuq7Yu6M3f_FH z%y4xkq;=5()PXs-AzI9``hDgSaja@;HO@zUsR)wjEw??)4aFq8V#%uv=zm7I{Aa82 z&)e3y56Lefvdz(9Y)e_wJ4YXax_wbVo8IyOLuK<$yK?t}x1&XR;7x+`@Kw}mw*Hzy zt#83b+SYM>-MdOL<#UsTpI}o)r-tNrmXW7H&{+Bf7;Qd|O5kZV6}_X6f=>guZRA&s z?U$V=Hc#mT`-xtBJi`T%%_s1;aU^~i*ZwuXk*;QRl7LD{WDV-$-Kh-fUkNMkFe2d; z()cDk03~xIXd0z)MBo_-VKQj`2m!!R@dHH-2dyRa`qubb@7n2~SDw0C<5HKlt)7A$OEHDR$F z9T34HXd98UQ08Kz^+jN7{RoK9CCZ-~}NU1!yjc z5=EG_e_|JY(l(K2Ca2D}ACccMl}a9z<0KERpxsRAL$rNBXq%JH$T84?#hK~qSH{*2 z{ z8gB{R%;48Dd);1&;VfX-db3*hW6lVi68TbdkF~*#>!b>iBH61U)Y5~vLg|0^+M3(F z_iH$aq&3bCOd#z8L4v2`+PphWf&wkkeZ4s4+Bl;Xg4BO_%ywKN^tNnLL|!dV;z$j@~&27p#V@aQeae z+S&Fo2DXTPuNH;{I-c!9~ew^p%q*=woi>6;k#6i z=8*QOL~`Cyb?nODP0g&e-(p!`OE1BR=_BnW3>d)e69`fZ=9AKb%^XrIlZ~6_$&iD5 zqJd5e2N>wIfSrgopY8B9-}VW(ewn+!F`aM(5Y#6|KnzK{rDYNUw&M%`;R2+2mlx_T zFO;^==u9N18*_|+)2mct32%bF2m8MTS4#?4NH4CmH z+$Ml+m@D(3vHFa^+7^>7hd_1u8HbOLdw)f`EGBIXn^uoc*)+FqW;{c{^C*iU<3Zn~ zJ5iF%OyV1V(KfQ=N#6GBjD%cd1duFBh|Yq@cf((dTCNJJBZ#ojO5I>FZe9=4E>*!S zn&r@h`Ag~;ICThRFVu`edwU>3lLw8C!~xN#H~{-{7su^>P@Gd$Y^Ai9k_;Cnk{;LT zDL&R-4%U}O(JEZOHL?^bB3Y51;zNu3DgoJx9GS-JOASZl^OJzjPTxYM7|%zg&>@46 z&`!+uTMTG(&oxfd?d@>W)-Q=f6F!F^3QDg|NlR^Xmr+LClD98GC%8rXl9AGW7sK9Y zLX8NyA4MeM8!2e$(|$9MMxw}IoI$Sk8&Qz%F z>q~X}iS>ok^>#phaa|o|7jEI<51ak3Vh&O#F{kJ{4#asMUp*J?s(l{7K~Js zv*tFWZ0`rmxc|+tSo;RF zQSaLUg=OBcb`hMvYcEbGuD=SH$&8wq9?Pm^x}j7ZV5^|^UtpKc^-n~T7Oy7(l{-->*B_R0fr$(aLYSsq4Ft=3b;?U8wIVzjw2ARZ-}2q@?96(-F|yKZ53U)ROHTCLZRObcr2q02f0%d8YbDt&)9AD6@}-A^tOP z|2eqplx4~t2JYeR7pf;%b?s-F{F0;Rprcjllw-XX-r^Q2nobheSxK(8_+RA#ttQi7 zPuk3;T`hMPw8!ogMpqKQ_!!_Vo6Q;hJ9~SA^YP0X?!`2;pMNgV?1LKfLGUmX?ni(M z12H8y>_DQ^44P&>7D?P9>f@aB1GeN#Q7Mn0Q=ev+&Z$pFlbm{a1Xlp$CO~xtK&?Fg z6d)f%RA&O*LtXF{m4C#<20;YjIeKn-Kl_hzIdv@mfwMhGO%j>&*| zJS*~)$Bgvx1fi$ZcmgR7p);>W{;9ZT)(}yCoV@)2C_&mdZXIFZW~BssvNdN6jEJ7t zEJ{l|H%@sZ(#j?3p%6604@tjyc_c;NRqqo`0Zgtx6NNrhM+Y@5Vmny2bq+yu)S`w3DY+i&JROE( z!c7hLTeQ~(|7q z|Mt%%b}Z3(kLqu8%ZndO5C@FaI)vqY-?Cft~m=tDfbe zIn&`tSX}gz6+wl{+LX<^mAK^7ul;IrCpwo2oMJIkc1C+u(|H9*a)XF*eG1LkikKlxXG>?D(mV%+ZzQ*Q4Q_|K=k*uaF^rY9$Zi@3r9TRsO zk+K(4kkBJDg-}5bj62%2LZpy<=e%BbkaHy;wW6tDw9XnIIVc)HvGk=YNZ&PoP#uCJL2JUbWq zls9Qt{wbLKns1u$dd^8JMcA^TYaL8cKEK(W;JK_x9*1+ATzjO{e7upV&+thep`j8Y z>Iu@x26e0~ndWA!+2z4aK-FZo8K4j-n{MOIL+x6Ail@S;-Eu>GsiS>EC1YO}^NPYY ztJYKa)#Fr8J?E_cAN17uI`}8b8mJOV#hZ&n!zFuCCFes<%@VIftyJcuekc>M#=mI=hVg!+4ZUi`vQ4>`bN3O=>eJ-phE)m%m5wXp(?iS;~oo5 ztr=gnY4Y6goD%0Tj)w^0U`BQ$(*Wmy%bJi``qq0H6k>k{i zFm_XItmJrmM|q*)S+wxE)zpTm(V5NDUP^1}{JQDhxXGJdRQIgS{XWea!!k3tpJfj3 zM!6q&iL9Acb`aV7-^F%ita&(N(tQ%Ez~PF?sfo#{$xY|$o#izc80=GFcF%^}PJrPK zUHlmBWnmoF<_o(=Vi)k}sRsRx-O1^`gEEHK`cJTG`^UxTI) z)k8VjO8v2iV0MfdlS9^?k8-W*H6=q0!%rAOeKuErbVPaI$OKl>Iceo$udmBck6R!+ z;C1f!v^|+CPBjm;S{C*vHk_3ySQPi+G{BEmp3|G&b-}|HMA)>@2o!^p6yPE zuw(%_GSPT}I4abzZFs3Wpw+y}09FB#?0XCl1whWL-7|IyRei}namSJ%_1cJU4ZNw> zC^SY5ZN4?BR`~)nXmfr@KHtv|6926nMNAj&4%?b0}RPYel0UV>@Xw) zH2Q~T8x3{I2~N@O#)yGw=?Mh>!U<1Y51;6Vbc@wH%V9@jwS7)KNl60+l-Z$14G55( zYO0AZf3}vDL4Mo8cJdqKtrsNYcqM-z#rsSrZc^zLf-cp4R@hsL0C7HY_)vmhjo{Y| z)KN*jP^Hb|ZvbJOxZec01}?w@l*14m?>#C#;N>uBeGgD_9U><@{0yt0UX!nK(|Xc7 z{fCM`y3m_m^rvC2rSxI^3dzG$F<=-=F8iSllu*a;CMQXJ6_fW9P7vNyQILT=FQCk8 zKn%+cM#Qi_22an2V8gHG*|Q1>B^88=7dq20R(XB&qlmBeZgjihh4YuIXZpi}*$@+3 zJs9l#P8#jr#2lVxJQ!MU`|JS3y+S*5;-*LX0#;r$pUc!V@AptCulT-!t^Z{0U8r43 zaJPXv2v>m$4#Dc;zk?Bx;Ge`)dOH4@6c))zTm9VcPgr4a z8h~V{*atWTcA7A!+n^1Ir4;aCJ~ARbZL$cD?}!Lw!qkW`CFCc7nooX$)BeNa{ih|JW{_3)~No-v_IH0xaGj z6*)k39sUHM==5@=gs30Fj|@$BD-^$H`i)uNCW56Ph?-^HmGx1HE|TObV%_2gnA{Ys zg~2sIPPS5KtfW=hLTVEI86d}&xFeiSD`=Jz0FrU2DLf%{n)-PJe-Xi70=$K|4@B@m z1G8NIv)OZFAfDFB5{WAK<7A8ewA$aLR1Ed!`}`#bT9@?qR~XY zI5RR|M1l0^lm>8_2^&Ow`oJ+p^h9HEpkcB7Q|smTkQsX$H?Ipj1PVPLMo0myS&+31 ztbT8WCRK~a30&ZfgDwEvuv*p+s|x#8h!zY(ov<_ zVBnb2nWC!88BD)LZ_QG_1ITxlD;Qw-ejqgLzni5RIbiNRHwuG>e?kQC8vbc5203+* z<1j+Iy8M~I!X}-91`M>=k9Hd0`bha_Fe2|GNClQxM{78#}J3$J`sE@z>>9^e(aru!&mC1gk&<6y~iu>2&pKnL050up%2 zocyU9?#vAz3YoIqD3W%+`ih&R;=_EXO`3zOM{KU; zPVHYncRXH}4AW+&WryRldsI2qgN>H@u5D+5)hPv&L7X=nCTJ(;5R(DM`JOtN^K8SM z!=oqw8WieePj6~#9eq;&^Ij4n2v= zkLf0AY0e)*7)vjvMrt$7GD0Igrr){T#>ub-bOTT|cjOprJ=NeG=Tj{@ltR#-BFR&5 W=_jSe9J{a`pchPyojAE}Jo~@(;Cqt* literal 49170 zcmcJ237B0)nfBRk-=(95QE>wu5+t$5Xc8B6Kp=#X$RYt*1^%9!bT{cN-Jv^ypok0v z27)>>jv5dccVrwz#ZeSRLB$0H#VwAbl14?13eF(lGBf<&`@U7D>YRH!!2Hjj=SlTf zRbPGe)wk7h>YO{dezZF=Hokr|asSfI6XR!%PEC&{*$GLSTB#-3s>w~s$mm#-9e>Wo z(G!x6uVAAN(rm-J;i;+VBr~+`=JlJBv$|7BcIf2fdc!7K%91ssXC|#|nMzvOp&sZa znSp65Tg8$*$Dbm3#fFW{H!RK4^p%sFx|_x)Cs3AVFMAmqEhTOv>267~HB+Nw>*EeY zH`xy@+DM4ZgnV~=4}(^hrW|CI#V%SUL~b+zJ^@Kea4x`3(=)AJFcADtSgWplFORq4 zo?#>qkVf(NWYd}?>m3Bhb)Jp%$w(sp$;XpWD3(~?*_Rj?lSlR(JQ0{FdNEZD_Z@1f zgwSCDLVJXKG&C~s6x54>rvmJ-^l1Qd@q&J#QTw-t=VedJIGJyn+B}N7q);cVY>Toi zBeiD`L_%dO#27YBjh{8%T`z$=J=qtv^N=h+vhbLVrhk%_X2-hg&9d>YsC3XFqH5Fb z`thzA^4;6sOU$7%|2}o|Ou52@`2_wgXl61IBN^GsqN=Ta{)0qbNWIJ#g~=(iRM%FN zkS;`0c$*^8`6yb9gw69R>2uFz@iSSsAgNZK_Iy>M@r$cfcVBXCR7cD2PK*FCSyGOv z4oe%aU3D!u*oBf0skdtQx?=bxrZP(PsB?(R$8AJvhM@eLc-kB?3RxgReTE^@Y* zFiXb2Cp3L<@k0pisUZMsZ*PGwwM^X~@4ob%kw?Ci9@!nX4u-qKqwB{vRKp9%bz0eq zgm$|eSqebW1=&Tk-h%nDY-~e+k<)ba*mQsqf?QE3sxA(Zy4meSG+>0=K&p~;^rc(SC4p*_(0AmyX4kUwsq*fZ{I`&0h zQD0{OLEsvI2NGc%;8L?(@w@KXJlGv zLi9G$AYk2@cZl<)8Zf9>CrH=_doGP0<*pA|eUD)4V#tG@C;<|k%TY2iYV1?!Pat{D ziNJ|$yXI-pol9G~6xgyFKqYq@Eh7O;PRYNq=Bnx3f}-Owgbp$#M?4D@#mU(KRmw>p zp+vgfE?J?!m=Tfj`q*rBRc%G6T;SDm)&2sWUa0m^C z*w;L^Wxmz{krs)`UzWbEy6_lADlxhJ`l*ycx;ok=%lW{ZEZfPp&^}bV-nQq;S(#;6QGLhL@9#ivdc} ze;dF{0N!qjrizp8$c}jXy2vu-i-?rdn^#RE7%c-rV!IXTx-@lj!Z20PN)@N(1D(3J zKy95!+L;wnxrzcrVxx7w>utbD?H_^-JC`fm70nio1;0=;b6ttvlJAyw`@M2t-&cU$ z#{EeHSUZr+7KPqyb-C~ToDKa~K5{gKACOA+*4O}s$RQ_tI|?;dUI|bxe-%K*p{oJz zy%6b6BoSZU8P)~zWSv4?7wkVYDWlaDM#+!DqV+^&X75$tYV@2yPfH?K33L@`Yiv+$ zc_^F#4Kk>qzY}>4{apYx^mhZ)(BA`4xbFq{Ag%R%03QkhAz87)`hP)sKV|s_>N@KE_>x?P*&obb^ln?d57y+AB&nVrC!{ZtQb?cyOb=pGyUyyLH8Zokw zELgZ9ShoiJeqc!=*9P#P0cvjk0P5QuCihO7(m#aKL7DNJOa3UASUA}l5K5mMX@m>} z2EP|c8P z$c!+ZI5YYzN@YfzZg!Bu%|LiD!CL_CAKWeK65O~h>2wbVr)!ci@=R%VWStOOk}gNe zI*k-rj=^EU&|)msk&MRgo%d6QHh`Hxa{;XKO<@!T@0RBuSP+8=;3M+`wGwo#0 zn@FEk{n6-6-v3nt-IRS>0KW$C=yGP8TN`hXHY+;7E|+d!v5d{=waxLloE1lMpnj#k zH{O1MYOO9E#cYfLMCUi&$iu$mXc{$$k)rJGo5*YVac2O(1@LG}`P%^V{VYjG0n!TA zX&H=(%vvJ}!z1z1SHEF(Zr?DzVWVkO(_I&BaONdXG+?za(b^X7s>M%mTw0;n{w|x7 z!S4l-2pY`yt<A#uU}VyaIyyytwDZeP`aJ`{u-rP zy8H&9W~6%o?jflm)j2yYv}UFcY74R_kY+XET~-%y96c~dxBGz6%kbXTD!qza{uZDZ z{tp8k!~Y3T4BroM@1W)fEt_7&{907O!%{9wS;Kf=3iLj!^z4m~jd5RI+5MI-wnE#G zl^{uhBM3R0djN&fJo<3pLk6YSl}er)SgZ-M)yN!x|y6t-V3_DmpAXnvG33Cbm9Y1q#$2~GSC%3zLlf+Y<#DaJUpi4x-)y(m~6V!yP?yQ_nG*!XZ}Lj;SXCq~BjzX$=I&j3!GYm@qo9v_*6g-bT?qa4c z1V8?#S*_S8m!7m7u%`%o5}-wcS$Ff6B%P1U;(i!IHh5HKO+9(~qMo4bL>W5=+bN0B zan7$QNHrW0V!>@<4Cy}F_XcgL1 zXWB!22{j4bHiKhi*xY4L6jv9ZPF;4oBO~_s9R*3wr!HK}_mpb8faNQOfd6~|EZcEU zUO}UfxB(uEM6OBc_c_ALp1Cl$r>t0N@?U68nK`M{hAQns$_b-Z+`E-!^H6i_zDNl| zKG{4NR=O9b)AU(XbhZyrqAnp}>1t7}OKE5JE@=eyE>W0)P)5J#m9&#$Db(;tz2E%7 z0j(^>o8D}clfA)HN;}n@@E0hR(4Px1r^Zt@E+1Z|&#@Xim#nKEk3u7Ed`MdcLj72B z(I#681kE$gCn~vGj8d_}*;W1z+-xa5X*3Lm>uW9Y$lR=JhV*&X-p{tA4*5OJ_*$J5+d)@~EsRna#1KoHVQ zM8aa?B`6j6QiHN%6a>+aVGm|2hNss|o}IYZg~II?tK37r0odDhwpW?vG)UY z2NKSp9Y7pPbv!S&V!!S(Pxb@a&H67p2Bb8h90X9z9~{6#49t!(epaE(o#NG*WDOG^ z%wJ|X$BJDc=zZiXYGH4zGgOkGO&=XUNYL+Ng%j#jh1ltt}uKpc$#RN|=Fx@8%Xq}tdlSr@bJOPfv zDN%=OGnP%{J^uiZ3*Q~3Uop#LP&!kok>d>2hatOkwK;x%hXCY9%1KabDKdIG`p}^M zk3renIbEk9X9SVBP(+x51!J~jE({pp0|x|ndLFKMJoKm zbMRHvW;#YUC|6RkXHmK0d<3loj*z>{zY$?oobr5= zEIn7}<^I4pow5e6=lMiY20#Fjq7Xs9ES86Fq_T(_< zp}gAJ-&lz{qoLO?EUXOTq0pJAzl%VuKz$ZH#w$=N)X=30x%{@HlUc6|%Iq|`qN|Dn>rL4*= z#JPTSY}2savZ-7`IIf(b?L@c>ZlrTtlsHs+9v;xr?-Jc>;>@T^1Hm$N|B`ts)!KBY zrzcli7b0RrMZ}(HzJ`762p&H}4en5i$~s}jV}^4#Qvu1i7HuOb+V+rCw4=wh50mN) zsRmHS9pwY4K~Qo3h*nbETMWvd!qV*k_agXqfcuu$E1I5_kFNu(`Q8YYn*l)JBVIA!ZP1a}gq+GjpoRQqlZeAR^rSRW}yyk^# z2!?s#cFX50d_?7$Z+10sg8V*&EY>xeI%M0QLtz*$sx@`!H2OwVm)f$Y;fg@{3aX7A zlq1d<_d*Avzz#@(y@U?bKRZwjyMpi9Zo|7$T}14Cz=GZHL(r1^awOtVD~|V~N-M*T&L^o(T`MtZ;0Ss*!Wcqp zif@Qs{UzihCA|yzAukN(usla;qD?5ZKr-i}&}#wx?q;y+5)IVvZ2;?o{bwu7#Q}ts zUkN0&)KG6lK^SUx^QPz>2gw%*$01QaUkB(GkpPdIZ%Ot~0KHAeYn(1B`d!&5iRY&g zq{Y)L-a|Rw!FB|>!BC+5CQF|KycF}7kw${X`IRi?Y!b~b)st@1CnvhfD$NQN*XyPA zC0_82I;Jztda-P$U+GkJ@d!Jk@awoimT&@hVR&h|UJMhpt-&>a-foblN~Su=`gcf4 zBK%p6yx4w;1#9)C!>^o*eg&>S1ggprYr`KqCqmcOhR!&%4-p=tm>) z0ff6;vC0b7l7MIBv8-4Qpfbp1B(7>ENmwK zMHriGsLW?)fRIKL8r8K?8eV=MTS7%~OW*IVl7y=*^KOM%_RD2BN zSpJX~{p=Au7{UTTk(tfg&W#SB-6^{dwT54MT9SVXF>Tmp!LoKL+ z5ROF?3E@uwBOzeaK?u)g_EMB_D-%T_MtoUrh*v7yy^w_Cg%l-E0qt$D@8O3_|+=?6hSN(bkvYU@I_3th#c0 zfEyrIQJQEDyyDbA2Q#)7ro_`^i$bnW-Ak^E(P}G8*8(i?e+?kMpQ6hYTr`x|pZNYz z|J5|wrPu9?KP!=JN5V@78AH9~M^hH~e5+5dgP798fs5{yh+SmKqF*6r&$SZ&Tu84{ z$0zN$svZ&=QHBhTVbgDe8($m!&TtS%NP_ z2d^RcB7o;=ia!k)I6XOzz;?|(zPlO5fyGQ`fS};r{PSz(=Dl`E$3Y0Xk%CfXO?~ z*>Zp>6>}KCE^N$Q7&EANH<_Yooq_r>(wqmdz<<`u`o|DA0&hJ}c1nAbqTcNVLGPCJ zZX+XygSvPks-*b}b|=3SQ)ET9%65N+b~M{!Ir!2;UT#QL57|61Ho1PJ zeC2O9c2Hc;&Jq05Ie`y5d34HU*#XomMa&aC+9EmGLWYk*b6#i5jyBMl4fm8Xn`5l7 zxPAfnrqx=sDSJQzbXI&8kWHRv<1fz!;f_{GRYo@y=tGo&-l2ff|?iD4(j`ch-s%Nr92t>odae)nQaR+zw^eR0oDZUMge4ik{Gw7|#Wy(;= zZvBJr>_}_Y&x~-8vJ5n5Gb0He7*SBMSSSn9b1-;)vL1S7!RTbUbPk-X_&#c65rC*EEYUdE7dI`i zvf>MG&sEZ9k3ePGM9QJfXNA$uBAW)do80j~M8rKMIi7N_doBT+g8np%hhx ze*v+$UN#5=G6^A}kjZ?x82+V@z;iE>pV3xXo&WsJ#G3A^@lE{L0L?E+(NfEZaeyhu zLQAqg2G2C}t+*JO}Lbr1@ymM&;?A zX^hxiHYoe7uTgBiM9aq0(9#|Showq5rwl@q$)5?jimFp+JCC}W1_eoB6H4a?1LiSi zR=SqZ<&8!eZo2|qqC9!9aHS9q`;vk+TP;cxM-Ff3l0$(ptm6ctM+R4iW}s zm)Fn0w>wI6IMg!EB#Z(KM6bm*p5|wE%5cPEah{hZHP64E%{b2U4Qw1l@B)B`5Zr2D z!a!KCbXhZdWw>(OST>kVFG*5JGFcpqdV@D=+9HS7G0dfSgP+!}H%08=$K^mEYs=5D zC`i(mlrl$Pjjm!0454e~tn+jZIE<*RLObRMN6W z4O*Qfb2W%4;QSM+6mZ^QppFh2kc4mGrz8v!})@P@m%t+Qg-eQ8NME?)L2fI>OpzVh%YJZ4xiyc(sP zml~IHk}Yxhae{Oon(=#qq~Q9#0A3To_XqG=0~-ne9{_mSLQA#zNAEd!ZM*^E)s7!K zyWv%qHSX%D5l24Cz#Vw`C55IN|A^Kagj(-|dfV$Va?usj<-YBVRjKI7>`AyF^R^g; z;h?d-jsn6%K)$?Q6ZfWAG6a-lClbn?Tn|B(y|4PTtdJLE8z&mnII)_qUoLCBZC~I& zWQneL>&2LC5C!RSSY5gnF#2s=4v4oC8t(!)Q{xNcNgmz}Umqm`k|FXH^0iBEjmxWD zi#f{c9kos=jA)vQFAA}fkN8d{k!vyHaKzWxj_fuleuA3MN65M4@HgrR7@;$E=VIML|s-Z{X%RDw8|U_NMk zY-pFSiR zZUvEk#y*SNqWxEqaIo8IEChidaMR!uTS{5vq;ea(*c+`OQZ7(`{r^F&a961{*$J?) z|8jA}NjD6LmvK)uIcmOz1S^lmA0A0mzcH-7=EgwO_)Q=2hIwEB95p^w6C#)+GY$Av z<8xI#h5-y@)rP9sO<=`S`vyF?@t>9?+kDW$Lyg{`Q*OulJW#DK0YP&ok~cD7e9b@? zFuoo@szXuYj!^my0~G>0KXSNaPAhT-zNx-4Lqv_3bJc&6mlVnI3@7XnPQLb_U1yD->#czYZV*oGZOIfD9#d}<4?f}9xTsiUi97@rhn!_1)cWq+3AM4wwWzfuj5r$pzEvv-@ zAZi1PIcZ*s-uOC$?vvG7EV&z474W$k($&~HzJJh+I6Lb*`ZSjT?0N^TB-c*@7t-vL z1Gpy;-pVE0XlWa~fjMv`A0X#w?58$B-tO`zTE?BV!s>Q&U8W@LUUH%$BcppN=!!Ky z>8KiA!i5;t7X!C=Mcf*sKNpR+2LsuTeBJ0Uz~ue*Ki6$*a!~3mKOWUVZ;1}Kxb7Eu zs~-5WCB2r3hNETg&K#*m8W{r)71(2m;E6Wt8d=uatRLkqRNT|8y!XW#U_&N6`H*XA z|14``4cMT`MLob5oNGnK7SO+iHY3PWJafIV*$VX$Z0%-iGw>y{OnFG5>_i|2JaBW( z*7zFNz?WoePce+XwgwA|Y|Ty@`0F2jUI|Nn_Pi3<#}K5V83`2MU^mXxoMZkR0ndNWi?841~N|VwlnNyTG!p zV~$GbM2aZ03TnuXC_#}2p+*KBaLc(&U(xs-KSNdr!cBG}p@z#irjMU>P!UBu zovEpLttA60o3n!V;lmlagi0LphPf29E3f#Mh9t$yj-kiyFy8IvqNOe|$qkgqYb2}} zp|F^b?(*jW)^%{)Acp*TwKECLZvsaBOJ66k5c+p6+E-0bt-4<{-=OAmkf*-)1NZC^ z1Bkl}9kVrK^dj>5VqPsJuD+VMc{F147SOJE4m+y<`DyjBY&)Sqr(+TXpA)$7>2d@6$_OM!;xFp%7gV*DypW~ zTNP}kQdc#NK2@a-D|L~o`jktAWzZZ8pP#SKny?-2S>wC8@>MuWekAHOl^;bA@jy#? zS^`|O`6^3tJoV5bgJH;>*NT2HAI20tCtC@63?f6JUO|POlyh&Bj*FV+$@QAP^l8{! z&qcwII-ccuV=0B~wmL!W9?9T5FkFBQFw|TQUP1@WS0l@tEwilv!Z1mdY}OV7%~KWQ z{u0CzZk$3FlveX(D5kdy6mCUA*9xce$#%|dYf(k!PX@Fd<7}=WSRDsrolO&{;sJX6 zEHaFMT}6uP*LCycYS(f=47<79ti^55xFiV2`^}R=C$t9mdh?XJ;;k^l625tEy{4`~ znj9nJ@wJiW)}9OM=3j#nCe`NARh;JQtkAyDhqOl;^`59zg(i+67|eOnDuZKPt8N(m zyRdF`=f0-Z?D(o^o97y)&OVwKf!VtGldVUmRSJAlZ3O35`;#h(d2|$K9${hDWVqmA zQ%?6+WZ^t7@Hk_=$qym%RRnq3DO!ykfpNJ5S3u>i^cc&y)tI}}Vmp@+`?Yy^Ou`=aL2cx)tfG>@_54@O>SX3TGa@Y#+{@t!{jHR zP9r%HU;|R)oyg|^Y^VqkjKdN{Xv${ zstj<4ZlL`DTL4(c=N(~m|iaIDY=u|`vQbnhO8tx`hgHFL@ znhl9l`XrVD6%FF#D)^+=AY9UUqFogI#wF+?X)yMz^j;!uaiPi4$sG?UtI-4%&15m8?!%%~z;vzAi7rX9jM|us3a1T#TG!Rki9>l|igJqKtSbLH4+udqt+b|?B#)+9 z(&pu5&Bjy-Medc>N*5Tt;tQY}ZeIqT)uP^qdm$$bH@b^OC+@2jYg9Mi^|}Y%UB{;oTr>UR($w;QDM%xGlYf zqE9NVMO}1>@nOprcLs$c-#QdX^x+P&hk%qqJN27C(G`>IdPj}4Ugog4kEXEiTrH|4nF+I^Ki~A!+Y2IwD zi-v4{CrD6;I!D7qSNzcup8m8BFiMn0s}nJ3wJmxTA0PB~n{0`?1@eg?s17hywh%a7 zFFsCRVnxnX?BkHS!d`hh6W91x8WLZoIF>-e9_E@8#cn~2ZK#!7Anz2w@pI*t668)s zZt)H@;7{1+?=+~j7X0fip8IH^nj*Qdh4!>kK(rlY=f!Dcc88degug4q2<8NMkf&_janaX&fA^+Ll^UAmhO(RrAk=qc=hG4*={+AMRmn z<6x9QjxGCL;T6cV-T;Ed1%Ye`m#Fw)IieMRYdByF-sd*o}Qh^SPVsetY4f3chm;o-P74%kg?xm zY6lRzhU9TETEB@*eFB7K@;3mK$$!$I*2UEG=zJ6}w*OrJwcezi=CvqQXw-nc)<15= zZl~FIO;zqp`ffF43jGwtGOnpc*mIe0v472L2vBZb`!uk$e)YtISg52ZDDoUO1xEY*{zSUh$(*PDaXWKkqvki8hCB_7ftd{S+24I7`MB^ zk8KA)F>vAtHti3F5$V!7E+_5jMEYh_@Wdv+#XzU@&jYNB=?m-tvq9?`BpkpOYZ8l) zFog)|t9_Abtd`UjG)K_-HrQPYc0~JXfv?urD>5JW9cnSYWJEH*1hDYm2&nd;r$xTF z`{_NT5)(|x9;e{TjYv!LGDfc%uXe;FRzoP1h}hM&bRLqklawwfH1BEQPZamv8`tx# zlvAdAs8R~0bxpm6TZOYl8`L^TcVz`!I^j%_(hs>=d~`X{5J zK(YxrX#O*R2lE>UIr@phZOb*Tto-HyMLc`<>uawycCWY)<%FX z$unEYL$tj^=rET!90LtlJu_VW$+~p|`7Z~gPe~t-s+<22`bhW8Ax(+F3_P2 zzCd_tuLPge9bzs0P+w-3kYwNfOXSQAIcw)P^t>jtf3lC-*UY}OA*w`gqibX4l)$Oh z_iLs1I>l)~jGO}5 zV7^`*Mazo)M6hLia>MZC*zoE#ljEyv@2DFZG;*9NL{bd?0?IaHuPCc@wz?MO+hW<~ zPo>qM0&$(evw5#4s6BYF&Jh@9@dQhpd>{m;+dT|yuP4Hj08V25;E5OKp7xa2HG{Bp z!LI|gDHeVdT zjkMQu=z!akK?-J*l7h_~5~~h{FjOs6B!#^!>!h%^fldm~G_buML+7i}?MWyzS}is2 zfzu?5k+wNQ(!~6!rb&%s#88}VuwNANCwO7SIGR zE(y=JX=Aij5Rl!r-%@HWJ=EDsdME`ngYHXnNI4Y$8K>eIRtNEqjE>po`S@c>%Ycu$ zXf*&>q>CK>)jMmulDs}hNW9;9+aJUarB*B zgt8lIpngM1f+{a1s;_QyK(r~!&_0{Sal4;}uho)U9aPT4K*T-B#&;Z9dJDR~F|bx3 z|AnA7ks^{M@f}ChxNkj3+LmqKLf%9EMii2KdN}ae=)1&Z4J}#d;6X^J7tc2v(Eb!? zhKam=!vf@=Wr=Qs6fY%+gxue3K>JfvqiSlS)3NIT!1|;md}Q4Ie=pR@WlxNM`n z_UMs!_F&H9Pn6@Qz5kpFdJum5K1fJ%RL{uw_zPCK?fU|gkZAkCn!nsfBugIAUw+3< zgTJUH$k+Wv9fRJtd%L3_E#eJKq0obZB^4J4zs+j$b|E(_J5KOnj@kl?W}zW z!LI=y!;Jmmx3DaI{G3StVY&7pfidEfk>3IlILQHMBg3qF!+*4_s(3lDNRA32x%RiL zjK5_oFJSc{R+cSnHtbJvkR`M))_fa%wC_N2h};ijwhYD>nLoe4-To=+sB9X4xez?W zic90~+KW<=>90ncXhw}xUz={oRR`EgDE(Jh)|vhhsNxx8aU{ST;?wmMHs$B-?L5H# zfk!5tJpqAUhHJ{mxOV#heJ4ASP<3oLMA`9KMs!Dw zhYzB}`6zV6FWp5o9JW}8_~lzb@9c$q_7DnLuW#Hl=)@~?T$KP$vXr9H5G~u;D~Oui zhbW^V^&1UvIv~-Rhu(EDHSYZoE3NeIcR%2v_Jdk}9a6a)YK6KOS}%nOxz&s2n8=>A zYOxjCYIbjc7QgZDUTtR8j#hRSff?Ii46h=7_A$U)Hk*a|S086ei_{kdX3z$oSsgy- zETY*LOy;9(F%tLlO__nTG+~z{I{TNB?(A=c8tj}d&eft?o-#0IAGQrgDV2I^Z_9GAXI z!y%D7C4UKgh9Q1OB3*9wr58q1UN+74fgE`ALj!}0Mx%Q;2m>_=Ym``UiVkWb$?qsl zmo=Ru(GYDqNA;B~Z(;Nxl*iY8aASN2RYv1Ln=B(5K|nH@RgN6oxl zMnRM$1acM-IAZmk%gkbk8UJXm?j`O+0!X4|0{c_cM$KF#+}DJ~VGsHckjiPl^Y>NJ zbpCNV){v3L?@`G3(D{2{ zmOGrkMy9GN9yvUMs;pJVKB*uXZ?&A8!p;CFMXU+ncmUTLNcH%SX^=70*H`1zg1D`# zB3fbCw&Am53fU806c<0e&0F6N=M z&XwMC#w_Pm(cNf27%(==bL>MwuyU@2rb*iN3bA#L{EG*_I(gD>mq(JDK^saT2NdS} za7L_)5!>i^2xe{}Ga0~*Xexc5iPAQ4d3>OS%rp=bQL#8thg)I1T4_-ZNIIWJf^!3Y z0f`=+L@qls->PCKWRzlax@)ww=g8nH#T977pd}|_4cfRGc%ob!HJvZ{nhtlDaZTUe z(MJeVMg5~#WUlY@p6D~9VZEd{A5@}e)b)DUiwily+)Be&lY(%>xy7a$AUI6n>Dqrfnj9*|3W%0wxM0X(u}^uaL#w`a4@#VrohTY5~gW zo-iFLlRQ8quBIjupf`SR6M?=}m~5>pJ5U0T3?hzE%XPj|M+eRZ)ZA0A>1!K|50VgD z2HhY&xOf0^-$ZgJk`D(Q>hI@PsMBXn43DTk_Bp%$_|sinEJ&(-^>+_C<;_fC&aOX2 zz$WnPyW_h4faiipskVQ}$JIfp_$Cpg=xU7X|=R>AQcv=YK=0BXbcT7c^o=9U&1wKEI# zOBwM@EOa4_c|l`uBKaGD4Euw83dOOjSO3^4n$+mH)Cjw)isxLTl%~gQ?AlWl{iugBcE>Lf zWFHn0fbZG}vb8F||KM`=97&MevH5V!LKy9QC^1eq#XMj z0{BLN2ihUW5&-sFw%L}Yg!n`Q!BdkqeA!LHp^$^F4t1O1nal9m*Tm$+@bu;>&!yE2 z4mI72Oli|ys;%aS3t&1jQE$~ z3di`w*!aZwrgQXG_*$$@pd?+=9JG7SWMEJ~c60y_;tP@=f@nma@a=?UqE}x>z@mqAu4Tdyr<=vJncBHih7- zH7`R9gD)RIZ8BGX+?9*a3A9vP2n-6XeB5^>%CR}JYh-7QPTA8v`-zeieKWB?q2h$N zqIeJ0d;B>YM~_ZAY60@i4pS;%b$5D`Kc*c#*PDuP$=lr+F)*!^fWV)q;eGMJEq+K}w{oXBoOP_R58X#0sn38CyE>@>0kSiS8vBYB zREQcVN0mVwgV)%~A4TC+RxU~%Bivb$k-mLiNS@cCJ=Pxd zh{2Cgmb82@Huz!Qa4Qf{Vn&#!F%4d86+QF=iy!u8^nJrCZ+Whn?sbbp(FG>9x--}< zq1fBKia9*ZczEWiw;r|u;wfTcCk0%bGHPjbP@h`?(<**pS!Wf$G_d_=EZv3D%>;jC zpu2AOYk+puR$t~A{QM9!P{27{T$EQLD+33l*Eq4ebe`+icQd8w*qdl8wuBfNe=8Ax z5$zLb^fIJ~sJHZo3{6`WvR|2gL)5p4U^xh)WJPyXeN>{0Ai0`Y_xk}xI|EL;8XzZI zi4#_!Lh4D=FlfkM8JMK%g;vP(pLkjUW@Ny~b|{noGRR5lzXSL`0Ypq2ydSs?`|rUN z@Q#`ls|T<)_y7|AI+vsxjf6Ed)0Xiu%xRE}q#BRmC$uJNPUPyo8wPL(4Q{T_cm@`Umg?4^}HJ)1h8a5fU9U@iwySR4y&mzaNPTq<*FpzlVXG8@#mce&jxuKszh5VID~YDsNxDb z6B0RI1FX(@7E3XJIe$(N8qh4&m}8(GuQwhC1U^t|;FMv`yqXVk>R^v^=39Mn#d9qk z{H7%e&a@`VH|VV|{~83^1yATf)QnORhiBMtYL%YBd1~+nr6dNiO4HA0K~OwbE56L? zYc1bXjT%|rVGB@yx|{rIeS?1K&s>9d6v(tpD0GTdVtSY*jP1o8rE{=wu&kc5zo8U& zSTg4&z|Pqx{30N-hB)Qq)))Y;+W~EynzT#j<5N?ku+T2Z@ILtxLfV@Hq@C>T=9b12 ztweLnnpp^F2WKaS?&C4GnRH(n0j0qaTFg^HnMYK5xj^94QJNFs83gUkhb61@>Vs6v z$wT^vLNj0uZZDmc3(3LlrR8g0ffV%sa0p=gYiM*b3JY2V&eN3FHSmyUOUBr60n_{w zP4_4p708k&{uB`pl?M5Bvt%c#qI$pj3MZxNS5bt_gteMp<$VYwNS&9qB9h{Z(%PH- z)P~JQ;YC38ghrkD=!sX8qy^g1 zUB+mD(Ss()WDaa@&QX>mkE9pyFz1!PWS_AzP;(4w$R|cJXC>?*5|nCY7Zkm)E-1bi zp?hO&kHOD50m*5gPFaL-X~t1TXrxECn#*IHjZ3 diff --git a/src/builtin/obj/subtype.olean b/src/builtin/obj/subtype.olean index a408f48c2c8befe949c5a735bd44ffe191870ee9..3a235d7592e0e70c4c2e618cec537750c2451b25 100644 GIT binary patch literal 2994 zcma)8%W@l45bb-%j>btO9*f8ln+U&>3gO`j4^zCWk~owD*@UoDjnKF(B1>X4A_3+CPW*jE_w+9j4+oL|WI7#-svvSn)M_xzr2)Oe%U}c) zt@#t0xs6KU5NM@}l%+F9gPy_g8zJH*T|g{cT2KZ$A672_MqIrJ*gQuT?#}THqO9qk zcNP_LoDAmq!jKu%(un=OY(#!EIZ6hjJROQ`Vx7)gv@jXzlVXd(sj}RkgOyQwo*QWJ z0^s^q_ zvDRN=Dxpxju+r2Y<5ze3eM7rSuHvtmJ_@z zUp{W|)};H!7Vyh>S-*iCBhkGDrQS-yUCnbalWOiRt5A=vku{&M7fxP+ozjf`fS`>o zk;G-loxq31H&TlhUD&jTon}eq)EM(^sEqjzV3P({0NaFD0qu$Y;`Om zbk(^ULfT|v*8!~vuL4;SUgIJSUI&adDLWwL0AiJH(p5m3I-stOYnC2r-gwxZDzjH~ zC8{Tetd&7 zKEi6)`#r?kz?E}zLzmAUucc$N4=0kx-mdsoS>N3n`?JIskzoam4B`9qOZWkxRr^E0 zyio?zyUpffcL$2^@UqicUc7ro!>eL7(0B?%7Qz8B?7J)%i%3m1Z11T>y&RmiW!KIB z%aM_qbWj-1q4lj2Ef_?jN*WhIn8*2PDAp;sk~&@V7HODDFC@(ZGDL^)7JS$c-v+X> zlC=%-9jw~t=2O6q*4SG61CS;2qe6U7_4!HfvOG&B#TV~qtXX_cD&^C_)MOYj2g`={ z<1biz_U+7x+kewLW&Y&2_)^ltAMn+)Q-Jmrjza;tyQS3i!><3b)cy?#1b@fAU&}%I zE7UX&gY-9jZ{y9wWimukJ3VU&P3^P>vW|uQ6Z*h_K5Sgdvw2euR-KdoUh2y}z11`( za4c=k)-^zFt97-b*K9HwO6{Y#7xH19$iQJ&xGcWnG<|_Zo2CaqHcejw>LD$H(%VC< z(a}FZ2ih}@TK@<<=HXz37wtm60n6Hj%#h@9yDZ0jHPEy9`OIRiRj64ZaW^N!Tlhcy EUj!2G&;S4c literal 3026 zcma)8Nsr@16s{_#+nyz1Igoa^5PF3X%S5ALX#_J!KpIfbTo5x{B1i4efpiiaPt$#a zKQVXc1Dx5!0saL)i1&TZc9|xT#!@QZtM}^d_3YUsO{SyqBsIlj$0zeymYc8BY?@9? zK^-Q!IZ8*yEglW?^Lc6_ch_9C#(gH}zWfs7pdfJX&t?-NERftXA~l@lCIsJNQ5XOP zSKJxJ>}JKVFx03lW$B#Oz^5_%2e7zB6(9?hYLteq`rT`Q0e7zhHrMHeJvf2_x4xn}HiokCWjzPmhe*!akL^D4{gMr;9BbCre|03R3FQ(>y?d zX81MDn&G=KT`VycM%F4LYs!v9mLHo2m{C!@f%hC` z~RFq9(Up_dWR24NdecQ=4EB0BQQZmDCCPR1wT8l!o5o{;rs zN-VQ=gQ56D^-80+0+(lxivE;bd|Rk;eMLR-whBl>%d?r*R2}Qm5Hn=gaFiz0CM%}N zD^vEINYqnyf3Uj$psh*u;WqG#ShN9vEG?0*Mj5B(i1N*Kh?%MpalUR_EK59JEp5ew zN1Krw60}h^Dt!TT?EPUi)Tw2g)*sr(NtLAMyP(zcJs|b`CBP;HUIuIv-T=I}7r1#c z&eF3SWW6tIS=kBP@jRQ&MuTyd$%HY?P^_1-RVPBtPfP#8vP3(gxnbq0`Z_%uJjtDf zOVQPYr>{88_Yk(BBKpkngl_?! zQs8aC_BFS-X=>fFw8c0k4(00Kkr6gXbZY1ntA>d!OsM`5 z9zc_(^(jxEyF OXR`fZdh{W_y|Oh60}u#h=H)Oj`WGZJz_>*aE>m%7ZhS#eY6^nO!04Kn;+C0{$^Za0 C@eu3) diff --git a/src/frontends/lean/notation.h b/src/frontends/lean/notation.h index e87d12105..757dd568e 100644 --- a/src/frontends/lean/notation.h +++ b/src/frontends/lean/notation.h @@ -7,6 +7,7 @@ Author: Leonardo de Moura #pragma once #include namespace lean { +constexpr unsigned g_heq_precedence = 50; constexpr unsigned g_arrow_precedence = 25; constexpr unsigned g_cartesian_product_precedence = 30; constexpr unsigned g_app_precedence = std::numeric_limits::max(); diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 1ac669993..3e00e5d40 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -84,6 +84,7 @@ static format g_geq_fmt = format("\u2265"); static format g_lift_fmt = highlight_keyword(format("lift")); static format g_inst_fmt = highlight_keyword(format("inst")); static format g_sig_fmt = highlight_keyword(format("sig")); +static format g_heq_fmt = highlight_keyword(format("==")); static format g_cartesian_product_fmt = highlight_keyword(format("#")); static format g_cartesian_product_n_fmt = highlight_keyword(format("\u2A2F")); @@ -271,6 +272,7 @@ class pp_fn { return false; case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let: case expr_kind::Sigma: case expr_kind::Pair: case expr_kind::Proj: + case expr_kind::HEq: return false; } return false; @@ -482,6 +484,8 @@ class pp_fn { return g_cartesian_product_precedence; } else if (is_lambda(e) || is_pi(e) || is_let(e) || is_exists(e) || is_sigma(e) || is_pair(e)) { return 0; + } else if (is_heq(e)) { + return g_heq_precedence; } else { return g_app_precedence; } @@ -1163,6 +1167,13 @@ class pp_fn { return result(group(r_format), r_weight); } + result pp_heq(expr const & a, unsigned depth) { + result p_lhs = pp_child(heq_lhs(a), depth); + result p_rhs = pp_child(heq_rhs(a), depth); + format r_format = group(format{p_lhs.first, space(), g_heq_fmt, line(), p_rhs.first}); + return mk_result(r_format, p_lhs.second + p_rhs.second + 1); + } + result pp(expr const & e, unsigned depth, bool main = false) { check_system("pretty printer"); if (!is_atomic(e) && (m_num_steps > m_max_steps || depth > m_max_depth)) { @@ -1199,6 +1210,7 @@ class pp_fn { case expr_kind::Type: r = pp_type(e); break; case expr_kind::Let: r = pp_let(e, depth); break; case expr_kind::MetaVar: r = pp_metavar(e, depth); break; + case expr_kind::HEq: r = pp_heq(e, depth); break; case expr_kind::Pair: r = pp_tuple(e, depth); break; case expr_kind::Proj: r = pp_proj(e, depth); break; } diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 412c4c4f6..9f4e4b038 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -22,6 +22,7 @@ namespace lean { static expr g_dummy(mk_var(0)); expr::expr():expr(g_dummy) {} +// Local context entries local_entry::local_entry(unsigned s, unsigned n):m_kind(local_entry_kind::Lift), m_s(s), m_n(n) {} local_entry::local_entry(unsigned s, expr const & v):m_kind(local_entry_kind::Inst), m_s(s), m_v(v) {} local_entry::~local_entry() {} @@ -87,10 +88,12 @@ void expr_cell::set_is_arrow(bool flag) { lean_assert(is_arrow() && *is_arrow() == flag); } +// Expr variables expr_var::expr_var(unsigned idx): expr_cell(expr_kind::Var, idx, false), m_vidx(idx) {} +// Expr constants expr_const::expr_const(name const & n, optional const & t): expr_cell(expr_kind::Constant, n.hash(), t && t->has_metavar()), m_name(n), @@ -99,6 +102,19 @@ void expr_const::dealloc(buffer & todelete) { dec_ref(m_type, todelete); delete(this); } + +// Expr heterogeneous equality +expr_heq::expr_heq(expr const & lhs, expr const & rhs): + expr_cell(expr_kind::HEq, ::lean::hash(lhs.hash(), rhs.hash()), lhs.has_metavar() || rhs.has_metavar()), + m_lhs(lhs), m_rhs(rhs), m_depth(std::max(get_depth(lhs), get_depth(rhs))+1) { +} +void expr_heq::dealloc(buffer & todelete) { + dec_ref(m_lhs, todelete); + dec_ref(m_rhs, todelete); + delete(this); +} + +// Expr dependent pairs expr_dep_pair::expr_dep_pair(expr const & f, expr const & s, expr const & t): expr_cell(expr_kind::Pair, ::lean::hash(f.hash(), s.hash()), f.has_metavar() || s.has_metavar() || t.has_metavar()), m_first(f), m_second(s), m_type(t), m_depth(std::max(get_depth(f), get_depth(s))+1) { @@ -109,6 +125,8 @@ void expr_dep_pair::dealloc(buffer & todelete) { dec_ref(m_type, todelete); delete(this); } + +// Expr pair projection expr_proj::expr_proj(bool f, expr const & e): expr_cell(expr_kind::Proj, ::lean::hash(17, e.hash()), e.has_metavar()), m_first(f), m_depth(get_depth(e)+1), m_expr(e) {} @@ -116,6 +134,8 @@ void expr_proj::dealloc(buffer & todelete) { dec_ref(m_expr, todelete); delete(this); } + +// Expr applications expr_app::expr_app(unsigned num_args, bool has_mv): expr_cell(expr_kind::App, 0, has_mv), m_num_args(num_args) { @@ -163,6 +183,8 @@ expr mk_app(unsigned n, expr const * as) { to_app(r)->m_depth = depth + 1; return r; } + +// Expr abstractions (and subclasses: Lambda, Pi and Sigma) expr_abstraction::expr_abstraction(expr_kind k, name const & n, expr const & t, expr const & b): expr_cell(k, ::lean::hash(t.hash(), b.hash()), t.has_metavar() || b.has_metavar()), m_name(n), @@ -175,14 +197,21 @@ void expr_abstraction::dealloc(buffer & todelete) { dec_ref(m_domain, todelete); delete(this); } + expr_lambda::expr_lambda(name const & n, expr const & t, expr const & e):expr_abstraction(expr_kind::Lambda, n, t, e) {} + expr_pi::expr_pi(name const & n, expr const & t, expr const & e):expr_abstraction(expr_kind::Pi, n, t, e) {} + expr_sigma::expr_sigma(name const & n, expr const & t, expr const & e):expr_abstraction(expr_kind::Sigma, n, t, e) {} + +// Expr Type expr_type::expr_type(level const & l): expr_cell(expr_kind::Type, l.hash(), false), m_level(l) { } expr_type::~expr_type() {} + +// Expr Let expr_let::expr_let(name const & n, optional const & t, expr const & v, expr const & b): expr_cell(expr_kind::Let, ::lean::hash(v.hash(), b.hash()), v.has_metavar() || b.has_metavar() || (t && t->has_metavar())), m_name(n), @@ -201,6 +230,8 @@ void expr_let::dealloc(buffer & todelete) { delete(this); } expr_let::~expr_let() {} + +// Expr Semantic attachment name value::get_unicode_name() const { return get_name(); } optional value::normalize(unsigned, expr const *) const { return none_expr(); } void value::display(std::ostream & out) const { out << get_name(); } @@ -244,10 +275,12 @@ static expr read_value(deserializer & d) { return it->second(d); } +// Expr Metavariable expr_metavar::expr_metavar(name const & n, local_context const & lctx): expr_cell(expr_kind::MetaVar, n.hash(), true), m_name(n), m_lctx(lctx) {} expr_metavar::~expr_metavar() {} + void expr_cell::dealloc() { try { buffer todo; @@ -268,6 +301,7 @@ void expr_cell::dealloc() { case expr_kind::Lambda: static_cast(it)->dealloc(todo); break; case expr_kind::Pi: static_cast(it)->dealloc(todo); break; case expr_kind::Sigma: static_cast(it)->dealloc(todo); break; + case expr_kind::HEq: static_cast(it)->dealloc(todo); break; case expr_kind::Let: static_cast(it)->dealloc(todo); break; } } @@ -306,6 +340,8 @@ unsigned get_depth(expr const & e) { case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::MetaVar: return 1; + case expr_kind::HEq: + return to_heq(e)->m_depth; case expr_kind::Pair: return to_pair(e)->m_depth; case expr_kind::Proj: @@ -333,6 +369,7 @@ expr copy(expr const & a) { case expr_kind::Pi: return mk_pi(abst_name(a), abst_domain(a), abst_body(a)); case expr_kind::Sigma: return mk_sigma(abst_name(a), abst_domain(a), abst_body(a)); case expr_kind::Let: return mk_let(let_name(a), let_type(a), let_value(a), let_body(a)); + case expr_kind::HEq: return mk_heq(heq_lhs(a), heq_rhs(a)); case expr_kind::MetaVar: return mk_metavar(metavar_name(a), metavar_lctx(a)); } lean_unreachable(); // LCOV_EXCL_LINE @@ -376,7 +413,7 @@ constexpr bool is_small(expr_kind k) { return 0 <= static_cast(k) && stati 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::Pair) && is_small(expr_kind::Proj) && is_small(expr_kind::Lambda) && is_small(expr_kind::Pi) && is_small(expr_kind::Sigma) && is_small(expr_kind::Type) && - is_small(expr_kind::Let) && is_small(expr_kind::MetaVar), "expr_kind is too big"); + is_small(expr_kind::Let) && is_small(expr_kind::HEq) && is_small(expr_kind::MetaVar), "expr_kind is too big"); class expr_serializer : public object_serializer { typedef object_serializer super; @@ -415,6 +452,7 @@ class expr_serializer : public object_serializer const & t, expr const & v, expr const & e); + friend expr mk_heq(expr const & lhs, expr const & rhs); friend expr mk_metavar(name const & n, local_context const & ctx); friend bool is_eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; } @@ -349,6 +351,22 @@ public: value const & get_value() const { return m_val; } }; + +/** \brief Heterogeneous equality */ +class expr_heq : public expr_cell { + expr m_lhs; + expr m_rhs; + unsigned m_depth; + friend expr_cell; + friend expr mk_heq(expr const & lhs, expr const & rhs); + void dealloc(buffer & todelete); + friend unsigned get_depth(expr const & e); +public: + expr_heq(expr const & lhs, expr const & rhs); + expr const & get_lhs() const { return m_lhs; } + expr const & get_rhs() const { return m_rhs; } +}; + /** \see local_entry */ @@ -432,6 +450,7 @@ inline bool is_pi(expr_cell * e) { return e->kind() == expr_kind::Pi; } inline bool is_sigma(expr_cell * e) { return e->kind() == expr_kind::Sigma; } inline bool is_type(expr_cell * e) { return e->kind() == expr_kind::Type; } inline bool is_let(expr_cell * e) { return e->kind() == expr_kind::Let; } +inline bool is_heq(expr_cell * e) { return e->kind() == expr_kind::HEq; } inline bool is_metavar(expr_cell * e) { return e->kind() == expr_kind::MetaVar; } inline bool is_abstraction(expr_cell * e) { return is_lambda(e) || is_pi(e) || is_sigma(e); } @@ -448,6 +467,7 @@ inline bool is_pi(expr const & e) { return e.kind() == expr_kind::Pi; } inline bool is_sigma(expr const & e) { return e.kind() == expr_kind::Sigma; } inline bool is_type(expr const & e) { return e.kind() == expr_kind::Type; } inline bool is_let(expr const & e) { return e.kind() == expr_kind::Let; } +inline bool is_heq(expr const & e) { return e.kind() == expr_kind::HEq; } inline bool is_metavar(expr const & e) { return e.kind() == expr_kind::MetaVar; } inline bool is_abstraction(expr const & e) { return is_lambda(e) || is_pi(e) || is_sigma(e); } // ======================================= @@ -487,6 +507,7 @@ inline expr mk_type(level const & l) { return expr(new expr_type(l)); } expr mk_type(); inline expr Type(level const & l) { return mk_type(l); } inline expr Type() { return mk_type(); } +inline expr mk_heq(expr const & lhs, expr const & rhs) { return expr(new expr_heq(lhs, rhs)); } inline expr mk_metavar(name const & n, local_context const & ctx = local_context()) { return expr(new expr_metavar(n, ctx)); } @@ -514,6 +535,7 @@ inline expr_pi * to_pi(expr_cell * e) { lean_assert(is_pi(e)); inline expr_sigma * to_sigma(expr_cell * e) { lean_assert(is_sigma(e)); return static_cast(e); } inline expr_type * to_type(expr_cell * e) { lean_assert(is_type(e)); return static_cast(e); } inline expr_let * to_let(expr_cell * e) { lean_assert(is_let(e)); return static_cast(e); } +inline expr_heq * to_heq(expr_cell * e) { lean_assert(is_heq(e)); return static_cast(e); } inline expr_metavar * to_metavar(expr_cell * e) { lean_assert(is_metavar(e)); return static_cast(e); } inline expr_var * to_var(expr const & e) { return to_var(e.raw()); } @@ -527,6 +549,7 @@ inline expr_pi * to_pi(expr const & e) { return to_pi(e.raw()) inline expr_sigma * to_sigma(expr const & e) { return to_sigma(e.raw()); } inline expr_let * to_let(expr const & e) { return to_let(e.raw()); } inline expr_type * to_type(expr const & e) { return to_type(e.raw()); } +inline expr_heq * to_heq(expr const & e) { return to_heq(e.raw()); } inline expr_metavar * to_metavar(expr const & e) { return to_metavar(e.raw()); } // ======================================= @@ -556,6 +579,8 @@ inline name const & let_name(expr_cell * e) { return to_let(e)->get inline expr const & let_value(expr_cell * e) { return to_let(e)->get_value(); } inline optional const & let_type(expr_cell * e) { return to_let(e)->get_type(); } inline expr const & let_body(expr_cell * e) { return to_let(e)->get_body(); } +inline expr const & heq_lhs(expr_cell * e) { return to_heq(e)->get_lhs(); } +inline expr const & heq_rhs(expr_cell * e) { return to_heq(e)->get_rhs(); } inline name const & metavar_name(expr_cell * e) { return to_metavar(e)->get_name(); } inline local_context const & metavar_lctx(expr_cell * e) { return to_metavar(e)->get_lctx(); } @@ -592,6 +617,8 @@ inline name const & let_name(expr const & e) { return to_let(e)->ge inline optional const & let_type(expr const & e) { return to_let(e)->get_type(); } inline expr const & let_value(expr const & e) { return to_let(e)->get_value(); } inline expr const & let_body(expr const & e) { return to_let(e)->get_body(); } +inline expr const & heq_lhs(expr const & e) { return to_heq(e)->get_lhs(); } +inline expr const & heq_rhs(expr const & e) { return to_heq(e)->get_rhs(); } inline name const & metavar_name(expr const & e) { return to_metavar(e)->get_name(); } inline local_context const & metavar_lctx(expr const & e) { return to_metavar(e)->get_lctx(); } /** \brief Return the depth of the given expression */ @@ -765,6 +792,12 @@ inline expr update_proj(expr const & e, expr const & new_arg) { else return e; } +inline expr update_heq(expr const & e, expr const & new_lhs, expr const & new_rhs) { + if (!is_eqp(heq_lhs(e), new_lhs) || !is_eqp(heq_rhs(e), new_rhs)) + return mk_heq(new_lhs, new_rhs); + else + return e; +} // ======================================= diff --git a/src/kernel/expr_eq.h b/src/kernel/expr_eq.h index 729033c17..28fa25154 100644 --- a/src/kernel/expr_eq.h +++ b/src/kernel/expr_eq.h @@ -64,6 +64,7 @@ class expr_eq_fn { if (!apply(arg(a, i), arg(b, i))) return false; return true; + case expr_kind::HEq: return heq_lhs(a) == heq_lhs(b) && heq_rhs(a) == heq_rhs(b); case expr_kind::Pair: return pair_first(a) == pair_first(b) && pair_second(a) == pair_second(b) && pair_type(a) == pair_type(b); case expr_kind::Proj: return proj_first(a) == proj_first(b) && proj_arg(a) == proj_arg(b); case expr_kind::Sigma: diff --git a/src/kernel/for_each_fn.h b/src/kernel/for_each_fn.h index 6efdc4785..7cc51ad2b 100644 --- a/src/kernel/for_each_fn.h +++ b/src/kernel/for_each_fn.h @@ -85,6 +85,10 @@ class for_each_fn { } goto begin_loop; } + case expr_kind::HEq: + todo.emplace_back(heq_lhs(e), offset); + todo.emplace_back(heq_rhs(e), offset); + goto begin_loop; case expr_kind::Pair: todo.emplace_back(pair_first(e), offset); todo.emplace_back(pair_second(e), offset); diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp index 54d2368e2..265376adf 100644 --- a/src/kernel/free_vars.cpp +++ b/src/kernel/free_vars.cpp @@ -42,7 +42,7 @@ protected: return var_idx(e) >= offset; case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let: case expr_kind::Sigma: - case expr_kind::Proj: case expr_kind::Pair: + case expr_kind::Proj: case expr_kind::Pair: case expr_kind::HEq: break; } @@ -86,6 +86,9 @@ protected: case expr_kind::Let: result = apply(let_type(e), offset) || apply(let_value(e), offset) || apply(let_body(e), offset + 1); break; + case expr_kind::HEq: + result = apply(heq_lhs(e), offset) || apply(heq_rhs(e), offset); + break; case expr_kind::Proj: result = apply(proj_arg(e), offset); break; @@ -178,6 +181,7 @@ class free_var_range_fn { case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let: case expr_kind::Sigma: case expr_kind::Proj: case expr_kind::Pair: + case expr_kind::HEq: break; } @@ -215,6 +219,9 @@ class free_var_range_fn { case expr_kind::Let: result = std::max({apply(let_type(e)), apply(let_value(e)), dec(apply(let_body(e)))}); break; + case expr_kind::HEq: + result = std::max(apply(heq_lhs(e)), apply(heq_rhs(e))); + break; case expr_kind::Proj: result = apply(proj_arg(e)); break; @@ -301,6 +308,7 @@ protected: case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let: case expr_kind::Sigma: case expr_kind::Proj: case expr_kind::Pair: + case expr_kind::HEq: break; } @@ -345,6 +353,9 @@ protected: case expr_kind::Let: result = apply(let_type(e), offset) || apply(let_value(e), offset) || apply(let_body(e), offset + 1); break; + case expr_kind::HEq: + result = apply(heq_lhs(e), offset) || apply(heq_rhs(e), offset); + break; case expr_kind::Proj: result = apply(proj_arg(e), offset); break; diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp index 6aeb89e18..41e17e089 100644 --- a/src/kernel/kernel_decls.cpp +++ b/src/kernel/kernel_decls.cpp @@ -8,7 +8,7 @@ Released under Apache 2.0 license as described in the file LICENSE. namespace lean { MK_CONSTANT(TypeU, name("TypeU")); MK_CONSTANT(Bool, name("Bool")); -MK_CONSTANT(heq_fn, name("heq")); +MK_CONSTANT(heq2_fn, name("heq2")); MK_CONSTANT(hrefl_fn, name("hrefl")); MK_CONSTANT(eq_fn, name("eq")); MK_CONSTANT(refl_fn, name("refl")); diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h index 34768f45a..eddc52f67 100644 --- a/src/kernel/kernel_decls.h +++ b/src/kernel/kernel_decls.h @@ -9,10 +9,10 @@ expr mk_TypeU(); bool is_TypeU(expr const & e); expr mk_Bool(); bool is_Bool(expr const & e); -expr mk_heq_fn(); -bool is_heq_fn(expr const & e); -inline bool is_heq(expr const & e) { return is_app(e) && is_heq_fn(arg(e, 0)) && num_args(e) == 5; } -inline expr mk_heq(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_heq_fn(), e1, e2, e3, e4}); } +expr mk_heq2_fn(); +bool is_heq2_fn(expr const & e); +inline bool is_heq2(expr const & e) { return is_app(e) && is_heq2_fn(arg(e, 0)) && num_args(e) == 5; } +inline expr mk_heq2(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_heq2_fn(), e1, e2, e3, e4}); } expr mk_hrefl_fn(); bool is_hrefl_fn(expr const & e); inline expr mk_hrefl_th(expr const & e1, expr const & e2) { return mk_app({mk_hrefl_fn(), e1, e2}); } diff --git a/src/kernel/max_sharing.cpp b/src/kernel/max_sharing.cpp index b3e2a7dee..5d9fe1cc0 100644 --- a/src/kernel/max_sharing.cpp +++ b/src/kernel/max_sharing.cpp @@ -52,6 +52,9 @@ struct max_sharing_fn::imp { case expr_kind::Var: case expr_kind::Type: case expr_kind::Value: res = a; break; + case expr_kind::HEq: + res = update_heq(a, apply(heq_lhs(a)), apply(heq_rhs(a))); + break; case expr_kind::Pair: res = update_pair(a, [=](expr const & f, expr const & s, expr const & t) { return std::make_tuple(apply(f), apply(s), apply(t)); diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index c67882126..fea5e8310 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -250,6 +250,12 @@ class normalizer::imp { } break; } + case expr_kind::HEq: { + expr new_lhs = normalize(heq_lhs(a), s, k); + expr new_rhs = normalize(heq_rhs(a), s, k); + r = update_heq(a, new_lhs, new_rhs); + break; + } case expr_kind::Pair: { expr new_first = normalize(pair_first(a), s, k); expr new_second = normalize(pair_second(a), s, k); diff --git a/src/kernel/replace_fn.h b/src/kernel/replace_fn.h index 48202f342..616e341be 100644 --- a/src/kernel/replace_fn.h +++ b/src/kernel/replace_fn.h @@ -144,6 +144,14 @@ public: switch (e.kind()) { case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: case expr_kind::MetaVar: lean_unreachable(); // LCOV_EXCL_LINE + case expr_kind::HEq: + if (check_index(f, 0) && !visit(heq_lhs(e), offset)) + goto begin_loop; + if (check_index(f, 1) && !visit(heq_rhs(e), offset)) + goto begin_loop; + r = update_heq(e, rs(-2), rs(-1)); + pop_rs(2); + break; case expr_kind::Pair: if (check_index(f, 0) && !visit(pair_first(e), offset)) goto begin_loop; diff --git a/src/kernel/replace_visitor.cpp b/src/kernel/replace_visitor.cpp index 0f8d19ce0..b912d2bdb 100644 --- a/src/kernel/replace_visitor.cpp +++ b/src/kernel/replace_visitor.cpp @@ -31,6 +31,10 @@ expr replace_visitor::visit_app(expr const & e, context const & ctx) { lean_assert(is_app(e)); return update_app(e, [&](expr const & c) { return visit(c, ctx); }); } +expr replace_visitor::visit_heq(expr const & e, context const & ctx) { + lean_assert(is_heq(e)); + return update_heq(e, visit(heq_lhs(e), ctx), visit(heq_rhs(e), ctx)); +} expr replace_visitor::visit_abst(expr const & e, context const & ctx) { lean_assert(is_abstraction(e)); return update_abst(e, [&](expr const & t, expr const & b) { @@ -87,6 +91,7 @@ expr replace_visitor::visit(expr const & e, context const & ctx) { case expr_kind::Constant: return save_result(e, visit_constant(e, ctx), shared); case expr_kind::Var: return save_result(e, visit_var(e, ctx), shared); case expr_kind::MetaVar: return save_result(e, visit_metavar(e, ctx), shared); + case expr_kind::HEq: return save_result(e, visit_heq(e, ctx), shared); case expr_kind::Pair: return save_result(e, visit_pair(e, ctx), shared); case expr_kind::Proj: return save_result(e, visit_proj(e, ctx), shared); case expr_kind::App: return save_result(e, visit_app(e, ctx), shared); diff --git a/src/kernel/replace_visitor.h b/src/kernel/replace_visitor.h index d13b4ead2..735bf71ee 100644 --- a/src/kernel/replace_visitor.h +++ b/src/kernel/replace_visitor.h @@ -30,6 +30,7 @@ protected: virtual expr visit_constant(expr const &, context const &); virtual expr visit_var(expr const &, context const &); virtual expr visit_metavar(expr const &, context const &); + virtual expr visit_heq(expr const &, context const &); virtual expr visit_pair(expr const &, context const &); virtual expr visit_proj(expr const &, context const &); virtual expr visit_app(expr const &, context const &); diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 9a5b7746a..60fdffdbf 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -210,6 +210,10 @@ class type_checker::imp { } case expr_kind::Type: return mk_type(ty_level(e) + 1); + case expr_kind::HEq: + if (m_infer_only) + return Bool; + break; case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let: case expr_kind::Sigma: case expr_kind::Proj: @@ -225,6 +229,7 @@ class type_checker::imp { return it->second; } + expr r; switch (e.kind()) { case expr_kind::MetaVar: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: lean_unreachable(); // LCOV_EXCL_LINE; @@ -238,13 +243,14 @@ class type_checker::imp { optional const & b = def.get_body(); lean_assert(b); expr t = infer_type_core(*b, def_ctx); - return save_result(e, lift_free_vars(t, var_idx(e) + 1), shared); + r = lift_free_vars(t, var_idx(e) + 1); + break; } case expr_kind::App: if (m_infer_only) { expr const & f = arg(e, 0); expr f_t = infer_type_core(f, ctx); - return save_result(e, get_range(f_t, e, ctx), shared); + r = get_range(f_t, e, ctx); } else { unsigned num = num_args(e); lean_assert(num >= 2); @@ -263,14 +269,23 @@ class type_checker::imp { throw app_type_mismatch_exception(env(), ctx, e, i, arg_types.size(), arg_types.data()); f_t = pi_body_at(f_t, c); i++; - if (i == num) - return save_result(e, f_t, shared); + if (i == num) { + r = f_t; + break; + } f_t = check_pi(f_t, e, ctx); } } + break; + case expr_kind::HEq: + lean_assert(!m_infer_only); + infer_type_core(heq_lhs(e), ctx); + infer_type_core(heq_rhs(e), ctx); + r = Bool; + break; case expr_kind::Pair: if (m_infer_only) { - return pair_type(e); + r = pair_type(e); } else { expr const & t = pair_type(e); expr sig = check_sigma(t, t, ctx); @@ -284,19 +299,21 @@ class type_checker::imp { if (!is_convertible(s_t, expected, ctx, mk_snd_justification)) { throw pair_type_mismatch_exception(env(), ctx, e, false, s_t, sig); } - return sig; + r = sig; } + break; case expr_kind::Proj: { expr t = check_sigma(infer_type_core(proj_arg(e), ctx), e, ctx); if (proj_first(e)) { - return abst_domain(t); + r = abst_domain(t); } else { expr const & b = abst_body(t); if (closed(b)) - return b; + r = b; else - return instantiate(b, mk_proj1(proj_arg(e))); + r = instantiate(b, mk_proj1(proj_arg(e))); } + break; } case expr_kind::Lambda: if (!m_infer_only) { @@ -305,10 +322,9 @@ class type_checker::imp { } { freset reset(m_cache); - return save_result(e, - mk_pi(abst_name(e), abst_domain(e), infer_type_core(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)))), - shared); + r = mk_pi(abst_name(e), abst_domain(e), infer_type_core(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)))); } + break; case expr_kind::Sigma: case expr_kind::Pi: { expr t1 = check_type(infer_type_core(abst_domain(e), ctx), abst_domain(e), ctx); if (is_bool(t1)) @@ -320,20 +336,22 @@ class type_checker::imp { t2 = check_type(infer_type_core(abst_body(e), new_ctx), abst_body(e), new_ctx); } if (is_bool(t2)) { - if (is_pi(e)) - return t2; - else + if (is_pi(e)) { + r = Bool; + break; + } else { t2 = Type(); + } } if (is_type(t1) && is_type(t2)) { - return save_result(e, mk_type(max(ty_level(t1), ty_level(t2))), shared); + r = mk_type(max(ty_level(t1), ty_level(t2))); } else { lean_assert(m_uc); justification jst = mk_max_type_justification(ctx, e); - expr r = m_menv->mk_metavar(ctx); + r = m_menv->mk_metavar(ctx); m_uc->push_back(mk_max_constraint(new_ctx, lift_free_vars(t1, 0, 1), t2, r, jst)); - return save_result(e, r, shared); } + break; } case expr_kind::Let: { optional lt; @@ -356,10 +374,11 @@ class type_checker::imp { { freset reset(m_cache); expr t = infer_type_core(let_body(e), extend(ctx, let_name(e), lt, let_value(e))); - return save_result(e, instantiate(t, let_value(e)), shared); + r = instantiate(t, let_value(e)); } + break; }} - lean_unreachable(); // LCOV_EXCL_LINE + return save_result(e, r, shared); } bool is_convertible_core(expr const & given, expr const & expected) { diff --git a/src/library/deep_copy.cpp b/src/library/deep_copy.cpp index 5e248feb8..87d32abaa 100644 --- a/src/library/deep_copy.cpp +++ b/src/library/deep_copy.cpp @@ -43,6 +43,7 @@ class deep_copy_fn { new_args.push_back(apply(old_arg)); return save_result(a, mk_app(new_args), sh); } + case expr_kind::HEq: return save_result(a, mk_heq(apply(heq_lhs(a)), apply(heq_rhs(a))), sh); case expr_kind::Pair: return save_result(a, mk_pair(apply(pair_first(a)), apply(pair_second(a)), apply(pair_type(a))), sh); case expr_kind::Proj: return save_result(a, mk_proj(proj_first(a), apply(proj_arg(a))), sh); case expr_kind::Lambda: return save_result(a, mk_lambda(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))), sh); diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 6e57a7278..c080eedb1 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -1675,6 +1675,12 @@ class elaborator::imp { m_conflict = mk_failure_justification(c); return false; } + case expr_kind::HEq: { + justification new_jst(new destruct_justification(c)); + push_new_eq_constraint(ctx, heq_lhs(a), heq_lhs(b), new_jst); + push_new_eq_constraint(ctx, heq_rhs(a), heq_rhs(b), new_jst); + return true; + } case expr_kind::Proj: if (proj_first(a) != proj_first(b)) { m_conflict = mk_failure_justification(c); diff --git a/src/library/expr_lt.cpp b/src/library/expr_lt.cpp index 130b76c03..b44da29d0 100644 --- a/src/library/expr_lt.cpp +++ b/src/library/expr_lt.cpp @@ -41,6 +41,11 @@ bool is_lt(expr const & a, expr const & b, bool use_hash) { return is_lt(arg(a, i), arg(b, i), use_hash); } lean_unreachable(); // LCOV_EXCL_LINE + case expr_kind::HEq: + if (heq_lhs(a) != heq_lhs(b)) + return is_lt(heq_lhs(a), heq_lhs(b), use_hash); + else + return is_lt(heq_rhs(a), heq_rhs(b), use_hash); case expr_kind::Pair: if (pair_first(a) != pair_first(b)) return is_lt(pair_first(a), pair_first(b), use_hash); diff --git a/src/library/fo_unify.cpp b/src/library/fo_unify.cpp index c65a3ab8e..83b2a67fe 100644 --- a/src/library/fo_unify.cpp +++ b/src/library/fo_unify.cpp @@ -62,6 +62,10 @@ optional fo_unify(expr e1, expr e2) { } } break; + case expr_kind::HEq: + todo.emplace_back(heq_lhs(e1), heq_lhs(e2)); + todo.emplace_back(heq_rhs(e1), heq_rhs(e2)); + break; case expr_kind::Proj: if (proj_first(e1) != proj_first(e2)) return optional(); diff --git a/src/library/hop_match.cpp b/src/library/hop_match.cpp index 369210893..ccde9e194 100644 --- a/src/library/hop_match.cpp +++ b/src/library/hop_match.cpp @@ -306,6 +306,10 @@ class hop_match_fn { } case expr_kind::Proj: return proj_first(p) == proj_first(t) && match(proj_arg(p), proj_arg(t), ctx, ctx_size); + case expr_kind::HEq: + return + match(heq_lhs(p), heq_lhs(t), ctx, ctx_size) && + match(heq_rhs(p), heq_rhs(t), ctx, ctx_size); case expr_kind::Pair: return match(pair_first(p), pair_first(t), ctx, ctx_size) && diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 8da1624cc..145f0eb96 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -495,6 +495,7 @@ static int expr_fields(lua_State * L) { case expr_kind::Type: return push_level(L, ty_level(e)); case expr_kind::Value: return to_value(e).push_lua(L); case expr_kind::App: lua_pushinteger(L, num_args(e)); expr_args(L); return 2; + case expr_kind::HEq: push_expr(L, heq_lhs(e)); push_expr(L, heq_rhs(e)); return 3; case expr_kind::Pair: push_expr(L, pair_first(e)); push_expr(L, pair_second(e)); push_expr(L, pair_type(e)); return 3; case expr_kind::Proj: lua_pushboolean(L, proj_first(e)); push_expr(L, proj_arg(e)); return 2; case expr_kind::Lambda: @@ -728,10 +729,14 @@ static void open_expr(lua_State * L) { SET_ENUM("Constant", expr_kind::Constant); SET_ENUM("Type", expr_kind::Type); SET_ENUM("Value", expr_kind::Value); + SET_ENUM("Pair", expr_kind::Pair); + SET_ENUM("Proj", expr_kind::Proj); SET_ENUM("App", expr_kind::App); + SET_ENUM("Sigma", expr_kind::Sigma); SET_ENUM("Lambda", expr_kind::Lambda); SET_ENUM("Pi", expr_kind::Pi); SET_ENUM("Let", expr_kind::Let); + SET_ENUM("HEq", expr_kind::HEq); SET_ENUM("MetaVar", expr_kind::MetaVar); lua_setglobal(L, "expr_kind"); } diff --git a/src/library/printer.cpp b/src/library/printer.cpp index 5d7167303..ab6cc2ac4 100644 --- a/src/library/printer.cpp +++ b/src/library/printer.cpp @@ -19,7 +19,7 @@ bool is_atomic(expr const & e) { return true; case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let: case expr_kind::Sigma: case expr_kind::Proj: - case expr_kind::Pair: + case expr_kind::Pair: case expr_kind::HEq: return false; } return false; @@ -118,6 +118,11 @@ struct print_expr_fn { case expr_kind::App: print_app(a, c); break; + case expr_kind::HEq: + print_child(heq_lhs(a), c); + out() << " == "; + print_child(heq_rhs(a), c); + break; case expr_kind::Pair: print_pair(a, c); break; diff --git a/src/library/rewriter/fo_match.cpp b/src/library/rewriter/fo_match.cpp index 424952da8..ca86a8d72 100644 --- a/src/library/rewriter/fo_match.cpp +++ b/src/library/rewriter/fo_match.cpp @@ -173,7 +173,7 @@ bool fo_match::match_main(expr const & p, expr const & t, unsigned o, subst_map return match_let(p, t, o, s); case expr_kind::MetaVar: return match_metavar(p, t, o, s); - case expr_kind::Proj: case expr_kind::Pair: case expr_kind::Sigma: + case expr_kind::Proj: case expr_kind::Pair: case expr_kind::Sigma: case expr_kind::HEq: // TODO(Leo): break; } diff --git a/src/library/rewriter/rewriter.h b/src/library/rewriter/rewriter.h index 9e980fb87..8ff027d6d 100644 --- a/src/library/rewriter/rewriter.h +++ b/src/library/rewriter/rewriter.h @@ -384,7 +384,7 @@ class apply_rewriter_fn { } } break; - case expr_kind::Proj: case expr_kind::Pair: case expr_kind::Sigma: + case expr_kind::HEq: case expr_kind::Proj: case expr_kind::Pair: case expr_kind::Sigma: // TODO(Leo): break; case expr_kind::Lambda: { diff --git a/src/library/simplifier/ceq.cpp b/src/library/simplifier/ceq.cpp index 69065a961..1ff223397 100644 --- a/src/library/simplifier/ceq.cpp +++ b/src/library/simplifier/ceq.cpp @@ -209,6 +209,10 @@ static bool is_permutation(expr const & lhs, expr const & rhs, unsigned offset, } else { return lhs == rhs; // free variable } + case expr_kind::HEq: + return + is_permutation(heq_lhs(lhs), heq_lhs(rhs), offset, p) && + is_permutation(heq_rhs(lhs), heq_rhs(rhs), offset, p); case expr_kind::Proj: return proj_first(lhs) == proj_first(rhs) && is_permutation(proj_arg(lhs), proj_arg(rhs), offset, p); case expr_kind::Pair: diff --git a/src/library/simplifier/simplifier.cpp b/src/library/simplifier/simplifier.cpp index b190aa9c4..9d8628cf0 100644 --- a/src/library/simplifier/simplifier.cpp +++ b/src/library/simplifier/simplifier.cpp @@ -193,6 +193,14 @@ class simplifier_cell::imp { } }; + static bool is_heq(expr const & e) { + return is_heq2(e); + } + + static expr mk_heq(expr const & A, expr const & B, expr const & a, expr const & b) { + return mk_heq2(A, B, a, b); + } + static expr mk_lambda(name const & n, expr const & d, expr const & b) { return ::lean::mk_lambda(n, d, b); } diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index f56bb8cdc..4ed7b20cb 100644 --- a/src/tests/kernel/expr.cpp +++ b/src/tests/kernel/expr.cpp @@ -84,6 +84,8 @@ static unsigned depth2(expr const & e) { return depth2(proj_arg(e)) + 1; case expr_kind::Pair: return std::max(depth2(pair_first(e)), depth2(pair_second(e))) + 1; + case expr_kind::HEq: + return std::max(depth2(heq_lhs(e)), depth2(heq_rhs(e))) + 1; } return 0; } @@ -145,6 +147,8 @@ static unsigned count_core(expr const & a, expr_set & s) { return count_core(proj_arg(a), s) + 1; case expr_kind::Pair: return count_core(pair_first(a), s) + count_core(pair_second(a), s) + count_core(pair_type(a), s) + 1; + case expr_kind::HEq: + return count_core(heq_lhs(a), s) + count_core(heq_rhs(a), s); } return 0; } diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp index 13cfde2ac..6f2e357ab 100644 --- a/src/tests/kernel/normalizer.cpp +++ b/src/tests/kernel/normalizer.cpp @@ -85,6 +85,8 @@ unsigned count_core(expr const & a, expr_set & s) { return count_core(proj_arg(a), s) + 1; case expr_kind::Pair: return count_core(pair_first(a), s) + count_core(pair_second(a), s) + count_core(pair_type(a), s) + 1; + case expr_kind::HEq: + return count_core(heq_lhs(a), s) + count_core(heq_rhs(a), s); } return 0; }