michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(kernel/formatter): add environment as an extra argument to the formatter

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-04-30 10:28:07 -07:00
parent 97e7e4e762
commit 3e222e2f22
10 changed files with 88 additions and 75 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
src/kernel/error_msgs.cpp
View file

@ -7,43 +7,44 @@ Author: Leonardo de Moura
#include "kernel/error_msgs.h" #include "kernel/error_msgs.h"
namespace lean { namespace lean {
static format pp_indent_expr(formatter const & fmt, options const & opts, expr const & e) { 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(e, opts))); 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) { 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, opts, 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) { 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, opts, 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) { expr const & expected_type, expr const & given_type) {
format r; format r;
r += format("type mismatch at application"); 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 += 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 += format("given type:");
r += pp_indent_expr(fmt, opts, given_type); r += pp_indent_expr(fmt, env, opts, given_type);
return r; 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) { expr const & expected_type, expr const & given_type) {
format r("type mismatch at definition '"); format r("type mismatch at definition '");
r += format(n); r += format(n);
r += format("', expected type"); 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 += compose(line(), format("given type:"));
r += pp_indent_expr(fmt, opts, given_type); r += pp_indent_expr(fmt, env, opts, given_type);
return r; 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"); 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 += format("level constraint:");
r += pp(lhs, rhs, opts); r += pp(lhs, rhs, opts);
return r; return r;

11
src/kernel/error_msgs.h
View file

@ -8,11 +8,12 @@ Author: Leonardo de Moura
#include "kernel/expr.h" #include "kernel/expr.h"
#include "kernel/formatter.h" #include "kernel/formatter.h"
namespace lean { namespace lean {
format pp_type_expected(formatter const & fmt, options const & opts, expr const & e); format pp_type_expected(formatter const & fmt, environment const & env, options const & opts, expr const & e);
format pp_function_expected(formatter const & fmt, 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, 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); 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); 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);
} }

2
src/kernel/formatter.cpp
View file

@ -134,7 +134,7 @@ std::ostream & operator<<(std::ostream & out, expr const & e) {
class simple_formatter_cell : public formatter_cell { class simple_formatter_cell : public formatter_cell {
public: 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()); std::ostringstream s; s << e; return format(s.str());
} }
}; };

4
src/kernel/formatter.h
View file

@ -17,7 +17,7 @@ class formatter_cell {
public: public:
virtual ~formatter_cell() {} virtual ~formatter_cell() {}
/** \brief Format the given expression. */ /** \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). \brief Smart-pointer for the actual formatter object (aka \c formatter_cell).
@ -26,7 +26,7 @@ class formatter {
std::shared_ptr<formatter_cell> m_cell; std::shared_ptr<formatter_cell> m_cell;
formatter(formatter_cell * c):m_cell(c) {} formatter(formatter_cell * c):m_cell(c) {}
public: 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<typename FCell> friend formatter mk_formatter(FCell && fcell); template<typename FCell> friend formatter mk_formatter(FCell && fcell);
}; };

28
src/kernel/type_checker.cpp
View file

@ -634,13 +634,13 @@ struct type_checker::imp {
expr r = mk_sort(mk_meta_univ(m_gen.next())); expr r = mk_sort(mk_meta_univ(m_gen.next()));
justification j = mk_justification(trace_back(s), justification j = mk_justification(trace_back(s),
[=](formatter const & fmt, options const & o, substitution const & subst) { [=](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)); add_cnstr(mk_eq_cnstr(e, r, j));
return r; return r;
} else { } else {
throw_kernel_exception(m_env, trace_back(s), 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<expr> telescope; buffer<expr> telescope;
if (!meta_to_telescope(e, telescope)) if (!meta_to_telescope(e, telescope))
throw_kernel_exception(m_env, trace_back(s), 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 ta = mk_sort(mk_meta_univ(m_gen.next()));
expr A = mk_metavar(m_gen.next(), mk_tele_pi(telescope, ta)); expr A = mk_metavar(m_gen.next(), mk_tele_pi(telescope, ta));
expr A_xs = mk_app_vars(A, telescope.size()); 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); expr r = mk_pi(g_x_name, A, B);
justification j = mk_justification(trace_back(s), justification j = mk_justification(trace_back(s),
[=](formatter const & fmt, options const & o, substitution const & subst) { [=](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)); add_cnstr(mk_eq_cnstr(e, r, j));
return r; return r;
} else { } else {
throw_kernel_exception(m_env, trace_back(s), 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)); lean_assert(is_constant(c));
return mk_justification(trace_back(c), return mk_justification(trace_back(c),
[=](formatter const & fmt, options const & o, substitution const & subst) { [=](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(c),
subst.instantiate_metavars_wo_jst(lhs), subst.instantiate_metavars_wo_jst(lhs),
subst.instantiate_metavars_wo_jst(rhs)); subst.instantiate_metavars_wo_jst(rhs));
@ -710,7 +710,7 @@ struct type_checker::imp {
lean_assert(is_app(e)); lean_assert(is_app(e));
return mk_justification(trace_back(e), return mk_justification(trace_back(e),
[=](formatter const & fmt, options const & o, substitution const & subst) { [=](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(e),
subst.instantiate_metavars_wo_jst(binder_domain(fn_type)), subst.instantiate_metavars_wo_jst(binder_domain(fn_type)),
subst.instantiate_metavars_wo_jst(arg_type)); subst.instantiate_metavars_wo_jst(arg_type));
@ -725,7 +725,7 @@ struct type_checker::imp {
lean_assert(is_let(e)); lean_assert(is_let(e));
return mk_justification(trace_back(e), return mk_justification(trace_back(e),
[=](formatter const & fmt, options const & o, substitution const & subst) { [=](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(let_type(e)),
subst.instantiate_metavars_wo_jst(val_type)); 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); }); delayed_justification jst([=]() { return mk_app_mismatch_jst(e, f_type, a_type); });
if (!is_conv(a_type, binder_domain(f_type), jst)) { if (!is_conv(a_type, binder_domain(f_type), jst)) {
throw_kernel_exception(m_env, trace_back(e), 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)); 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); }); delayed_justification jst([=]() { return mk_let_mismatch_jst(e, val_type); });
if (!is_conv(val_type, let_type(e), jst)) { if (!is_conv(val_type, let_type(e), jst)) {
throw_kernel_exception(m_env, trace_back(e), 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); 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()); expr val_type = checker.check(d.get_value());
if (!checker.is_conv(val_type, d.get_type())) { if (!checker.is_conv(val_type, d.get_type())) {
throw_kernel_exception(env, d.get_value(), 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);
});
} }
} }

64
src/library/error_handling/error_handling.cpp
View file

@ -17,46 +17,46 @@ Author: Leonardo de Moura
// #include "library/unsolved_metavar_exception.h" // #include "library/unsolved_metavar_exception.h"
namespace lean { namespace lean {
void display_error_pos(io_state const & ios, char const * strm_name, unsigned line, unsigned pos) { void display_error_pos(io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos) {
regular(ios) << strm_name << ":" << line << ":"; ios << strm_name << ":" << line << ":";
if (pos != static_cast<unsigned>(-1)) if (pos != static_cast<unsigned>(-1))
regular(ios) << pos << ":"; ios << pos << ":";
regular(ios) << " error:"; 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) { if (p) {
auto pos = p->get_pos_info(e); auto pos = p->get_pos_info(e);
display_error_pos(ios, p->get_file_name(), pos.first, pos.second); display_error_pos(ios, p->get_file_name(), pos.first, pos.second);
} else { } else {
regular(ios) << "error:"; ios << "error:";
} }
} }
void display_error_pos(io_state const & ios, pos_info_provider const * p, optional<expr> const & e) { void display_error_pos(io_state_stream const & ios, pos_info_provider const * p, optional<expr> const & e) {
if (e) { if (e) {
display_error_pos(ios, p, *e); display_error_pos(ios, p, *e);
} else if (p) { } else if (p) {
auto pos = p->get_some_pos(); auto pos = p->get_some_pos();
display_error_pos(ios, p->get_file_name(), pos.first, pos.second); display_error_pos(ios, p->get_file_name(), pos.first, pos.second);
} else { } 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()); 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(); // formatter fmt = ios.get_formatter();
// options opts = ios.get_options(); // options opts = ios.get_options();
// auto j = ex.get_justification(); // auto j = ex.get_justification();
// j = remove_detail(j); // 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 { // 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) { if (p) {
char const * msg = ex.get_msg(); char const * msg = ex.get_msg();
char const * space = msg && *msg == ' ' ? "" : " "; char const * space = msg && *msg == ' ' ? "" : " ";
switch (ex.get_source()) { switch (ex.get_source()) {
case script_exception::source::String: case script_exception::source::String:
display_error_pos(ios, p->get_file_name(), ex.get_line() + p->get_some_pos().first - 1, static_cast<unsigned>(-1)); display_error_pos(ios, p->get_file_name(), ex.get_line() + p->get_some_pos().first - 1, static_cast<unsigned>(-1));
regular(ios) << " executing script," << space << msg << endl; ios << " executing script," << space << msg << endl;
break; break;
case script_exception::source::File: case script_exception::source::File:
display_error_pos(ios, p->get_file_name(), p->get_some_pos().first, p->get_some_pos().second); 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; break;
case script_exception::source::Unknown: case script_exception::source::Unknown:
display_error_pos(ios, p->get_file_name(), p->get_some_pos().first, p->get_some_pos().second); 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; break;
} }
} else { } 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()) { switch (ex.get_source()) {
case script_exception::source::String: case script_exception::source::String:
if (p) { if (p) {
display_error_pos(ios, p->get_file_name(), ex.get_line() + p->get_some_pos().first - 1, static_cast<unsigned>(-1)); display_error_pos(ios, p->get_file_name(), ex.get_line() + p->get_some_pos().first - 1, static_cast<unsigned>(-1));
regular(ios) << " executing script" << endl; ios << " executing script" << endl;
} }
display_error(ios, nullptr, ex.get_exception()); display_error(ios, nullptr, ex.get_exception());
break; break;
case script_exception::source::File: case script_exception::source::File:
if (p) { if (p) {
display_error_pos(ios, p->get_file_name(), p->get_some_pos().first, p->get_some_pos().second); 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 { } else {
display_error_pos(ios, ex.get_file_name(), ex.get_line(), -1); 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()); display_error(ios, nullptr, ex.get_exception());
break; 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()); // 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) { // static void display_error(io_state_stream const & ios, pos_info_provider const *, parser_exception const & ex) {
// regular(ios) << ex.what() << endl; // 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()); // display_error_pos(ios, p, ex.get_expr());
// formatter fmt = ios.get_formatter(); // formatter fmt = ios.get_formatter();
// options opts = ios.get_options(); // options opts = ios.get_options();
// unsigned indent = get_pp_indent(opts); // unsigned indent = get_pp_indent(opts);
// format r = nest(indent, compose(line(), fmt(ex.get_expr(), 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) { // if (p) {
// name_set already_displayed; // name_set already_displayed;
// for_each(ex.get_expr(), [&](expr const & e, unsigned) -> bool { // 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); // name const & m = metavar_name(e);
// if (already_displayed.find(m) == already_displayed.end()) { // if (already_displayed.find(m) == already_displayed.end()) {
// already_displayed.insert(m); // 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); // display_error_pos(ios, p, e);
// regular(ios) << " unsolved metavar " << m << endl; // ios << " unsolved metavar " << m << endl;
// } // }
// } // }
// return true; // 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<kernel_exception const *>(&ex)) { if (auto k_ex = dynamic_cast<kernel_exception const *>(&ex)) {
display_error(ios, p, *k_ex); display_error(ios, p, *k_ex);
// } else if (auto e_ex = dynamic_cast<elaborator_exception const *>(&ex)) { // } else if (auto e_ex = dynamic_cast<elaborator_exception const *>(&ex)) {
@ -173,9 +173,9 @@ void display_error(io_state const & ios, pos_info_provider const * p, exception
// display_error(ios, p, *n_ex); // display_error(ios, p, *n_ex);
} else if (p) { } else if (p) {
display_error_pos(ios, p->get_file_name(), p->get_some_pos().first, p->get_some_pos().second); 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 { } else {
regular(ios) << "error: " << ex.what() << endl; ios << "error: " << ex.what() << endl;
} }
} }
} }

4
src/library/error_handling/error_handling.h
View file

@ -7,12 +7,12 @@ Author: Leonardo de Moura
#pragma once #pragma once
#include "util/exception.h" #include "util/exception.h"
#include "kernel/pos_info_provider.h" #include "kernel/pos_info_provider.h"
#include "library/io_state.h" #include "library/io_state_stream.h"
namespace lean { namespace lean {
/** /**
\brief Display exception in the regular stream of \c ios, using the configuration options and formatter from \c ios. \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. 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);
} }

2
src/library/io_state_stream.cpp
View file

@ -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) { io_state_stream const & operator<<(io_state_stream const & out, expr const & e) {
options const & opts = out.get_options(); 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; return out;
} }

8
src/library/io_state_stream.h
View file

@ -13,13 +13,15 @@ namespace lean {
*/ */
class io_state_stream { class io_state_stream {
protected: protected:
environment const & m_env;
io_state const & m_io_state; io_state const & m_io_state;
public: 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; virtual std::ostream & get_stream() const = 0;
void flush() { get_stream().flush(); } void flush() { get_stream().flush(); }
formatter get_formatter() const { return m_io_state.get_formatter(); } formatter get_formatter() const { return m_io_state.get_formatter(); }
options get_options() const { return m_io_state.get_options(); } 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 { class regular : public io_state_stream {
public: 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(); } 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 { class diagnostic : public io_state_stream {
public: 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(); } std::ostream & get_stream() const { return m_io_state.get_diagnostic_channel().get_stream(); }
}; };

7
src/shell/lean.cpp
View file

@ -36,14 +36,16 @@ Author: Leonardo de Moura
using lean::script_state; using lean::script_state;
using lean::unreachable_reached; using lean::unreachable_reached;
using lean::environment;
using lean::io_state; using lean::io_state;
using lean::io_state_stream;
using lean::regular;
#if 0 #if 0
using lean::shell; using lean::shell;
using lean::parser; using lean::parser;
using lean::invoke_debugger; using lean::invoke_debugger;
using lean::notify_assertion_violation; using lean::notify_assertion_violation;
using lean::environment;
#endif #endif
enum class input_kind { Unspecified, Lean, OLean, Lua }; enum class input_kind { Unspecified, Lean, OLean, Lua };
@ -238,7 +240,8 @@ int main(int argc, char ** argv) {
try { try {
S.dofile(argv[i]); S.dofile(argv[i]);
} catch (lean::exception & ex) { } 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; ok = false;
} }
} else { } else {