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

perf(util/name): more inlining

Browse source
This commit is contained in:
Leonardo de Moura 2016-02-02 09:49:50 -08:00
parent 187bce307e
commit a9cb9ff912
2 changed files with 11 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
src/util/name.cpp
View file

@ -111,15 +111,6 @@ name::name(char const * n):name(name(), n) {
name::name(unsigned k):name(name(), k, true) { name::name(unsigned k):name(name(), k, true) {
} }
name::name(name const & other):m_ptr(other.m_ptr) {
if (m_ptr)
m_ptr->inc_ref();
}
name::name(name && other):m_ptr(other.m_ptr) {
other.m_ptr = nullptr;
}
name::name(std::initializer_list<char const *> const & l):name() { name::name(std::initializer_list<char const *> const & l):name() {
if (l.size() == 0) { if (l.size() == 0) {
return; return;
@ -132,11 +123,6 @@ name::name(std::initializer_list<char const *> const & l):name() {
} }
} }
name::~name() {
if (m_ptr)
m_ptr->dec_ref();
}
static name * g_anonymous = nullptr; static name * g_anonymous = nullptr;
name const & name::anonymous() { name const & name::anonymous() {
@ -162,16 +148,6 @@ name_kind name::kind() const {
return m_ptr->m_is_string ? name_kind::STRING : name_kind::NUMERAL; return m_ptr->m_is_string ? name_kind::STRING : name_kind::NUMERAL;
} }
unsigned name::get_numeral() const {
lean_assert(is_numeral());
return m_ptr->m_k;
}
char const * name::get_string() const {
lean_assert(is_string());
return m_ptr->m_str;
}
/* Equality test core procedure, it is invoked by operator== */ /* Equality test core procedure, it is invoked by operator== */
bool eq_core(name::imp * i1, name::imp * i2) { bool eq_core(name::imp * i1, name::imp * i2) {
while (true) { while (true) {
@ -260,14 +236,6 @@ int cmp(name::imp * i1, name::imp * i2) {
else return it1 == limbs1.end() ? -1 : 1; else return it1 == limbs1.end() ? -1 : 1;
} }
bool name::is_atomic() const {
return m_ptr == nullptr || m_ptr->m_prefix == nullptr;
}
name name::get_prefix() const {
return is_atomic() ? name() : name(m_ptr->m_prefix);
}
static unsigned num_digits(unsigned k) { static unsigned num_digits(unsigned k) {
if (k == 0) if (k == 0)
return 1; return 1;

22
src/util/name.h
View file

@ -57,15 +57,15 @@ public:
name(std::string const & s):name(s.c_str()) {} name(std::string const & s):name(s.c_str()) {}
name(name const & prefix, char const * name); name(name const & prefix, char const * name);
name(name const & prefix, unsigned k); name(name const & prefix, unsigned k);
name(name const & other); name(name const & other):m_ptr(other.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
name(name && other); name(name && other):m_ptr(other.m_ptr) { other.m_ptr = nullptr; }
/** /**
\brief Create a hierarchical name using the given strings. \brief Create a hierarchical name using the given strings.
Example: <code>name{"foo", "bla", "tst"}</code> creates the hierarchical Example: <code>name{"foo", "bla", "tst"}</code> creates the hierarchical
name <tt>foo::bla::tst</tt>. name <tt>foo::bla::tst</tt>.
*/ */
name(std::initializer_list<char const *> const & l); name(std::initializer_list<char const *> const & l);
~name(); ~name() { if (m_ptr) m_ptr->dec_ref(); }
static name const & anonymous(); static name const & anonymous();
/** /**
\brief Create a unique internal name that is not meant to exposed \brief Create a unique internal name that is not meant to exposed
@ -107,22 +107,22 @@ public:
friend bool operator<=(name const & a, name const & b) { return cmp(a, b) <= 0; } friend bool operator<=(name const & a, name const & b) { return cmp(a, b) <= 0; }
friend bool operator>=(name const & a, name const & b) { return cmp(a, b) >= 0; } friend bool operator>=(name const & a, name const & b) { return cmp(a, b) >= 0; }
name_kind kind() const; name_kind kind() const;
bool is_anonymous() const { return kind() == name_kind::ANONYMOUS; } bool is_anonymous() const { return m_ptr == nullptr; }
bool is_string() const { return kind() == name_kind::STRING; } bool is_string() const { return m_ptr != nullptr && m_ptr->m_is_string; }
bool is_numeral() const { return kind() == name_kind::NUMERAL; } bool is_numeral() const { return m_ptr != nullptr && !m_ptr->m_is_string; }
explicit operator bool() const { return !is_anonymous(); } explicit operator bool() const { return m_ptr != nullptr; }
unsigned get_numeral() const; unsigned get_numeral() const { lean_assert(is_numeral()); return m_ptr->m_k; }
/** /**
\brief If the tail of the given hierarchical name is a string, then it returns this string. \brief If the tail of the given hierarchical name is a string, then it returns this string.
\pre is_string() \pre is_string()
*/ */
char const * get_string() const; char const * get_string() const { lean_assert(is_string()); return m_ptr->m_str; }
bool is_atomic() const; bool is_atomic() const { return m_ptr == nullptr || m_ptr->m_prefix == nullptr; }
/** /**
\brief Return the prefix of a hierarchical name \brief Return the prefix of a hierarchical name
\pre !is_atomic() \pre !is_atomic()
*/ */
name get_prefix() const; name get_prefix() const { return is_atomic() ? name() : name(m_ptr->m_prefix); }
/** \brief Convert this hierarchical name into a string. */ /** \brief Convert this hierarchical name into a string. */
std::string to_string(char const * sep = lean_name_separator) const; std::string to_string(char const * sep = lean_name_separator) const;
/** \brief Size of the this name (in characters). */ /** \brief Size of the this name (in characters). */