From ee531ec0e20af9fd384d7666e44b73af1501bf31 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 2 Jul 2014 14:09:01 -0700 Subject: [PATCH] feat(frontends/parser): improve error message when an apply tactic refers a local constant that is not marked as [fact] Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.cpp | 26 ++++++++++++++++---------- src/library/tactic/apply_tactic.cpp | 17 ++++++++++++++++- src/library/tactic/expr_to_tactic.h | 7 ++----- src/library/tactic/tactic.cpp | 3 +++ src/library/tactic/tactic.h | 8 ++++++++ tests/lean/run/tactic11.lean | 13 +++++++------ 6 files changed, 52 insertions(+), 22 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 07f7768db..868d70609 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -665,18 +665,24 @@ public: expr type = m_tc.infer(*meta); proof_state ps(goals(goal(*meta, type)), subst, m_ngen.mk_child()); if (optional t = get_tactic_for(subst, mvar)) { - proof_state_seq seq = (*t)(m_env, m_ios, ps); - if (auto r = seq.pull()) { - subst = r->first.get_subst(); - expr v = subst.instantiate_metavars_wo_jst(mvar); - if (has_metavar(v)) { - display_unsolved_proof_state(mvar, r->first, "unsolved subgoals"); + try { + proof_state_seq seq = (*t)(m_env, m_ios, ps); + if (auto r = seq.pull()) { + subst = r->first.get_subst(); + expr v = subst.instantiate_metavars_wo_jst(mvar); + if (has_metavar(v)) { + display_unsolved_proof_state(mvar, r->first, "unsolved subgoals"); + } else { + subst = subst.assign(mlocal_name(mvar), v); + } } else { - subst = subst.assign(mlocal_name(mvar), v); + // tactic failed to produce any result + display_unsolved_proof_state(mvar, ps, "tactic failed"); } - } else { - // tactic failed to produce any result - display_unsolved_proof_state(mvar, ps, "tactic failed"); + } catch (tactic_exception & ex) { + regular out(m_env, m_ios); + display_error_pos(out, m_pos_provider, ex.get_expr()); + out << " tactic failed: " << ex.what() << "\n"; } } } diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index 690b1def6..17bad97e0 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include #include "util/lazy_list_fn.h" +#include "util/sstream.h" #include "kernel/for_each_fn.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" @@ -59,6 +60,18 @@ void collect_simple_meta(expr const & e, buffer & metas) { }); } +/** \brief Throw an exception is \c v contains local constants, \c e is only used for position information. */ +void check_has_no_local(expr const & v, expr const & e) { + if (has_local(v)) { + for_each(v, [&](expr const & l, unsigned) { + if (is_local(l)) + throw tactic_exception(e, sstream() << "apply tactic contains reference to local '" << local_pp_name(l) + << "' which is not marked as [fact], so it is not visible to tactics"); + return has_local(l); + }); + } +} + tactic apply_tactic(expr const & _e) { return tactic([=](environment const & env, io_state const & ios, proof_state const & s) { goals const & gs = s.get_goals(); @@ -86,7 +99,9 @@ tactic apply_tactic(expr const & _e) { name_generator new_ngen(ngen); type_checker tc(env, new_ngen.mk_child()); expr new_e = subst.instantiate_metavars_wo_jst(e); - substitution new_subst = subst.assign(g.get_name(), g.abstract(new_e)); + expr new_p = g.abstract(new_e); + check_has_no_local(new_p, _e); + substitution new_subst = subst.assign(g.get_name(), new_p); buffer metas; collect_simple_meta(new_e, metas); goals new_gs = tail_gs; diff --git a/src/library/tactic/expr_to_tactic.h b/src/library/tactic/expr_to_tactic.h index dcc7af44c..447896454 100644 --- a/src/library/tactic/expr_to_tactic.h +++ b/src/library/tactic/expr_to_tactic.h @@ -9,11 +9,8 @@ Author: Leonardo de Moura #include "library/tactic/tactic.h" namespace lean { -class expr_to_tactic_exception : public exception { - expr m_expr; -public: - expr_to_tactic_exception(expr const & e, char const * msg):exception(msg), m_expr(e) {} - expr const & get_expr() const { return m_expr; } +class expr_to_tactic_exception : public tactic_exception { +public: expr_to_tactic_exception(expr const & e, char const * msg):tactic_exception(e, msg) {} }; typedef std::function expr_to_tactic_fn; diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index 40c7560ee..f01098b9f 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -19,6 +19,9 @@ Author: Leonardo de Moura #include "library/io_state_stream.h" namespace lean { +tactic_exception::tactic_exception(expr const & e, char const * msg):exception(msg), m_expr(e) {} +tactic_exception::tactic_exception(expr const & e, sstream const & strm):exception(strm), m_expr(e) {} + tactic tactic01(std::function(environment const &, io_state const & ios, proof_state const &)> f) { return tactic([=](environment const & env, io_state const & ios, proof_state const & s) { return mk_proof_state_seq([=]() { diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h index 2419cca4c..789ac11d2 100644 --- a/src/library/tactic/tactic.h +++ b/src/library/tactic/tactic.h @@ -14,6 +14,14 @@ Author: Leonardo de Moura #include "library/tactic/proof_state.h" namespace lean { +class tactic_exception : public exception { + expr m_expr; +public: + tactic_exception(expr const & e, char const * msg); + tactic_exception(expr const & e, sstream const & strm); + expr const & get_expr() const { return m_expr; } +}; + typedef lazy_list proof_state_seq; typedef std::function tactic; diff --git a/tests/lean/run/tactic11.lean b/tests/lean/run/tactic11.lean index 6801d8f2b..02dfca53c 100644 --- a/tests/lean/run/tactic11.lean +++ b/tests/lean/run/tactic11.lean @@ -1,8 +1,9 @@ -import logic +import standard +using tactic -exit -- TODO theorem tst (a b : Bool) (H : a ↔ b) : b ↔ a -:= have H1 [fact] : a → b, from iff_elim_left H, - by (apply iff_intro, - assume Hb, iff_mp_right H Hb, - assume Ha, H1 Ha) +:= have H1 [fact] : a → b, -- We need to mark H1 as fact, otherwise it is not visible by tactics + from iff_elim_left H, + by ⟦ iff_intro ⟧; + ⟦ assume Hb, iff_mp_right H Hb ⟧; + ⟦ assume Ha, H1 Ha ⟧