Add expr_formatter and expr_locator. Add better error messages. Improve simple printer.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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})

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;
 }
 

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);
 }

src/kernel/environment.cpp

@@ -31,6 +31,29 @@ struct environment::imp {
     // Object management
     std::vector<object*>                 m_objects;
     object_dictionary                    m_object_dictionary;
+    // Expression formatter && locator
+    std::shared_ptr<expr_formatter>      m_formatter;
+    std::shared_ptr<expr_locator>        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<imp> const & parent):
@@ -346,6 +371,24 @@ environment::environment(std::shared_ptr<imp> const & ptr):
 environment::~environment() {
 }
 
+void environment::set_formatter(std::shared_ptr<expr_formatter> 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<expr_locator> 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));
 }

src/kernel/environment.h

@@ -9,6 +9,8 @@ Author: Leonardo de Moura
 #include <memory>
 #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<expr_formatter> const & formatter);
+
+    /** \brief Return expression formatter. */
+    expr_formatter & get_formatter() const;
+
+    /** \brief Set expression locator. */
+    void set_locator(std::shared_ptr<expr_locator> const & locator);
+
+    /** \brief Return expression locator. */
+    expr_locator & get_locator() const;
+
     // =======================================
     // Parent/Child environment management
     /**

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));

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<unsigned, unsigned> 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<expr_formatter> mk_simple_expr_formatter() {
+    return std::shared_ptr<expr_formatter>(new simple_expr_formatter());
+}
+
+std::ostream & operator<<(std::ostream & out, std::pair<expr_formatter &, expr const &> 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;
+}
+}

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 <memory>
+#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<expr_formatter> mk_simple_expr_formatter();
+std::ostream & operator<<(std::ostream & out, std::pair<expr_formatter &, expr const &> const & p);
+}

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<unsigned, unsigned> expr_locator::get_location(expr const & e) const { lean_unreachable(); return mk_pair(0, 0); }
+
+std::shared_ptr<expr_locator> mk_dummy_expr_locator() {
+    return std::shared_ptr<expr_locator>(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());
+}
+}

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 <memory>
+#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<unsigned, unsigned> get_location(expr const & e) const;
+};
+/**
+   \brief Create a expression locator s.t. has_location always return false.
+*/
+std::shared_ptr<expr_locator> 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);
+}

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 <sstream>
 #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;
         }

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;
 }

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;
 }

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);