From eb96e6441fa87ff577e6489913bb2af07965c415 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 5 Sep 2013 09:51:17 -0700 Subject: [PATCH] Moved kernel exception formatting to kernel_exception_formatter.cpp. Signed-off-by: Leonardo de Moura --- src/frontends/lean/lean_parser.cpp | 1 + src/library/CMakeLists.txt | 2 +- src/library/formatter.cpp | 59 ----------- src/library/formatter.h | 13 +-- src/library/kernel_exception_formatter.cpp | 113 +++++++++++++++++++++ src/library/kernel_exception_formatter.h | 23 +++++ src/library/state.h | 12 --- 7 files changed, 143 insertions(+), 80 deletions(-) create mode 100644 src/library/kernel_exception_formatter.cpp create mode 100644 src/library/kernel_exception_formatter.h diff --git a/src/frontends/lean/lean_parser.cpp b/src/frontends/lean/lean_parser.cpp index f7438e137..0b5fdf2f1 100644 --- a/src/frontends/lean/lean_parser.cpp +++ b/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" diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index cefce227c..b63182861 100644 --- a/src/library/CMakeLists.txt +++ b/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}) diff --git a/src/library/formatter.cpp b/src/library/formatter.cpp index 41cf0dd6b..a48f4407c 100644 --- a/src/library/formatter.cpp +++ b/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(&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); - context const & ctx = _ex->get_context(); - expr const & app = _ex->get_application(); - format app_fmt = operator()(ctx, app, false, opts); - std::vector 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(&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 6bbdb18a2..470488a8e 100644 --- a/src/library/formatter.h +++ b/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 const & c):m_cell(c) {} - format operator()(expr const & e, options const & opts = options()) { return (*m_cell)(e, opts); } - format operator()(context const & c, options const & opts = options()) { 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()(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()); + format operator()(expr const & e, options const & opts = options()) const { return (*m_cell)(e, 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()) const { return (*m_cell)(c, e, format_ctx, 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()) const { return (*m_cell)(env, opts); } void set_interrupt(bool flag) { m_cell->set_interrupt(flag); } }; /** diff --git a/src/library/kernel_exception_formatter.cpp b/src/library/kernel_exception_formatter.cpp new file mode 100644 index 000000000..ac2abe3ca --- /dev/null +++ b/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(&ex)) + return pp(*_ex, opts); + else if (already_declared_exception const * _ex = dynamic_cast(&ex)) + return pp(*_ex, opts); + else if (app_type_mismatch_exception const * _ex = dynamic_cast(&ex)) + return pp(fmt, *_ex, opts); + else if (function_expected_exception const * _ex = dynamic_cast(&ex)) + return pp(fmt, *_ex, opts); + else if (type_expected_exception const * _ex = dynamic_cast(&ex)) + return pp(fmt, *_ex, opts); + else if (def_type_mismatch_exception const * _ex = dynamic_cast(&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 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; +} +} diff --git a/src/library/kernel_exception_formatter.h b/src/library/kernel_exception_formatter.h new file mode 100644 index 000000000..09dea1fc6 --- /dev/null +++ b/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); +} diff --git a/src/library/state.h b/src/library/state.h index d35b9928f..fe6eb56c8 100644 --- a/src/library/state.h +++ b/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 inline regular const & operator<<(regular const & out, T const & t) { out.m_state.get_regular_channel().get_stream() << t;