From 3e222e2f22867eee36ac329fad52457256693beb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 30 Apr 2014 10:28:07 -0700 Subject: [PATCH] refactor(kernel/formatter): add environment as an extra argument to the formatter Signed-off-by: Leonardo de Moura --- src/kernel/error_msgs.cpp | 31 ++++----- src/kernel/error_msgs.h | 11 ++-- src/kernel/formatter.cpp | 2 +- src/kernel/formatter.h | 4 +- src/kernel/type_checker.cpp | 28 ++++---- src/library/error_handling/error_handling.cpp | 64 +++++++++---------- src/library/error_handling/error_handling.h | 4 +- src/library/io_state_stream.cpp | 2 +- src/library/io_state_stream.h | 10 +-- src/shell/lean.cpp | 7 +- 10 files changed, 88 insertions(+), 75 deletions(-) diff --git a/src/kernel/error_msgs.cpp b/src/kernel/error_msgs.cpp index 4e3739438..ae2d26a1c 100644 --- a/src/kernel/error_msgs.cpp +++ b/src/kernel/error_msgs.cpp @@ -7,43 +7,44 @@ Author: Leonardo de Moura #include "kernel/error_msgs.h" namespace lean { -static format pp_indent_expr(formatter const & fmt, options const & opts, expr const & e) { - return nest(get_pp_indent(opts), compose(line(), fmt(e, opts))); +static format pp_indent_expr(formatter const & fmt, environment const & env, options const & opts, expr const & e) { + return nest(get_pp_indent(opts), compose(line(), fmt(env, e, opts))); } -format pp_type_expected(formatter const & fmt, options const & opts, expr const & e) { - return compose(format("type expected at"), pp_indent_expr(fmt, opts, e)); +format pp_type_expected(formatter const & fmt, environment const & env, options const & opts, expr const & e) { + return compose(format("type expected at"), pp_indent_expr(fmt, env, opts, e)); } -format pp_function_expected(formatter const & fmt, options const & opts, expr const & e) { - return compose(format("function expected at"), pp_indent_expr(fmt, opts, e)); +format pp_function_expected(formatter const & fmt, environment const & env, options const & opts, expr const & e) { + return compose(format("function expected at"), pp_indent_expr(fmt, env, opts, e)); } -format pp_app_type_mismatch(formatter const & fmt, options const & opts, expr const & app, +format pp_app_type_mismatch(formatter const & fmt, environment const & env, options const & opts, expr const & app, expr const & expected_type, expr const & given_type) { format r; r += format("type mismatch at application"); - r += pp_indent_expr(fmt, opts, app); + r += pp_indent_expr(fmt, env, opts, app); r += format("expected type:"); - r += pp_indent_expr(fmt, opts, expected_type); + r += pp_indent_expr(fmt, env, opts, expected_type); r += format("given type:"); - r += pp_indent_expr(fmt, opts, given_type); + r += pp_indent_expr(fmt, env, opts, given_type); return r; } -format pp_def_type_mismatch(formatter const & fmt, options const & opts, name const & n, +format pp_def_type_mismatch(formatter const & fmt, environment const & env, options const & opts, name const & n, expr const & expected_type, expr const & given_type) { format r("type mismatch at definition '"); r += format(n); r += format("', expected type"); - r += pp_indent_expr(fmt, opts, expected_type); + r += pp_indent_expr(fmt, env, opts, expected_type); r += compose(line(), format("given type:")); - r += pp_indent_expr(fmt, opts, given_type); + r += pp_indent_expr(fmt, env, opts, given_type); return r; } -format pp_def_lvl_cnstrs_satisfied(formatter const & fmt, options const & opts, expr const & e, level const & lhs, level const & rhs) { +format pp_def_lvl_cnstrs_satisfied(formatter const & fmt, environment const & env, options const & opts, expr const & e, + level const & lhs, level const & rhs) { format r("constand definition level constraints are not satisfied"); - r += pp_indent_expr(fmt, opts, e); + r += pp_indent_expr(fmt, env, opts, e); r += format("level constraint:"); r += pp(lhs, rhs, opts); return r; diff --git a/src/kernel/error_msgs.h b/src/kernel/error_msgs.h index b24b1f63e..207a2aac4 100644 --- a/src/kernel/error_msgs.h +++ b/src/kernel/error_msgs.h @@ -8,11 +8,12 @@ Author: Leonardo de Moura #include "kernel/expr.h" #include "kernel/formatter.h" namespace lean { -format pp_type_expected(formatter const & fmt, options const & opts, expr const & e); -format pp_function_expected(formatter const & fmt, options const & opts, expr const & e); -format pp_app_type_mismatch(formatter const & fmt, options const & opts, expr const & app, +format pp_type_expected(formatter const & fmt, environment const & env, options const & opts, expr const & e); +format pp_function_expected(formatter const & fmt, environment const & env, options const & opts, expr const & e); +format pp_app_type_mismatch(formatter const & fmt, environment const & env, options const & opts, expr const & app, expr const & expected_type, expr const & given_type); -format pp_def_type_mismatch(formatter const & fmt, options const & opts, name const & n, +format pp_def_type_mismatch(formatter const & fmt, environment const & env, options const & opts, name const & n, expr const & expected_type, expr const & given_type); -format pp_def_lvl_cnstrs_satisfied(formatter const & fmt, options const & opts, expr const & e, level const & lhs, level const & rhs); +format pp_def_lvl_cnstrs_satisfied(formatter const & fmt, environment const & env, options const & opts, expr const & e, + level const & lhs, level const & rhs); } diff --git a/src/kernel/formatter.cpp b/src/kernel/formatter.cpp index 83ef6c5ea..11bd1e2fa 100644 --- a/src/kernel/formatter.cpp +++ b/src/kernel/formatter.cpp @@ -134,7 +134,7 @@ std::ostream & operator<<(std::ostream & out, expr const & e) { class simple_formatter_cell : public formatter_cell { public: - virtual format operator()(expr const & e, options const &) { + virtual format operator()(environment const &, expr const & e, options const &) { std::ostringstream s; s << e; return format(s.str()); } }; diff --git a/src/kernel/formatter.h b/src/kernel/formatter.h index dd8fcaf1c..a6e2747be 100644 --- a/src/kernel/formatter.h +++ b/src/kernel/formatter.h @@ -17,7 +17,7 @@ class formatter_cell { public: virtual ~formatter_cell() {} /** \brief Format the given expression. */ - virtual format operator()(expr const & e, options const & opts) = 0; + virtual format operator()(environment const & env, expr const & e, options const & opts) = 0; }; /** \brief Smart-pointer for the actual formatter object (aka \c formatter_cell). @@ -26,7 +26,7 @@ class formatter { std::shared_ptr m_cell; formatter(formatter_cell * c):m_cell(c) {} public: - format operator()(expr const & e, options const & opts = options()) const { return (*m_cell)(e, opts); } + format operator()(environment const & env, expr const & e, options const & opts = options()) const { return (*m_cell)(env, e, opts); } template friend formatter mk_formatter(FCell && fcell); }; diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 5a273075a..30a07ff41 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -634,13 +634,13 @@ struct type_checker::imp { expr r = mk_sort(mk_meta_univ(m_gen.next())); justification j = mk_justification(trace_back(s), [=](formatter const & fmt, options const & o, substitution const & subst) { - return pp_type_expected(fmt, o, subst.instantiate_metavars_wo_jst(s)); + return pp_type_expected(fmt, m_env, o, subst.instantiate_metavars_wo_jst(s)); }); add_cnstr(mk_eq_cnstr(e, r, j)); return r; } else { throw_kernel_exception(m_env, trace_back(s), - [=](formatter const & fmt, options const & o) { return pp_type_expected(fmt, o, s); }); + [=](formatter const & fmt, options const & o) { return pp_type_expected(fmt, m_env, o, s); }); } } @@ -665,7 +665,7 @@ struct type_checker::imp { buffer telescope; if (!meta_to_telescope(e, telescope)) throw_kernel_exception(m_env, trace_back(s), - [=](formatter const & fmt, options const & o) { return pp_function_expected(fmt, o, s); }); + [=](formatter const & fmt, options const & o) { return pp_function_expected(fmt, m_env, o, s); }); expr ta = mk_sort(mk_meta_univ(m_gen.next())); expr A = mk_metavar(m_gen.next(), mk_tele_pi(telescope, ta)); expr A_xs = mk_app_vars(A, telescope.size()); @@ -680,13 +680,13 @@ struct type_checker::imp { expr r = mk_pi(g_x_name, A, B); justification j = mk_justification(trace_back(s), [=](formatter const & fmt, options const & o, substitution const & subst) { - return pp_function_expected(fmt, o, subst.instantiate_metavars_wo_jst(s)); + return pp_function_expected(fmt, m_env, o, subst.instantiate_metavars_wo_jst(s)); }); add_cnstr(mk_eq_cnstr(e, r, j)); return r; } else { throw_kernel_exception(m_env, trace_back(s), - [=](formatter const & fmt, options const & o) { return pp_function_expected(fmt, o, s); }); + [=](formatter const & fmt, options const & o) { return pp_function_expected(fmt, m_env, o, s); }); } } @@ -695,7 +695,7 @@ struct type_checker::imp { lean_assert(is_constant(c)); return mk_justification(trace_back(c), [=](formatter const & fmt, options const & o, substitution const & subst) { - return pp_def_lvl_cnstrs_satisfied(fmt, o, + return pp_def_lvl_cnstrs_satisfied(fmt, m_env, o, subst.instantiate_metavars_wo_jst(c), subst.instantiate_metavars_wo_jst(lhs), subst.instantiate_metavars_wo_jst(rhs)); @@ -710,7 +710,7 @@ struct type_checker::imp { lean_assert(is_app(e)); return mk_justification(trace_back(e), [=](formatter const & fmt, options const & o, substitution const & subst) { - return pp_app_type_mismatch(fmt, o, + return pp_app_type_mismatch(fmt, m_env, o, subst.instantiate_metavars_wo_jst(e), subst.instantiate_metavars_wo_jst(binder_domain(fn_type)), subst.instantiate_metavars_wo_jst(arg_type)); @@ -725,7 +725,7 @@ struct type_checker::imp { lean_assert(is_let(e)); return mk_justification(trace_back(e), [=](formatter const & fmt, options const & o, substitution const & subst) { - return pp_def_type_mismatch(fmt, o, let_name(e), + return pp_def_type_mismatch(fmt, m_env, o, let_name(e), subst.instantiate_metavars_wo_jst(let_type(e)), subst.instantiate_metavars_wo_jst(val_type)); }); @@ -824,7 +824,9 @@ struct type_checker::imp { delayed_justification jst([=]() { return mk_app_mismatch_jst(e, f_type, a_type); }); if (!is_conv(a_type, binder_domain(f_type), jst)) { throw_kernel_exception(m_env, trace_back(e), - [=](formatter const & fmt, options const & o) { return pp_app_type_mismatch(fmt, o, e, binder_domain(f_type), a_type); }); + [=](formatter const & fmt, options const & o) { + return pp_app_type_mismatch(fmt, m_env, o, e, binder_domain(f_type), a_type); + }); } } r = instantiate(binder_body(f_type), app_arg(e)); @@ -837,7 +839,9 @@ struct type_checker::imp { delayed_justification jst([=]() { return mk_let_mismatch_jst(e, val_type); }); if (!is_conv(val_type, let_type(e), jst)) { throw_kernel_exception(m_env, trace_back(e), - [=](formatter const & fmt, options const & o) { return pp_def_type_mismatch(fmt, o, let_name(e), let_type(e), val_type); }); + [=](formatter const & fmt, options const & o) { + return pp_def_type_mismatch(fmt, m_env, o, let_name(e), let_type(e), val_type); + }); } } r = infer_type_core(instantiate_with_trace(let_body(e), let_value(e)), infer_only); @@ -925,7 +929,9 @@ certified_definition check(environment const & env, name_generator const & g, de expr val_type = checker.check(d.get_value()); if (!checker.is_conv(val_type, d.get_type())) { throw_kernel_exception(env, d.get_value(), - [=](formatter const & fmt, options const & o) { return pp_def_type_mismatch(fmt, o, d.get_name(), d.get_type(), val_type); }); + [=](formatter const & fmt, options const & o) { + return pp_def_type_mismatch(fmt, env, o, d.get_name(), d.get_type(), val_type); + }); } } diff --git a/src/library/error_handling/error_handling.cpp b/src/library/error_handling/error_handling.cpp index 01dbe9e1e..023dbf272 100644 --- a/src/library/error_handling/error_handling.cpp +++ b/src/library/error_handling/error_handling.cpp @@ -17,46 +17,46 @@ Author: Leonardo de Moura // #include "library/unsolved_metavar_exception.h" namespace lean { -void display_error_pos(io_state const & ios, char const * strm_name, unsigned line, unsigned pos) { - regular(ios) << strm_name << ":" << line << ":"; +void display_error_pos(io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos) { + ios << strm_name << ":" << line << ":"; if (pos != static_cast(-1)) - regular(ios) << pos << ":"; - regular(ios) << " error:"; + ios << pos << ":"; + ios << " error:"; } -void display_error_pos(io_state const & ios, pos_info_provider const * p, expr const & e) { +void display_error_pos(io_state_stream const & ios, pos_info_provider const * p, expr const & e) { if (p) { auto pos = p->get_pos_info(e); display_error_pos(ios, p->get_file_name(), pos.first, pos.second); } else { - regular(ios) << "error:"; + ios << "error:"; } } -void display_error_pos(io_state const & ios, pos_info_provider const * p, optional const & e) { +void display_error_pos(io_state_stream const & ios, pos_info_provider const * p, optional const & e) { if (e) { display_error_pos(ios, p, *e); } else if (p) { auto pos = p->get_some_pos(); display_error_pos(ios, p->get_file_name(), pos.first, pos.second); } else { - regular(ios) << "error:"; + ios << "error:"; } } -void display_error(io_state const & ios, pos_info_provider const * p, exception const & ex); +void display_error(io_state_stream const & ios, pos_info_provider const * p, exception const & ex); -static void display_error(io_state 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, kernel_exception const & ex) { display_error_pos(ios, p, ex.get_main_expr()); - regular(ios) << " " << ex << endl; + ios << " " << ex << endl; } -// static void display_error(io_state const & ios, pos_info_provider const * p, elaborator_exception const & ex) { +// static void display_error(io_state_stream const & ios, pos_info_provider const * p, elaborator_exception const & ex) { // formatter fmt = ios.get_formatter(); // options opts = ios.get_options(); // auto j = ex.get_justification(); // j = remove_detail(j); -// regular(ios) << mk_pair(j.pp(fmt, opts, p, true), opts) << endl; +// ios << mk_pair(j.pp(fmt, opts, p, true), opts) << endl; // } // struct delta_pos_info_provider : public pos_info_provider { @@ -76,45 +76,45 @@ static void display_error(io_state const & ios, pos_info_provider const * p, ker // }; -static void display_error(io_state const & ios, pos_info_provider const * p, script_exception const & ex) { +static void display_error(io_state_stream const & ios, pos_info_provider const * p, script_exception const & ex) { if (p) { char const * msg = ex.get_msg(); char const * space = msg && *msg == ' ' ? "" : " "; switch (ex.get_source()) { case script_exception::source::String: display_error_pos(ios, p->get_file_name(), ex.get_line() + p->get_some_pos().first - 1, static_cast(-1)); - regular(ios) << " executing script," << space << msg << endl; + ios << " executing script," << space << msg << endl; break; case script_exception::source::File: display_error_pos(ios, p->get_file_name(), p->get_some_pos().first, p->get_some_pos().second); - regular(ios) << " executing external script (" << ex.get_file_name() << ":" << ex.get_line() << ")," << space << msg << endl; + ios << " executing external script (" << ex.get_file_name() << ":" << ex.get_line() << ")," << space << msg << endl; break; case script_exception::source::Unknown: display_error_pos(ios, p->get_file_name(), p->get_some_pos().first, p->get_some_pos().second); - regular(ios) << " executing script, exact error position is not available, " << ex.what() << endl; + ios << " executing script, exact error position is not available, " << ex.what() << endl; break; } } else { - regular(ios) << ex.what() << endl; + ios << ex.what() << endl; } } -static void display_error(io_state const & ios, pos_info_provider const * p, script_nested_exception const & ex) { +static void display_error(io_state_stream const & ios, pos_info_provider const * p, script_nested_exception const & ex) { switch (ex.get_source()) { case script_exception::source::String: if (p) { display_error_pos(ios, p->get_file_name(), ex.get_line() + p->get_some_pos().first - 1, static_cast(-1)); - regular(ios) << " executing script" << endl; + ios << " executing script" << endl; } display_error(ios, nullptr, ex.get_exception()); break; case script_exception::source::File: if (p) { display_error_pos(ios, p->get_file_name(), p->get_some_pos().first, p->get_some_pos().second); - regular(ios) << " executing external script (" << ex.get_file_name() << ":" << ex.get_line() << ")" << endl; + ios << " executing external script (" << ex.get_file_name() << ":" << ex.get_line() << ")" << endl; } else { display_error_pos(ios, ex.get_file_name(), ex.get_line(), -1); - regular(ios) << " executing script" << endl; + ios << " executing script" << endl; } display_error(ios, nullptr, ex.get_exception()); break; @@ -124,21 +124,21 @@ static void display_error(io_state const & ios, pos_info_provider const * p, scr } } -// static void display_error(io_state const & ios, pos_info_provider const *, parser_nested_exception const & ex) { +// static void display_error(io_state_stream const & ios, pos_info_provider const *, parser_nested_exception const & ex) { // display_error(ios, &(ex.get_provider()), ex.get_exception()); // } -// static void display_error(io_state const & ios, pos_info_provider const *, parser_exception const & ex) { -// regular(ios) << ex.what() << endl; +// static void display_error(io_state_stream const & ios, pos_info_provider const *, parser_exception const & ex) { +// ios << ex.what() << endl; // } -// static void display_error(io_state const & ios, pos_info_provider const * p, unsolved_metavar_exception const & ex) { +// static void display_error(io_state_stream const & ios, pos_info_provider const * p, unsolved_metavar_exception const & ex) { // display_error_pos(ios, p, ex.get_expr()); // formatter fmt = ios.get_formatter(); // options opts = ios.get_options(); // unsigned indent = get_pp_indent(opts); // format r = nest(indent, compose(line(), fmt(ex.get_expr(), opts))); -// regular(ios) << " " << ex.what() << mk_pair(r, opts) << endl; +// ios << " " << ex.what() << mk_pair(r, opts) << endl; // if (p) { // name_set already_displayed; // for_each(ex.get_expr(), [&](expr const & e, unsigned) -> bool { @@ -146,9 +146,9 @@ static void display_error(io_state const & ios, pos_info_provider const * p, scr // name const & m = metavar_name(e); // if (already_displayed.find(m) == already_displayed.end()) { // already_displayed.insert(m); -// for (unsigned i = 0; i < indent; i++) regular(ios) << " "; +// for (unsigned i = 0; i < indent; i++) ios << " "; // display_error_pos(ios, p, e); -// regular(ios) << " unsolved metavar " << m << endl; +// ios << " unsolved metavar " << m << endl; // } // } // return true; @@ -156,7 +156,7 @@ static void display_error(io_state const & ios, pos_info_provider const * p, scr // } // } -void display_error(io_state const & ios, pos_info_provider const * p, exception const & ex) { +void display_error(io_state_stream const & ios, pos_info_provider const * p, exception const & ex) { if (auto k_ex = dynamic_cast(&ex)) { display_error(ios, p, *k_ex); // } else if (auto e_ex = dynamic_cast(&ex)) { @@ -173,9 +173,9 @@ void display_error(io_state const & ios, pos_info_provider const * p, exception // display_error(ios, p, *n_ex); } else if (p) { display_error_pos(ios, p->get_file_name(), p->get_some_pos().first, p->get_some_pos().second); - regular(ios) << " " << ex.what() << endl; + ios << " " << ex.what() << endl; } else { - regular(ios) << "error: " << ex.what() << endl; + ios << "error: " << ex.what() << endl; } } } diff --git a/src/library/error_handling/error_handling.h b/src/library/error_handling/error_handling.h index feaebacca..b4e75bab4 100644 --- a/src/library/error_handling/error_handling.h +++ b/src/library/error_handling/error_handling.h @@ -7,12 +7,12 @@ Author: Leonardo de Moura #pragma once #include "util/exception.h" #include "kernel/pos_info_provider.h" -#include "library/io_state.h" +#include "library/io_state_stream.h" namespace lean { /** \brief Display exception in the regular stream of \c ios, using the configuration options and formatter from \c ios. Exceptions that contain expressions use the given \c pos_info_provider (if available) to retrieve line number information. */ -void display_error(io_state const & ios, pos_info_provider const * p, exception const & ex); +void display_error(io_state_stream const & ios, pos_info_provider const * p, exception const & ex); } diff --git a/src/library/io_state_stream.cpp b/src/library/io_state_stream.cpp index cdabdc6d2..317c462d2 100644 --- a/src/library/io_state_stream.cpp +++ b/src/library/io_state_stream.cpp @@ -14,7 +14,7 @@ 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) { options const & opts = out.get_options(); - out.get_stream() << mk_pair(out.get_formatter()(e, opts), opts); + out.get_stream() << mk_pair(out.get_formatter()(out.get_environment(), e, opts), opts); return out; } diff --git a/src/library/io_state_stream.h b/src/library/io_state_stream.h index f75fcf84a..b09d32705 100644 --- a/src/library/io_state_stream.h +++ b/src/library/io_state_stream.h @@ -13,13 +13,15 @@ namespace lean { */ class io_state_stream { protected: - io_state const & m_io_state; + environment const & m_env; + io_state const & m_io_state; public: - io_state_stream(io_state const & s):m_io_state(s) {} + io_state_stream(environment const & env, io_state const & s):m_env(env), m_io_state(s) {} virtual std::ostream & get_stream() const = 0; void flush() { get_stream().flush(); } formatter get_formatter() const { return m_io_state.get_formatter(); } options get_options() const { return m_io_state.get_options(); } + environment const & get_environment() const { return m_env; } }; /** @@ -28,7 +30,7 @@ public: */ class regular : public io_state_stream { public: - regular(io_state const & s):io_state_stream(s) {} + regular(environment const & env, io_state const & s):io_state_stream(env, s) {} std::ostream & get_stream() const { return m_io_state.get_regular_channel().get_stream(); } }; @@ -38,7 +40,7 @@ public: */ class diagnostic : public io_state_stream { public: - diagnostic(io_state const & s):io_state_stream(s) {} + diagnostic(environment const & env, io_state const & s):io_state_stream(env, s) {} std::ostream & get_stream() const { return m_io_state.get_diagnostic_channel().get_stream(); } }; diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 2eb95dbb5..d9f1b95bc 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -36,14 +36,16 @@ Author: Leonardo de Moura using lean::script_state; using lean::unreachable_reached; +using lean::environment; using lean::io_state; +using lean::io_state_stream; +using lean::regular; #if 0 using lean::shell; using lean::parser; using lean::invoke_debugger; using lean::notify_assertion_violation; -using lean::environment; #endif enum class input_kind { Unspecified, Lean, OLean, Lua }; @@ -238,7 +240,8 @@ int main(int argc, char ** argv) { try { S.dofile(argv[i]); } catch (lean::exception & ex) { - ::lean::display_error(ios, nullptr, ex); + environment env; // TODO(Leo): use global environment + ::lean::display_error(regular(env, ios), nullptr, ex); ok = false; } } else {