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

feat(library/error_handling): pretty print unifier exceptions

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-25 09:41:25 -07:00
parent 18a883ab1b
commit 6db6048bf8
4 changed files with 15 additions and 42 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/elaborator.cpp
View file

@ -159,7 +159,7 @@ public:
auto ss = unify_simple(m_subst, c); auto ss = unify_simple(m_subst, c);
m_subst = ss.second; m_subst = ss.second;
if (ss.first == unify_status::Failed) if (ss.first == unify_status::Failed)
throw unifier_exception(c.get_justification()); throw unifier_exception(c.get_justification(), m_subst);
} }
/** /**

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

@ -11,10 +11,8 @@ Author: Leonardo de Moura
#include "kernel/kernel_exception.h" #include "kernel/kernel_exception.h"
#include "kernel/for_each_fn.h" #include "kernel/for_each_fn.h"
#include "library/io_state_stream.h" #include "library/io_state_stream.h"
// #include "library/elaborator/elaborator_justification.h" #include "library/unifier.h"
// #include "library/elaborator/elaborator_exception.h"
#include "library/parser_nested_exception.h" #include "library/parser_nested_exception.h"
// #include "library/unsolved_metavar_exception.h"
namespace lean { namespace lean {
void display_error_pos(io_state_stream 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) {
@ -51,13 +49,12 @@ static void display_error(io_state_stream const & ios, pos_info_provider const *
ios << " " << ex << endl; ios << " " << ex << endl;
} }
// static void display_error(io_state_stream 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, unifier_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); ios << mk_pair(j.pp(fmt, opts, p, ex.get_substitution()), 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 {
// unsigned m_delta; // unsigned m_delta;
@ -132,37 +129,11 @@ static void display_error(io_state_stream const & ios, pos_info_provider const *
// ios << ex.what() << endl; // ios << ex.what() << endl;
// } // }
// 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)));
// ios << " " << ex.what() << mk_pair(r, opts) << endl;
// if (p) {
// name_set already_displayed;
// for_each(ex.get_expr(), [&](expr const & e, unsigned) -> bool {
// if (is_metavar(e)) {
// 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++) ios << " ";
// display_error_pos(ios, p, e);
// ios << " unsolved metavar " << m << endl;
// }
// }
// return true;
// });
// }
// }
void display_error(io_state_stream 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<unifier_exception const *>(&ex)) {
// display_error(ios, p, *e_ex); display_error(ios, p, *e_ex);
// } else if (auto m_ex = dynamic_cast<unsolved_metavar_exception const *>(&ex)) {
// display_error(ios, p, *m_ex);
} else if (auto ls_ex = dynamic_cast<script_nested_exception const *>(&ex)) { } else if (auto ls_ex = dynamic_cast<script_nested_exception const *>(&ex)) {
display_error(ios, p, *ls_ex); display_error(ios, p, *ls_ex);
} else if (auto s_ex = dynamic_cast<script_exception const *>(&ex)) { } else if (auto s_ex = dynamic_cast<script_exception const *>(&ex)) {

2
src/library/unifier.cpp
View file

@ -708,7 +708,7 @@ struct unifier_fn {
optional<substitution> failure() { optional<substitution> failure() {
lean_assert(in_conflict()); lean_assert(in_conflict());
if (m_use_exception) if (m_use_exception)
throw unifier_exception(*m_conflict); throw unifier_exception(*m_conflict, m_subst);
else else
return optional<substitution>(); return optional<substitution>();
} }

6
src/library/unifier.h
View file

@ -60,11 +60,13 @@ lazy_list<substitution> unify(environment const & env, expr const & lhs, expr co
class unifier_exception : public exception { class unifier_exception : public exception {
justification m_jst; justification m_jst;
substitution m_subst;
public: public:
unifier_exception(justification const & j):exception("unifier exception"), m_jst(j) {} unifier_exception(justification const & j, substitution const & s):exception("unifier exception"), m_jst(j), m_subst(s) {}
virtual exception * clone() const { return new unifier_exception(m_jst); } virtual exception * clone() const { return new unifier_exception(m_jst, m_subst); }
virtual void rethrow() const { throw *this; } virtual void rethrow() const { throw *this; }
justification const & get_justification() const { return m_jst; } justification const & get_justification() const { return m_jst; }
substitution const & get_substitution() const { return m_subst; }
}; };
void open_unifier(lua_State * L); void open_unifier(lua_State * L);