Moved kernel exception formatting to kernel_exception_formatter.cpp.

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

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 "kernel_exception_formatter.h"
 #include "metavar.h"
 #include "lean_frontend.h"
 #include "lean_elaborator.h"

src/library/CMakeLists.txt

@@ -1,4 +1,4 @@
 add_library(library basic_thms.cpp deep_copy.cpp max_sharing.cpp
   toplevel.cpp printer.cpp formatter.cpp context_to_lambda.cpp
-  state.cpp metavar.cpp update_expr.cpp)
+  state.cpp metavar.cpp update_expr.cpp kernel_exception_formatter.cpp)
 target_link_libraries(library ${LEAN_LIBS})

src/library/formatter.cpp

@@ -35,63 +35,4 @@ 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<unknown_name_exception const *>(&ex)) {
-        return format{format("unknown object '"), format(_ex->get_name()), format("'")};
-    } else if (already_declared_exception const * _ex = dynamic_cast<already_declared_exception const *>(&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<app_type_mismatch_exception const *>(&ex)) {
-        unsigned indent     = get_pp_indent(opts);
-        context const & ctx = _ex->get_context();
-        expr const & app    = _ex->get_application();
-        format app_fmt      = operator()(ctx, app, false, opts);
-        std::vector<expr> const & arg_types = _ex->get_arg_types();
-        auto it = arg_types.begin();
-        format f_type_fmt   = operator()(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    = operator()(ctx, a, false, opts);
-            if (is_pi(a) || is_lambda(a) || is_let(a))
-                arg_fmt = paren(arg_fmt);
-            format arg_type_fmt = operator()(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 arg_type_msg;
-        if (arg_types.size() > 2)
-            arg_type_msg = format("Arguments types:");
-        else
-            arg_type_msg = format("Argument type:");
-        return format({format("type mismatch at application"),
-                    nest(indent, compose(line(), app_fmt)),
-                    line(), format("Function type:"),
-                    nest(indent, compose(line(), f_type_fmt)),
-                    line(), arg_type_msg,
-                    arg_types_fmt});
-    } else if (function_expected_exception const * _ex = dynamic_cast<function_expected_exception const *>(&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<type_expected_exception const *>(&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<def_type_mismatch_exception const *>(&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());
-    }
-}
 }

src/library/formatter.h

@@ -37,7 +37,6 @@ public:
     /** \brief Request interruption */
     virtual void set_interrupt(bool flag) {}
 };
-class kernel_exception;
 /**
    \brief Smart-pointer for the actual formatter object (aka \c formatter_cell).
 */
@@ -46,13 +45,11 @@ class formatter {
 public:
     formatter(formatter_cell * c):m_cell(c) {}
     formatter(std::shared_ptr<formatter_cell> const & c):m_cell(c) {}
-    format operator()(expr const & e, options const & opts = options()) { return (*m_cell)(e, opts); }
+    format operator()(expr const & e, options const & opts = options()) const { return (*m_cell)(e, opts); }
-    format operator()(context const & c, options const & opts = options()) { return (*m_cell)(c, opts); }
+    format operator()(context const & c, options const & opts = options()) const { return (*m_cell)(c, opts); }
-    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()(context const & c, expr const & e, bool format_ctx = false, options const & opts = options()) const { return (*m_cell)(c, e, format_ctx, opts); }
-    format operator()(object const & obj, options const & opts = options()) { return (*m_cell)(obj, opts); }
+    format operator()(object const & obj, options const & opts = options()) const { return (*m_cell)(obj, opts); }
-    format operator()(environment const & env, options const & opts = options()) { return (*m_cell)(env, opts); }
+    format operator()(environment const & env, options const & opts = options()) const { 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());
     void set_interrupt(bool flag) { m_cell->set_interrupt(flag); }
 };
 /**

src/library/kernel_exception_formatter.cpp

@@ -0,0 +1,113 @@
+/*
+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 "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 & opts) {
+    return format{format("unknown object '"), format(ex.get_name()), format("'")};
+}
+
+format pp(already_declared_exception const & ex, options const & opts) {
+    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);
+    format r;
+    r += format("type mismatch at definition '");
+    r += format(ex.get_name());
+    r += format("', expected type");
+    r += nest(indent, compose(line(), fmt(ex.get_type(), opts)));
+    r += compose(line(), format("Given type:"));
+    r += nest(indent, compose(line(), fmt(ex.get_value_type(), 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

@@ -0,0 +1,23 @@
+/*
+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_exception.h"
+#include "formatter.h"
+#include "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.h

@@ -90,18 +90,6 @@ 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<typename T>
 inline regular const & operator<<(regular const & out, T const & t) {
     out.m_state.get_regular_channel().get_stream() << t;