From 93b17e2ec10e1b6a9e1106a3ca5c0e2041b4d273 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 4 Dec 2015 13:00:57 -0800 Subject: [PATCH] refactor(kernel/ext_exception): add ext_exception Now, any exception that requires pretty printing support should be a subclass of ext_exception --- src/kernel/ext_exception.h | 28 +++++++++++++++++++ src/kernel/kernel_exception.h | 11 +++----- src/library/blast/gexpr.cpp | 5 ++++ src/library/blast/gexpr.h | 2 +- src/library/error_handling/error_handling.cpp | 14 ++-------- src/library/generic_exception.h | 17 ++++++----- src/library/head_map.cpp | 4 +++ src/library/head_map.h | 2 ++ src/library/io_state_stream.cpp | 10 +------ src/library/io_state_stream.h | 21 ++++++++------ 10 files changed, 69 insertions(+), 45 deletions(-) create mode 100644 src/kernel/ext_exception.h diff --git a/src/kernel/ext_exception.h b/src/kernel/ext_exception.h new file mode 100644 index 000000000..95746bf2a --- /dev/null +++ b/src/kernel/ext_exception.h @@ -0,0 +1,28 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "util/exception.h" +#include "util/sexpr/options.h" +#include "kernel/formatter.h" +#include "kernel/expr.h" + +namespace lean { +/** \brief Base class for exceptions with support for pretty printing. */ +class ext_exception : public exception { +public: + ext_exception() {} + ext_exception(char const * msg):exception(msg) {} + ext_exception(sstream const & strm):exception(strm) {} + virtual ~ext_exception() noexcept {} + /** \brief Return a reference (if available) to the main expression associated with this exception. + This information is used to provide better error messages. */ + virtual optional get_main_expr() const { return none_expr(); } + virtual format pp(formatter const &) const { return format(what()); } + virtual throwable * clone() const { return new ext_exception(m_msg.c_str()); } + virtual void rethrow() const { throw *this; } +}; +} diff --git a/src/kernel/kernel_exception.h b/src/kernel/kernel_exception.h index 720f7462d..138a8439d 100644 --- a/src/kernel/kernel_exception.h +++ b/src/kernel/kernel_exception.h @@ -5,22 +5,19 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include -#include "util/exception.h" -#include "util/sexpr/options.h" #include "kernel/environment.h" -#include "kernel/formatter.h" +#include "kernel/ext_exception.h" namespace lean { class environment; /** \brief Base class for all kernel exceptions. */ -class kernel_exception : public exception { +class kernel_exception : public ext_exception { protected: environment m_env; public: kernel_exception(environment const & env):m_env(env) {} - kernel_exception(environment const & env, char const * msg):exception(msg), m_env(env) {} - kernel_exception(environment const & env, sstream const & strm):exception(strm), m_env(env) {} + kernel_exception(environment const & env, char const * msg):ext_exception(msg), m_env(env) {} + kernel_exception(environment const & env, sstream const & strm):ext_exception(strm), m_env(env) {} virtual ~kernel_exception() noexcept {} environment const & get_environment() const { return m_env; } /** diff --git a/src/library/blast/gexpr.cpp b/src/library/blast/gexpr.cpp index 768cb8581..912884579 100644 --- a/src/library/blast/gexpr.cpp +++ b/src/library/blast/gexpr.cpp @@ -35,4 +35,9 @@ std::ostream & operator<<(std::ostream & out, gexpr const & ge) { return out; } +io_state_stream const & operator<<(io_state_stream const & out, gexpr const & ge) { + out << ge.m_expr; + if (ge.is_universe_polymorphic()) out << " (poly)"; + return out; +} }} diff --git a/src/library/blast/gexpr.h b/src/library/blast/gexpr.h index 9d82e1730..77fd91803 100644 --- a/src/library/blast/gexpr.h +++ b/src/library/blast/gexpr.h @@ -49,5 +49,5 @@ public: bool operator==(gexpr const & ge1, gexpr const & ge2); inline bool operator!=(gexpr const & ge1, gexpr const & ge2) { return !operator==(ge1, ge2); } std::ostream & operator<<(std::ostream & out, gexpr const & ge); - +io_state_stream const & operator<<(io_state_stream const & out, gexpr const & ge); }} diff --git a/src/library/error_handling/error_handling.cpp b/src/library/error_handling/error_handling.cpp index 66b55bc1a..2cc6e1a26 100644 --- a/src/library/error_handling/error_handling.cpp +++ b/src/library/error_handling/error_handling.cpp @@ -8,12 +8,11 @@ Author: Leonardo de Moura #include #include "util/script_exception.h" #include "util/name_set.h" -#include "kernel/kernel_exception.h" +#include "kernel/ext_exception.h" #include "kernel/for_each_fn.h" #include "library/io_state_stream.h" #include "library/unifier.h" #include "library/parser_nested_exception.h" -#include "library/generic_exception.h" #include "library/flycheck.h" #include "library/pp_options.h" #include "library/error_handling/error_handling.h" @@ -79,12 +78,7 @@ void display_error_pos(io_state_stream const & ios, pos_info_provider const * p, void display_error(io_state_stream const & ios, pos_info_provider const * p, throwable const & ex); -static void display_error(io_state_stream const & ios, pos_info_provider const * p, kernel_exception const & ex) { - display_error_pos(ios, p, ex.get_main_expr()); - ios << " " << ex << endl; -} - -static void display_error(io_state_stream const & ios, pos_info_provider const * p, generic_exception const & ex) { +static void display_error(io_state_stream const & ios, pos_info_provider const * p, ext_exception const & ex) { display_error_pos(ios, p, ex.get_main_expr()); ios << " " << ex << endl; } @@ -147,10 +141,8 @@ static void display_error(io_state_stream const & ios, pos_info_provider const * void display_error(io_state_stream const & ios, pos_info_provider const * p, throwable const & ex) { flycheck_error err(ios); - if (auto k_ex = dynamic_cast(&ex)) { + if (auto k_ex = dynamic_cast(&ex)) { display_error(ios, p, *k_ex); - } else if (auto g_ex = dynamic_cast(&ex)) { - display_error(ios, p, *g_ex); } else if (auto e_ex = dynamic_cast(&ex)) { display_error(ios, p, *e_ex); } else if (auto ls_ex = dynamic_cast(&ex)) { diff --git a/src/library/generic_exception.h b/src/library/generic_exception.h index 7d9e68e1b..350d703e4 100644 --- a/src/library/generic_exception.h +++ b/src/library/generic_exception.h @@ -7,24 +7,23 @@ Author: Leonardo de Moura #pragma once #include #include "util/sstream.h" -#include "kernel/expr.h" -#include "kernel/formatter.h" +#include "kernel/ext_exception.h" namespace lean { -class generic_exception : public exception { +class generic_exception : public ext_exception { protected: optional m_main_expr; pp_fn m_pp_fn; public: generic_exception(char const * msg, optional const & m, pp_fn const & fn): - exception(msg), m_main_expr(m), m_pp_fn(fn) {} + ext_exception(msg), m_main_expr(m), m_pp_fn(fn) {} generic_exception(optional const & m, pp_fn const & fn): - exception(), m_main_expr(m), m_pp_fn(fn) {} + ext_exception(), m_main_expr(m), m_pp_fn(fn) {} virtual ~generic_exception() noexcept {} - virtual optional get_main_expr() const { return m_main_expr; } - virtual format pp(formatter const & fmt) const { return m_pp_fn(fmt); } - virtual throwable * clone() const { return new generic_exception(m_msg.c_str(), m_main_expr, m_pp_fn); } - virtual void rethrow() const { throw *this; } + virtual optional get_main_expr() const override { return m_main_expr; } + virtual format pp(formatter const & fmt) const override { return m_pp_fn(fmt); } + virtual throwable * clone() const override { return new generic_exception(m_msg.c_str(), m_main_expr, m_pp_fn); } + virtual void rethrow() const override { throw *this; } }; [[ noreturn ]] void throw_generic_exception(char const * msg, optional const & m); diff --git a/src/library/head_map.cpp b/src/library/head_map.cpp index 2cfabf592..8a785f89a 100644 --- a/src/library/head_map.cpp +++ b/src/library/head_map.cpp @@ -41,4 +41,8 @@ std::ostream & operator<<(std::ostream & out, head_index const & head_idx) { out << head_idx.m_kind; return out; } + +io_state_stream const & operator<<(io_state_stream const & out, head_index const & head_idx) { + return display(out, head_idx); +} } diff --git a/src/library/head_map.h b/src/library/head_map.h index 10a8bade2..bf8c6d7d3 100644 --- a/src/library/head_map.h +++ b/src/library/head_map.h @@ -25,6 +25,8 @@ struct head_index { friend std::ostream & operator<<(std::ostream & out, head_index const & head_idx); }; +io_state_stream const & operator<<(io_state_stream const & out, head_index const & head_idx); + /** \brief Very simple indexing data-structure that allow us to map the head symbol of an expression to a list of values. diff --git a/src/library/io_state_stream.cpp b/src/library/io_state_stream.cpp index 68884b8d2..fbbd29c3e 100644 --- a/src/library/io_state_stream.cpp +++ b/src/library/io_state_stream.cpp @@ -4,9 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "kernel/kernel_exception.h" #include "library/io_state_stream.h" -#include "library/generic_exception.h" namespace lean { io_state_stream const & operator<<(io_state_stream const & out, endl_class) { @@ -25,13 +23,7 @@ io_state_stream const & operator<<(io_state_stream const & out, expr const & e) return out; } -io_state_stream const & operator<<(io_state_stream const & out, kernel_exception const & ex) { - options const & opts = out.get_options(); - out.get_stream() << mk_pair(ex.pp(out.get_formatter()), opts); - return out; -} - -io_state_stream const & operator<<(io_state_stream const & out, generic_exception const & ex) { +io_state_stream const & operator<<(io_state_stream const & out, ext_exception const & ex) { options const & opts = out.get_options(); out.get_stream() << mk_pair(ex.pp(out.get_formatter()), opts); return out; diff --git a/src/library/io_state_stream.h b/src/library/io_state_stream.h index f6ec24d3d..60c5700fd 100644 --- a/src/library/io_state_stream.h +++ b/src/library/io_state_stream.h @@ -5,12 +5,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include +#include "kernel/ext_exception.h" +#include "library/generic_exception.h" #include "library/io_state.h" namespace lean { -/** - \brief Base class for \c regular and \c diagnostic wrapper classes. -*/ +/** \brief Base class for \c regular and \c diagnostic wrapper classes. */ class io_state_stream { protected: environment const & m_env; @@ -36,16 +37,20 @@ inline io_state_stream diagnostic(environment const & env, io_state const & ios) struct endl_class { endl_class() {} }; const endl_class endl; -class kernel_exception; -class generic_exception; +class ext_exception; io_state_stream const & operator<<(io_state_stream const & out, endl_class); io_state_stream const & operator<<(io_state_stream const & out, expr const & e); -io_state_stream const & operator<<(io_state_stream const & out, kernel_exception const & ex); -io_state_stream const & operator<<(io_state_stream const & out, generic_exception const & ex); +io_state_stream const & operator<<(io_state_stream const & out, ext_exception const & ex); io_state_stream const & operator<<(io_state_stream const & out, format const & f); -template io_state_stream const & operator<<(io_state_stream const & out, T const & t) { +template io_state_stream const & display(io_state_stream const & out, T const & t) { out.get_stream() << t; return out; } +inline io_state_stream const & operator<<(io_state_stream const & out, char const * d) { return display(out, d); } +inline io_state_stream const & operator<<(io_state_stream const & out, name const & d) { return display(out, d); } +inline io_state_stream const & operator<<(io_state_stream const & out, unsigned d) { return display(out, d); } +inline io_state_stream const & operator<<(io_state_stream const & out, std::string const & d) { return display(out, d); } +inline io_state_stream const & operator<<(io_state_stream const & out, options const & d) { return display(out, d); } +inline io_state_stream const & operator<<(io_state_stream const & out, pair const & d) { return display(out, d); } }