From 85bfa45e6a5d88b53f41776b04b1772a223c8968 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Sep 2013 18:38:47 -0700 Subject: [PATCH] refactor(kernel_exception): delete kernel_exception_formatter, and implement kernel_exception pretty printer as a virtual method Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser.cpp | 1 - src/kernel/CMakeLists.txt | 3 +- src/kernel/kernel_exception.cpp | 85 +++++++++++++++ src/kernel/kernel_exception.h | 9 ++ src/library/CMakeLists.txt | 5 +- src/library/kernel_exception_formatter.cpp | 115 --------------------- src/library/kernel_exception_formatter.h | 23 ----- src/library/state.cpp | 55 ++++++++++ src/library/state.h | 43 ++------ src/tests/kernel/type_checker.cpp | 2 +- src/tests/library/rewriter/rewriter.cpp | 1 + 11 files changed, 166 insertions(+), 176 deletions(-) create mode 100644 src/kernel/kernel_exception.cpp delete mode 100644 src/library/kernel_exception_formatter.cpp delete mode 100644 src/library/kernel_exception_formatter.h diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index bd07c0960..7f3f1cd8c 100644 --- a/src/frontends/lean/parser.cpp +++ b/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" diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index bd36eaa73..9946262dd 100644 --- a/src/kernel/CMakeLists.txt +++ b/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}) diff --git a/src/kernel/kernel_exception.cpp b/src/kernel/kernel_exception.cpp new file mode 100644 index 000000000..bf6af08e7 --- /dev/null +++ b/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 +#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 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; +} +} diff --git a/src/kernel/kernel_exception.h b/src/kernel/kernel_exception.h index 7bec23642..89e493df7 100644 --- a/src/kernel/kernel_exception.h +++ b/src/kernel/kernel_exception.h @@ -7,8 +7,10 @@ Author: Leonardo de Moura #pragma once #include #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 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; }; /** diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 5b2dd6baa..a6e8cc953 100644 --- a/src/library/CMakeLists.txt +++ b/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}) diff --git a/src/library/kernel_exception_formatter.cpp b/src/library/kernel_exception_formatter.cpp deleted file mode 100644 index 2c02619e9..000000000 --- a/src/library/kernel_exception_formatter.cpp +++ /dev/null @@ -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 -#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(&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 &) { - 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 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; -} -} diff --git a/src/library/kernel_exception_formatter.h b/src/library/kernel_exception_formatter.h deleted file mode 100644 index 5a10a6739..000000000 --- a/src/library/kernel_exception_formatter.h +++ /dev/null @@ -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); -} diff --git a/src/library/state.cpp b/src/library/state.cpp index 737d2d3d4..55ff1af0e 100644 --- a/src/library/state.cpp +++ b/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; +} } diff --git a/src/library/state.h b/src/library/state.h index 895021373..017257f51 100644 --- a/src/library/state.h +++ b/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 inline regular const & operator<<(regular const & out, T const & t) { diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp index f79165185..49ae26f47 100644 --- a/src/tests/kernel/type_checker.cpp +++ b/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); } diff --git a/src/tests/library/rewriter/rewriter.cpp b/src/tests/library/rewriter/rewriter.cpp index 169344de0..5bf0b1741 100644 --- a/src/tests/library/rewriter/rewriter.cpp +++ b/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"