From 71b8b6408e99bc2a45fdd5df43dc1ecbf343af28 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 31 Aug 2013 16:46:41 -0700 Subject: [PATCH] Handle (and pretty print) elaborator error messages in the lean default frontend Signed-off-by: Leonardo de Moura --- src/frontends/lean/lean_parser.cpp | 46 ++++++++++----- src/frontends/lean/lean_pp.cpp | 91 ++++++++++++++++++++++-------- src/library/elaborator.cpp | 87 +++++++++++++++++++++++----- src/library/elaborator.h | 9 +++ src/library/elaborator_exception.h | 6 +- src/library/formatter.cpp | 13 +++++ src/library/formatter.h | 3 + src/library/state.h | 12 ++++ 8 files changed, 214 insertions(+), 53 deletions(-) diff --git a/src/frontends/lean/lean_parser.cpp b/src/frontends/lean/lean_parser.cpp index 352c453dd..3b3d5c620 100644 --- a/src/frontends/lean/lean_parser.cpp +++ b/src/frontends/lean/lean_parser.cpp @@ -18,6 +18,7 @@ Author: Leonardo de Moura #include "expr_maps.h" #include "sstream.h" #include "kernel_exception.h" +#include "elaborator_exception.h" #include "metavar.h" #include "elaborator.h" #include "lean_frontend.h" @@ -552,7 +553,8 @@ class parser::imp { if (m_frontend.has_implicit_arguments(obj.get_name())) { std::vector const & imp_args = m_frontend.get_implicit_arguments(obj.get_name()); buffer args; - args.push_back(save(mk_constant(obj.get_name()), pos())); + pos_info p = pos(); + args.push_back(save(mk_constant(obj.get_name()), p)); // We parse all the arguments to make sure we // get all explicit arguments. for (unsigned i = 0; i < imp_args.size(); i++) { @@ -906,6 +908,15 @@ class parser::imp { } } + /** + \brief Create a new application and associate position of left with the resultant expression. + */ + expr mk_app_left(expr const & left, expr const & arg) { + auto it = m_expr_pos_info.find(left); + lean_assert(it != m_expr_pos_info.end()); + return save(mk_app(left, arg), it->second); + } + /** \brief Auxiliary method used when processing the 'inside' of an expression. */ @@ -914,12 +925,12 @@ class parser::imp { case scanner::token::Id: return parse_led_id(left); case scanner::token::Eq: return parse_eq(left); case scanner::token::Arrow: return parse_arrow(left); - case scanner::token::LeftParen: return mk_app(left, parse_lparen()); - case scanner::token::IntVal: return mk_app(left, parse_int()); - case scanner::token::DecimalVal: return mk_app(left, parse_decimal()); - case scanner::token::StringVal: return mk_app(left, parse_string()); - case scanner::token::Placeholder: return mk_app(left, parse_placeholder()); - case scanner::token::Type: return mk_app(left, parse_type()); + case scanner::token::LeftParen: return mk_app_left(left, parse_lparen()); + case scanner::token::IntVal: return mk_app_left(left, parse_int()); + case scanner::token::DecimalVal: return mk_app_left(left, parse_decimal()); + case scanner::token::StringVal: return mk_app_left(left, parse_string()); + case scanner::token::Placeholder: return mk_app_left(left, parse_placeholder()); + case scanner::token::Type: return mk_app_left(left, parse_type()); default: return left; } } @@ -961,13 +972,7 @@ class parser::imp { /*@}*/ expr elaborate(expr const & e) { - if (has_metavar(e)) { - expr r = m_elaborator(e); - m_elaborator.clear(); - return r; - } else { - return e; - } + return m_elaborator(e); } /** @@ -1410,7 +1415,12 @@ class parser::imp { display_error(msg, m_scanner.get_line(), m_scanner.get_pos()); } void display_error(kernel_exception const & ex) { - display_error_pos(ex.get_main_expr()); + display_error_pos(m_elaborator.get_original(ex.get_main_expr())); + regular(m_frontend) << " " << ex << endl; + sync(); + } + void display_error(elaborator_exception const & ex) { + display_error_pos(m_elaborator.get_original(ex.get_expr())); regular(m_frontend) << " " << ex << endl; sync(); } @@ -1477,6 +1487,12 @@ public: display_error(ex); if (m_use_exceptions) throw; + } catch (elaborator_exception & ex) { + m_found_errors = true; + if (m_show_errors) + display_error(ex); + if (m_use_exceptions) + throw; } catch (interrupted & ex) { if (m_verbose) regular(m_frontend) << "\n!!!Interrupted!!!" << endl; diff --git a/src/frontends/lean/lean_pp.cpp b/src/frontends/lean/lean_pp.cpp index 24d9beb31..621ed7ccf 100644 --- a/src/frontends/lean/lean_pp.cpp +++ b/src/frontends/lean/lean_pp.cpp @@ -66,6 +66,10 @@ static format g_let_fmt = highlight_keyword(format("let")); static format g_in_fmt = highlight_keyword(format("in")); static format g_assign_fmt = highlight_keyword(format(":=")); static format g_geq_fmt = format("\u2265"); +static format g_lift_fmt = highlight_keyword(format("lift")); +static format g_lower_fmt = highlight_keyword(format("lower")); +static format g_subst_fmt = highlight_keyword(format("subst")); + static name g_pp_max_depth {"lean", "pp", "max_depth"}; static name g_pp_max_steps {"lean", "pp", "max_steps"}; @@ -98,18 +102,17 @@ static name g_nu("\u03BD"); /** \brief Return a fresh name for the given abstraction or let. By fresh, we mean a name that is not used for any constant in - abst_body(e). If fe != nullptr, then the resultant name also does - not clash with the name of any object defined in fe. + abst_body(e). The resultant name is based on abst_name(e). */ -name get_unused_name(expr const & e, frontend const * fe = nullptr) { +name get_unused_name(expr const & e) { lean_assert(is_abstraction(e) || is_let(e)); name const & n = is_abstraction(e) ? abst_name(e) : let_name(e); name n1 = n; unsigned i = 1; expr const & b = is_abstraction(e) ? abst_body(e) : let_body(e); - while (occurs(n1, b) || (fe != nullptr && fe->find_object(n1))) { + while (occurs(n1, b)) { n1 = name(n, i); i++; } @@ -190,7 +193,7 @@ class pp_fn { result pp_constant(expr const & e) { name const & n = const_name(e); if (is_metavar(e)) { - return mk_result(format("_"), 1); + return mk_result(format{format("?M"), format(metavar_idx(e))}, 1); } else if (has_implicit_arguments(n)) { return mk_result(format(m_frontend.get_explicit_version(n)), 1); } else { @@ -852,6 +855,32 @@ class pp_fn { return mk_result(r_format, p_arg1.second + p_arg2.second + 1); } + result pp_lower(expr const & e, unsigned depth) { + expr arg; unsigned s, n; + is_lower(e, arg, s, n); + result p_arg = pp_child(arg, depth); + format r_format = format{g_lower_fmt, colon(), format(s), colon(), format(s), nest(m_indent, compose(line(), p_arg.first))}; + return mk_result(r_format, p_arg.second + 1); + } + + result pp_lift(expr const & e, unsigned depth) { + expr arg; unsigned s, n; + is_lift(e, arg, s, n); + result p_arg = pp_child(arg, depth); + format r_format = format{g_lift_fmt, colon(), format(s), colon(), format(s), nest(m_indent, compose(line(), p_arg.first))}; + return mk_result(r_format, p_arg.second + 1); + } + + result pp_subst(expr const & e, unsigned depth) { + expr arg, v; unsigned i; + is_subst(e, arg, i, v); + result p_arg = pp_child(arg, depth); + result p_v = pp_child(v, depth); + format r_format = format{g_subst_fmt, colon(), format(i), + nest(m_indent, format{line(), p_arg.first, line(), p_v.first})}; + return mk_result(r_format, p_arg.second + p_v.second + 1); + } + result pp(expr const & e, unsigned depth, bool main = false) { check_interrupted(m_interrupted); if (!is_atomic(e) && (m_num_steps > m_max_steps || depth > m_max_depth)) { @@ -864,16 +893,24 @@ class pp_fn { return mk_result(format(it->second), 1); } result r; - switch (e.kind()) { - case expr_kind::Var: r = pp_var(e); break; - case expr_kind::Constant: r = pp_constant(e); break; - case expr_kind::Value: r = pp_value(e); break; - case expr_kind::App: r = pp_app(e, depth); break; - case expr_kind::Lambda: - case expr_kind::Pi: r = pp_abstraction(e, depth); break; - case expr_kind::Type: r = pp_type(e); break; - case expr_kind::Eq: r = pp_eq(e, depth); break; - case expr_kind::Let: r = pp_let(e, depth); break; + if (is_lower(e)) { + r = pp_lower(e, depth); + } else if (is_lift(e)) { + r = pp_lift(e, depth); + } else if (is_subst(e)) { + r = pp_subst(e, depth); + } else { + switch (e.kind()) { + case expr_kind::Var: r = pp_var(e); break; + case expr_kind::Constant: r = pp_constant(e); break; + case expr_kind::Value: r = pp_value(e); break; + case expr_kind::App: r = pp_app(e, depth); break; + case expr_kind::Lambda: + case expr_kind::Pi: r = pp_abstraction(e, depth); break; + case expr_kind::Type: r = pp_type(e); break; + case expr_kind::Eq: r = pp_eq(e, depth); break; + case expr_kind::Let: r = pp_let(e, depth); break; + } } if (!main && m_extra_lets && is_shared(e) && r.second > m_alias_min_weight) { name new_aux = name(m_aux, m_aliases_defs.size()+1); @@ -965,6 +1002,10 @@ public: void set_interrupt(bool flag) { m_interrupted = flag; } + + void register_local(name const & n) { + m_local_names.insert(n); + } }; class pp_formatter_cell : public formatter_cell { @@ -979,17 +1020,20 @@ class pp_formatter_cell : public formatter_cell { } format pp(context const & c, expr const & e, bool include_e, options const & opts) { + pp_fn fn(m_frontend, opts); + scoped_set_interruptable_ptr set(m_pp_fn, &fn); unsigned indent = get_pp_indent(opts); format r; bool first = true; expr c2 = context_to_lambda(c, e); while (is_fake_context(c2)) { check_interrupted(m_interrupted); - name n1 = get_unused_name(c2, &m_frontend); - format entry = format{format(n1), space(), colon(), space(), pp(fake_context_domain(c2), opts)}; + name n1 = get_unused_name(c2); + fn.register_local(n1); + format entry = format{format(n1), space(), colon(), space(), fn(fake_context_domain(c2))}; expr val = fake_context_value(c2); if (val) - entry += format{space(), g_assign_fmt, nest(indent, format{line(), pp(val, opts)})}; + entry += format{space(), g_assign_fmt, nest(indent, format{line(), fn(val)})}; if (first) { r = group(entry); first = false; @@ -1000,9 +1044,9 @@ class pp_formatter_cell : public formatter_cell { } if (include_e) { if (first) - r += format{line(), pp(c2, opts)}; + r += format{line(), fn(c2)}; else - r = pp(c2, opts); + r = fn(c2); } else { return r; } @@ -1090,14 +1134,17 @@ public: if (format_ctx) { return pp(c, e, true, opts); } else { + pp_fn fn(m_frontend, opts); + scoped_set_interruptable_ptr set(m_pp_fn, &fn); expr c2 = context_to_lambda(c, e); while (is_fake_context(c2)) { check_interrupted(m_interrupted); - name n1 = get_unused_name(c2, &m_frontend); + name n1 = get_unused_name(c2); + fn.register_local(n1); expr const & rest = fake_context_rest(c2); c2 = instantiate_with_closed(rest, mk_constant(n1)); } - return pp(c2, opts); + return fn(c2); } } diff --git a/src/library/elaborator.cpp b/src/library/elaborator.cpp index e9c219a67..af7049b5a 100644 --- a/src/library/elaborator.cpp +++ b/src/library/elaborator.cpp @@ -19,6 +19,8 @@ Author: Leonardo de Moura namespace lean { static name g_overload_name(name(name(name(0u), "library"), "overload")); static expr g_overload = mk_constant(g_overload_name); +static format g_assignment_fmt = format(":="); +static format g_unification_fmt = format("\u2248"); bool is_overload_marker(expr const & e) { return e == g_overload; @@ -65,12 +67,19 @@ class elaborator::imp { environment const & m_env; name_set const * m_available_defs; elaborator const * m_owner; + expr m_root; constraint_queue m_constraints; metavars m_metavars; bool m_add_constraints; + // The following mapping is used to store the relationship + // between elaborated expressions and non-elaborated expressions. + // We need that because a frontend may associate line number information + // with the original non-elaborated expressions. + expr_map m_trace; + volatile bool m_interrupted; expr metavar_type(expr const & m) { @@ -434,7 +443,14 @@ class elaborator::imp { } return n; }; - replace_fn replacer(proc); + + auto tracer = [&](expr const & old_e, expr const & new_e) { + if (!is_eqp(new_e, old_e)) { + m_trace[new_e] = old_e; + } + }; + + replace_fn replacer(proc, tracer); return replacer(e); } @@ -444,14 +460,14 @@ class elaborator::imp { solve_core(); bool cont = false; bool progress = false; - unsigned unsolved_midx = 0; + // unsigned unsolved_midx = 0; for (unsigned midx = 0; midx < num_meta; midx++) { if (m_metavars[midx].m_assignment) { if (has_assigned_metavar(m_metavars[midx].m_assignment)) { m_metavars[midx].m_assignment = instantiate(m_metavars[midx].m_assignment); } if (has_metavar(m_metavars[midx].m_assignment)) { - unsolved_midx = midx; + // unsolved_midx = midx; cont = true; // must continue } else { if (m_metavars[midx].m_type && !m_metavars[midx].m_type_cnstr) { @@ -473,7 +489,7 @@ class elaborator::imp { if (!cont) return; if (!progress) - throw unsolved_placeholder_exception(*m_owner, m_metavars[unsolved_midx].m_ctx, m_metavars[unsolved_midx].m_mvar); + throw unsolved_placeholder_exception(*m_owner, context(), m_root); } } @@ -494,8 +510,7 @@ public: } void clear() { - m_constraints.clear(); - m_metavars.clear(); + m_trace.clear(); } void set_interrupt(bool flag) { @@ -524,23 +539,69 @@ public: return m_env; } + struct resetter { + imp & m_ref; + resetter(imp & r):m_ref(r) {} + ~resetter() { m_ref.m_constraints.clear(); m_ref.m_metavars.clear(); } + }; + expr operator()(expr const & e, elaborator const & elb) { - // std::cout << "ELABORATIMG: " << e << "\n"; - m_owner = &elb; - unsigned num_meta = m_metavars.size(); - m_add_constraints = true; - infer(e, context()); - solve(num_meta); - return instantiate(e); + if (has_metavar(e)) { + resetter r(*this); + m_owner = &elb; + m_root = e; + unsigned num_meta = m_metavars.size(); + m_add_constraints = true; + infer(e, context()); + solve(num_meta); + return instantiate(e); + } else { + return e; + } + } + + expr const & get_original(expr const & e) const { + expr const * r = &e; + while (true) { + auto it = m_trace.find(*r); + if (it == m_trace.end()) { + return *r; + } else { + r = &(it->second); + } + } + } + + format pp(formatter & f, options const & o) const { + format r; + bool first = true; + for (unsigned i = 0; i < m_metavars.size(); i++) { + metavar_info const & info = m_metavars[i]; + expr m = ::lean::mk_metavar(i); + if (first) first = false; else r += line(); + format r_assignment; + if (info.m_assignment) + r_assignment = f(info.m_assignment, o); + else + r_assignment = highlight(format("[unassigned]")); + r += group(format{f(m,o), space(), g_assignment_fmt, line(), r_assignment}); + } + for (auto c : m_constraints) { + if (first) first = false; else r += line(); + r += group(format{f(c.m_lhs, o), space(), g_unification_fmt, line(), f(c.m_rhs, o)}); + } + return r; } }; elaborator::elaborator(environment const & env):m_ptr(new imp(env, nullptr)) {} elaborator::~elaborator() {} expr elaborator::mk_metavar() { return m_ptr->mk_metavar(); } expr elaborator::operator()(expr const & e) { return (*m_ptr)(e, *this); } +expr const & elaborator::get_original(expr const & e) const { return m_ptr->get_original(e); } void elaborator::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); } void elaborator::clear() { m_ptr->clear(); } environment const & elaborator::get_environment() const { return m_ptr->get_environment(); } void elaborator::display(std::ostream & out) const { m_ptr->display(out); } +format elaborator::pp(formatter & f, options const & o) const { return m_ptr->pp(f,o); } void elaborator::print(imp * ptr) { ptr->display(std::cout); } } diff --git a/src/library/elaborator.h b/src/library/elaborator.h index fa02c6d5a..b8fc4be31 100644 --- a/src/library/elaborator.h +++ b/src/library/elaborator.h @@ -7,6 +7,7 @@ Author: Leonardo de Moura #pragma once #include #include "environment.h" +#include "formatter.h" namespace lean { /** @@ -26,6 +27,13 @@ public: expr operator()(expr const & e); + /** + \brief If \c e is an expression instantiated by the elaborator, then it + returns the expression (the one with "holes") used to generate \c e. + Otherwise, it just returns \c e. + */ + expr const & get_original(expr const & e) const; + void set_interrupt(bool flag); void interrupt() { set_interrupt(true); } void reset_interrupt() { set_interrupt(false); } @@ -35,6 +43,7 @@ public: environment const & get_environment() const; void display(std::ostream & out) const; + format pp(formatter & f, options const & o) const; }; /** \brief Return true iff \c e is a special constant used to mark application of overloads. */ bool is_overload_marker(expr const & e); diff --git a/src/library/elaborator_exception.h b/src/library/elaborator_exception.h index bb340e5ba..025fd0cc1 100644 --- a/src/library/elaborator_exception.h +++ b/src/library/elaborator_exception.h @@ -37,7 +37,7 @@ public: class unsolved_placeholder_exception : public elaborator_exception { public: unsolved_placeholder_exception(elaborator const & elb, context const & ctx, expr const & e):elaborator_exception(elb, ctx, e) {} - virtual char const * what() const noexcept { return "unsolved placeholder, system could not fill this placeholder"; } + virtual char const * what() const noexcept { return "unsolved placeholder"; } }; class unification_app_mismatch_exception : public elaborator_exception { @@ -45,12 +45,12 @@ class unification_app_mismatch_exception : public elaborator_exception { public: unification_app_mismatch_exception(elaborator const & elb, context const & ctx, expr const & s, unsigned pos):elaborator_exception(elb, ctx, s), m_arg_pos(pos) {} unsigned get_arg_pos() const { return m_arg_pos; } - virtual char const * what() const noexcept { return "failed to solve unification problem during elaboration"; } + virtual char const * what() const noexcept { return "application type mismatch during term elaboration"; } }; class unification_type_mismatch_exception : public elaborator_exception { public: unification_type_mismatch_exception(elaborator const & elb, context const & ctx, expr const & s):elaborator_exception(elb, ctx, s) {} - virtual char const * what() const noexcept { return "failed to solve unification problem during elaboration"; } + virtual char const * what() const noexcept { return "type mismatch during term elaboration"; } }; } diff --git a/src/library/formatter.cpp b/src/library/formatter.cpp index deda34e74..b5d201ebd 100644 --- a/src/library/formatter.cpp +++ b/src/library/formatter.cpp @@ -8,6 +8,9 @@ Author: Leonardo de Moura #include "formatter.h" #include "printer.h" #include "kernel_exception.h" +#include "elaborator_exception.h" +#include "elaborator.h" + namespace lean { class simple_formatter_cell : public formatter_cell { public: @@ -76,4 +79,14 @@ format formatter::operator()(kernel_exception const & ex, options const & opts) return format(ex.what()); } } + +format formatter::operator()(elaborator_exception const & ex, options const & opts) { + unsigned indent = get_pp_indent(opts); + format expr_f = operator()(ex.get_context(), ex.get_expr(), false, opts); + format elb_f = ex.get_elaborator().pp(*this, opts); + return format({format(ex.what()), space(), format("at term"), + nest(indent, compose(line(), expr_f)), + line(), format("Elaborator state"), + nest(indent, compose(line(), elb_f))}); +} } diff --git a/src/library/formatter.h b/src/library/formatter.h index 254eff420..43392bc5b 100644 --- a/src/library/formatter.h +++ b/src/library/formatter.h @@ -38,6 +38,7 @@ public: virtual void set_interrupt(bool flag) {} }; class kernel_exception; +class elaborator_exception; class formatter { std::shared_ptr m_cell; public: @@ -50,6 +51,8 @@ public: format operator()(environment const & env, options const & opts = options()) { return (*m_cell)(env, opts); } /** \brief Pretty print a kernel exception using the this formatter */ format operator()(kernel_exception const & ex, options const & opts = options()); + /** \brief Pretty print a elaborator exception using the this formatter */ + format operator()(elaborator_exception const & ex, options const & opts = options()); void set_interrupt(bool flag) { m_cell->set_interrupt(flag); } }; diff --git a/src/library/state.h b/src/library/state.h index d35b9928f..c25647347 100644 --- a/src/library/state.h +++ b/src/library/state.h @@ -102,6 +102,18 @@ inline diagnostic const & operator<<(diagnostic const & out, kernel_exception co return out; } +inline regular const & operator<<(regular const & out, elaborator_exception const & ex) { + options const & opts = out.m_state.get_options(); + out.m_state.get_regular_channel().get_stream() << mk_pair(out.m_state.get_formatter()(ex, opts), opts); + return out; +} + +inline diagnostic const & operator<<(diagnostic const & out, elaborator_exception const & ex) { + options const & opts = out.m_state.get_options(); + out.m_state.get_diagnostic_channel().get_stream() << mk_pair(out.m_state.get_formatter()(ex, opts), opts); + return out; +} + template inline regular const & operator<<(regular const & out, T const & t) { out.m_state.get_regular_channel().get_stream() << t;