diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index bd229b466..c7c627631 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -885,10 +885,11 @@ public: /** \brief Store the pair (pos(e), type(r)) in the flyinfo_data if m_flyinfo is true. */ void save_flyinfo_data(expr const & e, expr const & r) { if (m_flyinfo && m_pos_provider) { - auto p = m_pos_provider->get_pos_info(e); - type_checker::scope scope(*m_tc[m_relax_main_opaque]); - expr t = m_tc[m_relax_main_opaque]->infer(r); - m_flyinfo_data.push_back(mk_pair(p, t)); + if (auto p = m_pos_provider->get_pos_info(e)) { + type_checker::scope scope(*m_tc[m_relax_main_opaque]); + expr t = m_tc[m_relax_main_opaque]->infer(r); + m_flyinfo_data.push_back(mk_pair(*p, t)); + } } } diff --git a/src/frontends/lean/parser_pos_provider.cpp b/src/frontends/lean/parser_pos_provider.cpp index 17b5d2c70..e2060bb0a 100644 --- a/src/frontends/lean/parser_pos_provider.cpp +++ b/src/frontends/lean/parser_pos_provider.cpp @@ -15,19 +15,19 @@ parser_pos_provider::parser_pos_provider(pos_info_table_ptr const & pos_table, parser_pos_provider::~parser_pos_provider() {} -std::pair parser_pos_provider::get_pos_info(expr const & e) const { +optional parser_pos_provider::get_pos_info(expr const & e) const { if (!m_pos_table) - return get_some_pos(); + return optional(); tag t = e.get_tag(); if (t == nulltag) - return get_some_pos(); + return optional(); auto it = m_pos_table->find(t); if (it == m_pos_table->end()) - return get_some_pos(); - return it->second; + return optional(); + return optional(it->second); } -std::pair parser_pos_provider::get_some_pos() const { +pos_info parser_pos_provider::get_some_pos() const { return m_pos; } diff --git a/src/frontends/lean/parser_pos_provider.h b/src/frontends/lean/parser_pos_provider.h index 4924c35cc..95c7ff958 100644 --- a/src/frontends/lean/parser_pos_provider.h +++ b/src/frontends/lean/parser_pos_provider.h @@ -12,7 +12,6 @@ Author: Leonardo de Moura #include "kernel/pos_info_provider.h" namespace lean { -typedef std::pair pos_info; typedef std::unordered_map pos_info_table; typedef std::shared_ptr pos_info_table_ptr; @@ -23,8 +22,8 @@ class parser_pos_provider : public pos_info_provider { public: parser_pos_provider(pos_info_table_ptr const & pos_table, std::string const & strm_name, pos_info const & some_pos); virtual ~parser_pos_provider(); - virtual std::pair get_pos_info(expr const & e) const; - virtual std::pair get_some_pos() const; + virtual optional get_pos_info(expr const & e) const; + virtual pos_info get_some_pos() const; virtual char const * get_file_name() const; }; } diff --git a/src/kernel/pos_info_provider.cpp b/src/kernel/pos_info_provider.cpp index 518d3d766..03be0886f 100644 --- a/src/kernel/pos_info_provider.cpp +++ b/src/kernel/pos_info_provider.cpp @@ -12,7 +12,7 @@ char const * pos_info_provider::get_file_name() const { } format pos_info_provider::pp(expr const & e) const { try { - auto p = get_pos_info(e); + auto p = get_pos_info_or_some(e); return format{format(get_file_name()), colon(), format(p.first), colon(), format(p.second), colon()}; } catch (exception &) { return format(); diff --git a/src/kernel/pos_info_provider.h b/src/kernel/pos_info_provider.h index 5b751bfb5..e273ed193 100644 --- a/src/kernel/pos_info_provider.h +++ b/src/kernel/pos_info_provider.h @@ -1,5 +1,5 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include "kernel/expr.h" namespace lean { +typedef std::pair pos_info; //!< Line and column information /** \brief Abstract class for providing expression position information (line number and column). */ @@ -18,14 +19,18 @@ 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. + Return none if the information is not available */ - virtual std::pair get_pos_info(expr const & e) const = 0; + virtual optional get_pos_info(expr const & e) const = 0; virtual char const * get_file_name() const; - virtual std::pair get_some_pos() const = 0; + virtual pos_info get_some_pos() const = 0; + pos_info get_pos_info_or_some(expr const & e) const { + if (auto it = get_pos_info(e)) + return *it; + else + return get_some_pos(); + } - 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. diff --git a/src/library/error_handling/error_handling.cpp b/src/library/error_handling/error_handling.cpp index cb6ae9432..466433581 100644 --- a/src/library/error_handling/error_handling.cpp +++ b/src/library/error_handling/error_handling.cpp @@ -43,7 +43,7 @@ void display_error_pos(io_state_stream const & ios, char const * strm_name, unsi void display_error_pos(io_state_stream const & ios, pos_info_provider const * p, expr const & e) { if (p) { - auto pos = p->get_pos_info(e); + auto pos = p->get_pos_info_or_some(e); display_error_pos(ios, p->get_file_name(), pos.first, pos.second); } else { ios << "error:"; diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index a702f18e4..5152a6606 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -184,9 +184,9 @@ static register_bin_tac reg_orelse(g_or_else_tac_name, [](tactic const & t1, tac static register_unary_tac reg_repeat(g_repeat_tac_name, [](tactic const & t1) { return repeat(t1); }); static register_tac reg_state(name(g_tac, "state"), [](type_checker &, expr const & e, pos_info_provider const * p) { if (p) - return trace_state_tactic(std::string(p->get_file_name()), p->get_pos_info(e)); - else - return trace_state_tactic(); + if (auto it = p->get_pos_info(e)) + return trace_state_tactic(std::string(p->get_file_name()), *it); + return trace_state_tactic(); }); static register_tac reg_trace(name(g_tac, "trace"), [](type_checker & tc, expr const & e, pos_info_provider const *) { buffer args;