From 1779b29355d687120fd4aafb78bd187430b3b44f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 24 Sep 2013 01:43:58 -0700
Subject: [PATCH] Implement map using splay_trees

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/tests/util/CMakeLists.txt |  3 ++
 src/tests/util/splay_map.cpp  | 32 ++++++++++++++++++
 src/util/splay_map.h          | 61 +++++++++++++++++++++++++++++++++++
 3 files changed, 96 insertions(+)
 create mode 100644 src/tests/util/splay_map.cpp
 create mode 100644 src/util/splay_map.h

diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt
index ac3e02ba7..fe9af0c9f 100644
--- a/src/tests/util/CMakeLists.txt
+++ b/src/tests/util/CMakeLists.txt
@@ -37,3 +37,6 @@ add_test(memory ${CMAKE_CURRENT_BINARY_DIR}/memory)
 add_executable(splay_tree splay_tree.cpp)
 target_link_libraries(splay_tree ${EXTRA_LIBS})
 add_test(splay_tree ${CMAKE_CURRENT_BINARY_DIR}/splay_tree)
+add_executable(splay_map splay_map.cpp)
+target_link_libraries(splay_map ${EXTRA_LIBS})
+add_test(splay_map ${CMAKE_CURRENT_BINARY_DIR}/splay_map)
diff --git a/src/tests/util/splay_map.cpp b/src/tests/util/splay_map.cpp
new file mode 100644
index 000000000..e475fcd86
--- /dev/null
+++ b/src/tests/util/splay_map.cpp
@@ -0,0 +1,32 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <iostream>
+#include "util/test.h"
+#include "util/splay_map.h"
+#include "util/name.h"
+using namespace lean;
+
+struct int_cmp { int operator()(int i1, int i2) const { return i1 < i2 ? -1 : (i1 > i2 ? 1 : 0); } };
+
+typedef splay_map<int, name, int_cmp> int2name;
+
+static void tst0() {
+    int2name m1;
+    m1[10] = name("t1");
+    m1[20] = name("t2");
+    int2name m2(m1);
+    m2[10] = name("t3");
+    lean_assert(m1[10] == name("t1"));
+    lean_assert(m1[20] == name("t2"));
+    lean_assert(m2[10] == name("t3"));
+    lean_assert(m2[20] == name("t2"));
+}
+
+int main() {
+    tst0();
+    return has_violations() ? 1 : 0;
+}
diff --git a/src/util/splay_map.h b/src/util/splay_map.h
new file mode 100644
index 000000000..d7b317b22
--- /dev/null
+++ b/src/util/splay_map.h
@@ -0,0 +1,61 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <utility>
+#include "util/pair.h"
+#include "util/splay_tree.h"
+
+namespace lean {
+/**
+   \brief Wrapper for implementing maps using splay trees.
+*/
+template<typename K, typename T, typename CMP>
+class splay_map : public CMP {
+    typedef std::pair<K, T> entry;
+    struct entry_cmp : public CMP {
+        entry_cmp(CMP const & c):CMP(c) {}
+        int operator()(entry const & e1, entry const & e2) const { return CMP::operator()(e1.first, e2.first); }
+    };
+    splay_tree<entry, entry_cmp> m_map;
+public:
+    splay_map(CMP const & cmp = CMP()):m_map(entry_cmp(cmp)) {}
+
+    void swap(splay_map & m) { m_map.swap(m.m_map); }
+    bool empty() const { return m_map.empty(); }
+    void clear() { m_map.clear(); }
+    bool is_eqp(splay_map const & m) const { return m_map.is_eqp(m); }
+    unsigned size() const { return m_map.size(); }
+    void insert(K const & k, T const & v) { m_map.insert(mk_pair(k, v)); }
+    entry const * find(K const & k) const { return m_map.find(mk_pair(k, T())); }
+    bool contains(K const & k) const { return m_map.contains(mk_pair(k, T())); }
+    entry const * find_memoize(K const & k) { return m_map.contains(mk_pair(k, T())); }
+    void erase(K const & k) { m_map.erase(mk_pair(k, T())); }
+
+    class ref {
+        splay_map & m_map;
+        K const &   m_key;
+    public:
+        ref(splay_map & m, K const & k):m_map(m), m_key(k) {}
+        ref & operator=(T const & v) { m_map.insert(m_key, v); return *this; }
+        operator T const &() {
+            entry const * e = m_map.find(m_key);
+            if (e) {
+                return e->second;
+            } else {
+                m_map.insert(m_key, T());
+                return m_map.find(m_key)->second;
+            }
+        }
+    };
+
+    /**
+       \brief Returns a reference to the value that is mapped to a key equivalent to key,
+       performing an insertion if such key does not already exist.
+    */
+    ref operator[](K const & k) { return ref(*this, k); }
+};
+}