refactor(kernel/pos_info_provider): get_pos_info return none if position is not available

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

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);
+            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));
+                m_flyinfo_data.push_back(mk_pair(*p, t));
+            }
         }
     }
 

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<unsigned, unsigned> parser_pos_provider::get_pos_info(expr const & e) const {
+optional<pos_info> parser_pos_provider::get_pos_info(expr const & e) const {
     if (!m_pos_table)
-        return get_some_pos();
+        return optional<pos_info>();
     tag t = e.get_tag();
     if (t == nulltag)
-        return get_some_pos();
+        return optional<pos_info>();
     auto it = m_pos_table->find(t);
     if (it == m_pos_table->end())
-        return get_some_pos();
+        return optional<pos_info>();
-    return it->second;
+    return optional<pos_info>(it->second);
 }
 
-std::pair<unsigned, unsigned> parser_pos_provider::get_some_pos() const {
+pos_info parser_pos_provider::get_some_pos() const {
     return m_pos;
 }
 

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<unsigned, unsigned> pos_info;
 typedef std::unordered_map<unsigned, pos_info> pos_info_table;
 typedef std::shared_ptr<pos_info_table> 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<unsigned, unsigned> get_pos_info(expr const & e) const;
+    virtual optional<pos_info> get_pos_info(expr const & e) const;
-    virtual std::pair<unsigned, unsigned> get_some_pos() const;
+    virtual pos_info get_some_pos() const;
     virtual char const * get_file_name() const;
 };
 }

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

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<unsigned, unsigned> 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<unsigned, unsigned> get_pos_info(expr const & e) const = 0;
+    virtual optional<pos_info> get_pos_info(expr const & e) const = 0;
     virtual char const * get_file_name() const;
-    virtual std::pair<unsigned, unsigned> 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.

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:";

src/library/tactic/expr_to_tactic.cpp

@@ -184,8 +184,8 @@ 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));
+            if (auto it = p->get_pos_info(e))
-        else
+                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 *) {