From f0edf2b4a32fac994fe68c2c589238a9c20dd248 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 24 Aug 2013 13:16:43 -0700 Subject: [PATCH] Pretty print kernel exceptions. Improve default lean frontend error messages. Signed-off-by: Leonardo de Moura --- src/frontends/lean/lean_parser.cpp | 40 ++++++++++++++++++++++----- src/kernel/kernel_exception.h | 9 ++++++ src/library/formatter.cpp | 44 +++++++++++++++++++++++++++++- src/library/formatter.h | 4 ++- src/library/state.h | 12 ++++++++ 5 files changed, 100 insertions(+), 9 deletions(-) diff --git a/src/frontends/lean/lean_parser.cpp b/src/frontends/lean/lean_parser.cpp index 63de7d0e2..591ea754c 100644 --- a/src/frontends/lean/lean_parser.cpp +++ b/src/frontends/lean/lean_parser.cpp @@ -17,6 +17,7 @@ Author: Leonardo de Moura #include "option_declarations.h" #include "expr_maps.h" #include "sstream.h" +#include "kernel_exception.h" #include "lean_frontend.h" #include "lean_parser.h" #include "lean_scanner.h" @@ -1157,13 +1158,31 @@ class parser_fn { } /*@}*/ - void error(char const * msg, unsigned line, unsigned pos) { - regular(m_frontend) << "Error (line: " << line << ", pos: " << pos << ") " << msg << endl; + void display_error_pos(unsigned line, unsigned pos) { regular(m_frontend) << "Error (line: " << line << ", pos: " << pos << ")"; } + void display_error_pos(pos_info const & p) { display_error_pos(p.first, p.second); } + void display_error_pos(expr const & e) { + if (e) { + auto it = m_expr_pos_info.find(e); + if (it == m_expr_pos_info.end()) + return display_error_pos(m_last_cmd_pos); + else + return display_error_pos(it->second); + } else { + return display_error_pos(m_last_cmd_pos); + } + } + void display_error(char const * msg, unsigned line, unsigned pos) { + display_error_pos(line, pos); + regular(m_frontend) << " " << msg << endl; sync(); } - - void error(char const * msg) { - error(msg, m_scanner.get_line(), m_scanner.get_pos()); + void display_error(char const * msg) { + 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()); + regular(m_frontend) << " " << ex << endl; + sync(); } public: @@ -1206,14 +1225,21 @@ public: if (m_use_exceptions) { throw parser_exception(ex.what(), ex.m_pos.first, ex.m_pos.second); } else { - error(ex.what(), ex.m_pos.first, ex.m_pos.second); + display_error(ex.what(), ex.m_pos.first, ex.m_pos.second); + } + } catch (kernel_exception & ex) { + m_found_errors = true; + if (m_use_exceptions) { + throw; + } else { + display_error(ex); } } catch (exception & ex) { m_found_errors = true; if (m_use_exceptions) { throw; } else { - error(ex.what()); + display_error(ex.what()); } } } diff --git a/src/kernel/kernel_exception.h b/src/kernel/kernel_exception.h index b69a4df08..ede7fc795 100644 --- a/src/kernel/kernel_exception.h +++ b/src/kernel/kernel_exception.h @@ -20,6 +20,12 @@ public: kernel_exception(environment const & env, char const * msg):exception(msg), m_env(env) {} virtual ~kernel_exception() noexcept {} environment const & get_environment() const { return m_env; } + /** + \brief Return a reference to the main expression associated with this exception. + Return the null expression if there is none. This information is used to provide + better error messages. + */ + virtual expr const & get_main_expr() const { return expr::null(); } }; /** \brief Base class for unknown universe or object exceptions. */ @@ -96,6 +102,7 @@ public: virtual ~app_type_mismatch_exception() {} context const & get_context() const { return m_context; } expr const & get_application() const { return m_app; } + virtual expr const & get_main_expr() const { return get_application(); } unsigned get_arg_pos() const { return m_arg_pos; } expr const & get_expected_type() const { return m_expected_type; } expr const & get_given_type() const { return m_given_type; } @@ -119,6 +126,7 @@ public: virtual ~function_expected_exception() {} context const & get_context() const { return m_context; } expr const & get_expr() const { return m_expr; } + virtual expr const & get_main_expr() const { return get_expr(); } virtual char const * what() const noexcept { return "function expected"; } }; @@ -139,6 +147,7 @@ public: virtual ~type_expected_exception() {} context const & get_context() const { return m_context; } expr const & get_expr() const { return m_expr; } + virtual expr const & get_main_expr() const { return get_expr(); } virtual char const * what() const noexcept { return "type expected"; } }; diff --git a/src/library/formatter.cpp b/src/library/formatter.cpp index 03a70f65a..deda34e74 100644 --- a/src/library/formatter.cpp +++ b/src/library/formatter.cpp @@ -7,7 +7,7 @@ Author: Leonardo de Moura #include #include "formatter.h" #include "printer.h" - +#include "kernel_exception.h" namespace lean { class simple_formatter_cell : public formatter_cell { public: @@ -34,4 +34,46 @@ public: formatter mk_simple_formatter() { return formatter(new simple_formatter_cell()); } + +format formatter::operator()(kernel_exception const & ex, options const & opts) { + if (unknown_name_exception const * _ex = dynamic_cast(&ex)) { + return format{format("unknown object '"), format(_ex->get_name()), format("'")}; + } else if (already_declared_exception const * _ex = dynamic_cast(&ex)) { + return format{format("invalid object declaration, environment already has an object named '"), + format(_ex->get_name()), format("'")}; + } else if (app_type_mismatch_exception const * _ex = dynamic_cast(&ex)) { + unsigned indent = get_pp_indent(opts); + format app_f = operator()(_ex->get_context(), _ex->get_application(), false, opts); + format given_f = operator()(_ex->get_context(), _ex->get_given_type(), false, opts); + format expected_f = operator()(_ex->get_context(), _ex->get_expected_type(), false, opts); + unsigned arg_pos = _ex->get_arg_pos(); + return format({format("type mismatch at application argument"), space(), format(arg_pos), space(), format("of"), + nest(indent, compose(line(), app_f)), + line(), format("expected type"), + nest(indent, compose(line(), expected_f)), + line(), format("given type"), + nest(indent, compose(line(), given_f))}); + } else if (function_expected_exception const * _ex = dynamic_cast(&ex)) { + unsigned indent = get_pp_indent(opts); + format expr_f = operator()(_ex->get_context(), _ex->get_expr(), false, opts); + return format({format("function expected at"), + nest(indent, compose(line(), expr_f))}); + } else if (type_expected_exception const * _ex = dynamic_cast(&ex)) { + unsigned indent = get_pp_indent(opts); + format expr_f = operator()(_ex->get_context(), _ex->get_expr(), false, opts); + return format({format("type expected, got"), + nest(indent, compose(line(), expr_f))}); + } else if (def_type_mismatch_exception const * _ex = dynamic_cast(&ex)) { + unsigned indent = get_pp_indent(opts); + format name_f = format(_ex->get_name()); + format type_f = operator()(_ex->get_type(), opts); + format value_f = operator()(_ex->get_value_type(), opts); + return format({format("type mismatch at definition '"), name_f, format("', expected type"), + nest(indent, compose(line(), type_f)), + line(), format("given type"), + nest(indent, compose(line(), value_f))}); + } else { + return format(ex.what()); + } +} } diff --git a/src/library/formatter.h b/src/library/formatter.h index 519bfa3da..51d764ed7 100644 --- a/src/library/formatter.h +++ b/src/library/formatter.h @@ -35,7 +35,7 @@ public: /** \brief Format the given environment */ virtual format operator()(environment const & env, options const & opts) = 0; }; - +class kernel_exception; class formatter { std::shared_ptr m_cell; public: @@ -46,6 +46,8 @@ public: format operator()(context const & c, expr const & e, bool format_ctx = false, options const & opts = options()) { return (*m_cell)(c, e, format_ctx, opts); } format operator()(object const & obj, options const & opts = options()) { return (*m_cell)(obj, opts); } 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()); }; formatter mk_simple_formatter(); diff --git a/src/library/state.h b/src/library/state.h index db38d0953..5bf0538a1 100644 --- a/src/library/state.h +++ b/src/library/state.h @@ -89,6 +89,18 @@ inline diagnostic const & operator<<(diagnostic const & out, object const & obj) return out; } +inline regular const & operator<<(regular const & out, kernel_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, kernel_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;