michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

perf(src/util/name): inline hash

Browse source
This commit is contained in:
Leonardo de Moura 2016-02-02 09:21:01 -08:00
parent c779590517
commit 187bce307e
2 changed files with 61 additions and 55 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

85
src/util/name.cpp
View file

@ -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<name::imp *> & 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<name::imp *> & 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) {

31
src/util/name.h
View file

@ -10,6 +10,7 @@ Author: Leonardo de Moura
#include <functional>
#include <algorithm>
#include <utility>
#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<name::imp *> & 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);