From 392b347f53d22ed3b3ed8370ac5c3e89fb471b22 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Aug 2013 19:12:23 -0700 Subject: [PATCH] Add expr_formatter and expr_locator. Add better error messages. Improve simple printer. Signed-off-by: Leonardo de Moura --- src/kernel/CMakeLists.txt | 2 +- src/kernel/context.cpp | 20 +++- src/kernel/context.h | 2 + src/kernel/environment.cpp | 43 ++++++++ src/kernel/environment.h | 14 +++ src/kernel/expr.cpp | 39 -------- src/kernel/expr_formatter.cpp | 172 ++++++++++++++++++++++++++++++++ src/kernel/expr_formatter.h | 35 +++++++ src/kernel/expr_locator.cpp | 35 +++++++ src/kernel/expr_locator.h | 35 +++++++ src/kernel/type_check.cpp | 61 ++++++----- src/tests/kernel/type_check.cpp | 15 +++ src/util/sexpr/format.cpp | 4 + src/util/sexpr/format.h | 1 + 14 files changed, 410 insertions(+), 68 deletions(-) create mode 100644 src/kernel/expr_formatter.cpp create mode 100644 src/kernel/expr_formatter.h create mode 100644 src/kernel/expr_locator.cpp create mode 100644 src/kernel/expr_locator.h diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index e65a3c6a8..55f9041a6 100644 --- a/src/kernel/CMakeLists.txt +++ b/src/kernel/CMakeLists.txt @@ -1,5 +1,5 @@ add_library(kernel expr.cpp max_sharing.cpp free_vars.cpp abstract.cpp instantiate.cpp deep_copy.cpp normalize.cpp level.cpp environment.cpp type_check.cpp context.cpp builtin.cpp basic_thms.cpp toplevel.cpp - object.cpp pp.cpp) + object.cpp expr_formatter.cpp expr_locator.cpp pp.cpp) target_link_libraries(kernel ${LEAN_LIBS}) diff --git a/src/kernel/context.cpp b/src/kernel/context.cpp index d472bc1ad..2279e6d5a 100644 --- a/src/kernel/context.cpp +++ b/src/kernel/context.cpp @@ -6,19 +6,29 @@ Author: Leonardo de Moura */ #include "context.h" #include "exception.h" +#include "expr_formatter.h" namespace lean { -std::ostream & operator<<(std::ostream & out, context const & c) { +format pp(expr_formatter & fmt, context const & c) { if (c) { + format r; if (tail(c)) - out << tail(c) << "\n"; + r = format{pp(fmt, tail(c)), line()}; context_entry const & e = head(c); if (e.get_name().is_anonymous()) - out << "_"; + r += format("_"); else - out << e.get_name(); - out << " : " << e.get_type(); + r += format(e.get_name()); + r += format{space(), colon(), space(), fmt(e.get_type(), tail(c))}; + return r; + } else { + return format(); } +} + +std::ostream & operator<<(std::ostream & out, context const & c) { + auto fmt = mk_simple_expr_formatter(); + out << pp(*fmt, c); return out; } diff --git a/src/kernel/context.h b/src/kernel/context.h index a3bb01e26..ca5298ef1 100644 --- a/src/kernel/context.h +++ b/src/kernel/context.h @@ -35,5 +35,7 @@ inline context extend(context const & c, name const & n, expr const & t) { inline bool empty(context const & c) { return is_nil(c); } +class expr_formatter; +format pp(expr_formatter & f, context const & c); std::ostream & operator<<(std::ostream & out, context const & c); } diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 9065ec59c..cd023851c 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -31,6 +31,29 @@ struct environment::imp { // Object management std::vector m_objects; object_dictionary m_object_dictionary; + // Expression formatter && locator + std::shared_ptr m_formatter; + std::shared_ptr m_locator; + + expr_formatter & get_formatter() { + if (m_formatter) { + return *m_formatter; + } else { + // root environments always have a formatter. + lean_assert(has_parent()); + return m_parent->get_formatter(); + } + } + + expr_locator & get_locator() { + if (m_locator) { + return *m_locator; + } else { + // root environments always have a locator. + lean_assert(has_parent()); + return m_parent->get_locator(); + } + } /** \brief Return true iff this environment has children. @@ -316,6 +339,8 @@ struct environment::imp { imp(): m_num_children(0) { init_uvars(); + m_formatter = mk_simple_expr_formatter(); + m_locator = mk_dummy_expr_locator(); } explicit imp(std::shared_ptr const & parent): @@ -346,6 +371,24 @@ environment::environment(std::shared_ptr const & ptr): environment::~environment() { } +void environment::set_formatter(std::shared_ptr const & formatter) { + lean_assert(formatter); + m_imp->m_formatter = formatter; +} + +expr_formatter & environment::get_formatter() const { + return m_imp->get_formatter(); +} + +void environment::set_locator(std::shared_ptr const & locator) { + lean_assert(locator); + m_imp->m_locator = locator; +} + +expr_locator & environment::get_locator() const { + return m_imp->get_locator(); +} + environment environment::mk_child() const { return environment(new imp(m_imp)); } diff --git a/src/kernel/environment.h b/src/kernel/environment.h index ed51d9e54..f73228ded 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -9,6 +9,8 @@ Author: Leonardo de Moura #include #include "object.h" #include "level.h" +#include "expr_formatter.h" +#include "expr_locator.h" namespace lean { /** @@ -28,6 +30,18 @@ public: environment(); ~environment(); + /** \brief Set expression formatter. */ + void set_formatter(std::shared_ptr const & formatter); + + /** \brief Return expression formatter. */ + expr_formatter & get_formatter() const; + + /** \brief Set expression locator. */ + void set_locator(std::shared_ptr const & locator); + + /** \brief Return expression locator. */ + expr_locator & get_locator() const; + // ======================================= // Parent/Child environment management /** diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index caced6aca..777407977 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -188,45 +188,6 @@ bool is_arrow(expr const & t) { return is_pi(t) && !has_free_var(abst_body(t), 0); } -// Low-level pretty printer -std::ostream & operator<<(std::ostream & out, expr const & a) { - switch (a.kind()) { - case expr_kind::Var: out << "#" << var_idx(a); break; - case expr_kind::Constant: out << const_name(a); break; - case expr_kind::App: - out << "("; - for (unsigned i = 0; i < num_args(a); i++) { - if (i > 0) out << " "; - out << arg(a, i); - } - out << ")"; - break; - case expr_kind::Eq: out << "(" << eq_lhs(a) << " = " << eq_rhs(a) << ")"; break; - case expr_kind::Lambda: out << "(fun " << abst_name(a) << " : " << abst_domain(a) << " => " << abst_body(a) << ")"; break; - case expr_kind::Pi: - if (!is_arrow(a)) { - out << "(pi " << abst_name(a) << " : " << abst_domain(a) << ", " << abst_body(a) << ")"; - } else if (!is_arrow(abst_domain(a))) { - out << abst_domain(a) << " -> " << abst_body(a); - } else { - out << "(" << abst_domain(a) << ") -> " << abst_body(a); - } - break; - case expr_kind::Let: out << "(let " << let_name(a) << " := " << let_value(a) << " in " << let_body(a) << ")"; break; - case expr_kind::Type: { - level const & l = ty_level(a); - if (l == level()) { - out << "Type"; - } else { - out << "(Type " << ty_level(a) << ")"; - } - break; - } - case expr_kind::Value: to_value(a).display(out); break; - } - return out; -} - expr copy(expr const & a) { switch (a.kind()) { case expr_kind::Var: return mk_var(var_idx(a)); diff --git a/src/kernel/expr_formatter.cpp b/src/kernel/expr_formatter.cpp new file mode 100644 index 000000000..70c72b973 --- /dev/null +++ b/src/kernel/expr_formatter.cpp @@ -0,0 +1,172 @@ +/* +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 "expr_formatter.h" +#include "exception.h" + +namespace lean { +void expr_formatter::pp(std::ostream & out, expr const & e, context const & c) { + out << mk_pair(operator()(e, c), get_options()); +} + +void expr_formatter::pp(std::ostream & out, expr const & e) { + pp(out, e, context()); +} + +format expr_formatter::nest(format const & f) { + return ::lean::nest(get_pp_indent(get_options()), f); +} + +bool is_atomic(expr const & e) { + switch (e.kind()) { + case expr_kind::Var: case expr_kind::Constant: case expr_kind::Value: case expr_kind::Type: + return true; + case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Eq: case expr_kind::Let: + return false; + } + return false; +} + +class simple_expr_formatter : public expr_formatter { + static thread_local std::ostream * m_out; + + std::ostream & out() { return *m_out; } + + void print_child(expr const & a, context const & c) { + if (is_atomic(a)) { + print(a, c); + } else { + out() << "("; + print(a, c); + out() << ")"; + } + } + + void print_value(expr const & a) { + to_value(a).display(out()); + } + + void print_type(expr const & a) { + if (a == Type()) { + out() << "Type"; + } else { + out() << "Type " << ty_level(a); + } + } + + void print_eq(expr const & a, context const & c) { + print_child(eq_lhs(a), c); + out() << " = "; + print_child(eq_rhs(a), c); + } + + void print_app(expr const & a, context const & c) { + print_child(arg(a, 0), c); + for (unsigned i = 1; i < num_args(a); i++) { + out() << " "; + print_child(arg(a, i), c); + } + } + + void print_arrow_body(expr const & a, context const & c) { + if (is_atomic(a) || is_arrow(a)) + return print(a, c); + else + return print_child(a, c); + } + + void print(expr const & a, context const & c) { + switch (a.kind()) { + case expr_kind::Var: + try { + context const & c1 = lookup(c, var_idx(a)); + out() << head(c1).get_name(); + } catch (exception & ex) { + out() << "#" << var_idx(a); + } + break; + case expr_kind::Constant: + out() << const_name(a); + break; + case expr_kind::App: + print_app(a, c); + break; + case expr_kind::Eq: + print_eq(a, c); + break; + case expr_kind::Lambda: + out() << "fun " << abst_name(a) << " : "; + print_child(abst_domain(a), c); + out() << ", "; + print_child(abst_body(a), extend(c, abst_name(a), abst_domain(a))); + break; + case expr_kind::Pi: + if (!is_arrow(a)) { + out() << "Pi " << abst_name(a) << " : "; + print_child(abst_domain(a), c); + out() << ", "; + print_child(abst_body(a), extend(c, abst_name(a), abst_domain(a))); + break; + } else { + print_child(abst_domain(a), c); + out() << " -> "; + print_arrow_body(abst_body(a), extend(c, abst_name(a), abst_domain(a))); + } + break; + case expr_kind::Let: + out() << "let " << let_name(a) << " := "; + print_child(let_value(a), c); + out() << " in "; + print_child(let_body(a), extend(c, let_name(a), let_value(a))); + break; + case expr_kind::Type: + print_type(a); + break; + case expr_kind::Value: + print_value(a); + break; + } + } + +public: + virtual ~simple_expr_formatter() {} + + virtual format operator()(expr const & e, context const & c) { + std::ostringstream s; + m_out = &s; + print(e, c); + return format(s.str()); + } + + virtual bool has_location(expr const & e) const { return false; } + + virtual std::pair get_location(expr const & e) const { return mk_pair(0,0); } + + virtual options get_options() const { return options(); } + + void print(std::ostream & out, expr const & a, context const & c) { + m_out = &out; + print(a, c); + } +}; +thread_local std::ostream * simple_expr_formatter::m_out = 0; + +std::shared_ptr mk_simple_expr_formatter() { + return std::shared_ptr(new simple_expr_formatter()); +} + +std::ostream & operator<<(std::ostream & out, std::pair const & p) { + p.first.pp(out, p.second); + return out; +} + +static simple_expr_formatter g_simple_formatter; + +std::ostream & operator<<(std::ostream & out, expr const & a) { + g_simple_formatter.print(out, a, context()); + return out; +} +} diff --git a/src/kernel/expr_formatter.h b/src/kernel/expr_formatter.h new file mode 100644 index 000000000..e5188bd9b --- /dev/null +++ b/src/kernel/expr_formatter.h @@ -0,0 +1,35 @@ +/* +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 +#include "context.h" +#include "options.h" + +namespace lean { +/** \brief Abstract class for formatting expressions. */ +class expr_formatter { +public: + virtual ~expr_formatter() {} + /** \brief Convert expression in the given context into a format object. */ + virtual format operator()(expr const & e, context const & c) = 0; + /** \brief Return options for pretty printing. */ + virtual options get_options() const = 0; + + void pp(std::ostream & out, expr const & e, context const & c); + void pp(std::ostream & out, expr const & e); + + /** \brief Nest the given format object using the setting provided by get_options. */ + format nest(format const & f); +}; + +/** + \brief Create simple expression formatter. + It is mainly useful for pretty printing. +*/ +std::shared_ptr mk_simple_expr_formatter(); +std::ostream & operator<<(std::ostream & out, std::pair const & p); +} diff --git a/src/kernel/expr_locator.cpp b/src/kernel/expr_locator.cpp new file mode 100644 index 000000000..f611dad47 --- /dev/null +++ b/src/kernel/expr_locator.cpp @@ -0,0 +1,35 @@ +/* +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 "expr_locator.h" +#include "exception.h" + +namespace lean { +expr_locator::~expr_locator() {} +bool expr_locator::has_location(expr const & e) const { return false; } +std::pair expr_locator::get_location(expr const & e) const { lean_unreachable(); return mk_pair(0, 0); } + +std::shared_ptr mk_dummy_expr_locator() { + return std::shared_ptr(new expr_locator()); +} + +void throw_exception(expr_locator const & loc, expr const & src, char const * msg) { + if (loc.has_location(src)) { + std::ostringstream s; + auto p = loc.get_location(src); + s << "(line: " << p.first << ", pos: " << p.second << ") " << msg; + throw exception(s.str()); + } else { + throw exception(msg); + } +} + +void throw_exception(expr_locator const & loc, expr const & src, format const & msg) { + std::ostringstream s; + s << msg; + throw_exception(loc, src, s.str().c_str()); +} +} diff --git a/src/kernel/expr_locator.h b/src/kernel/expr_locator.h new file mode 100644 index 000000000..c0fc0b778 --- /dev/null +++ b/src/kernel/expr_locator.h @@ -0,0 +1,35 @@ +/* +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 +#include "expr.h" + +namespace lean { +/** + \brief Abstract class that specifies the API to retrieve + expression location (line and position). +*/ +class expr_locator { +public: + virtual ~expr_locator(); + /** \brief Return true iff the expression has location information associated with it. */ + virtual bool has_location(expr const & e) const; + /** \brief Return location (line, pos) associated with expression. \pre has_location() */ + virtual std::pair get_location(expr const & e) const; +}; +/** + \brief Create a expression locator s.t. has_location always return false. +*/ +std::shared_ptr mk_dummy_expr_locator(); + +/** + \brief Throw an exception with the given msg, and include location + of the given expression (if available). +*/ +void throw_exception(expr_locator const & loc, expr const & src, char const * msg); +void throw_exception(expr_locator const & loc, expr const & src, format const & msg); +} diff --git a/src/kernel/type_check.cpp b/src/kernel/type_check.cpp index 2d62a25e2..01115b9a2 100644 --- a/src/kernel/type_check.cpp +++ b/src/kernel/type_check.cpp @@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include #include "type_check.h" #include "scoped_map.h" +#include "environment.h" #include "normalize.h" #include "instantiate.h" #include "builtin.h" @@ -56,6 +56,20 @@ struct infer_type_fn { return lift_free_vars(head(def_c).get_type(), length(c) - (length(def_c) - 1)); } + expr_formatter & fmt() { return m_env.get_formatter(); } + + format nl_indent(format const & f) { return fmt().nest(format{line(), f}); } + + void throw_exception(expr const & src, format const & msg) { + ::lean::throw_exception(m_env.get_locator(), src, msg); + } + + /** \brief Include context (if not empty) in the formatted message */ + void push_context(format & msg, context const & ctx) { + if (!empty(ctx)) + msg += format{format("in context: "), nl_indent(pp(fmt(), ctx)), line()}; + } + level infer_universe(expr const & t, context const & ctx) { lean_trace("type_check", tout << "infer universe\n" << t << "\n";); expr u = normalize(infer_type(t, ctx), m_env, ctx); @@ -63,30 +77,30 @@ struct infer_type_fn { return ty_level(u); if (u == Bool) return level(); - std::ostringstream buffer; - buffer << "type expected, "; - if (!empty(ctx)) - buffer << "in context:\n" << ctx << "\n"; - buffer << "got:\n" << t; - throw exception(buffer.str()); + format msg = format("type expected, "); + push_context(msg, ctx); + msg += format{format("got:"), nl_indent(fmt()(t, ctx))}; + throw_exception(t, msg); + lean_unreachable(); + return level(); } - expr check_pi(expr const & e, context const & ctx) { + expr check_pi(expr const & e, expr const & s, context const & ctx) { if (is_pi(e)) return e; expr r = normalize(e, m_env, ctx); if (is_pi(r)) return r; - std::ostringstream buffer; - buffer << "function expected, "; - if (!empty(ctx)) - buffer << "in context:\n" << ctx << "\n"; - buffer << "got:\n" << e; - throw exception(buffer.str()); + format msg = format("function expected, "); + push_context(msg, ctx); + msg += format{format("got:"), nl_indent(fmt()(s, ctx))}; + throw_exception(s, msg); + lean_unreachable(); + return expr(); } expr infer_pi(expr const & e, context const & ctx) { - return check_pi(infer_type(e, ctx), ctx); + return check_pi(infer_type(e, ctx), e, ctx); } expr infer_type(expr const & e, context const & ctx) { @@ -120,13 +134,14 @@ struct infer_type_fn { expr const & c = arg(e, i); expr c_t = infer_type(c, ctx); if (!is_convertible(abst_domain(f_t), c_t, m_env, ctx)) { - std::ostringstream buffer; - buffer << "type mismatch at argument " << i << " of\n" << e - << "\nexpected type:\n" << abst_domain(f_t) - << "\ngiven type:\n" << c_t; - if (!empty(ctx)) - buffer << "\nin context:\n" << ctx; - throw exception(buffer.str()); + format msg = format{format("type mismatch at argument "), format(i), format("of"), + nl_indent(fmt()(e, ctx)), line(), + format("expected type:"), + nl_indent(fmt()(abst_domain(f_t), ctx)), line(), + format("given type:"), + nl_indent(fmt()(c_t, ctx))}; + push_context(msg, ctx); + throw_exception(arg(e,i), msg); } if (closed(abst_body(f_t))) f_t = abst_body(f_t); @@ -139,7 +154,7 @@ struct infer_type_fn { r = f_t; break; } - check_pi(f_t, ctx); + check_pi(f_t, e, ctx); } break; } diff --git a/src/tests/kernel/type_check.cpp b/src/tests/kernel/type_check.cpp index 18534baa3..fd9dc5b01 100644 --- a/src/tests/kernel/type_check.cpp +++ b/src/tests/kernel/type_check.cpp @@ -101,6 +101,20 @@ static void tst5() { lean_assert(Implies(P, prop) == prop2); } +static void tst6() { + environment env = mk_toplevel(); + expr A = Const("A"); + expr f = Const("f"); + expr x = Const("x"); + expr t = Fun({A, Type()}, Fun({f, arrow(Int, A)}, Fun({x, Int}, f(x, x)))); + try { + infer_type(t, env); + lean_unreachable(); + } catch (exception & ex) { + std::cout << "Error: " << ex.what() << "\n"; + } +} + int main() { continue_on_violation(true); tst1(); @@ -108,5 +122,6 @@ int main() { tst3(); tst4(); tst5(); + tst6(); return has_violations() ? 1 : 0; } diff --git a/src/util/sexpr/format.cpp b/src/util/sexpr/format.cpp index 966898b24..d0ddd8c23 100644 --- a/src/util/sexpr/format.cpp +++ b/src/util/sexpr/format.cpp @@ -108,6 +108,7 @@ static format g_space(" "); static format g_lp("("); static format g_rp(")"); static format g_comma(","); +static format g_colon(":"); static format g_dot("."); format const & line() { return g_line; @@ -124,6 +125,9 @@ format const & rp() { format const & comma() { return g_comma; } +format const & colon() { + return g_colon; +} format const & dot() { return g_dot; } diff --git a/src/util/sexpr/format.h b/src/util/sexpr/format.h index 6ec48f97f..2f3b3005d 100644 --- a/src/util/sexpr/format.h +++ b/src/util/sexpr/format.h @@ -219,6 +219,7 @@ format const & space(); format const & lp(); format const & rp(); format const & comma(); +format const & colon(); format const & dot(); format group(format const & f); format above(format const & f1, format const & f2);