From a4efefb6ff830e6e561a33eb4896872b46e4a02d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 5 May 2015 19:21:27 -0700 Subject: [PATCH] feat(library/tactic/rewrite_tactic): display type error message when rewrite tactic fails --- src/library/tactic/rewrite_tactic.cpp | 33 +++++++++++++++++++-------- tests/lean/550.lean.expected.out | 10 +++++++- 2 files changed, 33 insertions(+), 10 deletions(-) diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index 25f35db1a..820a036af 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -1427,28 +1427,43 @@ class rewrite_fn { } } - void process_failure(expr const & elem, bool type_error) { + void process_failure(expr const & elem, bool type_error, kernel_exception * ex = nullptr) { + std::shared_ptr saved_ex; + if (ex) + saved_ex.reset(static_cast(ex->clone())); if (m_ps.report_failure()) { proof_state curr_ps(m_ps, cons(m_g, tail(m_ps.get_goals())), m_subst, m_ngen); if (!m_use_trace || !m_trace_initialized) { throw tactic_exception("rewrite step failed", some_expr(elem), curr_ps, - [=](formatter const &) { - if (type_error) - return format("invalid 'rewrite' tactic, " + [=](formatter const & fmt) { + format r; + if (type_error) { + r = format("invalid 'rewrite' tactic, " "rewrite step produced type incorrect term"); - else - return format("invalid 'rewrite' tactic, rewrite step failed"); + if (saved_ex) { + r += saved_ex->pp(fmt); + r += line(); + } + } else { + r = format("invalid 'rewrite' tactic, rewrite step failed"); + } + return r; }); } else { trace saved_trace = m_trace; throw tactic_exception("rewrite step failed", some_expr(elem), curr_ps, [=](formatter const & fmt) { format r; - if (type_error) + if (type_error) { r += format("invalid 'rewrite' tactic, " "step produced type incorrect term, details: "); - else + if (saved_ex) { + r += saved_ex->pp(fmt); + r += line(); + } + } else { r += format("invalid 'rewrite' tactic, "); + } r += saved_trace.pp(fmt); return r; }); @@ -1481,7 +1496,7 @@ public: return proof_state_seq(); } } catch (kernel_exception & ex) { - process_failure(elem, true); + process_failure(elem, true, &ex); return proof_state_seq(); } } diff --git a/tests/lean/550.lean.expected.out b/tests/lean/550.lean.expected.out index ab3b4e8c5..c07a78000 100644 --- a/tests/lean/550.lean.expected.out +++ b/tests/lean/550.lean.expected.out @@ -1,4 +1,12 @@ -550.lean:44:72: error:invalid 'rewrite' tactic, step produced type incorrect term, details: rewrite step failed using pattern +550.lean:44:72: error:invalid 'rewrite' tactic, step produced type incorrect term, details: type mismatch at application + eq.rec (eq.rec (eq.refl function.id) (eq.symm linv)) +term + eq.rec (eq.refl function.id) (eq.symm linv) +has type + x = function.id +but is expected to have type + finv ∘ func = function.id +rewrite step failed using pattern finv ∘ func proof state: A : Type,