refactor(kernel_exception): delete kernel_exception_formatter, and implement kernel_exception pretty printer as a virtual method

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/parser.cpp

@@ -28,7 +28,6 @@ Author: Leonardo de Moura
 #include "kernel/printer.h"
 #include "library/arith/arith.h"
 #include "library/state.h"
-#include "library/kernel_exception_formatter.h"
 #include "library/placeholder.h"
 #include "frontends/lean/frontend.h"
 #include "frontends/lean/elaborator.h"

src/kernel/CMakeLists.txt

@@ -1,6 +1,7 @@
 add_library(kernel expr.cpp free_vars.cpp abstract.cpp instantiate.cpp
   normalizer.cpp context.cpp level.cpp object.cpp environment.cpp
   type_checker.cpp builtin.cpp occurs.cpp metavar.cpp trace.cpp
-  unification_constraint.cpp printer.cpp formatter.cpp)
+  unification_constraint.cpp printer.cpp formatter.cpp
+  kernel_exception.cpp)
 
 target_link_libraries(kernel ${LEAN_LIBS})

src/kernel/kernel_exception.cpp

@@ -0,0 +1,85 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <vector>
+#include "kernel/kernel_exception.h"
+
+namespace lean {
+format kernel_exception::pp(formatter const &, options const &) const {
+    return format(what());
+}
+
+format unknown_name_exception::pp(formatter const &, options const &) const {
+    return format{format("unknown object '"), format(get_name()), format("'")};
+}
+
+format already_declared_exception::pp(formatter const &, options const &) const {
+    return format{format("invalid object declaration, environment already has an object named '"), format(get_name()), format("'")};
+}
+
+format app_type_mismatch_exception::pp(formatter const & fmt, options const & opts) const {
+    unsigned indent     = get_pp_indent(opts);
+    context const & ctx = get_context();
+    expr const & app    = get_application();
+    format app_fmt      = fmt(ctx, app, false, opts);
+    std::vector<expr> const & arg_types = get_arg_types();
+    auto it = arg_types.begin();
+    format f_type_fmt   = fmt(ctx, *it, false, opts);
+    format arg_types_fmt;
+    ++it;
+    for (unsigned i = 1; it != arg_types.end(); ++it, ++i) {
+        expr const & a    = arg(app, i);
+        format arg_fmt    = fmt(ctx, a, false, opts);
+        if (is_pi(a) || is_lambda(a) || is_let(a))
+            arg_fmt = paren(arg_fmt);
+        format arg_type_fmt = fmt(ctx, *it, false, opts);
+        arg_types_fmt += nest(indent, compose(line(), group(format{arg_fmt, space(), colon(), nest(indent, format{line(), arg_type_fmt})})));
+    }
+    format r;
+    r += format("type mismatch at application");
+    r += nest(indent, compose(line(), app_fmt));
+    r += compose(line(), format("Function type:"));
+    r += nest(indent, compose(line(), f_type_fmt));
+    r += line();
+    if (arg_types.size() > 2)
+        r += format("Arguments types:");
+    else
+        r += format("Argument type:");
+    r += arg_types_fmt;
+    return r;
+}
+
+format function_expected_exception::pp(formatter const & fmt, options const & opts) const {
+    unsigned indent = get_pp_indent(opts);
+    format expr_fmt = fmt(get_context(), get_expr(), false, opts);
+    format r;
+    r += format("function expected at");
+    r += nest(indent, compose(line(), expr_fmt));
+    return r;
+}
+
+format type_expected_exception::pp(formatter const & fmt, options const & opts) const {
+    unsigned indent = get_pp_indent(opts);
+    format expr_fmt = fmt(get_context(), get_expr(), false, opts);
+    format r;
+    r += format("type expected, got");
+    r += nest(indent, compose(line(), expr_fmt));
+    return r;
+}
+
+format def_type_mismatch_exception::pp(formatter const & fmt, options const & opts) const {
+    unsigned indent     = get_pp_indent(opts);
+    context const & ctx = get_context();
+    format r;
+    r += format("type mismatch at definition '");
+    r += format(get_name());
+    r += format("', expected type");
+    r += nest(indent, compose(line(), fmt(ctx, get_type(), false, opts)));
+    r += compose(line(), format("Given type:"));
+    r += nest(indent, compose(line(), fmt(ctx, get_value_type(), false, opts)));
+    return r;
+}
+}

src/kernel/kernel_exception.h

@@ -7,8 +7,10 @@ Author: Leonardo de Moura
 #pragma once
 #include <vector>
 #include "util/exception.h"
+#include "util/sexpr/options.h"
 #include "kernel/context.h"
 #include "kernel/environment.h"
+#include "kernel/formatter.h"
 
 namespace lean {
 class environment;
@@ -27,6 +29,7 @@ public:
         better error messages.
     */
     virtual expr const & get_main_expr() const { return expr::null(); }
+    virtual format pp(formatter const & fmt, options const & opts) const;
 };
 
 /** \brief Base class for unknown universe or object exceptions. */
@@ -36,6 +39,7 @@ public:
     unknown_name_exception(environment const & env, name const & n):kernel_exception(env), m_name(n) {}
     virtual ~unknown_name_exception() {}
     name const & get_name() const { return m_name; }
+    virtual format pp(formatter const & fmt, options const & opts) const;
 };
 
 /** \brief Exception used to report that a universe variable is not known in a given environment. */
@@ -60,6 +64,7 @@ public:
     virtual ~already_declared_exception() noexcept {}
     name const & get_name() const { return m_name; }
     virtual char const * what() const noexcept { return "invalid object declaration, environment already has an object the given name"; }
+    virtual format pp(formatter const & fmt, options const & opts) const;
 };
 
 /**
@@ -103,6 +108,7 @@ public:
     virtual expr const & get_main_expr() const { return get_application(); }
     std::vector<expr> const & get_arg_types() const { return m_arg_types; }
     virtual char const * what() const noexcept { return "application argument type mismatch"; }
+    virtual format pp(formatter const & fmt, options const & opts) const;
 };
 
 /**
@@ -124,6 +130,7 @@ public:
     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"; }
+    virtual format pp(formatter const & fmt, options const & opts) const;
 };
 
 /**
@@ -145,6 +152,7 @@ public:
     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"; }
+    virtual format pp(formatter const & fmt, options const & opts) const;
 };
 
 /**
@@ -178,6 +186,7 @@ public:
     expr const & get_value_type() const { return m_value_type; }
     virtual expr const & get_main_expr() const { return m_value; }
     virtual char const * what() const noexcept { return "definition type mismatch"; }
+    virtual format pp(formatter const & fmt, options const & opts) const;
 };
 
 /**

src/library/CMakeLists.txt

@@ -1,6 +1,5 @@
 add_library(library basic_thms.cpp deep_copy.cpp max_sharing.cpp
-  context_to_lambda.cpp state.cpp update_expr.cpp
-  kernel_exception_formatter.cpp reduce.cpp light_checker.cpp
-  placeholder.cpp ho_unifier.cpp expr_lt.cpp)
+  context_to_lambda.cpp state.cpp update_expr.cpp reduce.cpp
+  light_checker.cpp placeholder.cpp ho_unifier.cpp expr_lt.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/kernel_exception_formatter.cpp

@@ -1,115 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <vector>
-#include "library/kernel_exception_formatter.h"
-
-namespace lean {
-/*
-  The following ad-hoc dynamic dispatch is ugly, but we can't define
-  pp as a virtual method in kernel_exception because
-  the formatter is not part of the kernel.
-*/
-format pp(formatter const & fmt, kernel_exception const & ex, options const & opts) {
-    if (unknown_name_exception const * _ex = dynamic_cast<unknown_name_exception const *>(&ex))
-        return pp(*_ex, opts);
-    else if (already_declared_exception const * _ex = dynamic_cast<already_declared_exception const *>(&ex))
-        return pp(*_ex, opts);
-    else if (app_type_mismatch_exception const * _ex = dynamic_cast<app_type_mismatch_exception const *>(&ex))
-        return pp(fmt, *_ex, opts);
-    else if (function_expected_exception const * _ex = dynamic_cast<function_expected_exception const *>(&ex))
-        return pp(fmt, *_ex, opts);
-    else if (type_expected_exception const * _ex = dynamic_cast<type_expected_exception const *>(&ex))
-        return pp(fmt, *_ex, opts);
-    else if (def_type_mismatch_exception const * _ex = dynamic_cast<def_type_mismatch_exception const *>(&ex))
-        return pp(fmt, *_ex, opts);
-    else
-        return format(ex.what());
-}
-
-format pp(unknown_name_exception const & ex, options const &) {
-    return format{format("unknown object '"), format(ex.get_name()), format("'")};
-}
-
-format pp(already_declared_exception const & ex, options const &) {
-    return format{format("invalid object declaration, environment already has an object named '"), format(ex.get_name()), format("'")};
-}
-
-format pp(formatter const & fmt, app_type_mismatch_exception const & ex, options const & opts) {
-    unsigned indent     = get_pp_indent(opts);
-    context const & ctx = ex.get_context();
-    expr const & app    = ex.get_application();
-    format app_fmt      = fmt(ctx, app, false, opts);
-    std::vector<expr> const & arg_types = ex.get_arg_types();
-    auto it = arg_types.begin();
-    format f_type_fmt   = fmt(ctx, *it, false, opts);
-    format arg_types_fmt;
-    ++it;
-    for (unsigned i = 1; it != arg_types.end(); ++it, ++i) {
-        expr const & a    = arg(app, i);
-        format arg_fmt    = fmt(ctx, a, false, opts);
-        if (is_pi(a) || is_lambda(a) || is_let(a))
-            arg_fmt = paren(arg_fmt);
-        format arg_type_fmt = fmt(ctx, *it, false, opts);
-        arg_types_fmt += nest(indent, compose(line(), group(format{arg_fmt, space(), colon(), nest(indent, format{line(), arg_type_fmt})})));
-    }
-    format r;
-    r += format("type mismatch at application");
-    r += nest(indent, compose(line(), app_fmt));
-    r += compose(line(), format("Function type:"));
-    r += nest(indent, compose(line(), f_type_fmt));
-    r += line();
-    if (arg_types.size() > 2)
-        r += format("Arguments types:");
-    else
-        r += format("Argument type:");
-    r += arg_types_fmt;
-    return r;
-}
-
-format pp(formatter const & fmt, function_expected_exception const & ex, options const & opts) {
-    unsigned indent = get_pp_indent(opts);
-    format expr_fmt = fmt(ex.get_context(), ex.get_expr(), false, opts);
-    format r;
-    r += format("function expected at");
-    r += nest(indent, compose(line(), expr_fmt));
-    return r;
-}
-
-format pp(formatter const & fmt, type_expected_exception const & ex, options const & opts) {
-    unsigned indent = get_pp_indent(opts);
-    format expr_fmt = fmt(ex.get_context(), ex.get_expr(), false, opts);
-    format r;
-    r += format("type expected, got");
-    r += nest(indent, compose(line(), expr_fmt));
-    return r;
-}
-
-format pp(formatter const & fmt, def_type_mismatch_exception const & ex, options const & opts) {
-    unsigned indent     = get_pp_indent(opts);
-    context const & ctx = ex.get_context();
-    format r;
-    r += format("type mismatch at definition '");
-    r += format(ex.get_name());
-    r += format("', expected type");
-    r += nest(indent, compose(line(), fmt(ctx, ex.get_type(), false, opts)));
-    r += compose(line(), format("Given type:"));
-    r += nest(indent, compose(line(), fmt(ctx, ex.get_value_type(), false, opts)));
-    return r;
-}
-
-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(pp(out.m_state.get_formatter(), ex, opts), opts);
-    return out;
-}
-
-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(pp(out.m_state.get_formatter(), ex, opts), opts);
-    return out;
-}
-}

src/library/kernel_exception_formatter.h

@@ -1,23 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "kernel/kernel_exception.h"
-#include "kernel/formatter.h"
-#include "library/state.h"
-
-namespace lean {
-/** \brief Pretty print an arbitrary kernel exception using the given formatter */
-format pp(formatter const & fmt, kernel_exception const & ex, options const & opts = options());
-format pp(unknown_name_exception const & ex, options const & opts = options());
-format pp(already_declared_exception const & ex, options const & opts = options());
-format pp(formatter const & fmt, app_type_mismatch_exception const & ex, options const & opts = options());
-format pp(formatter const & fmt, function_expected_exception const & ex, options const & opts = options());
-format pp(formatter const & fmt, type_expected_exception const & ex, options const & opts = options());
-format pp(formatter const & fmt, def_type_mismatch_exception const & ex, options const & opts = options());
-regular const & operator<<(regular const & out, kernel_exception const & ex);
-diagnostic const & operator<<(diagnostic const & out, kernel_exception const & ex);
-}

src/library/state.cpp

@@ -4,6 +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/state.h"
 
 namespace lean {
@@ -39,4 +40,58 @@ void state::set_options(options const & opts) {
 void state::set_formatter(formatter const & f) {
     m_formatter = f;
 }
+
+void regular::flush() {
+    m_state.get_regular_channel().get_stream().flush();
+}
+
+void diagnostic::flush() {
+    m_state.get_diagnostic_channel().get_stream().flush();
+}
+
+regular const & operator<<(regular const & out, endl_class) {
+    out.m_state.get_regular_channel().get_stream() << std::endl;
+    return out;
+}
+
+diagnostic const & operator<<(diagnostic const & out, endl_class) {
+    out.m_state.get_diagnostic_channel().get_stream() << std::endl;
+    return out;
+}
+
+regular const & operator<<(regular const & out, expr const & e) {
+    options const & opts = out.m_state.get_options();
+    out.m_state.get_regular_channel().get_stream() << mk_pair(out.m_state.get_formatter()(e, opts), opts);
+    return out;
+}
+
+diagnostic const & operator<<(diagnostic const & out, expr const & e) {
+    options const & opts = out.m_state.get_options();
+    out.m_state.get_diagnostic_channel().get_stream() << mk_pair(out.m_state.get_formatter()(e, opts), opts);
+    return out;
+}
+
+regular const & operator<<(regular const & out, object const & obj) {
+    options const & opts = out.m_state.get_options();
+    out.m_state.get_regular_channel().get_stream() << mk_pair(out.m_state.get_formatter()(obj, opts), opts);
+    return out;
+}
+
+diagnostic const & operator<<(diagnostic const & out, object const & obj) {
+    options const & opts = out.m_state.get_options();
+    out.m_state.get_diagnostic_channel().get_stream() << mk_pair(out.m_state.get_formatter()(obj, opts), opts);
+    return out;
+}
+
+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(ex.pp(out.m_state.get_formatter(), opts), opts);
+    return out;
+}
+
+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(ex.pp(out.m_state.get_formatter(), opts), opts);
+    return out;
+}
 }

src/library/state.h

@@ -49,7 +49,7 @@ public:
 struct regular {
     state const & m_state;
     regular(state const & s):m_state(s) {}
-    void flush() { m_state.get_regular_channel().get_stream().flush(); }
+    void flush();
 };
 
 /**
@@ -59,44 +59,23 @@ struct regular {
 struct diagnostic {
     state const & m_state;
     diagnostic(state const & s):m_state(s) {}
-    void flush() { m_state.get_diagnostic_channel().get_stream().flush(); }
+    void flush();
 };
 
 // hack for using std::endl with channels
 struct endl_class { endl_class() {} };
 const endl_class endl;
-inline regular const & operator<<(regular const & out, endl_class) {
-    out.m_state.get_regular_channel().get_stream() << std::endl;
-    return out;
-}
-inline diagnostic const & operator<<(diagnostic const & out, endl_class) {
-    out.m_state.get_diagnostic_channel().get_stream() << std::endl;
-    return out;
-}
 
-inline regular const & operator<<(regular const & out, expr const & e) {
-    options const & opts = out.m_state.get_options();
-    out.m_state.get_regular_channel().get_stream() << mk_pair(out.m_state.get_formatter()(e, opts), opts);
-    return out;
-}
+class kernel_exception;
 
-inline diagnostic const & operator<<(diagnostic const & out, expr const & e) {
-    options const & opts = out.m_state.get_options();
-    out.m_state.get_diagnostic_channel().get_stream() << mk_pair(out.m_state.get_formatter()(e, opts), opts);
-    return out;
-}
-
-inline regular const & operator<<(regular const & out, object const & obj) {
-    options const & opts = out.m_state.get_options();
-    out.m_state.get_regular_channel().get_stream() << mk_pair(out.m_state.get_formatter()(obj, opts), opts);
-    return out;
-}
-
-inline diagnostic const & operator<<(diagnostic const & out, object const & obj) {
-    options const & opts = out.m_state.get_options();
-    out.m_state.get_diagnostic_channel().get_stream() << mk_pair(out.m_state.get_formatter()(obj, opts), opts);
-    return out;
-}
+regular const &    operator<<(regular const & out,    endl_class);
+diagnostic const & operator<<(diagnostic const & out, endl_class);
+regular const &    operator<<(regular const & out,    expr const & e);
+diagnostic const & operator<<(diagnostic const & out, expr const & e);
+regular const &    operator<<(regular const & out,    object const & obj);
+diagnostic const & operator<<(diagnostic const & out, object const & obj);
+regular const &    operator<<(regular const & out,    kernel_exception const & ex);
+diagnostic const & operator<<(diagnostic const & out, kernel_exception const & ex);
 
 template<typename T>
 inline regular const & operator<<(regular const & out, T const & t) {

src/tests/kernel/type_checker.cpp

@@ -16,11 +16,11 @@ Author: Leonardo de Moura
 #include "kernel/builtin.h"
 #include "kernel/normalizer.h"
 #include "kernel/printer.h"
+#include "kernel/kernel_exception.h"
 #include "library/basic_thms.h"
 #include "library/arith/arith.h"
 #include "library/all/all.h"
 #include "library/state.h"
-#include "library/kernel_exception_formatter.h"
 using namespace lean;
 
 expr c(char const * n) { return mk_constant(n); }

src/tests/library/rewriter/rewriter.cpp

@@ -9,6 +9,7 @@ Author: Soonho Kong
 #include "kernel/context.h"
 #include "kernel/expr.h"
 #include "kernel/printer.h"
+#include "library/state.h"
 #include "library/all/all.h"
 #include "library/arith/arith.h"
 #include "library/arith/nat.h"