feat(kernel/pos_info_provider): add save_pos_info

Allows the elaborator to contribute new info locations

src/frontends/lean/parser.cpp

@@ -258,7 +258,7 @@ name parser::mk_anonymous_inst_name() {
     return n;
 }
 
-expr parser::save_pos(expr e, pos_info p) {
+expr parser::save_pos(expr const & e, pos_info p) {
     auto t = get_tag(e);
     if (!m_pos_table.contains(t))
         m_pos_table.insert(t, p);

src/frontends/lean/parser.h

@@ -219,7 +219,7 @@ public:
 
     /** \brief Return the current position information */
     virtual pos_info pos() const override final { return pos_info(m_scanner.get_line(), m_scanner.get_pos()); }
-    expr save_pos(expr e, pos_info p);
+    virtual expr save_pos(expr const & e, pos_info p) override final;
     expr rec_save_pos(expr const & e, pos_info p);
     expr rec_save_pos(expr const & e, optional<pos_info> p) { return p ? rec_save_pos(e, *p) : e; }
     expr update_pos(expr e, pos_info p);
@@ -232,7 +232,7 @@ public:
     optional<std::string> get_doc_string() const { return m_doc_string; }
 
     parser_pos_provider get_parser_pos_provider(pos_info const & some_pos) const {
-        return parser_pos_provider(m_pos_table, m_file_name, some_pos);
+        return parser_pos_provider(m_pos_table, m_file_name, some_pos, m_next_tag_idx);
     }
 
     expr mk_app(expr fn, expr arg, pos_info const & p);

src/frontends/lean/parser_pos_provider.cpp

@@ -11,8 +11,8 @@ Author: Leonardo de Moura
 
 namespace lean {
 parser_pos_provider::parser_pos_provider(pos_info_table const & pos_table,
-                                         std::string const & strm_name, pos_info const & some_pos):
-    m_pos_table(pos_table), m_strm_name(strm_name), m_pos(some_pos) {}
+                                         std::string const & strm_name, pos_info const & some_pos, unsigned next_tag_idx):
+    m_pos_table(pos_table), m_strm_name(strm_name), m_pos(some_pos), m_next_tag_idx(next_tag_idx) {}
 
 parser_pos_provider::~parser_pos_provider() {}
 
@@ -33,4 +33,21 @@ pos_info parser_pos_provider::get_some_pos() const {
 char const * parser_pos_provider::get_file_name() const {
     return m_strm_name.c_str();
 }
+
+tag parser_pos_provider::get_tag(expr e) {
+    tag t = e.get_tag();
+    if (t == nulltag) {
+        t = m_next_tag_idx;
+        e.set_tag(t);
+        m_next_tag_idx++;
+    }
+    return t;
+}
+
+expr parser_pos_provider::save_pos(expr const & e, pos_info pos) {
+    auto t = e.get_tag();
+    if (!m_pos_table.contains(t))
+        m_pos_table.insert(t, pos);
+    return e;
+}
 }

src/frontends/lean/parser_pos_provider.h

@@ -21,11 +21,16 @@ class parser_pos_provider : public pos_info_provider {
     pos_info_table m_pos_table;
     std::string    m_strm_name;
     pos_info       m_pos;
+    unsigned       m_next_tag_idx;
+
+    tag get_tag(expr e);
 public:
-    parser_pos_provider(pos_info_table const & pos_table, std::string const & strm_name, pos_info const & some_pos);
+    parser_pos_provider(pos_info_table const & pos_table, std::string const & strm_name, pos_info const & some_pos,
+                        unsigned next_tag_idx);
     virtual ~parser_pos_provider();
     virtual optional<pos_info> get_pos_info(expr const & e) const;
     virtual pos_info get_some_pos() const;
+    expr save_pos(expr const & e, pos_info pos) override;
     virtual char const * get_file_name() const;
 };
 }

src/kernel/pos_info_provider.h

@@ -31,6 +31,10 @@ public:
             return get_some_pos();
     }
 
+    virtual expr save_pos(expr const &, pos_info) {
+        lean_unreachable();
+    }
+
     /**
        \brief Pretty print position information for the given expression.
        Return a null format object if expression is not associated with position information.