michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/tactic/rewrite_tactic): display type error message when

Browse source 
rewrite tactic fails
This commit is contained in:
Leonardo de Moura 2015-05-05 19:21:27 -07:00
parent 9bb8c5c98a
commit a4efefb6ff
2 changed files with 33 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

33
src/library/tactic/rewrite_tactic.cpp
View file

@ -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<kernel_exception> saved_ex;
if (ex)
saved_ex.reset(static_cast<kernel_exception*>(ex->clone()));
if (m_ps.report_failure()) { if (m_ps.report_failure()) {
proof_state curr_ps(m_ps, cons(m_g, tail(m_ps.get_goals())), m_subst, m_ngen); 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) { if (!m_use_trace || !m_trace_initialized) {
throw tactic_exception("rewrite step failed", some_expr(elem), curr_ps, throw tactic_exception("rewrite step failed", some_expr(elem), curr_ps,
[=](formatter const &) { [=](formatter const & fmt) {
if (type_error) format r;
return format("invalid 'rewrite' tactic, " if (type_error) {
r = format("invalid 'rewrite' tactic, "
"rewrite step produced type incorrect term"); "rewrite step produced type incorrect term");
else if (saved_ex) {
return format("invalid 'rewrite' tactic, rewrite step failed"); r += saved_ex->pp(fmt);
r += line();
}
} else {
r = format("invalid 'rewrite' tactic, rewrite step failed");
}
return r;
}); });
} else { } else {
trace saved_trace = m_trace; trace saved_trace = m_trace;
throw tactic_exception("rewrite step failed", some_expr(elem), curr_ps, throw tactic_exception("rewrite step failed", some_expr(elem), curr_ps,
[=](formatter const & fmt) { [=](formatter const & fmt) {
format r; format r;
if (type_error) if (type_error) {
r += format("invalid 'rewrite' tactic, " r += format("invalid 'rewrite' tactic, "
"step produced type incorrect term, details: "); "step produced type incorrect term, details: ");
else if (saved_ex) {
r += saved_ex->pp(fmt);
r += line();
}
} else {
r += format("invalid 'rewrite' tactic, "); r += format("invalid 'rewrite' tactic, ");
}
r += saved_trace.pp(fmt); r += saved_trace.pp(fmt);
return r; return r;
}); });
@ -1481,7 +1496,7 @@ public:
return proof_state_seq(); return proof_state_seq();
} }
} catch (kernel_exception & ex) { } catch (kernel_exception & ex) {
process_failure(elem, true); process_failure(elem, true, &ex);
return proof_state_seq(); return proof_state_seq();
} }
} }

10
tests/lean/550.lean.expected.out
View file

@ -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 finv ∘ func
proof state: proof state:
A : Type, A : Type,