From d3ec5ccac119d8380d30a85b22cb3e6166acd0be Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 4 Sep 2014 07:42:18 -0700
Subject: [PATCH] refactor(library/declaration_index): store declarations in a
 map

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/CMakeLists.txt                |  2 +-
 src/library/declaration_index.cpp | 25 +++++++++++++------------
 src/library/declaration_index.h   |  8 +++++---
 3 files changed, 19 insertions(+), 16 deletions(-)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index cf0b98a3a..196843f9c 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -320,5 +320,5 @@ endif()
 
 add_custom_target(clean-olean
    WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../library
-   COMMAND find . -type f -name '*.olean' -delete && find . -type f -name '*.d' -delete && find . -type f -name '*.clean' -delete && find . -type f -name '*.ilean' -delete
+   COMMAND find . -type f -name '*.olean' -delete && find . -type f -name '*.d' -delete && find . -type f -name '*.clean' -delete && find . -type f -name '*.ilean' -delete && find . -type f -name 'TAGS' -delete
    )
diff --git a/src/library/declaration_index.cpp b/src/library/declaration_index.cpp
index 0760d85fa..3d6452516 100644
--- a/src/library/declaration_index.cpp
+++ b/src/library/declaration_index.cpp
@@ -9,23 +9,24 @@ Author: Leonardo de Moura
 
 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_entries.emplace_back(entry_kind::Declaration, fname, p, n, k, t);
+    m_decls.insert(n, decl(fname, p, k, t));
 }
 void declaration_index::add_ref(std::string const fname, pos_info const & p, name const & n) {
-    m_entries.emplace_back(entry_kind::Reference, fname, p, n, name(), expr());
+    m_refs.emplace_back(fname, p, n);
 }
 void declaration_index::save(io_state_stream const & out) const {
-    entry_kind k; std::string fname; pos_info p; name n, dk; expr t;
-    for (auto const & e : m_entries) {
-        std::tie(k, fname, p, n, dk, t) = e;
-        out << (k == entry_kind::Declaration ? "d" : "r") << "|" << fname << "|" << p.first
-            << "|" << p.second << "|" << n;
-        if (k == entry_kind::Declaration) {
-            out << "|" << dk << "|";
-            options const & opts = out.get_options();
+    std::string fname; pos_info p; name n, k; expr t;
+    options const & opts = out.get_options();
+    m_decls.for_each([&](name const & n, decl const & d) {
+            std::tie(fname, p, k, t) = d;
+            out << "d" << "|" << fname << "|" << p.first << "|" << p.second << "|" << n;
+            out << "|" << k << "|";
             out.get_stream() << mk_pair(flatten(out.get_formatter()(t)), opts);
-        }
-        out << endl;
+            out << endl;
+        });
+    for (auto const & r : m_refs) {
+        std::tie(fname, p, n) = r;
+        out << "r" << "|" << fname << "|" << p.first << "|" << p.second << "|" << n << endl;
     }
 }
 }
diff --git a/src/library/declaration_index.h b/src/library/declaration_index.h
index 1bd3656ce..0e7fed4bf 100644
--- a/src/library/declaration_index.h
+++ b/src/library/declaration_index.h
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include <utility>
 #include <string>
 #include "util/name.h"
+#include "util/name_map.h"
 #include "kernel/expr.h"
 #include "kernel/pos_info_provider.h"
 #include "library/io_state_stream.h"
@@ -17,9 +18,10 @@ Author: Leonardo de Moura
 namespace lean {
 /** \brief Datastructure for storing where a given declaration was defined. */
 class declaration_index {
-    enum class entry_kind { Declaration, Reference };
-    typedef std::tuple<entry_kind, std::string, pos_info, name, name, expr> entry;
-    std::vector<entry> m_entries;
+    typedef std::tuple<std::string, pos_info, name, expr> decl;
+    typedef std::tuple<std::string, pos_info, name> ref;
+    name_map<decl>   m_decls;
+    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_ref(std::string const fname, pos_info const & p, name const & n);