From 9e966a0e57c6f6e3457106346511acffd722a626 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 21 Jul 2013 15:56:18 -0700
Subject: [PATCH] Add total order for hierarchical names

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/tests/util/name.cpp | 19 +++++++++++++++++++
 src/util/name.cpp       | 40 ++++++++++++++++++++++++++++++++++++++++
 src/util/name.h         |  9 ++++++++-
 3 files changed, 67 insertions(+), 1 deletion(-)

diff --git a/src/tests/util/name.cpp b/src/tests/util/name.cpp
index fb6c3a229..a4f02564e 100644
--- a/src/tests/util/name.cpp
+++ b/src/tests/util/name.cpp
@@ -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() {
diff --git a/src/util/name.cpp b/src/util/name.cpp
index 4f201ca59..cb56d0013 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -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;
 }
diff --git a/src/util/name.h b/src/util/name.h
index e565c1643..42405e1ec 100644
--- a/src/util/name.h
+++ b/src/util/name.h
@@ -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; }