refactor(library/declaration_index): store declarations in a map

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-09-04 07:42:18 -07:00
parent f9a90b9920
commit d3ec5ccac1
3 changed files with 19 additions and 16 deletions

View file

@ -320,5 +320,5 @@ endif()
add_custom_target(clean-olean add_custom_target(clean-olean
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../library 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
) )

View file

@ -9,23 +9,24 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
void declaration_index::add_decl(std::string const fname, pos_info const & p, name const & n, name const & k, expr const & t) { 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) { 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 { void declaration_index::save(io_state_stream const & out) const {
entry_kind k; std::string fname; pos_info p; name n, dk; expr t; std::string fname; pos_info p; name n, k; expr t;
for (auto const & e : m_entries) { options const & opts = out.get_options();
std::tie(k, fname, p, n, dk, t) = e; m_decls.for_each([&](name const & n, decl const & d) {
out << (k == entry_kind::Declaration ? "d" : "r") << "|" << fname << "|" << p.first std::tie(fname, p, k, t) = d;
<< "|" << p.second << "|" << n; out << "d" << "|" << fname << "|" << p.first << "|" << p.second << "|" << n;
if (k == entry_kind::Declaration) { out << "|" << k << "|";
out << "|" << dk << "|";
options const & opts = out.get_options();
out.get_stream() << mk_pair(flatten(out.get_formatter()(t)), opts); 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;
} }
} }
} }

View file

@ -10,6 +10,7 @@ Author: Leonardo de Moura
#include <utility> #include <utility>
#include <string> #include <string>
#include "util/name.h" #include "util/name.h"
#include "util/name_map.h"
#include "kernel/expr.h" #include "kernel/expr.h"
#include "kernel/pos_info_provider.h" #include "kernel/pos_info_provider.h"
#include "library/io_state_stream.h" #include "library/io_state_stream.h"
@ -17,9 +18,10 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
/** \brief Datastructure for storing where a given declaration was defined. */ /** \brief Datastructure for storing where a given declaration was defined. */
class declaration_index { class declaration_index {
enum class entry_kind { Declaration, Reference }; typedef std::tuple<std::string, pos_info, name, expr> decl;
typedef std::tuple<entry_kind, std::string, pos_info, name, name, expr> entry; typedef std::tuple<std::string, pos_info, name> ref;
std::vector<entry> m_entries; name_map<decl> m_decls;
std::vector<ref> m_refs;
public: public:
void add_decl(std::string const fname, pos_info const & p, name const & n, name const & k, expr const & t); 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); void add_ref(std::string const fname, pos_info const & p, name const & n);