From 6334ff24ebfccfffe90a978eef8c8b65f84899df Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 9 Feb 2017 19:06:56 -0800 Subject: [PATCH] fix(frontends/lean/tactic_notation): erase position information quoted terms occurring inside `[...] See new test for understanding the problem. Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser.cpp | 5 ++++ src/frontends/lean/parser.h | 1 + src/frontends/lean/tactic_notation.cpp | 28 ++++++++++++++++++++ src/library/tactic/elaborate.cpp | 4 ++- tests/lean/quote_error_pos.lean | 5 ---- tests/lean/quote_error_pos.lean.expected.out | 6 +++++ 6 files changed, 43 insertions(+), 6 deletions(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 8388cb2311..aa11af9b4d 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -318,6 +318,11 @@ expr parser::save_pos(expr e, pos_info p) { return e; } +void parser::erase_pos(expr const & e) { + auto t = get_tag(e); + m_pos_table.erase(t); +} + expr parser::update_pos(expr e, pos_info p) { auto t = get_tag(e); m_pos_table.insert(t, p); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 46205ebf7f..8d5e208f80 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -225,6 +225,7 @@ public: expr save_pos(expr e, pos_info p); expr rec_save_pos(expr const & e, pos_info p); expr update_pos(expr e, pos_info p); + void erase_pos(expr const & e); pos_info pos_of(expr const & e, pos_info default_pos) const; pos_info pos_of(expr const & e) const { return pos_of(e, pos()); } pos_info cmd_pos() const { return m_last_cmd_pos; } diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp index bdbe905c5b..0e1104910f 100644 --- a/src/frontends/lean/tactic_notation.cpp +++ b/src/frontends/lean/tactic_notation.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "kernel/abstract.h" +#include "kernel/for_each_fn.h" #include "library/annotation.h" #include "library/constants.h" #include "library/quote.h" @@ -584,14 +585,41 @@ expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) { } } +/* +Consider the following example: + + meta def apply_zero_add (a : pexpr) : tactic unit := + `[apply zero_add %%a] -- We don't want the error to be reported here when 'a' does not have the expected type. + + example (a : nat) : 0 + a = a := + begin + apply_zero_add `(tt), -- Error should be here + end + +We address the issue above by erasing position information from quoted terms nested in 'e'. +*/ +static void erase_quoted_terms_pos_info(parser & p, expr const & e) { + for_each(e, [&](expr const & e, unsigned) { + if (is_quote(e)) { + for_each(get_quote_expr(e), [&](expr const & e, unsigned) { + p.erase_pos(e); + return true; + }); + } + return true; + }); +} + expr parse_auto_quote_tactic_block(parser & p, unsigned, expr const *, pos_info const & pos) { name const & tac_class = get_tactic_name(); bool use_rstep = false; bool report_error = false; expr r = parse_tactic(p, tac_class, use_rstep, report_error); + erase_quoted_terms_pos_info(p, r); while (p.curr_is_token(get_comma_tk())) { p.next(); expr next = parse_tactic(p, tac_class, use_rstep, report_error); + erase_quoted_terms_pos_info(p, next); r = p.mk_app({p.save_pos(mk_constant(get_pre_monad_and_then_name()), pos), r, next}, pos); } p.check_token_next(get_rbracket_tk(), "invalid auto-quote tactic block, ']' expected"); diff --git a/src/library/tactic/elaborate.cpp b/src/library/tactic/elaborate.cpp index 5e1ae3c443..6d590d20bc 100644 --- a/src/library/tactic/elaborate.cpp +++ b/src/library/tactic/elaborate.cpp @@ -28,9 +28,11 @@ static bool report_failure(elaborator_exception const & ex, expr const & mvar, c if (!ref) return false; optional d = s.mctx().find_metavar_decl(mvar); if (!d) return false; + optional pos = pip->get_pos_info(*ref); + if (!pos) return false; auto tc = std::make_shared(s.env(), s.get_options(), s.mctx(), d->get_context()); message_builder out(pip, tc, s.env(), get_global_ios(), pip->get_file_name(), - pip->get_pos_info_or_some(*ref), ERROR); + *pos, ERROR); out.set_exception(ex); out << line() + format(header) + line() + s.pp(); out.report(); diff --git a/tests/lean/quote_error_pos.lean b/tests/lean/quote_error_pos.lean index a458f37a66..d4810fe782 100644 --- a/tests/lean/quote_error_pos.lean +++ b/tests/lean/quote_error_pos.lean @@ -8,9 +8,6 @@ begin apply_zero_add `(tt), -- Error should be here end -/- --- This test is stil failing, Lean is reporting an error inside of `[apply ...] --- Possible solution: erase position information from quoted terms inside of `[...] meta def apply_zero_add2 (a : pexpr) : tactic unit := `[apply zero_add %%a] @@ -18,5 +15,3 @@ example (a : nat) : 0 + a = a := begin apply_zero_add2 `(tt), -- Error should be here end - --/ diff --git a/tests/lean/quote_error_pos.lean.expected.out b/tests/lean/quote_error_pos.lean.expected.out index 9015ac908d..5ee037f139 100644 --- a/tests/lean/quote_error_pos.lean.expected.out +++ b/tests/lean/quote_error_pos.lean.expected.out @@ -4,3 +4,9 @@ a : ℕ state: a : ℕ ⊢ 0 + a = a +quote_error_pos.lean:16:2: error: failed to synthesize type class instance for +a : ℕ +⊢ add_monoid bool +state: +a : ℕ +⊢ 0 + a = a