From 187bce307e6bfe313172b4e57d2b734f261e307e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 2 Feb 2016 09:21:01 -0800 Subject: [PATCH] perf(src/util/name): inline hash --- src/util/name.cpp | 85 ++++++++++++++++++----------------------------- src/util/name.h | 31 +++++++++++++++-- 2 files changed, 61 insertions(+), 55 deletions(-) diff --git a/src/util/name.cpp b/src/util/name.cpp index 8c393cb07f..ac237ce151 100644 --- a/src/util/name.cpp +++ b/src/util/name.cpp @@ -13,7 +13,6 @@ Author: Leonardo de Moura #include "util/name.h" #include "util/sstream.h" #include "util/debug.h" -#include "util/rc.h" #include "util/buffer.h" #include "util/memory_pool.h" #include "util/hash.h" @@ -24,49 +23,34 @@ Author: Leonardo de Moura namespace lean { constexpr char const * anonymous_str = "[anonymous]"; -/** \brief Actual implementation of hierarchical names. */ -struct name::imp { - MK_LEAN_RC() - bool m_is_string; - unsigned m_hash; - imp * m_prefix; - union { - char * m_str; - unsigned m_k; - }; - void dealloc(); - - imp(bool s, imp * p):m_rc(1), m_is_string(s), m_hash(0), m_prefix(p) { if (p) p->inc_ref(); } - - static void display_core(std::ostream & out, imp * p, char const * sep) { - lean_assert(p != nullptr); - if (p->m_prefix) { - display_core(out, p->m_prefix, sep); - out << sep; - } - if (p->m_is_string) - out << p->m_str; - else - out << p->m_k; +void name::imp::display_core(std::ostream & out, imp * p, char const * sep) { + lean_assert(p != nullptr); + if (p->m_prefix) { + display_core(out, p->m_prefix, sep); + out << sep; } + if (p->m_is_string) + out << p->m_str; + else + out << p->m_k; +} - static void display(std::ostream & out, imp * p, char const * sep = lean_name_separator) { - if (p == nullptr) - out << anonymous_str; - else - display_core(out, p, sep); - } +void name::imp::display(std::ostream & out, imp * p, char const * sep) { + if (p == nullptr) + out << anonymous_str; + else + display_core(out, p, sep); +} - friend void copy_limbs(imp * p, buffer & limbs) { - limbs.clear(); - while (p != nullptr) { - limbs.push_back(p); - p = p->m_prefix; - } - std::reverse(limbs.begin(), limbs.end()); +void copy_limbs(name::imp * p, buffer & limbs) { + limbs.clear(); + while (p != nullptr) { + limbs.push_back(p); + p = p->m_prefix; } -}; + std::reverse(limbs.begin(), limbs.end()); +} DEF_THREAD_MEMORY_POOL(get_numeric_name_allocator, sizeof(name::imp)); @@ -188,18 +172,13 @@ char const * name::get_string() const { return m_ptr->m_str; } -bool operator==(name const & a, name const & b) { - name::imp * i1 = a.m_ptr; - name::imp * i2 = b.m_ptr; +/* Equality test core procedure, it is invoked by operator== */ +bool eq_core(name::imp * i1, name::imp * i2) { while (true) { - if (i1 == i2) - return true; - if ((i1 == nullptr) != (i2 == nullptr)) - return false; - if (i1->m_hash != i2->m_hash) - return false; lean_assert(i1 != nullptr); lean_assert(i2 != nullptr); + lean_assert(i1 && i2); + lean_assert(i1->m_hash == i2->m_hash); if (i1->m_is_string != i2->m_is_string) return false; if (i1->m_is_string) { @@ -211,6 +190,12 @@ bool operator==(name const & a, name const & b) { } i1 = i1->m_prefix; i2 = i2->m_prefix; + if (i1 == i2) + return true; + if ((i1 == nullptr) != (i2 == nullptr)) + return false; + if (i1->m_hash != i2->m_hash) + return false; } } @@ -326,10 +311,6 @@ size_t name::utf8_size() const { return size_core(true); } -unsigned name::hash() const { - return m_ptr ? m_ptr->m_hash : 11; -} - bool name::is_safe_ascii() const { imp * i = m_ptr; while (i) { diff --git a/src/util/name.h b/src/util/name.h index 2f5f562a0b..4e0e13faa4 100644 --- a/src/util/name.h +++ b/src/util/name.h @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include #include #include +#include "util/rc.h" #include "util/pair.h" #include "util/lua.h" #include "util/serializer.h" @@ -24,7 +25,22 @@ enum class name_kind { ANONYMOUS, STRING, NUMERAL }; */ class name { public: - struct imp; + /** \brief Actual implementation of hierarchical names. */ + struct imp { + MK_LEAN_RC() + bool m_is_string; + unsigned m_hash; + imp * m_prefix; + union { + char * m_str; + unsigned m_k; + }; + void dealloc(); + imp(bool s, imp * p):m_rc(1), m_is_string(s), m_hash(0), m_prefix(p) { if (p) p->inc_ref(); } + static void display_core(std::ostream & out, imp * p, char const * sep); + static void display(std::ostream & out, imp * p, char const * sep = lean_name_separator); + friend void copy_limbs(imp * p, buffer & limbs); + }; private: friend int cmp(imp * i1, imp * i2); friend class name_deserializer; @@ -69,7 +85,16 @@ public: name & operator=(name && other); /** \brief Return true iff \c n1 is a prefix of \c n2. */ friend bool is_prefix_of(name const & n1, name const & n2); - friend bool operator==(name const & a, name const & b); + friend bool eq_core(name::imp * i1, name::imp * i2); + friend bool operator==(name const & a, name const & b) { + if (a.m_ptr == b.m_ptr) + return true; + if ((a.m_ptr == nullptr) != (b.m_ptr == nullptr)) + return false; + if (a.m_ptr->m_hash != b.m_ptr->m_hash) + return false; + return eq_core(a.m_ptr, b.m_ptr); + } friend bool operator!=(name const & a, name const & b) { return !(a == b); } friend bool operator==(name const & a, char const * b); friend bool operator!=(name const & a, char const * b) { return !(a == b); } @@ -104,7 +129,7 @@ public: size_t size() const; /** \brief Size of the this name in unicode. */ size_t utf8_size() const; - unsigned hash() const; + unsigned hash() const { return m_ptr ? m_ptr->m_hash : 11; } /** \brief Return true iff the name contains only safe ASCII chars */ bool is_safe_ascii() const; friend std::ostream & operator<<(std::ostream & out, name const & n);