From dc0e7a4472c30f40efa352fded45ff960c02951e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 14 Oct 2013 14:37:35 -0700 Subject: [PATCH] feat(pos_info_provider): add position information provider for expressions Signed-off-by: Leonardo de Moura --- src/kernel/CMakeLists.txt | 2 +- src/kernel/pos_info_provider.cpp | 18 ++++++++++++++++ src/kernel/pos_info_provider.h | 31 +++++++++++++++++++++++++++ src/kernel/trace.h | 8 +++++-- src/kernel/type_checker_trace.cpp | 22 +++++++++++++++---- src/kernel/type_checker_trace.h | 8 +++---- src/kernel/unification_constraint.cpp | 20 ++++++++--------- src/kernel/unification_constraint.h | 14 ++++++------ src/library/elaborator/elaborator.cpp | 2 +- src/tests/kernel/metavar.cpp | 2 +- src/util/sexpr/format.h | 2 ++ src/util/sexpr/sexpr.h | 2 ++ 12 files changed, 101 insertions(+), 30 deletions(-) create mode 100644 src/kernel/pos_info_provider.cpp create mode 100644 src/kernel/pos_info_provider.h diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index 36ca3fc83..4389df644 100644 --- a/src/kernel/CMakeLists.txt +++ b/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}) diff --git a/src/kernel/pos_info_provider.cpp b/src/kernel/pos_info_provider.cpp new file mode 100644 index 000000000..9ad8c79f8 --- /dev/null +++ b/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(); + } +} +} diff --git a/src/kernel/pos_info_provider.h b/src/kernel/pos_info_provider.h new file mode 100644 index 000000000..b9a3c38c3 --- /dev/null +++ b/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 +#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 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; +}; +} diff --git a/src/kernel/trace.h b/src/kernel/trace.h index 49fda4d04..1d706c780 100644 --- a/src/kernel/trace.h +++ b/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 & 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 & r) const { if (m_ptr) m_ptr->get_children(r); } bool has_children() const; diff --git a/src/kernel/type_checker_trace.cpp b/src/kernel/type_checker_trace.cpp index 6223980c4..c4e88a88c 100644 --- a/src/kernel/type_checker_trace.cpp +++ b/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."); diff --git a/src/kernel/type_checker_trace.h b/src/kernel/type_checker_trace.h index aeab22a2d..e492da23b 100644 --- a/src/kernel/type_checker_trace.h +++ b/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 &) 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 &) 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 &) 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 &) const; virtual expr const & get_main_expr() const; context const & get_context() const { return m_ctx; } diff --git a/src/kernel/unification_constraint.cpp b/src/kernel/unification_constraint.cpp index 3ab972297..ef3f0301c 100644 --- a/src/kernel/unification_constraint.cpp +++ b/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) { diff --git a/src/kernel/unification_constraint.h b/src/kernel/unification_constraint.h index af2b62de8..53dfe1fc6 100644 --- a/src/kernel/unification_constraint.h +++ b/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); diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 02f4572af..5e9e26fd9 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/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"; } } diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp index 7ef37ce32..60cd248a3 100644 --- a/src/tests/kernel/metavar.cpp +++ b/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 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; } diff --git a/src/util/sexpr/format.h b/src/util/sexpr/format.h index 1619516bf..2f8b362bc 100644 --- a/src/util/sexpr/format.h +++ b/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); diff --git a/src/util/sexpr/sexpr.h b/src/util/sexpr/sexpr.h index bc304a071..d2cf8b717 100644 --- a/src/util/sexpr/sexpr.h +++ b/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);