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

Add total order for hierarchical names

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-07-21 15:56:18 -07:00
parent ecb7316943
commit 9e966a0e57
3 changed files with 67 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/tests/util/name.cpp
View file

@ -23,6 +23,25 @@ static void tst1() {
lean_assert(n != name());
lean_assert(name().get_kind() == name::kind::ANONYMOUS);
lean_assert(name(name(), "foo") == name("foo"));
lean_assert(name(n, 1) < name(n, 2));
std::cout << "cmp(" << name(n, 1) << ", " << name(n, 2) << ") = " << cmp(name(n,1), name(n, 2)) << "\n";
lean_assert(!(name(n, 1) >= name(n, 2)));
lean_assert(name(n, 1) < name(name(n, 1), 1));
lean_assert(n < name(n, 1));
lean_assert(name(n, 2) > name(name(n, 1), 1));
lean_assert(name(name("aa"), 2) < name(name(n, 1), 1));
lean_assert(name(n, "aaa") < name(n, "xxx"));
lean_assert(name(n, 1) < name(n, "xxx"));
lean_assert(name(n, 1) < name(name(n, "xxx"), 1));
lean_assert(name() < name(name(n, "xxx"), 1));
lean_assert(name(1) < name(name(n, "xxx"), 1));
lean_assert(name(1) < name(2));
lean_assert(name(2) > name(1));
lean_assert(name(1) > name());
lean_assert(name(2) < name(name("foo"), 1));
lean_assert(name(0u) < name(name(1), "foo"));
lean_assert(name(2) > name(name(1), "foo"));
}
int main() {

40
src/util/name.cpp
View file

@ -5,10 +5,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <cstring>
#include <vector>
#include <algorithm>
#include "name.h"
#include "debug.h"
#include "rc.h"
#include "hash.h"
#include "trace.h"
namespace lean {
@ -58,6 +61,15 @@ struct name::imp {
else
display_core(out, sep, p);
}
friend void copy_limbs(imp * p, std::vector<name::imp *> & limbs) {
limbs.clear();
while (p != nullptr) {
limbs.push_back(p);
p = p->m_prefix;
}
std::reverse(limbs.begin(), limbs.end());
}
};
name::name(imp * p) {
@ -163,6 +175,34 @@ bool operator==(name const & a, name const & b) {
}
}
int cmp(name::imp * i1, name::imp * i2) {
static thread_local std::vector<name::imp *> limbs1;
static thread_local std::vector<name::imp *> limbs2;
copy_limbs(i1, limbs1);
copy_limbs(i2, limbs2);
auto it1 = limbs1.begin();
auto it2 = limbs2.begin();
for (; it1 != limbs1.end() && it2 != limbs2.end(); ++it1, ++it2) {
i1 = *it1;
i2 = *it2;
if (i1->m_is_string != i2->m_is_string)
return i1->m_is_string ? 1 : -1;
if (i1->m_is_string) {
int c = strcmp(i1->m_str, i2->m_str);
if (c != 0)
return c;
}
else if (i1->m_k != i2->m_k) {
return i1->m_k < i2->m_k ? -1 : 1;
}
}
if (it1 == limbs1.end() && it2 == limbs2.end())
return 0;
else return it1 == limbs1.end() ? -1 : 1;
}
bool name::is_atomic() const {
return m_imp == nullptr || m_imp->m_prefix == nullptr;
}

9
src/util/name.h
View file

@ -16,8 +16,9 @@ constexpr char const * default_name_separator = "::";
*/
class name {
struct imp;
friend int cmp(imp * i1, imp * i2);
imp * m_imp;
name(imp * p);
explicit name(imp * p);
public:
enum class kind { ANONYMOUS, STRING, NUMERAL };
name();
@ -32,6 +33,12 @@ public:
name & operator=(name && other);
friend bool operator==(name const & a, name const & b);
friend bool operator!=(name const & a, name const & b) { return !(a == b); }
// total order on hierarchical names.
friend int cmp(name const & a, name const & b) { return cmp(a.m_imp, b.m_imp); }
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; }
kind get_kind() const;
bool is_anonymous() const { return get_kind() == kind::ANONYMOUS; }
bool is_string() const { return get_kind() == kind::STRING; }