feat(library/declaration_index): add 'a|abbreviation-name|declaration-name' entries in .ilean files

src/frontends/lean/builtin_cmds.cpp

@@ -184,7 +184,7 @@ static void check_identifier(parser & p, environment const & env, name const & n
 }
 
 // add id as an abbreviation for d
-static environment add_abbrev(environment const & env, name const & id, name const & d) {
+static environment add_abbrev(parser & p, environment const & env, name const & id, name const & d) {
     declaration decl = env.get(d);
     buffer<level> ls;
     for (name const & l : decl.get_univ_params())
@@ -193,6 +193,7 @@ static environment add_abbrev(environment const & env, name const & id, name con
     bool opaque = false;
     name const & ns = get_namespace(env);
     name full_id    = ns + id;
+    p.add_abbrev_index(full_id, d);
     environment new_env = module::add(env, check(env, mk_definition(env, full_id, decl.get_univ_params(), decl.get_type(), value, opaque)));
     if (full_id != id)
         new_env = add_expr_alias_rec(new_env, id, full_id);
@@ -238,7 +239,7 @@ environment open_export_cmd(parser & p, bool open) {
                         if (open)
                             env = add_expr_alias(env, as+to_id, ns+from_id);
                         else
-                            env = add_abbrev(env, as+to_id, ns+from_id);
+                            env = add_abbrev(p, env, as+to_id, ns+from_id);
                     }
                 } else if (p.curr_is_token_or_id(g_hiding)) {
                     p.next();
@@ -257,7 +258,7 @@ environment open_export_cmd(parser & p, bool open) {
                         if (open)
                             env = add_expr_alias(env, as+id, ns+id);
                         else
-                            env = add_abbrev(env, as+id, ns+id);
+                            env = add_abbrev(p, env, as+id, ns+id);
                     }
                 } else {
                     throw parser_error("invalid 'open/export' command option, identifier, 'hiding' or 'renaming' expected", p.pos());
@@ -277,7 +278,7 @@ environment open_export_cmd(parser & p, bool open) {
                                 !is_exception(d.get_name(), ns, exceptions.size(), exceptions.data())) {
                                 name new_id = d.get_name().replace_prefix(ns, as);
                                 if (!new_id.is_anonymous())
-                                    new_env = add_abbrev(new_env, new_id, d.get_name());
+                                    new_env = add_abbrev(p, new_env, new_id, d.get_name());
                             }
                         });
                     env = new_env;

src/frontends/lean/parser.cpp

@@ -132,6 +132,11 @@ void parser::add_ref_index(name const & n, pos_info const & pos) {
         m_index->add_ref(get_stream_name(), pos, n);
 }
 
+void parser::add_abbrev_index(name const & a, name const & d) {
+    if (m_index)
+        m_index->add_abbrev(a, d);
+}
+
 bool parser::are_info_lines_valid(unsigned start_line, unsigned end_line) const {
     if (!m_info_manager)
         return true; // we are not tracking info

src/frontends/lean/parser.h

@@ -198,6 +198,7 @@ public:
     void set_index(declaration_index * i) { m_index = i; }
     void add_decl_index(name const & n, pos_info const & pos, name const & k, expr const & t);
     void add_ref_index(name const & n, pos_info const & pos);
+    void add_abbrev_index(name const & a, name const & d);
 
     environment const & env() const { return m_env; }
     io_state const & ios() const { return m_ios; }

src/library/declaration_index.cpp

@@ -11,6 +11,9 @@ namespace lean {
 void declaration_index::add_decl(std::string const fname, pos_info const & p, name const & n, name const & k, expr const & t) {
     m_decls.insert(n, decl(fname, p, k, t));
 }
+void declaration_index::add_abbrev(name const & n, name const & d) {
+    m_abbrevs.emplace_back(n, d);
+}
 void declaration_index::add_ref(std::string const fname, pos_info const & p, name const & n) {
     m_refs.emplace_back(fname, p, n);
 }
@@ -24,6 +27,9 @@ void declaration_index::save(io_state_stream const & out) const {
             out.get_stream() << mk_pair(flatten(out.get_formatter()(t)), opts);
             out << endl;
         });
+    for (auto const & a : m_abbrevs) {
+        out << "a" << "|" << a.first << "|" << a.second << endl;
+    }
     for (auto const & r : m_refs) {
         std::tie(fname, p, n) = r;
         out << "r" << "|" << fname << "|" << p.first << "|" << p.second << "|" << n << endl;

src/library/declaration_index.h

@@ -20,10 +20,13 @@ namespace lean {
 class declaration_index {
     typedef std::tuple<std::string, pos_info, name, expr> decl;
     typedef std::tuple<std::string, pos_info, name> ref;
+    typedef pair<name, name> abbrev;
     name_map<decl>      m_decls;
+    std::vector<abbrev> m_abbrevs;
     std::vector<ref>    m_refs;
 public:
     void add_decl(std::string const fname, pos_info const & p, name const & n, name const & k, expr const & t);
+    void add_abbrev(name const & n, name const & d);
     void add_ref(std::string const fname, pos_info const & p, name const & n);
     void save(io_state_stream const & out) const;
 };