From ed3df178ac95ddfd03d38ecf7b026a8545767dcb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 24 Jul 2013 11:00:29 -0700
Subject: [PATCH] Improve hash for hierarchical names.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/sexpr/sexpr.cpp     |  4 ++--
 src/tests/util/name.cpp | 18 ++++++++++++++++++
 src/util/hash.cpp       |  2 +-
 src/util/hash.h         |  2 +-
 src/util/name.cpp       | 29 +++++++++++++----------------
 5 files changed, 35 insertions(+), 20 deletions(-)

diff --git a/src/sexpr/sexpr.cpp b/src/sexpr/sexpr.cpp
index 998615a0cc..1bc79821ef 100644
--- a/src/sexpr/sexpr.cpp
+++ b/src/sexpr/sexpr.cpp
@@ -26,10 +26,10 @@ struct sexpr_cell {
 struct sexpr_string : public sexpr_cell {
     std::string m_value;
     sexpr_string(char const * v):
-        sexpr_cell(sexpr_kind::STRING, hash(v, strlen(v), 13)),
+        sexpr_cell(sexpr_kind::STRING, hash_str(strlen(v), v, 13)),
         m_value(v) {}
     sexpr_string(std::string const & v):
-        sexpr_cell(sexpr_kind::STRING, hash(v.c_str(), v.size(), 13)),
+        sexpr_cell(sexpr_kind::STRING, hash_str(v.size(), v.c_str(), 13)),
         m_value(v) {}
 };
 
diff --git a/src/tests/util/name.cpp b/src/tests/util/name.cpp
index 6cdbeaf29c..f379031f14 100644
--- a/src/tests/util/name.cpp
+++ b/src/tests/util/name.cpp
@@ -44,8 +44,26 @@ static void tst1() {
     lean_assert(name(2) > name(name(1), "foo"));
 }
 
+static name mk_big_name(unsigned num) {
+    name n("foo");
+    for (unsigned i = 0; i < num; i++) {
+        n = name(n, "bla");
+    }
+    return n;
+}
+
+static void tst2() {
+    name n1 = mk_big_name(2000);
+    name n2 = mk_big_name(2000);
+    lean_assert(n1.hash() == n2.hash());
+    for (unsigned i = 0; i < 10000; i++)
+        n1.hash();
+    std::cout << "n1.hash(): " << n1.hash() << "\n";
+}
+
 int main() {
     continue_on_violation(true);
     tst1();
+    tst2();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/util/hash.cpp b/src/util/hash.cpp
index d6fc9efbfe..c4a8f6361e 100644
--- a/src/util/hash.cpp
+++ b/src/util/hash.cpp
@@ -20,7 +20,7 @@ void mix(unsigned & a, unsigned & b, unsigned & c) {
 
 // Bob Jenkin's hash function.
 // http://burtleburtle.net/bob/hash/doobs.html
-unsigned hash(char const * str, unsigned length, unsigned init_value) {
+unsigned hash_str(unsigned length, char const * str, unsigned init_value) {
     register unsigned a, b, c, len;
 
     /* Set up the internal state */
diff --git a/src/util/hash.h b/src/util/hash.h
index 9d4ddfe5a9..e015aaffb6 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -11,7 +11,7 @@ namespace lean {
 
 void mix(unsigned & a, unsigned & b, unsigned & c);
 
-unsigned hash(char const * str, unsigned length, unsigned init_value);
+unsigned hash_str(unsigned len, char const * str, unsigned init_value);
 
 inline unsigned hash(unsigned h1, unsigned h2) {
     h2 -= h1; h2 ^= (h1 << 8);
diff --git a/src/util/name.cpp b/src/util/name.cpp
index 109cb43fc9..c783dfcbeb 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -20,6 +20,7 @@ constexpr char const * anonymous_str = "[anonymous]";
 struct name::imp {
     MK_LEAN_RC()
     bool     m_is_string;
+    unsigned m_hash;
     imp *    m_prefix;
     union {
         char * m_str;
@@ -41,7 +42,7 @@ struct name::imp {
         }
     }
 
-    imp(bool s, imp * p):m_rc(1), m_is_string(s), m_prefix(p) { if (p) p->inc_ref(); }
+    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, char const * sep, imp * p) {
         lean_assert(p != nullptr);
@@ -89,11 +90,19 @@ name::name(name const & prefix, char const * name) {
     m_imp      = new (mem) imp(true, prefix.m_imp);
     memcpy(mem + sizeof(imp), name, sz + 1);
     m_imp->m_str       = mem + sizeof(imp);
+    if (m_imp->m_prefix)
+        m_imp->m_hash = hash_str(sz, name, m_imp->m_prefix->m_hash);
+    else
+        m_imp->m_hash = hash_str(sz, name, 0);
 }
 
 name::name(name const & prefix, unsigned k) {
     m_imp      = new imp(false, prefix.m_imp);
     m_imp->m_k = k;
+    if (m_imp->m_prefix)
+        m_imp->m_hash = ::lean::hash(m_imp->m_prefix->m_hash, k);
+    else
+        m_imp->m_hash = k;
 }
 
 name::name(char const * n):name(name(), n) {
@@ -158,6 +167,8 @@ bool operator==(name const & a, name const & b) {
             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);
         if (i1->m_is_string != i2->m_is_string)
@@ -251,21 +262,7 @@ size_t name::size(char const * sep) const {
 }
 
 unsigned name::hash() const {
-    if (m_imp == nullptr)
-        return 17;
-    else {
-        unsigned h = 13;
-        imp const * i = m_imp;
-        do {
-            if (i->m_is_string)
-                h = ::lean::hash(i->m_str, strlen(i->m_str), h);
-            else
-                h = ::lean::hash(h, i->m_k);
-            i = i->m_prefix;
-        }
-        while (i != nullptr);
-        return h;
-    }
+    return m_imp->m_hash;
 }
 
 std::ostream & operator<<(std::ostream & out, name const & n) {