From 24528ff68587f32a641e7a5d9195abfa16500370 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 7 Feb 2014 17:54:29 -0800 Subject: [PATCH] fix(library/elaborator): fix glitches in the elaborator that were forcing us to provide parameters explicitly Signed-off-by: Leonardo de Moura --- src/builtin/obj/sum.olean | Bin 9197 -> 9217 bytes src/builtin/sum.lean | 2 +- src/frontends/lean/frontend_elaborator.cpp | 1 + src/frontends/lean/pp.cpp | 2 +- src/kernel/expr.h | 1 + src/kernel/normalizer.cpp | 1 + src/kernel/value.h | 1 + src/library/arith/int.cpp | 1 + src/library/arith/nat.cpp | 1 + src/library/arith/real.cpp | 1 + src/library/elaborator/elaborator.cpp | 33 +++++++++++++++++---- 11 files changed, 36 insertions(+), 8 deletions(-) diff --git a/src/builtin/obj/sum.olean b/src/builtin/obj/sum.olean index c8d422d1fb105b42c1db8277ef6550a97ba709c2..d40e91c1104eafb747c263ffb6140d049ae64831 100644 GIT binary patch delta 2207 zcmZuyU1-}?6u;+mYvy7qcFR}4)}%IdOk}N{op~tKc32b~6nzt8E7|DQCS4lm^d+u+ z5Pay+`yg~LK9b60GigIj*g4q@!B&vRDh(FmZ7jU2@Da9p?$Lq58Ho01+DWjQ;itmTRC5Jq zvia2Dfdi@Z(BLqnhNe}N5K%fc`r5GDbyidBa>Gy!_&I$nHJTkx+wbdrl7D-oQSx~{ z(pfVB`L`h7fwY12$VZ>qsYo4tZoi4_p^0~*N#A+}x}x3UVLlROx@=EJTjMi+8110) zIw9;9ANNB-Mf-O&SSW&D*1DX-?kv^;a79;Jte1T}fd4f`6p*f!)>MNv3`xBOq%PT9 zYA}<}WgP@)9>SmeoJ)_Sq&wvLaGx=@y|#Mag6jlyt|O?a1M4!wa;^j#TJZ5PY|(-e zbj&;ewrGE@X%1r70qX`fZ-V?`L$$jKn%<%pXvquYGFQ=tllZ;Bi$1sx!QrA3FZ8Us zQt)Wb{+5bOP~MHx_79Bah3^!*CD{FiIOY?uF0LBChqW^X_pd6Q@RaOoZ6dTW&lQ#1 zWL=^FmbKNcc1{F2oYLyULd|XYm`f#Kpn)rdP_cAQCOzj{5aDvNUL05A74Mu##k7@N z70P_+ZRgT`aT4jY;Vm!2)}b9biH#|cY4v#4TiXluHFAfp)yKNeWA|&A(FK>2 zu;xl7NgBp>M;gL~N7sr0 zgI~*T%@Fkd=fYs~I>-$@Q4A~+q2Eg}9Ewmj>e~r=YhB5^7u<@yXN;}f(NI{@GGO48 z1Js)ZT73^74*mal@e~TGbW;z0XM?BHSi38tDEIUMO)l)!`o6AOLR`0tGP-3@$P5`; z9~Mx!3sO`AO%OfT;YhQHjZ+K4K^&~Xb(Uct>rJK7DZmT7**lBp?{=vwog|mW!tJF2dg~FSAg)`1II0eqU{jqVM zyoce~g3qA0KOBz&#yH3jH(o1ohjdc+7WL zd!}I3#4f``yLrWC;&IB^x8v~#buyJb5=HxEd}rb)bn!IttKg8H3E=tF3C-Cx*YYM6 z$n*PyXfe(R-2wcY88K3h-#}=2w1n_0+Bm?4k7_q`IJ;D!#UT1J&S91J`r;)v2AzPh IXPSEc118Eos{jB1 delta 2116 zcmZuyU1(fI6rMBH-s-wa(`K`|*(AF+&DNRs{P+a=ymfK2$6Wboh@J@&}4aet(00&mZ-H+m7V{H#TZ8j(Fr{_&6v4h6V*+e=%u>oFVLd)h#;x4w_ShuZx!qL6CVb&>{i0OQ8 z*v}X8IYljy9BGB(dXU>!D=awL;kvfL*CE<@l?@EufT}YK+6{6ofAluUvDQ^OUl{fK z_wV;}gZ&4gRdifbSytuzktYrY(!lGO=*?G+E^oFsndapE$!+d9{5}Wy0;B_ECx7(5 zIh#z;88e&gWYhKa-OftA57hU#W!OzQdLRDPR9G6FGw;;5mp+L>+)U9vX_l;U^drzv zCGdb=4M209NU^Mn>J-+~SjWLtf?i`?UCA04qM`JyDBwsglMUiY6-eXUs6x^2&yN-h z!Rga1>}Jd}ZhALNXigl_2|6!3N`V#cDsyT^4j=>JoTDFyh~|Xg(9}&}E9PgnwH8tZ zaM3)-MUYG8mWH+iD1{bmqD7lXRMHUHd}Qx2n|Q(D04gC-gxJ*65=!t>F{c|Ewk*Qn zinQ@9ut5T`dIf8#3@1dti_r_#$ke2=iT`d0O`vJhm&%sFYGwBxsGyflF5S$m`VB@D z)~X3>95PkHg0zx?o`Z@%CbpoeEeKmt9bu^6NUSAslYqDzfo2Uji5!nYu*_nriu_q& z&6Y+tD*%$7>l@$)q^Y<>92F}F*P5pqo4Q_%>F_o~^`=;LNz;!&5L_?W=n1=CzHXNr zGd=G@`Z3(-1L?XnW@^f)h%UW^Yq-;-j!RO28@C;~O*X z)s=2tE}1>(hY0Kk5rYvQ)5YA7&jU)%Mn(}KDa}hY8L&VwT?lgoSiuR=&?eBIR*Wpn z^=**tQO0dgls>Q!Ou&?HsT*VtNY zykEnv*m!y?9JKgb0PlcoI}>#kfOUL%dg^!xAblfSk{y{TL9)zDZILX<*1OEt>2)+~ zE~M|_H?1vmCml8WGIwl#&_TMR{ON~;eHEu_gZ%U E3uwPMasU7T diff --git a/src/builtin/sum.lean b/src/builtin/sum.lean index 3c98b0436..5e01be3dc 100644 --- a/src/builtin/sum.lean +++ b/src/builtin/sum.lean @@ -68,7 +68,7 @@ theorem inr_inj {A B : (Type U)} {b1 b2 : B} : inr A b1 = inr A b2 → b1 = b2 show b1 = b2, from optional::injectivity (calc some b1 = proj2 (pair (@none A) (some b1)) : refl (some b1) - ... = proj2 (pair (@none A) (some b2)) : @proj2_congr _ _ (pair (@none A) (some b1)) (pair (@none A) (some b2)) rep_eq + ... = proj2 (pair (@none A) (some b2)) : proj2_congr rep_eq ... = some b2 : refl (some b2)) theorem distinct {A B : (Type U)} (a : A) (b : B) : inl a B ≠ inr A b diff --git a/src/frontends/lean/frontend_elaborator.cpp b/src/frontends/lean/frontend_elaborator.cpp index 5ed76cb7c..abde40740 100644 --- a/src/frontends/lean/frontend_elaborator.cpp +++ b/src/frontends/lean/frontend_elaborator.cpp @@ -41,6 +41,7 @@ struct choice_value : public value { virtual expr get_type() const { lean_unreachable(); } // LCOV_EXCL_LINE virtual void write(serializer & ) const { lean_unreachable(); } // LCOV_EXCL_LINE virtual name get_name() const { return name("Choice"); } + virtual bool is_atomic_pp(bool /* unicode */, bool /* coercion */) const { return false; } // NOLINT virtual void display(std::ostream & out) const { out << "(Choice"; for (auto c : m_choices) { diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 3ee879ba5..c29d1b2cc 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -262,7 +262,7 @@ class pp_fn { case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: return true; case expr_kind::Value: - return !is_choice(e); + return to_value(e).is_atomic_pp(m_unicode, m_coercion); case expr_kind::MetaVar: return !metavar_lctx(e); case expr_kind::App: diff --git a/src/kernel/expr.h b/src/kernel/expr.h index fc1350661..c229af204 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -331,6 +331,7 @@ public: virtual void display(std::ostream & out) const; virtual format pp() const; virtual format pp(bool unicode, bool coercion) const; + virtual bool is_atomic_pp(bool unicode, bool coercion) const = 0; virtual int push_lua(lua_State * L) const; virtual unsigned hash() const; virtual void write(serializer & s) const = 0; diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index d556d0e2a..20f42d765 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -67,6 +67,7 @@ public: expr const & get_expr() const { return m_expr; } context const & get_context() const { return m_ctx; } value_stack const & get_stack() const { return m_stack; } + virtual bool is_atomic_pp(bool /* unicode */, bool /* coercion */) const { return false; } // NOLINT }; expr mk_closure(expr const & e, context const & ctx, value_stack const & s) { return mk_value(*(new closure(e, ctx, s))); } diff --git a/src/kernel/value.h b/src/kernel/value.h index 0ad7336a1..bb0e43b48 100644 --- a/src/kernel/value.h +++ b/src/kernel/value.h @@ -17,6 +17,7 @@ public: named_value(name const & n):m_name(n) {} virtual ~named_value() {} virtual name get_name() const { return m_name; } + virtual bool is_atomic_pp(bool /* unicode */, bool /* coercion */) const { return true; } // NOLINT }; /** diff --git a/src/library/arith/int.cpp b/src/library/arith/int.cpp index 939370059..2f3f98b46 100644 --- a/src/library/arith/int.cpp +++ b/src/library/arith/int.cpp @@ -44,6 +44,7 @@ public: else return format(m_val); } + virtual bool is_atomic_pp(bool /* unicode */, bool coercion) const { return !coercion || m_val < 0; } virtual unsigned hash() const { return m_val.hash(); } virtual int push_lua(lua_State * L) const { return push_mpz(L, m_val); } mpz const & get_num() const { return m_val; } diff --git a/src/library/arith/nat.cpp b/src/library/arith/nat.cpp index 37f611e69..ec575c418 100644 --- a/src/library/arith/nat.cpp +++ b/src/library/arith/nat.cpp @@ -36,6 +36,7 @@ public: virtual void display(std::ostream & out) const { out << m_val; } virtual format pp() const { return format(m_val); } virtual format pp(bool, bool) const { return pp(); } + virtual bool is_atomic_pp(bool /* unicode */, bool /* coercion */) const { return true; } // NOLINT virtual unsigned hash() const { return m_val.hash(); } virtual int push_lua(lua_State * L) const { return push_mpz(L, m_val); } mpz const & get_num() const { return m_val; } diff --git a/src/library/arith/real.cpp b/src/library/arith/real.cpp index ed8a8a5fb..0ff87f0e2 100644 --- a/src/library/arith/real.cpp +++ b/src/library/arith/real.cpp @@ -48,6 +48,7 @@ public: else return format(m_val); } + virtual bool is_atomic_pp(bool /* unicode */, bool coercion) const { return !coercion; } virtual unsigned hash() const { return m_val.hash(); } virtual int push_lua(lua_State * L) const { return push_mpq(L, m_val); } mpq const & get_num() const { return m_val; } diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 032a4e36b..dc3a75633 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -538,11 +538,6 @@ class elaborator::imp { swap(new_a, new_b); push_new_constraint(is_eq(c), *new_ctx, new_a, new_b, new_jst); return Processed; - } else if (!has_metavar(b)) { - // Failure, there is no way to unify - // ?m[lift:s:n, ...] with a term that contains variables in [s, s+n] - m_conflict = mk_failure_justification(c); - return Failed; } } } @@ -562,6 +557,28 @@ class elaborator::imp { return Continue; } + bool check_metavar_lift(unification_constraint const & c, expr const & a, expr const & b) { + if (is_metavar(a) && has_local_context(a) && !has_metavar(b)) { + lean_assert(!is_assigned(a)); + local_entry const & me = head(metavar_lctx(a)); + if (me.is_lift()) { + // a is of the form ?m[lift:s:n] + unsigned s = me.s(); + unsigned n = me.n(); + if (has_free_var(b, s, s + n, m_state.m_menv)) { + // Failure, there is no way to unify + // ?m[lift:s:n, ...] with a term that contains variables in [s, s+n] + + // In older commits, this check was being done inside of process_metavar. + // This was incorrect. This check must be performed AFTER b is normalized. + m_conflict = mk_failure_justification(c); + return false; + } + } + } + return true; + } + justification mk_subst_justification(unification_constraint const & c, buffer const & subst_justifications) { if (subst_justifications.size() == 1) { return justification(new substitution_justification(c, subst_justifications[0])); @@ -729,6 +746,8 @@ class elaborator::imp { expr new_a = normalize_step(ctx, a); expr new_b = normalize_step(ctx, b); if (new_a == a && new_b == b) { + if (is_meta(a) || is_meta(b)) + break; // we do not unfold if one of the arguments is a metavar or metavar_app int w_a = get_unfolding_weight(a); int w_b = get_unfolding_weight(b); if (w_a >= 0 || w_b >= 0) { @@ -1687,7 +1706,9 @@ class elaborator::imp { } } - if (!is_meta(a) && !is_meta(b) && normalize_head(a, b, c)) { return true; } + if (!is_meta_app(a) && !is_meta_app(b) && normalize_head(a, b, c)) { return true; } + + if (!check_metavar_lift(c, a, b) || !check_metavar_lift(c, b, a)) { return false; } if (process_simple_ho_match(ctx, a, b, true, c) || process_simple_ho_match(ctx, b, a, false, c))