feat(pos_info_provider): add position information provider for expressions

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

src/kernel/CMakeLists.txt

@@ -2,6 +2,6 @@ add_library(kernel expr.cpp free_vars.cpp abstract.cpp instantiate.cpp
   normalizer.cpp context.cpp level.cpp object.cpp environment.cpp
   type_checker.cpp builtin.cpp occurs.cpp metavar.cpp trace.cpp
   unification_constraint.cpp printer.cpp formatter.cpp
-  kernel_exception.cpp type_checker_trace.cpp)
+  kernel_exception.cpp type_checker_trace.cpp pos_info_provider.cpp)
 
 target_link_libraries(kernel ${LEAN_LIBS})

src/kernel/pos_info_provider.cpp

@@ -0,0 +1,18 @@
+/*
+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 "kernel/pos_info_provider.h"
+
+namespace lean {
+format pos_info_provider::pp(expr const & e) const {
+    try {
+        auto p = get_pos_info(e);
+        return paren(format{format("line"), colon(), space(), format(p.first), colon(), space(), format("pos"), colon(), space(), format(p.second)});
+    } catch (exception &) {
+        return format();
+    }
+}
+}

src/kernel/pos_info_provider.h

@@ -0,0 +1,31 @@
+/*
+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 <utility>
+#include "util/sexpr/format.h"
+#include "kernel/expr.h"
+
+namespace lean {
+/**
+   \brief Abstract class for providing expression position information (line number and position).
+*/
+class pos_info_provider {
+public:
+    virtual ~pos_info_provider() {}
+    /**
+       \brief Return the line number and position associated with the given expression.
+       Throws an exception if the given expression does not have this kind of information associated with it.
+    */
+    virtual std::pair<unsigned, unsigned> get_pos_info(expr const & e) const = 0;
+    unsigned get_line(expr const & e) const { return get_pos_info(e).first; }
+    unsigned get_pos(expr const & e) const { return get_pos_info(e).second; }
+    /**
+       \brief Pretty print position information for the given expression.
+       Return a null format object if expression is not associated with position information.
+    */
+    virtual format pp(expr const & e) const;
+};
+}

src/kernel/trace.h

@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "util/sexpr/format.h"
 #include "kernel/expr.h"
 #include "kernel/formatter.h"
+#include "kernel/pos_info_provider.h"
 
 namespace lean {
 class trace;
@@ -27,7 +28,7 @@ class trace_cell {
 public:
     trace_cell():m_rc(0) {}
     virtual ~trace_cell() {}
-    virtual format pp(formatter const & fmt, options const & opts) const = 0;
+    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const = 0;
     virtual void get_children(buffer<trace_cell*> & r) const = 0;
     virtual expr const & get_main_expr() const { return expr::null(); }
     bool is_shared() const { return get_rc() > 1; }
@@ -53,7 +54,10 @@ public:
 
     trace & operator=(trace const & s) { LEAN_COPY_REF(trace, s); }
     trace & operator=(trace && s) { LEAN_MOVE_REF(trace, s); }
-    format pp(formatter const & fmt, options const & opts) const { lean_assert(m_ptr); return m_ptr->pp(fmt, opts); }
+    format pp(formatter const & fmt, options const & opts, pos_info_provider const * p = nullptr, bool display_children = true) const {
+        lean_assert(m_ptr);
+        return m_ptr->pp(fmt, opts, p, display_children);
+    }
     expr const & get_main_expr() const { return m_ptr ? m_ptr->get_main_expr() : expr::null(); }
     void get_children(buffer<trace_cell*> & r) const { if (m_ptr) m_ptr->get_children(r); }
     bool has_children() const;

src/kernel/type_checker_trace.cpp

@@ -8,13 +8,24 @@ Author: Leonardo de Moura
 
 namespace lean {
 
+void add_pos_info(format & r, expr const & e, pos_info_provider const * p) {
+    if (!p)
+        return;
+    format f = p->pp(e);
+    if (!f)
+        return;
+    r += f;
+    r += space();
+}
+
 function_expected_trace_cell::~function_expected_trace_cell() {
 }
 
-format function_expected_trace_cell::pp(formatter const & fmt, options const & opts) const {
+format function_expected_trace_cell::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool) const {
     unsigned indent = get_pp_indent(opts);
     format expr_fmt = fmt(m_ctx, m_app, false, opts);
     format r;
+    add_pos_info(r, get_main_expr(), p);
     r += format("Function expected at");
     r += nest(indent, compose(line(), expr_fmt));
     return r;
@@ -30,9 +41,10 @@ expr const & function_expected_trace_cell::get_main_expr() const {
 app_type_match_trace_cell::~app_type_match_trace_cell() {
 }
 
-format app_type_match_trace_cell::pp(formatter const & fmt, options const & opts) const {
+format app_type_match_trace_cell::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool) const {
     unsigned indent = get_pp_indent(opts);
     format r;
+    add_pos_info(r, get_main_expr(), p);
     r += format("Type of argument ");
     r += format(m_i);
     r += format(" must be convertible to the expected type in the application of");
@@ -58,10 +70,11 @@ expr const & app_type_match_trace_cell::get_main_expr() const {
 type_expected_trace_cell::~type_expected_trace_cell() {
 }
 
-format type_expected_trace_cell::pp(formatter const & fmt, options const & opts) const {
+format type_expected_trace_cell::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool) const {
     unsigned indent = get_pp_indent(opts);
     format expr_fmt = fmt(m_ctx, m_type, false, opts);
     format r;
+    add_pos_info(r, get_main_expr(), p);
     r += format("Type expected at");
     r += nest(indent, compose(line(), expr_fmt));
     return r;
@@ -77,8 +90,9 @@ expr const & type_expected_trace_cell::get_main_expr() const {
 def_type_match_trace_cell::~def_type_match_trace_cell() {
 }
 
-format def_type_match_trace_cell::pp(formatter const &, options const &) const {
+format def_type_match_trace_cell::pp(formatter const &, options const &, pos_info_provider const * p, bool) const {
     format r;
+    add_pos_info(r, get_main_expr(), p);
     r += format("Type of definition '");
     r += format(get_name());
     r += format("' must be convertible to expected type.");

src/kernel/type_checker_trace.h

@@ -27,7 +27,7 @@ class function_expected_trace_cell : public trace_cell {
 public:
     function_expected_trace_cell(context const & c, expr const & app):m_ctx(c), m_app(app) {}
     virtual ~function_expected_trace_cell();
-    virtual format pp(formatter const & fmt, options const & opts) const;
+    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const;
     virtual void get_children(buffer<trace_cell*> &) const;
     virtual expr const & get_main_expr() const;
     context const & get_context() const { return m_ctx; }
@@ -52,7 +52,7 @@ class app_type_match_trace_cell : public trace_cell {
 public:
     app_type_match_trace_cell(context const & c, expr const & a, unsigned i):m_ctx(c), m_app(a), m_i(i) {}
     virtual ~app_type_match_trace_cell();
-    virtual format pp(formatter const & fmt, options const & opts) const;
+    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const;
     virtual void get_children(buffer<trace_cell*> &) const;
     virtual expr const & get_main_expr() const;
     context const & get_context() const { return m_ctx; }
@@ -75,7 +75,7 @@ class type_expected_trace_cell : public trace_cell {
 public:
     type_expected_trace_cell(context const & c, expr const & t):m_ctx(c), m_type(t) {}
     virtual ~type_expected_trace_cell();
-    virtual format pp(formatter const & fmt, options const & opts) const;
+    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const;
     virtual void get_children(buffer<trace_cell*> &) const;
     virtual expr const & get_main_expr() const;
     context const & get_context() const { return m_ctx; }
@@ -112,7 +112,7 @@ class def_type_match_trace_cell : public trace_cell {
 public:
     def_type_match_trace_cell(context const & c, name const & n, expr const & v):m_ctx(c), m_name(n), m_value(v) {}
     virtual ~def_type_match_trace_cell();
-    virtual format pp(formatter const & fmt, options const & opts) const;
+    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const;
     virtual void get_children(buffer<trace_cell*> &) const;
     virtual expr const & get_main_expr() const;
     context const & get_context() const { return m_ctx; }

src/kernel/unification_constraint.cpp

@@ -23,10 +23,10 @@ static format add_context(formatter const & fmt, options const & opts, context c
     return group(format{ctx_fmt, space(), turnstile, line(), body});
 }
 
-static format add_trace(formatter const & fmt, options const & opts, format const & body, trace const & tr, bool include_trace) {
+static format add_trace(formatter const & fmt, options const & opts, format const & body, trace const & tr, pos_info_provider const * p, bool include_trace) {
     if (tr && include_trace) {
         unsigned indent  = get_pp_indent(opts);
-        return format{body, line(), format("Trace:"), nest(indent, compose(line(), tr.pp(fmt, opts)))};
+        return format{body, line(), format("Trace:"), nest(indent, compose(line(), tr.pp(fmt, opts, p)))};
     } else {
         return body;
     }
@@ -52,11 +52,11 @@ unification_constraint_eq::unification_constraint_eq(context const & c, expr con
 unification_constraint_eq::~unification_constraint_eq() {
 }
 
-format unification_constraint_eq::pp(formatter const & fmt, options const & opts, bool include_trace) const {
+format unification_constraint_eq::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const {
     format op   = mk_unification_op(opts);
     format body = mk_binary(fmt, opts, m_ctx, m_lhs, m_rhs, op);
     body = add_context(fmt, opts, m_ctx, body);
-    return add_trace(fmt, opts, body, m_trace, include_trace);
+    return add_trace(fmt, opts, body, m_trace, p, include_trace);
 }
 
 unification_constraint_convertible::unification_constraint_convertible(context const & c, expr const & from, expr const & to, trace const & t):
@@ -68,12 +68,12 @@ unification_constraint_convertible::unification_constraint_convertible(context c
 unification_constraint_convertible::~unification_constraint_convertible() {
 }
 
-format unification_constraint_convertible::pp(formatter const & fmt, options const & opts, bool include_trace) const {
+format unification_constraint_convertible::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const {
     bool unicode = get_pp_unicode(opts);
     format op    = unicode ? format("\u227A") /* ≺ */ : format("<<");
     format body  = mk_binary(fmt, opts, m_ctx, m_from, m_to, op);
     body = add_context(fmt, opts, m_ctx, body);
-    return add_trace(fmt, opts, body, m_trace, include_trace);
+    return add_trace(fmt, opts, body, m_trace, p, include_trace);
 }
 
 unification_constraint_max::unification_constraint_max(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, trace const & t):
@@ -86,14 +86,14 @@ unification_constraint_max::unification_constraint_max(context const & c, expr c
 unification_constraint_max::~unification_constraint_max() {
 }
 
-format unification_constraint_max::pp(formatter const & fmt, options const & opts, bool include_trace) const {
+format unification_constraint_max::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const {
     format op       = mk_unification_op(opts);
     format lhs1_fmt = fmt(m_ctx, m_lhs1, false, opts);
     format lhs2_fmt = fmt(m_ctx, m_lhs2, false, opts);
     format rhs_fmt  = fmt(m_ctx, m_rhs, false, opts);
     format body     = group(format{format("max"), lp(), lhs1_fmt, comma(), nest(4, compose(line(), lhs2_fmt)), space(), op, line(), rhs_fmt});
     body = add_context(fmt, opts, m_ctx, body);
-    return add_trace(fmt, opts, body, m_trace, include_trace);
+    return add_trace(fmt, opts, body, m_trace, p, include_trace);
 }
 
 unification_constraint_choice::unification_constraint_choice(context const & c, expr const & mvar, unsigned num, trace const & t):
@@ -105,7 +105,7 @@ unification_constraint_choice::unification_constraint_choice(context const & c,
 unification_constraint_choice::~unification_constraint_choice() {
 }
 
-format unification_constraint_choice::pp(formatter const & fmt, options const & opts, bool include_trace) const {
+format unification_constraint_choice::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const {
     bool unicode    = get_pp_unicode(opts);
     format m_fmt    = fmt(m_ctx, m_mvar, false, opts);
     format eq_op    = mk_unification_op(opts);
@@ -118,7 +118,7 @@ format unification_constraint_choice::pp(formatter const & fmt, options const &
     }
     body = group(body);
     body = add_context(fmt, opts, m_ctx, body);
-    return add_trace(fmt, opts, body, m_trace, include_trace);
+    return add_trace(fmt, opts, body, m_trace, p, include_trace);
 }
 
 unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, trace const & t) {

src/kernel/unification_constraint.h

@@ -46,7 +46,7 @@ public:
     unification_constraint_kind kind() const { return m_kind; }
     trace const & get_trace() const { return m_trace; }
     context const & get_context() const { return m_ctx; }
-    virtual format pp(formatter const & fmt, options const & opts, bool include_trace = false) const = 0;
+    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const = 0;
 };
 
 class unification_constraint {
@@ -69,9 +69,9 @@ public:
 
     operator bool() const { return m_ptr != nullptr; }
 
-    format pp(formatter const & fmt, options const & opts, bool include_trace = false) const {
+    format pp(formatter const & fmt, options const & opts, pos_info_provider const * p = nullptr, bool include_trace = false) const {
         lean_assert(m_ptr);
-        return m_ptr->pp(fmt, opts, include_trace);
+        return m_ptr->pp(fmt, opts, p, include_trace);
     }
 
     friend unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, trace const & t);
@@ -91,7 +91,7 @@ public:
     virtual ~unification_constraint_eq();
     expr const & get_lhs() const { return m_lhs; }
     expr const & get_rhs() const { return m_rhs; }
-    virtual format pp(formatter const & fmt, options const & opts, bool include_trace = false) const;
+    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const;
 };
 
 /**
@@ -107,7 +107,7 @@ public:
     virtual ~unification_constraint_convertible();
     expr const & get_from() const { return m_from; }
     expr const & get_to() const   { return m_to; }
-    virtual format pp(formatter const & fmt, options const & opts, bool include_trace = false) const;
+    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const;
 };
 
 /**
@@ -123,7 +123,7 @@ public:
     expr const & get_lhs1() const { return m_lhs1; }
     expr const & get_lhs2() const { return m_lhs2; }
     expr const & get_rhs() const  { return m_rhs; }
-    virtual format pp(formatter const & fmt, options const & opts, bool include_trace = false) const;
+    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const;
 };
 
 /**
@@ -142,7 +142,7 @@ public:
     expr const & get_choice(unsigned idx) const { lean_assert(idx < m_num_choices); return m_choices[idx]; }
     expr const * begin_choices() const          { return m_choices; }
     expr const * end_choices() const            { return m_choices + m_num_choices; }
-    virtual format pp(formatter const & fmt, options const & opts, bool include_trace = false) const;
+    virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const;
 };
 
 unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, trace const & t);

src/library/elaborator/elaborator.cpp

@@ -32,7 +32,7 @@ public:
 
         formatter fmt = mk_simple_formatter();
         for (unsigned i = 0; i < num_cnstrs; i++) {
-            std::cout << cnstrs[i].pp(fmt, options(), true) << "\n";
+            std::cout << cnstrs[i].pp(fmt, options(), nullptr, true) << "\n";
         }
     }
 

src/tests/kernel/metavar.cpp

@@ -36,7 +36,7 @@ std::ostream & operator<<(std::ostream & out, substitution const & env) {
 std::ostream & operator<<(std::ostream & out, buffer<unification_constraint> const & uc) {
     formatter fmt = mk_simple_formatter();
     for (auto c : uc) {
-        out << c.pp(fmt, options(), true) << "\n";
+        out << c.pp(fmt, options(), nullptr, true) << "\n";
     }
     return out;
 }

src/util/sexpr/format.h

@@ -185,6 +185,8 @@ public:
     }
     unsigned hash() const { return m_value.hash(); }
 
+    operator bool() const { return m_value; }
+
     friend format compose(format const & f1, format const & f2);
     friend format nest(int i, format const & f);
     friend format highlight(format const & f, format::format_color const c);

src/util/sexpr/sexpr.h

@@ -57,6 +57,8 @@ public:
 
     sexpr_kind kind() const;
 
+    operator bool() const { return m_ptr != nullptr; }
+
     friend bool is_nil(sexpr const & s) { return s.m_ptr == nullptr; }
     friend sexpr const & head(sexpr const & s);
     friend sexpr const & tail(sexpr const & s);