From 27ab49ae9d09713e9191afebd382668f890a4134 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 18 Jan 2014 02:47:11 -0800 Subject: [PATCH] feat(library/simplifier): bottom-up simplifier skeleton Signed-off-by: Leonardo de Moura --- src/builtin/heq.lean | 4 +- src/builtin/kernel.lean | 4 +- src/builtin/obj/heq.olean | Bin 1990 -> 1988 bytes src/builtin/obj/kernel.olean | Bin 25020 -> 25014 bytes src/kernel/free_vars.cpp | 11 +- src/kernel/type_checker.cpp | 30 +- src/kernel/type_checker.h | 12 + src/library/heq_decls.h | 6 +- src/library/simplifier/CMakeLists.txt | 2 +- src/library/simplifier/ceq.cpp | 2 +- src/library/simplifier/ceq.h | 2 +- src/library/simplifier/register_module.h | 2 + src/library/simplifier/simplifier.cpp | 435 +++++++++++++++++++++++ src/library/simplifier/simplifier.h | 15 + 14 files changed, 504 insertions(+), 21 deletions(-) create mode 100644 src/library/simplifier/simplifier.cpp create mode 100644 src/library/simplifier/simplifier.h diff --git a/src/builtin/heq.lean b/src/builtin/heq.lean index 5bc638247..f992acf88 100644 --- a/src/builtin/heq.lean +++ b/src/builtin/heq.lean @@ -4,10 +4,10 @@ infixl 50 == : heq axiom heq_eq {A : TypeU} (a b : A) : a == b ↔ a = b -definition to_eq {A : TypeU} {a b : A} (H : a == b) : a = b +theorem to_eq {A : TypeU} {a b : A} (H : a == b) : a = b := (heq_eq a b) ◂ H -definition to_heq {A : TypeU} {a b : A} (H : a = b) : a == b +theorem to_heq {A : TypeU} {a b : A} (H : a = b) : a == b := (symm (heq_eq a b)) ◂ H theorem hrefl {A : TypeU} (a : A) : a == a diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 53607ac7f..1edc637e9 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -173,8 +173,8 @@ theorem eqt_elim {a : Bool} (H : a = true) : a theorem eqf_elim {a : Bool} (H : a = false) : ¬ a := not_intro (λ Ha : a, H ◂ Ha) -theorem congr1 {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (a : A) (H : f = g) : f a = g a -:= substp (fun h : (∀ x : A, B x), f a = h a) (refl (f a)) H +theorem congr1 {A B : TypeU} {f g : A → B} (a : A) (H : f = g) : f a = g a +:= substp (fun h : A → B, f a = h a) (refl (f a)) H theorem congr2 {A B : TypeU} {a b : A} (f : A → B) (H : a = b) : f a = f b := substp (fun x : A, f a = f x) (refl (f a)) H diff --git a/src/builtin/obj/heq.olean b/src/builtin/obj/heq.olean index 3dfde29b2f304938a755f3dea2b76967b84f9ab1..3bf24218e2c4493ce162f6462554f64eaf171df5 100644 GIT binary patch delta 20 acmX@ce}sR+AEuIwiT@7*$<2ounb`nkR0zTV delta 22 bcmX@Ye~f>^ALf+Qw2A)?f~d_08JXDtc8&>W diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index 395f6b4f808ba1dd36335c95adb0edc929441e48..b11d31aedb1cdcf6d733e4ba22166aad8e66ab3f 100644 GIT binary patch delta 6230 zcmbVQdu&zp9Y4Qw&pEfy-j+h4@5iOR?d@%)!zFL$&)}+7t zJ>U29cYf#h+FAATS#|n{dGyPIqN=drGx)E-F$eK$gyV}BkVjJmNw4HpwG`S6s}vw| z1RMwOfPmuxHVK%@kb2K=0@G#0ln>!?h^q5*!NgE!ey&?gs&lj>e|O6SptXt21UM0( zNAykt=oK&v;I{%!W=QS!WBm)&7Bpvk1e$x{wjKCY8MLRMOBgTGNI_`$uL9?QrfuaW zz&wCDvV4F#vI2lQvO<7i(NM&Y`dYwZfZxCaV-vtgDL{!Ac~oN3=oJzjE%drGKsOzF zqtI9C2pR|x2m{jDk42D8Sw&B!X}5e#HS_3|qNytRL~eDN4e&DH=^L zr4_GN*>rpHS1LrCO8VbTS&}~TE(5IWBi2)Nz*4_o2*-GD(w5T=;dHbig zja2}Kg<}QEAom5Zi|HM&Pj%3j-dxs@I(0WYvVUr0N~j#2qJs38r+_}0x?I_rDTfvEW$wU_6p z=jgWbz=RXv0Pl1F<_Y?FdE3UrfF<{CAWtD!po}I_1xw~BJP&Er041kj=e{t*>j3C! zF@;_1fX6(_WDw2cw5Xy)ouI81xv8)yD$UdMctwpmMZc@a%|0xdl6Dtw!rDB2QBj&I z;YuyeP?5hSOCoz0iV+Qd&3EZ;e^4E!U;87Pd|?#%0(mM+Cp-}4Hr&xP&8zHlEXXFp`W_}4!NDc7O93cuUR+s4?f!lO>MAX?O4Tr&ExP+SwB&t-#MWMqj^4Y#&H-PMPOMHo}-%8y3o%1bza zgt>AP%A{4KK}5Nd$=AvgLSwzwLeNwqnh;7%a+u+mU#|SPjwm_)Y>Y81&n~eZ%>?U- z4t?Clbxe{&?HzNw{C90KEOT)CdTI*fQ%3E0%9u7KPZA=N5ceyn6F_sP6)KZfO7DRl>pOn*>aqYc3t)ksHzt-L>c5bROAX!?xW>|IEqaikP0 zUMi9^*JE_gjHB*@aLCA}twF!X{6s&1We+W$IV0^-0^sQ2k#^?y{G=#85% zs{hcjSsm(C`gB&U`&B;+nd8Yj`=PvSDBum@9{lQ}hv0{qO=o6@s#7(q17bB6X$u<= z7Ap-)I)Y_^%7!vWBdDvPoj2}ZG|W;(bjUTCK5rN|sl+ECoMUFgSjzvFkH$Av=at2* zdyqQy1jwSij5-^ORSE5AoaQcyI`yl@*{t$X}XSKCS9IWGPOCmhT1Tsq>=9jTRYv<)IYIP6k_*N z=cDc&Yg(DpSs`(jFka_NXQ`jkLQOeqwT!qH7KW(gU}##A=>=YGf&Q;(Ok7e&U=!tF@Ch&GWna z;GH!{PtKbWk~%@Jb&wZqM!WFKXB0Cmkab8)GEO_W4P-r|E=rld#p&c{YaiV^zkCq} z+tSa`-N5S9QGO07X;>+M-j`!rjI~cQeVxSg;-~Z1sqE9}Jrlm>nEVC!{S-x5$~ z=&_dK%r_+XM;Wc%J40t$inHH=)6%^f`!2-J_~>y@7L9AoDE$MT--gEMu}ad7gPQ4} zj9g4UTuq{m))Gf#U#7cS`&2%iZ{5bHj!;{>I!=$Y)vJ#wtF6q*gy0B$*0wkEN?eo7 zjk-t=Eok&!73XhaHtXAXwd53Fo&@q5eYn6^b}~sedg>MT^#VU^o95p-WjIQd4l|wP z1G1ph#duQ02|Fd3#b|({absB+sVU>fQj)C+3%z+ua9vQbKnhf)IlP(}Ya2U`;gLaz z&$gW+Q+1gs5{Tg`m6<#WUek$JO1nB9*anQAokjiOx+yam)N&1CM?X_Wcrv{f&Q%l1 z+cB9ghx3PL#2Cd3JAaH98oVGo|5dl#fVDU zzpy#;W^f@hDk2`=On+OLTTq$I%tSe(>D26{%v&etYkxLCIL!aj7&f*KDSBSMgG5FDxk@_QZ-TGN^=&zEs%b?eZH14h95tqj+zWENME*T9i2k0$bH5s80kT$9I zfZvv{GWqtfyTv`p-4N8v+g?)4qczYTP;T1a?rRYD&|x=-^t$$k!Bomzl$8}5BZ*hE zGr`-Dn~LM7PWE}4xwy6=jAv9pN0>gQ6$j!2k@yg>@fm98&|r8{nqcihAd2Yq#kmXC zOZC<>!Z5CzZLocJTYw#HX3xQrNd+B6*)VOR4(hxpl{DLZ6zRxvq;Xc!mX5sP|2tFj zShdlBawIn>9z~`0MB?AeIGsrkLv|Y$d{*0=ZF88X^akM$Fxz*QP}S_@H?_Ql)z6T%@hCD{0!cOCRW$5ys7aTJ$2( z>~L^tARHYxL}#CpyBSlTKc59p80hB!d6Rk-d%k@f*w}T7xr$y`+M4+Y2*t?8~%Cuv`Ixf)L|@VbpIbVnw}wkZg9V|klq z_tZ}uk$4^uEE3O#_Vi?DB0s8#7eniRkxukP_^RnjPlqFUc!!oOtIrzM4?6a3bfB|< zURw6D+(bAI-M&0WIrQV@E#Kv2trf2E69lm~hc*Xs^#kyA3t;X0m zDOf7RTzm@UMeo3*lL96SWPKYaXE5n}$A=syJ=-zoy|QPF(3306Q%AsqO~Y~1TPyEm z%X50mb&eWnQ*UKS0}SX(1nFx&zeiI5r}^UGH@$_*Mdy06TN~q~giMH;j4pW=cUJJD zlMW<|MlTRt05ydIeZ71l|JkY>dZup*L%;2-l`mrl-Qg_boPpWtuHcmq-q-qW;%mhZ z`}rW(m#`X^2<1RN6mtq~Xe`%G1B4!3C%MJ2b^-||M5(N z^N%SOr6KyokOYPav*2T)+DX^?1Nk_zMU{?r$5~A+t91B&-dNsTRk!F~W_7S7IrpK+ ziJjOHicX3?^8bnHded`IA%_oWx>8bazAw0CpgdLTA@%N|dj^(pg5MhO%Xf#s%j%{G+j84@PrczuNCWRD$7zlX$eDlu;6nlvJIQU3KF3R6wpmoz)P*C(ACG59bK- zV9KqVJoj16tZc!S^Ka~chW~A6HIKGyJV`=IZ=u&$ax0K)1%cnKV@W8 zT`bZ^bwrGpk3K6S5rtG$CK!IR+j(G0v;msLl8X?&F*vZMiEI7#n!NB0=7$RO#5(s;G>Av}$?u{LXiGHwn}~nwgwE z_k8C&@9%t%mtIw8UR5vb&80N&$a2TrWZg#?+o5;02nRH#_|w z81uGnzZ1VIjrQlYrNzP^`nS;Kyrz`5WOg=~@~JR?%))U($OYkHLB|8te&+#=2sNKE z^&deCfnI}Z1Fotlz?%SX(c%1ZFT65LFTIu@$n;`{u~G<{dNn^!jiuCr@2BL7v;fF? zbh@CdlreQth(L`k#eje3e{~U9#Ma4F7b&@Ly~?3G3;(5>X_K$Ju0;Z|k(taEfVq%r zh$oPzQ;z(Ytt@2SU7(pQ^tmsr=2D}-d-B}j0>E&`@CikjcNNq{^gDk*EvBpf9F{P0 z!X7qc|AZMy&BZ7ZRZRy|^XR<^%hgtzIq?Ct^~K*#oUW3$Vk{H$4^VPoyE;I32TFa1 znP5msNCkP>!fKEVKfExH&?|v`g_vp{cR)@B_>liqEF$J{T3;N>IEevFpA5u2Nlz8G zY&rs53IIiFJ_r9nG8#oXl$+1tdyCcvGylLXcUp=X*yU^sh*=>m*iw0k>E)&i!~7~k3K1xm@E;H^qi&qU^q*hJrBX~2EXQc zx+_?%j?lBgs2;vBWcUK5lupd(cexF(_Jx{DyPV6Iet~{e`pwMuWsa29F;G9EzfK-a z^`Uv0pW;)7>tUz)E*%anR9EP7XoJq02)s#4%A(~rA;9BdptB~C@mTnl)JQ7D0*^!I z$`(z7J07Gx?v5uD@;r%j%EXwnhF5E#w(`g7Wil$+ljnNp8J{o!LG$D$gh>TS-LP)| zq^$ninyI-kRkOl&mBT&dT-&#v8baeKt!gBtRgBG*0My8wSO99YUTUhyS03uFSmQKcdJVl&u}Sl{ zfIlh5-=Zy`aOJl$7lTs|7XfXiKUJ>OQSKZvsS}fow*j;Vj-UY2;am@BbJhK7y%f^* zsyozI1nZjo9kqk8ed;D{sIF8EbfkI?w~IHcJJc?!s;Mg2g-{wtWluB?ON*y~~J0|J0mhpnf zsI9%A_EKtHtFs>>ymYlXk9O5fRKKDp>Z%x?tMjQp)5mqcS6k@p)Jy6!dVJaW|%qj^7N+i6wN9@Du*uNuz>+sNU)U-e|bW% zzR1x8T3Ww=Tlo*`r>R1E)H8-Ysvj}hACNE%Ff(t={BIT0h#BR%ftdDGL{CX;6X5|` zJfl$g>8mp;yoIh&CuU49C>$1LqaDJg>Il6h5gOevJvmN#SX^u$JY=9;F80(B8|h2xLa%VodeYY<`e1{m@Va;mAN z5>Be98$qQl$i}!)0w!tq0??kV?c{6r%{~lt2f#MHv6V5dcYN#XK>hI7@d zHmWyiZ*v#t_wD9tK9gk5EGv5ub)q%`Aiq{OfL>5+x9nVM08*`;v}tD0+YRfib#!!Q zO_Ssaa;*al&`o#ZS55|kS%>vZrimq1ABNoqMBZ6johW}>57Mq##q-fvEdA{^3M;C; z{1~&OfF%J#yQ1}=X8L>((~IxV>Q&jNQ5+@?aMnwLBEiJLYt$ zJQ|p@oev|8Eeq5M`d&+&`X~LSrBuC3AGUlq^ICkS6ten)_RXE)mlLHq30iK%vm=K9 z^Aw0T>7BWONv8(Qbq|(eu8PKvnaGSxvmFY~E9gfxncmna%1WwCeG!j>SYeMG%wp6t zpPf9Mg^7AZ`iw#dhfdZ7jLAklCL5dSwRxe*HHy(B{Ww90jL6$)YzRRsB<9 zlEf-If0$L+8;mxt&((dsK+RLbBNGcAoRov!t?|W(gcZxz9yiz`iwR}a-#WW&8n_^Y z6Uxw(Z=}%e6^Tfd(UsQRjr)1XJy?o)a;kLA+la9U|4RYcBN($CaET8_B*=upIm9?T z)uzj}LZZd>{dDViI=k5FPmlQtlXR?b9a5-$JNRV*0s|cXvbYR4D5fll=SgMxbyeNY zXnQs^G*j99$^f!w<1k{QZP~R_GT08KSnLWAr&9m?uKa6!HC?@KJ>MoHtJgAF$IH6L z2roEuL8!*CvEMx&hIv49e_O*pWz;UJVh9pzV2W$<6?U7FPAQf{I0_qmVJI#@FE6yuv_gMs6N9 zPCIt)P#sdly2IcSYWoIPa%{E~`bH^;^-MF2OLS>rx{k-~YYa@{QWGO$x6w3I@gV1* zQj)6%M2FZg~i$$P^kti1l`)S-4ez9Ow&n1 z9_@Jmxd7X2lLi*%v`Ss9VajdmLKcd>M!Y$|Om2?_mS`Z@YV8Vov~_fysIsN0P8pgE zZA21SzX5THN=Yp09P|tud%nE^EKTn7h1o=ZS-iru4GJ#_<+$sh4Q!7fn!IZG&$>bP zE-A{w4y6wqvBwX-oWHoFg`RC24PVW(04K>84HdYOx|m|=O;1iA*I}Pc)Dx}sN_*uK z?+>D7Y8ky2Z7Jv&v{3sb+j>{TO0}P$nx&yiS1y{HyHa7H{k*&wnaGY|9|w#8J3;p^ z9h3eHzT+mZqGy)QaUQ|&lk~;XP{b9v4V1x7U)M61VYcqRkm+8>7_lG2XI$K4<-56$|9g4uY6x{u$WE!qkFQEcMv`Q>n4wk5KtB}9 zF;NzUQzAKBDMJh#J~QjrOMel6@;k>vD~glf#W4DXGlI^n*uk2sRu(&3L1>`vm8ISW zDDZgb;g#e1#Ve_4tVp9WCQ#m!^fSni(FnMl#KlpI0#UQcw+LMh#te+e9;9DEEPM|d zp^04`e4)6ztAgQAyQ<{A@1TyH<*^(tE8$PRGkn@LNoA0)JG;Lpp*13o%T;1a%y!h3 zAs2rACIg%0WTBs8EV*2O$yvi7cA)?|h%=^rxz>(RRFIWkWN@{bq7ejV6*8?Oy z9Ghgc!A8FIeA*ov?_t!HEzA-h=yKN5)Si{>`r)3S>ZD)x)Xu*bWQox3Aft&RiX$UB zH2Ti+M;_PR(z%Bbry~{ssRn)vnX#%kxfwiC4V|=Y)ne9lW>ruwPEIF%u&P)`{2=BZ ziurudjd*Bv(7}2VpR)Uph(Q~f;68C9_Qt6HkpX$;b!4UE32LYG7Z7>WS~-7{k(ZPuQavwYKB?A_HAz uCi;b?Wn<(VD-ai~3^(LyYqOhV6TJ00Y%~pX>-mIS_%2DYj#BU1w*LaB$`lm< diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp index 5a791eac5..706033632 100644 --- a/src/kernel/free_vars.cpp +++ b/src/kernel/free_vars.cpp @@ -220,7 +220,10 @@ public: }; unsigned free_var_range(expr const & e, metavar_env const & menv) { - return free_var_range_fn(some_menv(menv))(e); + if (closed(e)) + return 0; + else + return free_var_range_fn(some_menv(menv))(e); } unsigned free_var_range(expr const & e) { @@ -346,7 +349,7 @@ public: }; bool has_free_var(expr const & e, unsigned low, unsigned high, optional const & menv) { - return high > low && has_free_var_in_range_fn(low, high, menv)(e); + return high > low && !closed(e) && has_free_var_in_range_fn(low, high, menv)(e); } bool has_free_var(expr const & e, unsigned low, unsigned high, metavar_env const & menv) { return has_free_var(e, low, high, some_menv(menv)); } bool has_free_var(expr const & e, unsigned low, unsigned high) { return has_free_var(e, low, high, none_menv()); } @@ -366,7 +369,7 @@ bool has_free_var_ge(expr const & e, unsigned low, metavar_env const & menv) { r bool has_free_var_ge(expr const & e, unsigned low) { return has_free_var(e, low, std::numeric_limits::max()); } expr lower_free_vars(expr const & e, unsigned s, unsigned d, optional const & DEBUG_CODE(menv)) { - if (d == 0) + if (d == 0 || closed(e)) return e; lean_assert(s >= d); lean_assert(!has_free_var(e, s-d, s, menv)); @@ -397,7 +400,7 @@ context_entry lower_free_vars(context_entry const & e, unsigned s, unsigned d, m } expr lift_free_vars(expr const & e, unsigned s, unsigned d, optional const & menv) { - if (d == 0) + if (d == 0 || closed(e)) return e; return replace(e, [=](expr const & e, unsigned offset) -> expr { if (is_var(e) && var_idx(e) >= s + offset) { diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 1b38bf910..cec32fa2e 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -18,6 +18,16 @@ Author: Leonardo de Moura #include "kernel/type_checker_justification.h" namespace lean { +expr pi_body_at(expr const & pi, expr const & a) { + lean_assert(is_pi(pi)); + if (closed(abst_body(pi))) + return abst_body(pi); + else if (closed(a)) + return instantiate_with_closed(abst_body(pi), a); + else + return instantiate(abst_body(pi), a); +} + static name g_x_name("x"); /** \brief Auxiliary functional object used to implement infer_type. */ class type_checker::imp { @@ -225,12 +235,7 @@ class type_checker::imp { auto mk_justification = [&](){ return mk_app_type_match_justification(ctx, e, i); }; if (!is_convertible(c_t, abst_domain(f_t), ctx, mk_justification)) throw app_type_mismatch_exception(env(), ctx, e, arg_types.size(), arg_types.data()); - if (closed(abst_body(f_t))) - f_t = abst_body(f_t); - else if (closed(c)) - f_t = instantiate_with_closed(abst_body(f_t), c); - else - f_t = instantiate(abst_body(f_t), c); + f_t = pi_body_at(f_t, c); i++; if (i == num) return save_result(e, f_t, shared); @@ -426,6 +431,16 @@ public: return is_bool(normalize(t, ctx, true)); } + expr ensure_pi(expr const & e, context const & ctx) { + set_ctx(ctx); + update_menv(none_menv()); + try { + return check_pi(e, expr(), ctx); + } catch (exception &) { + throw exception("internal bug, expression is not a Pi"); + } + } + void clear_cache() { m_cache.clear(); m_normalizer.clear(); @@ -474,6 +489,9 @@ bool type_checker::is_convertible(expr const & t1, expr const & t2, context cons void type_checker::check_type(expr const & e, context const & ctx) { m_ptr->check_type(e, ctx); } +expr type_checker::ensure_pi(expr const & e, context const & ctx) { + return m_ptr->ensure_pi(e, ctx); +} bool type_checker::is_proposition(expr const & e, context const & ctx, optional const & menv) { return m_ptr->is_proposition(e, ctx, menv); } diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 3cb3e4350..dec926739 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -14,6 +14,15 @@ Author: Leonardo de Moura namespace lean { class environment; class normalizer; + +/** + \brief Given pi == (Pi x : A, B x), return (B a) + + \pre is_pi(pi) + \pre type of a is A +*/ +expr pi_body_at(expr const & pi, expr const & a); + /** \brief Lean Type Checker. It can also be used to infer types, universes and check whether a type \c A is convertible to a type \c B. @@ -87,6 +96,9 @@ public: bool is_flex_proposition(expr const & e, context const & ctx, metavar_env const & menv); bool is_flex_proposition(expr const & e, context const & ctx = context()); + /** \brief Return a Pi if \c e is convertible to Pi. Throw an exception otherwise. */ + expr ensure_pi(expr const & e, context const & ctx = context()); + /** \brief Reset internal caches */ void clear(); diff --git a/src/library/heq_decls.h b/src/library/heq_decls.h index 83533e845..f22e4e518 100644 --- a/src/library/heq_decls.h +++ b/src/library/heq_decls.h @@ -14,12 +14,10 @@ bool is_heq_eq_fn(expr const & e); inline expr mk_heq_eq_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_heq_eq_fn(), e1, e2, e3}); } expr mk_to_eq_fn(); bool is_to_eq_fn(expr const & e); -inline bool is_to_eq(expr const & e) { return is_app(e) && is_to_eq_fn(arg(e, 0)); } -inline expr mk_to_eq(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_to_eq_fn(), e1, e2, e3, e4}); } +inline expr mk_to_eq_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_to_eq_fn(), e1, e2, e3, e4}); } expr mk_to_heq_fn(); bool is_to_heq_fn(expr const & e); -inline bool is_to_heq(expr const & e) { return is_app(e) && is_to_heq_fn(arg(e, 0)); } -inline expr mk_to_heq(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_to_heq_fn(), e1, e2, e3, e4}); } +inline expr mk_to_heq_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_to_heq_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/library/simplifier/CMakeLists.txt b/src/library/simplifier/CMakeLists.txt index 103193e20..1264715a2 100644 --- a/src/library/simplifier/CMakeLists.txt +++ b/src/library/simplifier/CMakeLists.txt @@ -1,2 +1,2 @@ -add_library(simplifier ceq.cpp) +add_library(simplifier ceq.cpp simplifier.cpp rewrite_rule_set.cpp) target_link_libraries(simplifier ${LEAN_LIBS}) diff --git a/src/library/simplifier/ceq.cpp b/src/library/simplifier/ceq.cpp index 66a753561..cf5a3a6ac 100644 --- a/src/library/simplifier/ceq.cpp +++ b/src/library/simplifier/ceq.cpp @@ -1,5 +1,5 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura diff --git a/src/library/simplifier/ceq.h b/src/library/simplifier/ceq.h index ac4527ae5..0c397bee0 100644 --- a/src/library/simplifier/ceq.h +++ b/src/library/simplifier/ceq.h @@ -1,5 +1,5 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura diff --git a/src/library/simplifier/register_module.h b/src/library/simplifier/register_module.h index 89e643b00..f66488490 100644 --- a/src/library/simplifier/register_module.h +++ b/src/library/simplifier/register_module.h @@ -7,10 +7,12 @@ Author: Leonardo de Moura #pragma once #include "util/script_state.h" #include "library/simplifier/ceq.h" +#include "library/simplifier/simplifier.h" namespace lean { inline void open_simplifier_module(lua_State * L) { open_ceq(L); + open_simplifier(L); } inline void register_simplifier_module() { script_state::register_module(open_simplifier_module); diff --git a/src/library/simplifier/simplifier.cpp b/src/library/simplifier/simplifier.cpp new file mode 100644 index 000000000..6e2302ae7 --- /dev/null +++ b/src/library/simplifier/simplifier.cpp @@ -0,0 +1,435 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include "util/flet.h" +#include "util/interrupt.h" +#include "kernel/type_checker.h" +#include "kernel/free_vars.h" +#include "kernel/instantiate.h" +#include "kernel/kernel.h" +#include "library/heq_decls.h" +#include "library/kernel_bindings.h" +#include "library/expr_pair.h" +#include "library/hop_match.h" + +#ifndef LEAN_SIMPLIFIER_PROOFS +#define LEAN_SIMPLIFIER_PROOFS true +#endif + +#ifndef LEAN_SIMPLIFIER_CONTEXTUAL +#define LEAN_SIMPLIFIER_CONTEXTUAL true +#endif + +#ifndef LEAN_SIMPLIFIER_SINGLE_PASS +#define LEAN_SIMPLIFIER_SINGLE_PASS false +#endif + +#ifndef LEAN_SIMPLIFIER_BETA +#define LEAN_SIMPLIFIER_BETA true +#endif + +#ifndef LEAN_SIMPLIFIER_UNFOLD +#define LEAN_SIMPLIFIER_UNFOLD false +#endif + +#ifndef LEAN_SIMPLIFIER_MAX_STEPS +#define LEAN_SIMPLIFIER_MAX_STEPS std::numeric_limits::max() +#endif + +namespace lean { +static name g_simplifier_proofs {"simplifier", "proofs"}; +static name g_simplifier_contextual {"simplifier", "contextual"}; +static name g_simplifier_single_pass {"simplifier", "single_pass"}; +static name g_simplifier_beta {"simplifier", "beta"}; +static name g_simplifier_unfold {"simplifier", "unfold"}; +static name g_simplifier_max_steps {"simplifier", "max_steps"}; + +RegisterBoolOption(g_simplifier_proofs, LEAN_SIMPLIFIER_PROOFS, "(simplifier) generate proofs"); +RegisterBoolOption(g_simplifier_contextual, LEAN_SIMPLIFIER_CONTEXTUAL, "(simplifier) contextual simplification"); +RegisterBoolOption(g_simplifier_single_pass, LEAN_SIMPLIFIER_SINGLE_PASS, "(simplifier) if false then the simplifier keeps applying simplifications as long as possible"); +RegisterBoolOption(g_simplifier_beta, LEAN_SIMPLIFIER_BETA, "(simplifier) use beta-reductions"); +RegisterBoolOption(g_simplifier_unfold, LEAN_SIMPLIFIER_UNFOLD, "(simplifier) unfolds non-opaque definitions"); +RegisterUnsignedOption(g_simplifier_max_steps, LEAN_SIMPLIFIER_MAX_STEPS, "(simplifier) maximum number of steps"); + +bool get_simplifier_proofs(options const & opts) { + return opts.get_bool(g_simplifier_proofs, LEAN_SIMPLIFIER_PROOFS); +} +bool get_simplifier_contextual(options const & opts) { + return opts.get_bool(g_simplifier_contextual, LEAN_SIMPLIFIER_CONTEXTUAL); +} +bool get_simplifier_single_pass(options const & opts) { + return opts.get_bool(g_simplifier_single_pass, LEAN_SIMPLIFIER_SINGLE_PASS); +} +bool get_simplifier_beta(options const & opts) { + return opts.get_bool(g_simplifier_beta, LEAN_SIMPLIFIER_BETA); +} +bool get_simplifier_unfold(options const & opts) { + return opts.get_bool(g_simplifier_unfold, LEAN_SIMPLIFIER_UNFOLD); +} +unsigned get_simplifier_max_steps(options const & opts) { + return opts.get_unsigned(g_simplifier_max_steps, LEAN_SIMPLIFIER_MAX_STEPS); +} + +class simplifier_fn { + ro_environment m_env; + type_checker m_tc; + bool m_has_heq; + context m_ctx; + + // Configuration + bool m_proofs_enabled; + bool m_contextual; + bool m_single_pass; + bool m_beta; + bool m_unfold; + unsigned m_max_steps; + + struct result { + expr m_out; + optional m_proof; + bool m_heq_proof; + explicit result(expr const & out, bool heq_proof = false):m_out(out), m_heq_proof(heq_proof) {} + result(expr const & out, expr const & pr, bool heq_proof = false):m_out(out), m_proof(pr), m_heq_proof(heq_proof) {} + }; + + struct set_context { + flet m_set; + set_context(simplifier_fn & s, context const & new_ctx):m_set(s.m_ctx, new_ctx) {} + }; + + /** + \brief Return a lambda with body \c new_body, and name and domain from abst. + */ + static expr mk_lambda(expr const & abst, expr const & new_body) { + return ::lean::mk_lambda(abst_name(abst), abst_domain(abst), new_body); + } + + bool is_proposition(expr const & e) { + return m_tc.is_proposition(e, m_ctx); + } + + expr infer_type(expr const & e) { + return m_tc.infer_type(e, m_ctx); + } + + expr ensure_pi(expr const & e) { + return m_tc.ensure_pi(e, m_ctx); + } + + expr mk_congr1_th(expr const & f_type, expr const & f, expr const & new_f, expr const & a, expr const & Heq_f) { + expr const & A = abst_domain(f_type); + expr const & B = lower_free_vars(abst_body(f_type), 1, 1); + return ::lean::mk_congr1_th(A, B, f, new_f, a, Heq_f); + } + + expr mk_congr2_th(expr const & f_type, expr const & a, expr const & new_a, expr const & f, expr const & Heq_a) { + expr const & A = abst_domain(f_type); + expr const & B = lower_free_vars(abst_body(f_type), 1, 1); + return ::lean::mk_congr2_th(A, B, a, new_a, f, Heq_a); + } + + expr mk_congr_th(expr const & f_type, expr const & f, expr const & new_f, expr const & a, expr const & new_a, + expr const & Heq_f, expr const & Heq_a) { + expr const & A = abst_domain(f_type); + expr const & B = lower_free_vars(abst_body(f_type), 1, 1); + return ::lean::mk_congr_th(A, B, f, new_f, a, new_a, Heq_f, Heq_a); + } + + expr mk_hcongr_th(expr const & f_type, expr const & new_f_type, expr const & f, expr const & new_f, + expr const & a, expr const & new_a, expr const & Heq_f, expr const & Heq_a) { + return ::lean::mk_hcongr_th(abst_domain(f_type), + abst_domain(new_f_type), + mk_lambda(f_type, abst_body(f_type)), + mk_lambda(new_f_type, abst_body(new_f_type)), + f, new_f, a, new_a, Heq_f, Heq_a); + } + + expr mk_app_prefix(unsigned i, expr const & a) { + lean_assert(i > 0); + if (i == 1) + return arg(a, 0); + else + return mk_app(i, &arg(a, 0)); + } + + expr mk_app_prefix(unsigned i, buffer const & args) { + lean_assert(i > 0); + if (i == 1) + return args[0]; + else + return mk_app(i, args.data()); + } + + result simplify_app(expr const & e) { + lean_assert(is_app(e)); + buffer new_args; + buffer> proofs; // used only if m_proofs_enabled + buffer f_types, new_f_types; // used only if m_proofs_enabled + buffer heq_proofs; // used only if m_has_heq && m_proofs_enabled + bool changed = false; + expr f = arg(e, 0); + expr f_type = infer_type(f); + result res_f = simplify(f); + expr new_f = res_f.m_out; + expr new_f_type; + if (new_f != f) + changed = true; + new_args.push_back(new_f); + if (m_proofs_enabled) { + proofs.push_back(res_f.m_proof); + f_types.push_back(f_type); + new_f_type = res_f.m_heq_proof ? infer_type(new_f) : f_type; + new_f_types.push_back(new_f_type); + if (m_has_heq) + heq_proofs.push_back(res_f.m_heq_proof); + } + unsigned num = num_args(e); + for (unsigned i = 1; i < num; i++) { + f_type = ensure_pi(f_type); + bool f_arrow = is_arrow(f_type); + expr const & a = arg(e, i); + result res_a(a); + if (m_has_heq || f_arrow) { + res_a = simplify(a); + if (res_a.m_out != a) + changed = true; + } + expr new_a = res_a.m_out; + new_args.push_back(new_a); + if (m_proofs_enabled) { + proofs.push_back(res_a.m_proof); + if (m_has_heq) + heq_proofs.push_back(res_a.m_heq_proof); + bool changed_f_type = !is_eqp(f_type, new_f_type); + if (f_arrow) { + f_type = lower_free_vars(abst_body(f_type), 1, 1); + new_f_type = changed_f_type ? lower_free_vars(abst_body(new_f_type), 1, 1) : f_type; + } else if (is_eqp(a, new_a)) { + f_type = pi_body_at(f_type, a); + new_f_type = changed_f_type ? pi_body_at(new_f_type, a) : f_type; + } else { + f_type = pi_body_at(f_type, a); + new_f_type = pi_body_at(new_f_type, new_a); + } + f_types.push_back(f_type); + new_f_types.push_back(new_f_type); + } + } + + if (!changed) { + return rewrite_app(result(e)); + } else if (!m_proofs_enabled) { + return rewrite_app(result(mk_app(new_args))); + } else { + expr out = mk_app(new_args); + unsigned i = 0; + while (i < num && !proofs[i]) { + // skip "reflexive" proofs + i++; + } + if (i == num) + return result(out); + expr pr; + bool heq_proof = false; + if (i == 0) { + pr = *(proofs[0]); + heq_proof = heq_proofs[0]; + } else if (m_has_heq && heq_proofs[i]) { + expr f = mk_app_prefix(i, new_args); + pr = mk_hcongr_th(f_types[i-1], f_types[i-1], f, f, arg(e, i), new_args[i], + mk_hrefl_th(f_types[i-1], f), *(proofs[i])); + heq_proof = true; + } else { + expr f = mk_app_prefix(i, new_args); + pr = mk_congr2_th(f_types[i-1], arg(e, i), new_args[i], f, *(proofs[i])); + } + i++; + for (; i < num; i++) { + expr f = mk_app_prefix(i, e); + expr new_f = mk_app_prefix(i, new_args); + if (proofs[i]) { + if (m_has_heq && heq_proofs[i]) { + if (!heq_proof) + pr = mk_to_heq_th(f_types[i], f, new_f, pr); + pr = mk_hcongr_th(f_types[i-1], new_f_types[i-1], f, new_f, arg(e, i), new_args[i], pr, *(proofs[i])); + heq_proof = true; + } else { + pr = mk_congr_th(f_types[i-1], f, new_f, arg(e, i), new_args[i], pr, *(proofs[i])); + } + } else if (heq_proof) { + pr = mk_hcongr_th(f_types[i-1], new_f_types[i-1], f, new_f, arg(e, i), arg(e, i), + pr, mk_hrefl_th(abst_domain(f_types[i-1]), arg(e, i))); + } else { + lean_assert(!heq_proof); + pr = mk_congr1_th(f_types[i-1], f, new_f, arg(e, i), pr); + } + } + return rewrite_app(result(out, pr, heq_proof)); + } + } + + result rewrite_app(result const & r) { + return r; + } + + result simplify_var(expr const & e) { + if (m_has_heq) { + // TODO(Leo) + return result(e); + } else { + return result(e); + } + } + + result simplify_constant(expr const & e) { + lean_assert(is_constant(e)); + if (m_unfold) { + auto obj = m_env->find_object(const_name(e)); + if (should_unfold(obj)) { + expr e = obj->get_value(); + if (m_single_pass) { + return result(e); + } else { + return simplify(e); + } + } + } +#if 1 + if (const_name(e) == "a") { + auto obj = m_env->find_object("a_eq_0"); + if (obj) { + expr r = arg(obj->get_type(), 3); + return result(r, mk_constant("a_eq_0")); + } + } +#endif + + return result(e); + } + + result simplify_lambda(expr const & e) { + lean_assert(is_lambda(e)); + if (m_has_heq) { + // TODO(Leo) + return result(e); + } else { + set_context set(*this, extend(m_ctx, abst_name(e), abst_domain(e))); + result res_body = simplify(abst_body(e)); + lean_assert(!res_body.m_heq_proof); + expr new_body = res_body.m_out; + if (is_eqp(new_body, abst_body(e))) + return result(e); + expr out = mk_lambda(e, new_body); + if (!m_proofs_enabled) + return result(out); + expr body_type = infer_type(abst_body(e)); + expr pr = mk_funext_th(abst_domain(e), mk_lambda(e, body_type), e, out, + mk_lambda(e, *(res_body.m_proof))); + return result(out, pr); + } + } + + result simplify_pi(expr const & e) { + lean_assert(is_pi(e)); + if (m_has_heq) { + // TODO(Leo) + return result(e); + } else if (is_proposition(e)) { + set_context set(*this, extend(m_ctx, abst_name(e), abst_domain(e))); + result res_body = simplify(abst_body(e)); + lean_assert(!res_body.m_heq_proof); + expr new_body = res_body.m_out; + if (is_eqp(new_body, abst_body(e))) + return result(e); + expr out = mk_pi(abst_name(e), abst_domain(e), new_body); + if (!m_proofs_enabled) + return result(out); + expr pr = mk_allext_th(abst_domain(e), + mk_lambda(e, abst_body(e)), + mk_lambda(e, abst_body(out)), + mk_lambda(e, *(res_body.m_proof))); + return result(out, pr); + } else { + // if the environment does not contain heq axioms, then we don't simplify Pi's that are not forall's + return result(e); + } + } + + result simplify(expr const & e) { + check_system("simplifier"); + switch (e.kind()) { + case expr_kind::Var: return simplify_var(e); + case expr_kind::Constant: return simplify_constant(e); + case expr_kind::Type: + case expr_kind::MetaVar: + case expr_kind::Value: return result(e); + case expr_kind::App: return simplify_app(e); + case expr_kind::Lambda: return simplify_lambda(e); + case expr_kind::Pi: return simplify_pi(e); + case expr_kind::Let: return simplify(instantiate(let_body(e), let_value(e))); + } + lean_unreachable(); + } + + void set_options(options const & o) { + m_proofs_enabled = get_simplifier_proofs(o); + m_contextual = get_simplifier_contextual(o); + m_single_pass = get_simplifier_single_pass(o); + m_beta = get_simplifier_beta(o); + m_unfold = true; // get_simplifier_unfold(o); + m_max_steps = get_simplifier_max_steps(o); + } + +public: + simplifier_fn(ro_environment const & env, options const & o): + m_env(env), m_tc(env) { + m_has_heq = m_env->imported("heq"); + set_options(o); + } + + expr_pair operator()(expr const & e, context const & ctx) { + set_context set(*this, ctx); + auto r = simplify(e); + if (r.m_proof) { + return mk_pair(r.m_out, *(r.m_proof)); + } else { + return mk_pair(r.m_out, mk_refl_th(infer_type(r.m_out), r.m_out)); + } + } +}; + +expr_pair simplify(expr const & e, ro_environment const & env, context const & ctx, options const & opts) { + return simplifier_fn(env, opts)(e, ctx); +} + +static int simplify_core(lua_State * L, expr const & e, ro_shared_environment const & env) { + int nargs = lua_gettop(L); + context ctx; + options opts; + if (nargs >= 3) + ctx = to_context(L, 3); + if (nargs >= 4) + opts = to_options(L, 4); + auto r = simplify(e, env, ctx, opts); + push_expr(L, r.first); + push_expr(L, r.second); + return 2; +} + +static int simplify(lua_State * L) { + int nargs = lua_gettop(L); + expr const & e = to_expr(L, 1); + if (nargs == 1) + return simplify_core(L, e, ro_shared_environment(L)); + else + return simplify_core(L, e, ro_shared_environment(L, 2)); +} + +void open_simplifier(lua_State * L) { + SET_GLOBAL_FUN(simplify, "simplify"); +} +} diff --git a/src/library/simplifier/simplifier.h b/src/library/simplifier/simplifier.h new file mode 100644 index 000000000..d697fd9b1 --- /dev/null +++ b/src/library/simplifier/simplifier.h @@ -0,0 +1,15 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "util/lua.h" +#include "kernel/environment.h" +#include "library/expr_pair.h" + +namespace lean { +expr_pair simplify(expr const & e, ro_environment const & env, context const & ctx, options const & opts); +void open_simplifier(lua_State * L); +}