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

@@ -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<expr> 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; }
+};
+}

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 <vector>
-#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, char const * msg):ext_exception(msg), m_env(env) {}
-    kernel_exception(environment const & env, sstream const & strm):exception(strm), 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; }
     /**

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;
+}
 }}

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);
 }}

src/library/error_handling/error_handling.cpp

@@ -8,12 +8,11 @@ Author: Leonardo de Moura
 #include <string>
 #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) {
+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;
-}
-
-static void display_error(io_state_stream const & ios, pos_info_provider const * p, generic_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<kernel_exception const *>(&ex)) {
+    if (auto k_ex = dynamic_cast<ext_exception const *>(&ex)) {
         display_error(ios, p, *k_ex);
-    } else if (auto g_ex = dynamic_cast<generic_exception const *>(&ex)) {
-        display_error(ios, p, *g_ex);
     } else if (auto e_ex = dynamic_cast<unifier_exception const *>(&ex)) {
         display_error(ios, p, *e_ex);
     } else if (auto ls_ex = dynamic_cast<script_nested_exception const *>(&ex)) {

src/library/generic_exception.h

@@ -7,24 +7,23 @@ Author: Leonardo de Moura
 #pragma once
 #include <string>
 #include "util/sstream.h"
-#include "kernel/expr.h"
+#include "kernel/ext_exception.h"
-#include "kernel/formatter.h"
 
 namespace lean {
-class generic_exception : public exception {
+class generic_exception : public ext_exception {
 protected:
     optional<expr> m_main_expr;
     pp_fn          m_pp_fn;
 public:
     generic_exception(char const * msg, optional<expr> 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<expr> 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<expr> get_main_expr() const { return m_main_expr; }
+    virtual optional<expr> get_main_expr() const override { return m_main_expr; }
-    virtual format pp(formatter const & fmt) const { return m_pp_fn(fmt); }
+    virtual format pp(formatter const & fmt) const override { return m_pp_fn(fmt); }
-    virtual throwable * clone() const { return new generic_exception(m_msg.c_str(), m_main_expr, m_pp_fn); }
+    virtual throwable * clone() const override { return new generic_exception(m_msg.c_str(), m_main_expr, m_pp_fn); }
-    virtual void rethrow() const { throw *this; }
+    virtual void rethrow() const override { throw *this; }
 };
 
 [[ noreturn ]] void throw_generic_exception(char const * msg, optional<expr> const & m);

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);
+}
 }

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.

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) {
+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;
-}
-
-io_state_stream const & operator<<(io_state_stream const & out, generic_exception const & ex) {
     options const & opts = out.get_options();
     out.get_stream() << mk_pair(ex.pp(out.get_formatter()), opts);
     return out;

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 <string>
+#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 ext_exception;
-class generic_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, ext_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, format const & f);
-template<typename T> io_state_stream const & operator<<(io_state_stream const & out, T const & t) {
+template<typename T> 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<format const &, options const &> const & d) { return display(out, d); }
 }