From 95720b1670487119099cb22c0a32dabcab8e4651 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 28 Jun 2015 19:58:57 -0700 Subject: [PATCH] fix(frontends/lean/elaborator): fixes #687 --- src/frontends/lean/elaborator.cpp | 28 ++++++++++++++++++---------- src/frontends/lean/elaborator.h | 7 +++++-- tests/lean/run/687.lean | 31 +++++++++++++++++++++++++++++++ 3 files changed, 54 insertions(+), 12 deletions(-) create mode 100644 tests/lean/run/687.lean diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 37f8adb09..2836d168a 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -81,13 +81,15 @@ struct elaborator::choice_expr_elaborator : public choice_iterator { elaborator & m_elab; local_context m_context; local_context m_full_context; + bool m_in_equation_lhs; expr m_meta; expr m_type; expr m_choice; unsigned m_idx; - choice_expr_elaborator(elaborator & elab, local_context const & ctx, local_context const & full_ctx, + + choice_expr_elaborator(elaborator & elab, local_context const & ctx, local_context const & full_ctx, bool in_equation_lhs, expr const & meta, expr const & type, expr const & c): - m_elab(elab), m_context(ctx), m_full_context(full_ctx), m_meta(meta), + m_elab(elab), m_context(ctx), m_full_context(full_ctx), m_in_equation_lhs(in_equation_lhs), m_meta(meta), m_type(type), m_choice(c), m_idx(get_num_choices(m_choice)) { } @@ -98,8 +100,9 @@ struct elaborator::choice_expr_elaborator : public choice_iterator { expr const & f = get_app_fn(c); m_elab.save_identifier_info(f); try { - flet set1(m_elab.m_context, m_context); - flet set2(m_elab.m_full_context, m_full_context); + flet set1(m_elab.m_context, m_context); + flet set2(m_elab.m_full_context, m_full_context); + flet set3(m_elab.m_in_equation_lhs, m_in_equation_lhs); pair rcs = m_elab.visit(c); expr r = rcs.first; constraint_seq cs = rcs.second; @@ -314,9 +317,10 @@ expr elaborator::visit_choice(expr const & e, optional const & t, constrai register_meta(m); local_context ctx = m_context; local_context full_ctx = m_full_context; + bool in_equation_lhs = m_in_equation_lhs; auto fn = [=](expr const & meta, expr const & type, substitution const & /* s */, name_generator && /* ngen */) { - return choose(std::make_shared(*this, ctx, full_ctx, meta, type, e)); + return choose(std::make_shared(*this, ctx, full_ctx, in_equation_lhs, meta, type, e)); }; auto pp_fn = [=](formatter const & fmt, pos_info_provider const * pos_prov, substitution const &, bool is_main, bool) { format r = pp_previous_error_header(fmt, pos_prov, some_expr(e), is_main); @@ -553,12 +557,13 @@ pair elaborator::mk_delayed_coercion( } /** \brief Given a term a : a_type, ensure it has type \c expected_type. Apply coercions if needed */ -pair elaborator::ensure_has_type( - expr const & a, expr const & a_type, expr const & expected_type, justification const & j) { +pair elaborator::ensure_has_type_core( + expr const & a, expr const & a_type, expr const & expected_type, bool use_expensive_coercions, justification const & j) { bool lifted_coe = false; - if (has_coercions_from(a_type, lifted_coe) && ((!lifted_coe && is_meta(expected_type)) || (lifted_coe && is_pi_meta(expected_type)))) { + if (use_expensive_coercions && + has_coercions_from(a_type, lifted_coe) && ((!lifted_coe && is_meta(expected_type)) || (lifted_coe && is_pi_meta(expected_type)))) { return mk_delayed_coercion(a, a_type, expected_type, j); - } else if (!m_in_equation_lhs && is_meta(a_type) && has_coercions_to(expected_type)) { + } else if (use_expensive_coercions && !m_in_equation_lhs && is_meta(a_type) && has_coercions_to(expected_type)) { return mk_delayed_coercion(a, a_type, expected_type, j); } else { pair dcs; @@ -668,7 +673,10 @@ expr elaborator::visit_app(expr const & e, constraint_seq & cs) { expr a_type = infer_type(a, a_cs); expr r = mk_app(f, a, e.get_tag()); justification j = mk_app_justification(r, f_type, a, a_type); - auto new_a_cs = ensure_has_type(a, a_type, d_type, j); + // If the application is an equations expression, then we are compiling a match-with, and expensive + // coercions should not be considered. + bool use_expensive_coercions = !is_equations(app_fn(e)); + auto new_a_cs = ensure_has_type_core(a, a_type, d_type, use_expensive_coercions, j); expr new_a = new_a_cs.first; cs += f_cs + new_a_cs.second + a_cs; return update_app(r, app_fn(r), new_a); diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index e2299255a..2f03fe49a 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -124,9 +124,12 @@ class elaborator : public coercion_info_manager { expr apply_coercion(expr const & a, expr a_type, expr d_type); pair mk_delayed_coercion(expr const & a, expr const & a_type, expr const & expected_type, justification const & j); + pair ensure_has_type_core(expr const & a, expr const & a_type, expr const & expected_type, + bool use_expensive_coercions, justification const & j); pair ensure_has_type(expr const & a, expr const & a_type, expr const & expected_type, - justification const & j); - + justification const & j) { + return ensure_has_type_core(a, a_type, expected_type, true, j); + } bool is_choice_app(expr const & e); expr visit_choice_app(expr const & e, constraint_seq & cs); expr visit_app(expr const & e, constraint_seq & cs); diff --git a/tests/lean/run/687.lean b/tests/lean/run/687.lean new file mode 100644 index 000000000..5aea838b9 --- /dev/null +++ b/tests/lean/run/687.lean @@ -0,0 +1,31 @@ +import data.fin + +section rot +open nat fin eq.ops algebra +open eq.ops + +definition rotr₀ {n : nat} : fin n → fin n := +match n with +| 0 := take i, elim0 i +| (succ k) := madd (-maxi) +end + +definition rotr₁ {n : nat} : fin n → fin n := +match n with +| zero := take i, elim0 i +| (succ k) := madd (-maxi) +end + +definition rotr₂ : ∀ {n : nat}, fin n → fin n +| 0 i := elim0 i +| (succ n) i := madd (has_neg.neg maxi) i + +definition rotr₃ : ∀ {n : nat}, fin n → fin n +| 0 := take i, elim0 i +| (succ n) := madd (-maxi) + +definition rotr₄ : ∀ {n : nat}, fin n → fin n +| 0 i := elim0 i +| (succ n) i := madd (-maxi) i + +end rot