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

Clean elaborator_exception pretty printing

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-05 10:05:33 -07:00
parent eb96e6441f
commit c22bd8b6ed
2 changed files with 79 additions and 74 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

148
src/frontends/lean/lean_elaborator_exception.cpp
View file

@ -8,6 +8,17 @@ Author: Leonardo de Moura
#include "lean_elaborator.h"
namespace lean {
format pp_elaborator_state(formatter fmt, elaborator const & elb, options const & opts) {
unsigned indent = get_pp_indent(opts);
format r;
if (elb.has_constraints()) {
format elb_fmt = elb.pp(fmt, opts);
r += compose(line(), format("Elaborator state"));
r += nest(indent, compose(line(), elb_fmt));
}
return r;
}
format pp(formatter fmt, context const & ctx, std::vector<expr> const & exprs, std::vector<expr> const & types, options const & opts) {
unsigned indent = get_pp_indent(opts);
lean_assert(exprs.size() == types.size());
@ -21,93 +32,84 @@ format pp(formatter fmt, context const & ctx, std::vector<expr> const & exprs, s
return r;
}
format pp_elaborator_state(formatter fmt, elaborator const & elb, options const & opts) {
unsigned indent = get_pp_indent(opts);
format elaborator_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;
if (elb.has_constraints()) {
format elb_fmt = elb.pp(fmt, opts);
r += compose(line(), format("Elaborator state"));
r += nest(indent, compose(line(), elb_fmt));
}
r += format{format(what()), space(), format("at term")};
r += nest(indent, compose(line(), expr_fmt));
r += pp_elaborator_state(fmt, get_elaborator(), opts);
return r;
}
format pp(formatter fmt, elaborator_exception const & ex, options const & opts) {
unsigned indent = get_pp_indent(opts);
context const & ctx = ex.get_context();
if (overload_exception const * _ex = dynamic_cast<overload_exception const *>(&ex)) {
format r;
r += format{format(ex.what()), line(), format("Candidates:")};
r += pp(fmt, ctx, _ex->get_fs(), _ex->get_f_types(), opts);
r += format{line(), format("Arguments:")};
r += pp(fmt, ctx, _ex->get_args(), _ex->get_arg_types(), opts);
return r;
} else if (unification_app_mismatch_exception const * _ex = dynamic_cast<unification_app_mismatch_exception const *>(&ex)) {
unsigned indent = get_pp_indent(opts);
auto const & elb = _ex->get_elaborator();
auto const & ctx = _ex->get_context();
expr const & app = _ex->get_expr();
auto const & args = _ex->get_args();
auto const & types = _ex->get_types();
auto args_it = args.begin();
auto types_it = types.begin();
format app_fmt = fmt(ctx, app, false, opts);
format r = format{format(_ex->what()), nest(indent, compose(line(), app_fmt))};
format fun_type_fmt = fmt(ctx, *types_it, false, opts);
r += compose(line(), format("Function type:"));
r += nest(indent, compose(line(), fun_type_fmt));
++args_it;
++types_it;
if (args.size() > 2)
r += compose(line(), format("Arguments types:"));
else
r += compose(line(), format("Argument type:"));
for (; args_it != args.end(); ++args_it, ++types_it) {
format arg_fmt = fmt(ctx, *args_it, false, opts);
format type_fmt = fmt(ctx, *types_it, false, opts);
r += nest(indent, compose(line(), group(format{arg_fmt, space(), colon(), nest(indent, format{line(), type_fmt})})));
}
r += pp_elaborator_state(fmt, elb, opts);
return r;
} else if (unification_type_mismatch_exception const * _ex = dynamic_cast<unification_type_mismatch_exception const *>(&ex)) {
unsigned indent = get_pp_indent(opts);
auto const & elb = _ex->get_elaborator();
auto const & ctx = _ex->get_context();
expr const & e = _ex->get_expr();
expr const & p = _ex->get_processed_expr();
expr const & exp = _ex->get_expected_type();
expr const & given = _ex->get_given_type();
format r = format{format(_ex->what()), nest(indent, compose(line(), fmt(ctx, e, false, opts)))};
if (p != e) {
r += compose(line(), format("Term after elaboration:"));
r += nest(indent, compose(line(), fmt(ctx, p, false, opts)));
}
r += compose(line(), format("Expected type:"));
r += nest(indent, compose(line(), fmt(ctx, exp, false, opts)));
if (given) {
r += compose(line(), format("Got:"));
r += nest(indent, compose(line(), fmt(ctx, given, false, opts)));
}
r += pp_elaborator_state(fmt, elb, opts);
return r;
} else {
auto const & elb = ex.get_elaborator();
format expr_fmt = fmt(ctx, ex.get_expr(), false, opts);
format r = format{format(ex.what()), space(), format("at term"), nest(indent, compose(line(), expr_fmt))};
r += pp_elaborator_state(fmt, elb, opts);
return r;
format overload_exception::pp(formatter const & fmt, options const & opts) const {
context const & ctx = get_context();
format r;
r += format{format(what()), line(), format("Candidates:")};
r += ::lean::pp(fmt, ctx, get_fs(), get_f_types(), opts);
r += format{line(), format("Arguments:")};
r += ::lean::pp(fmt, ctx, get_args(), get_arg_types(), opts);
return r;
}
format unification_app_mismatch_exception::pp(formatter const & fmt, options const & opts) const {
unsigned indent = get_pp_indent(opts);
auto const & ctx = get_context();
expr const & app = get_expr();
auto args_it = get_args().begin();
auto args_end = get_args().end();
auto types_it = get_types().begin();
format app_fmt = fmt(ctx, app, false, opts);
format r = format{format(what()), nest(indent, compose(line(), app_fmt))};
format fun_type_fmt = fmt(ctx, *types_it, false, opts);
r += compose(line(), format("Function type:"));
r += nest(indent, compose(line(), fun_type_fmt));
++args_it;
++types_it;
if (get_args().size() > 2)
r += compose(line(), format("Arguments types:"));
else
r += compose(line(), format("Argument type:"));
for (; args_it != args_end; ++args_it, ++types_it) {
format arg_fmt = fmt(ctx, *args_it, false, opts);
format type_fmt = fmt(ctx, *types_it, false, opts);
r += nest(indent, compose(line(), group(format{arg_fmt, space(), colon(), nest(indent, format{line(), type_fmt})})));
}
r += pp_elaborator_state(fmt, get_elaborator(), opts);
return r;
}
format unification_type_mismatch_exception::pp(formatter const & fmt, options const & opts) const {
unsigned indent = get_pp_indent(opts);
auto const & ctx = get_context();
expr const & e = get_expr();
expr const & p = get_processed_expr();
expr const & exp = get_expected_type();
expr const & given = get_given_type();
format r = format{format(what()), nest(indent, compose(line(), fmt(ctx, e, false, opts)))};
if (p != e) {
r += compose(line(), format("Term after elaboration:"));
r += nest(indent, compose(line(), fmt(ctx, p, false, opts)));
}
r += compose(line(), format("Expected type:"));
r += nest(indent, compose(line(), fmt(ctx, exp, false, opts)));
if (given) {
r += compose(line(), format("Got:"));
r += nest(indent, compose(line(), fmt(ctx, given, false, opts)));
}
r += pp_elaborator_state(fmt, get_elaborator(), opts);
return r;
}
regular const & operator<<(regular const & out, elaborator_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);
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, elaborator_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);
out.m_state.get_diagnostic_channel().get_stream() << mk_pair(ex.pp(out.m_state.get_formatter(), opts), opts);
return out;
}
}

5
src/frontends/lean/lean_elaborator_exception.h
View file

@ -27,6 +27,7 @@ public:
elaborator const & get_elaborator() const { return m_elb; }
expr const & get_expr() const { return m_expr; }
context const & get_context() const { return m_context; }
virtual format pp(formatter const & fmt, options const & opts) const;
};
class invalid_placeholder_exception : public elaborator_exception {
@ -54,6 +55,7 @@ public:
std::vector<expr> const & get_args() const { return m_args; }
std::vector<expr> const & get_types() const { return m_types; }
virtual char const * what() const noexcept { return "application type mismatch during term elaboration"; }
virtual format pp(formatter const & fmt, options const & opts) const;
};
class unification_type_mismatch_exception : public elaborator_exception {
@ -69,6 +71,7 @@ public:
expr const & get_expected_type() const { return m_expected_type; }
expr const & get_given_type() const { return m_given_type; }
virtual char const * what() const noexcept { return "type mismatch during term elaboration"; }
virtual format pp(formatter const & fmt, options const & opts) const;
};
class overload_exception : public elaborator_exception {
@ -91,6 +94,7 @@ public:
std::vector<expr> const & get_f_types() const { return m_f_types; }
std::vector<expr> const & get_args() const { return m_args; }
std::vector<expr> const & get_arg_types() const { return m_arg_types; }
virtual format pp(formatter const & fmt, options const & opts) const;
};
class no_overload_exception : public overload_exception {
@ -111,7 +115,6 @@ public:
virtual char const * what() const noexcept { return "ambiguous overloads"; }
};
format pp(formatter fmt, elaborator_exception const & ex, options const & opts);
regular const & operator<<(regular const & out, elaborator_exception const & ex);
diagnostic const & operator<<(diagnostic const & out, elaborator_exception const & ex);
}