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

fix(frontends/lean/elaborator): error localization for 'expr_to_tactic' failures

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-23 09:45:16 -07:00
parent 6fcba192b2
commit 2c330e704e
2 changed files with 6 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/frontends/lean/elaborator.cpp
View file

@ -901,7 +901,7 @@ optional<expr> elaborator::get_pre_tactic_for(substitution & subst, expr const &
}
}
optional<tactic> elaborator::pre_tactic_to_tactic(expr const & pre_tac, expr const & mvar) {
optional<tactic> elaborator::pre_tactic_to_tactic(expr const & pre_tac) {
try {
bool relax = m_relax_main_opaque;
auto fn = [=](goal const & g, name_generator const & ngen, expr const & e) {
@ -914,7 +914,8 @@ optional<tactic> elaborator::pre_tactic_to_tactic(expr const & pre_tac, expr con
return optional<tactic>(expr_to_tactic(env(), fn, pre_tac, pip()));
} catch (expr_to_tactic_exception & ex) {
auto out = regular(env(), ios());
display_error_pos(out, pip(), mvar);
flycheck_error err(out);
display_error_pos(out, pip(), ex.get_expr());
out << " " << ex.what();
out << pp_indent_expr(out.get_formatter(), pre_tac) << endl << "failed at:"
<< pp_indent_expr(out.get_formatter(), ex.get_expr()) << endl;
@ -924,7 +925,7 @@ optional<tactic> elaborator::pre_tactic_to_tactic(expr const & pre_tac, expr con
optional<tactic> elaborator::get_local_tactic_hint(substitution & subst, expr const & mvar, name_set & visited) {
if (auto pre_tac = get_pre_tactic_for(subst, mvar, visited)) {
return pre_tactic_to_tactic(*pre_tac, mvar);
return pre_tactic_to_tactic(*pre_tac);
} else {
return optional<tactic>();
}
@ -990,7 +991,7 @@ void elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name_set
} else if (m_use_tactic_hints) {
// using tactic_hints
for (expr const & pre_tac : get_tactic_hints(env())) {
if (auto tac = pre_tactic_to_tactic(pre_tac, mvar)) {
if (auto tac = pre_tactic_to_tactic(pre_tac)) {
bool show_failure = false;
if (try_using(subst, mvar, ps, *tac, show_failure))
return;

2
src/frontends/lean/elaborator.h
View file

@ -123,7 +123,7 @@ class elaborator : public coercion_info_manager {
unify_result_seq solve(constraint_seq const & cs);
void display_unsolved_proof_state(expr const & mvar, proof_state const & ps, char const * msg);
optional<expr> get_pre_tactic_for(substitution & subst, expr const & mvar, name_set & visited);
optional<tactic> pre_tactic_to_tactic(expr const & pre_tac, expr const & mvar);
optional<tactic> pre_tactic_to_tactic(expr const & pre_tac);
optional<tactic> get_local_tactic_hint(substitution & subst, expr const & mvar, name_set & visited);
bool try_using(substitution & subst, expr const & mvar, proof_state const & ps, tactic const & tac,
bool show_failure);