From 869ad261c51ca86e753573d7cfc7d8db23a09ad5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 27 Jun 2015 16:19:38 -0700 Subject: [PATCH] fix(frontends/lean/elaborator): fixes #689 --- src/frontends/lean/elaborator.cpp | 22 ++++++++++++++++++++++ src/frontends/lean/elaborator.h | 3 +++ tests/lean/689.lean | 1 + tests/lean/689.lean.expected.out | 1 + 4 files changed, 27 insertions(+) create mode 100644 tests/lean/689.lean create mode 100644 tests/lean/689.lean.expected.out diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 7c82bb271e..37f8adb09d 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1679,6 +1679,7 @@ void elaborator::display_unsolved_proof_state(expr const & mvar, proof_state con optional elaborator::get_pre_tactic_for(expr const & mvar) { if (auto it = m_local_tactic_hints.find(mlocal_name(mvar))) { + m_used_local_tactic_hints.insert(mlocal_name(mvar)); return some_expr(*it); } else { return none_expr(); @@ -2038,6 +2039,25 @@ std::tuple elaborator::apply(substitution & s, expr con return std::make_tuple(r, to_list(new_ps.begin(), new_ps.end())); } +void elaborator::check_used_local_tactic_hints() { + expr_struct_map pretac2name; + // the same pretac may be processed several times because of choice-exprs + m_local_tactic_hints.for_each([&](name const & n, expr const & e) { + if (m_used_local_tactic_hints.contains(n)) + pretac2name.insert(mk_pair(e, n)); + }); + m_local_tactic_hints.for_each([&](name const & n, expr const & e) { + if (!m_used_local_tactic_hints.contains(n) && + pretac2name.find(e) == pretac2name.end()) { + char const * msg = "unnecessary tactic was provided, placeholder was automatically synthesized by the elaborator"; + if (auto it = m_mvar2meta.find(n)) + throw_elaborator_exception(msg, *it); + else + throw exception(msg); + } + }); +} + auto elaborator::operator()(list const & ctx, expr const & e, bool _ensure_type) -> std::tuple { m_context.set_ctx(ctx); @@ -2052,6 +2072,7 @@ auto elaborator::operator()(list const & ctx, expr const & e, bool _ensure auto result = apply(s, r); check_sort_assignments(s); copy_info_to_manager(s); + check_used_local_tactic_hints(); return result; } @@ -2078,6 +2099,7 @@ std::tuple elaborator::operator()(expr const & t, expr new_r_v = apply(s, r_v, univ_params, new_params); check_sort_assignments(s); copy_info_to_manager(s); + check_used_local_tactic_hints(); return std::make_tuple(new_r_t, new_r_v, to_list(new_params.begin(), new_params.end())); } diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index fd6ad597c5..e2299255af 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -48,6 +48,7 @@ class elaborator : public coercion_info_manager { // mapping from metavariable name ?m to tactic expression that should be used to solve it. // this mapping is populated by the 'by tactic-expr' expression. local_tactic_hints m_local_tactic_hints; + name_set m_used_local_tactic_hints; // set of metavariables that we already reported unsolved/unassigned name_set m_displayed_errors; // if m_no_info is true, we do not collect information when true, @@ -180,6 +181,8 @@ class elaborator : public coercion_info_manager { expr process_obtain_expr(list const & s_list, list const & from_list, expr const & goal, bool first, constraint_seq & cs, expr const & src); expr visit_obtain_expr(expr const & e, constraint_seq & cs); + + void check_used_local_tactic_hints(); public: elaborator(elaborator_context & ctx, name_generator && ngen, bool nice_mvar_names = false); std::tuple operator()(list const & ctx, expr const & e, bool _ensure_type); diff --git a/tests/lean/689.lean b/tests/lean/689.lean new file mode 100644 index 0000000000..01043b9a13 --- /dev/null +++ b/tests/lean/689.lean @@ -0,0 +1 @@ +check @eq (begin exact empty end) unit.star diff --git a/tests/lean/689.lean.expected.out b/tests/lean/689.lean.expected.out new file mode 100644 index 0000000000..750959212b --- /dev/null +++ b/tests/lean/689.lean.expected.out @@ -0,0 +1 @@ +689.lean:1:29: error: unnecessary tactic was provided, placeholder was automatically synthesized by the elaborator