From 181a739a5e1a8bf8d43aa1fa37cf451c1c9f190c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 2 Jul 2014 16:26:06 -0700 Subject: [PATCH] feat(frontends/lean/elaborator): report unassigned metavariables as goals Signed-off-by: Leonardo de Moura --- src/frontends/lean/builtin_cmds.cpp | 2 +- src/frontends/lean/elaborator.cpp | 44 +++++++++++++++++++++++------ src/frontends/lean/elaborator.h | 2 +- src/frontends/lean/parser.cpp | 4 +-- src/frontends/lean/parser.h | 2 +- 5 files changed, 41 insertions(+), 13 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index bf7f4ad2c..4baa7614d 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -78,7 +78,7 @@ environment check_cmd(parser & p) { mk_section_params(collect_locals(e), p, section_ps); e = p.lambda_abstract(section_ps, e); level_param_names ls = to_level_param_names(collect_univ_params(e)); - e = p.elaborate(e); + e = p.elaborate(e, false); expr type = type_checker(p.env()).check(e, ls); p.regular_stream() << e << " : " << type << endl; return p.env(); diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index b502f6f72..1d500490f 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -46,6 +46,8 @@ class elaborator { constraints m_constraints; tactic_hints m_tactic_hints; mvar2meta m_mvar2meta; + name_set m_displayed_errors; // set of metavariables that we already reported unsolved/unassigned + bool m_check_unassigned; /** \brief Auxiliary object for creating backtracking points. @@ -118,11 +120,13 @@ class elaborator { } public: - elaborator(environment const & env, io_state const & ios, name_generator const & ngen, pos_info_provider * pp): + elaborator(environment const & env, io_state const & ios, name_generator const & ngen, pos_info_provider * pp, + bool check_unassigned): m_env(env), m_ios(ios), m_plugin([](constraint const &, name_generator const &) { return lazy_list>(); }), m_ngen(ngen), m_tc(env, m_ngen.mk_child(), mk_default_converter(m_env, optional(0))), m_pos_provider(pp) { + m_check_unassigned = check_unassigned; } expr mk_local(name const & n, expr const & t, binder_info const & bi) { @@ -645,9 +649,13 @@ public: } void display_unsolved_proof_state(expr const & mvar, proof_state const & ps, char const * msg) { - regular out(m_env, m_ios); - display_error_pos(out, m_pos_provider, mvar); - out << " unsolved placeholder, " << msg << "\n" << ps << "\n"; + lean_assert(is_metavar(mvar)); + if (!m_displayed_errors.contains(mlocal_name(mvar))) { + m_displayed_errors.insert(mlocal_name(mvar)); + regular out(m_env, m_ios); + display_error_pos(out, m_pos_provider, mvar); + out << " unsolved placeholder, " << msg << "\n" << ps << "\n"; + } } expr solve_unassigned_mvars(substitution & subst, expr const & e) { @@ -689,10 +697,30 @@ public: return subst.instantiate(e); } + void display_unassigned_mvars(expr const & e) { + if (has_metavar(e)) { + for_each(e, [&](expr const & e, unsigned) { + if (!is_metavar(e)) + return has_metavar(e); + if (auto it = m_mvar2meta.find(mlocal_name(e))) { + expr meta = *it; + expr meta_type = type_checker(m_env).infer(meta); + goal g(meta, meta_type); + display_unsolved_proof_state(e, proof_state(goals(g), substitution(), m_ngen), + "don't know how to synthesize it"); + } + return false; + }); + } + } + /** \brief Apply substitution and solve remaining metavariables using tactics. */ expr apply(substitution & s, expr const & e) { expr r = s.instantiate(e); - return solve_unassigned_mvars(s, r); + r = solve_unassigned_mvars(s, r); + if (m_check_unassigned) + display_unassigned_mvars(r); + return r; } expr operator()(expr const & e) { @@ -754,12 +782,12 @@ public: static name g_tmp_prefix = name::mk_internal_unique_name(); -expr elaborate(environment const & env, io_state const & ios, expr const & e, pos_info_provider * pp) { - return elaborator(env, ios, name_generator(g_tmp_prefix), pp)(e); +expr elaborate(environment const & env, io_state const & ios, expr const & e, pos_info_provider * pp, bool check_unassigned) { + return elaborator(env, ios, name_generator(g_tmp_prefix), pp, check_unassigned)(e); } std::pair elaborate(environment const & env, io_state const & ios, name const & n, expr const & t, expr const & v, pos_info_provider * pp) { - return elaborator(env, ios, name_generator(g_tmp_prefix), pp)(t, v, n); + return elaborator(env, ios, name_generator(g_tmp_prefix), pp, true)(t, v, n); } } diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 664629dec..6bcf1a953 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -12,7 +12,7 @@ Author: Leonardo de Moura #include "library/io_state.h" namespace lean { -expr elaborate(environment const & env, io_state const & ios, expr const & e, pos_info_provider * pp = nullptr); +expr elaborate(environment const & env, io_state const & ios, expr const & e, pos_info_provider * pp = nullptr, bool check_unassigned = true); std::pair elaborate(environment const & env, io_state const & ios, name const & n, expr const & t, expr const & v, pos_info_provider * pp = nullptr); } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 47b376d58..63b108cec 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -484,9 +484,9 @@ expr parser::mk_Type() { } } -expr parser::elaborate(expr const & e) { +expr parser::elaborate(expr const & e, bool check_unassigned) { parser_pos_provider pp(m_pos_table, get_stream_name(), m_last_cmd_pos); - return ::lean::elaborate(m_env, m_ios, e, &pp); + return ::lean::elaborate(m_env, m_ios, e, &pp, check_unassigned); } expr parser::elaborate(environment const & env, expr const & e) { diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 7b5e8cc96..3bdc94d46 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -258,7 +258,7 @@ public: */ struct no_undef_id_error_scope { parser & m_p; bool m_old; no_undef_id_error_scope(parser &); ~no_undef_id_error_scope(); }; - expr elaborate(expr const & e); + expr elaborate(expr const & e, bool check_unassigned = true); expr elaborate(environment const & env, expr const & e); std::pair elaborate(name const & n, expr const & t, expr const & v);