refactor(util/splay_tree): replace find with splay_find

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/metavar.cpp

@@ -92,7 +92,7 @@ context metavar_env::get_context(expr const & m) const {
 }
 
 context metavar_env::get_context(name const & m) const {
-    auto it = const_cast<metavar_env*>(this)->m_metavar_data.splay_find(m);
+    auto it = m_metavar_data.find(m);
     lean_assert(it);
     return it->m_context;
 }
@@ -112,7 +112,7 @@ expr metavar_env::get_type(expr const & m) {
 }
 
 expr metavar_env::get_type(name const & m) {
-    auto it = const_cast<metavar_env*>(this)->m_metavar_data.splay_find(m);
+    auto it = m_metavar_data.find(m);
     lean_assert(it);
     if (it->m_type) {
         return *(it->m_type);
@@ -124,7 +124,7 @@ expr metavar_env::get_type(name const & m) {
 }
 
 bool metavar_env::has_type(name const & m) const {
-    auto it = const_cast<metavar_env*>(this)->m_metavar_data.splay_find(m);
+    auto it = m_metavar_data.find(m);
     lean_assert(it);
     return static_cast<bool>(it->m_type);
 }
@@ -148,7 +148,7 @@ optional<justification> metavar_env::get_justification(name const & m) const {
 }
 
 bool metavar_env::is_assigned(name const & m) const {
-    auto it = const_cast<metavar_env*>(this)->m_metavar_data.splay_find(m);
+    auto it = m_metavar_data.find(m);
     return it && it->m_subst;
 }
 
@@ -160,7 +160,7 @@ bool metavar_env::is_assigned(expr const & m) const {
 void metavar_env::assign(name const & m, expr const & t, justification const & jst) {
     lean_assert(!is_assigned(m));
     inc_timestamp();
-    auto it = const_cast<metavar_env*>(this)->m_metavar_data.splay_find(m);
+    auto it = m_metavar_data.find(m);
     lean_assert(it);
     it->m_subst         = t;
     it->m_justification = jst;
@@ -206,7 +206,7 @@ optional<std::pair<expr, justification>> metavar_env::get_subst_jst(expr const &
 }
 
 optional<std::pair<expr, justification>> metavar_env::get_subst_jst(name const & m) const {
-    auto it = const_cast<metavar_env*>(this)->m_metavar_data.splay_find(m);
+    auto it = const_cast<metavar_env*>(this)->m_metavar_data.find(m);
     if (it->m_subst) {
         expr s = *(it->m_subst);
         if (has_assigned_metavar(s, *this)) {

src/library/substitution.cpp

@@ -13,7 +13,7 @@ namespace lean {
 expr find(substitution & s, expr e) {
     while (true) {
         if (is_metavar(e)) {
-            expr * it = s.splay_find(metavar_name(e));
+            expr * it = s.find(metavar_name(e));
             if (it == nullptr)
                 return e;
             e = *it;
@@ -61,11 +61,11 @@ static int substitution_find(lua_State * L) {
     if (is_expr(L, 2)) {
         expr const & e = to_expr(L, 2);
         if (is_metavar(e))
-            it = s.splay_find(metavar_name(e));
+            it = s.find(metavar_name(e));
         else
             throw exception("arg #2 must be a metavariable");
     } else {
-        it = s.splay_find(to_name_ext(L, 2));
+        it = s.find(to_name_ext(L, 2));
     }
     if (it)
         push_expr(L, find(s, *it));

src/library/tactic/proof_builder.cpp

@@ -14,7 +14,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 expr find(proof_map const & m, name const & n) {
-    expr * r = const_cast<proof_map&>(m).splay_find(n);
+    expr const * r = m.find(n);
     if (r)
         return *r;
     throw exception(sstream() << "proof for goal '" << n << "' not found");

src/tests/util/splay_tree.cpp

@@ -66,7 +66,7 @@ static void tst1() {
     s.insert(34);
     std::cout << s2 << "\n";
     std::cout << s << "\n";
-    int const * v = s.splay_find(11);
+    int const * v = s.find(11);
     lean_assert(*v == 11);
     std::cout << s << "\n";
     lean_assert(!s.empty());
@@ -159,9 +159,9 @@ static void tst4() {
     int_splay_tree s;
     s.insert(10);
     s.insert(20);
-    lean_assert(s.splay_find(30) == nullptr);
-    lean_assert(*(s.splay_find(20)) == 20);
-    lean_assert(*(s.splay_find(10)) == 10);
+    lean_assert(s.find(30) == nullptr);
+    lean_assert(*(s.find(20)) == 20);
+    lean_assert(*(s.find(10)) == 10);
 }
 
 int main() {

src/util/splay_map.cpp

@@ -44,7 +44,7 @@ static int lua_splay_map_erase(lua_State * L) {
 
 static int lua_splay_map_find(lua_State * L) {
     lua_splay_map & m = to_lua_splay_map(L, 1);
-    luaref * val = m.splay_find(luaref(L, 2));
+    luaref const * val = m.find(luaref(L, 2));
     if (val) {
         lean_assert(val->get_state() == L);
         val->push();

src/util/splay_map.h

@@ -37,9 +37,9 @@ public:
     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())); }
+    T const * find(K const & k) const { auto e = m_map.find(mk_pair(k, T())); return e ? &(e->second) : nullptr; }
+    T * find(K const & k) { auto e = m_map.find(mk_pair(k, T())); return e ? &(const_cast<T&>(e->second)) : nullptr; }
     bool contains(K const & k) const { return m_map.contains(mk_pair(k, T())); }
-    T * splay_find(K const & k) { auto e = m_map.splay_find(mk_pair(k, T())); return e ? &(const_cast<T&>(e->second)) : nullptr; }
     void erase(K const & k) { m_map.erase(mk_pair(k, T())); }
 
     class ref {
@@ -49,12 +49,12 @@ 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 &() const {
-            entry const * e = m_map.find(m_key);
+            T const * e = m_map.find(m_key);
             if (e) {
-                return e->second;
+                return *e;
             } else {
                 m_map.insert(m_key, T());
-                return m_map.find(m_key)->second;
+                return *(m_map.find(m_key));
             }
         }
     };

src/util/splay_tree.h

@@ -353,19 +353,15 @@ public:
         If the splay tree does not contain any value equal to \c v, then return \c nullptr.
 
         \remark <tt>find(v) != nullptr</tt> iff <tt>contains(v)</tt>
+
+        \warning The content of the tree is not modified, but it is "reorganized".
     */
     T const * find(T const & v) const {
-        node const * n = m_ptr;
-        while (true) {
-            if (n == nullptr)
-                return nullptr;
-            int c = cmp(v, n->m_value);
-            if (c < 0)
-                n = n->m_left;
-            else if (c > 0)
-                n = n->m_right;
-            else
-                return &(n->m_value);
+        if (const_cast<splay_tree*>(this)->pull(v)) {
+            lean_assert(cmp(m_ptr->m_value, v) == 0);
+            return &(m_ptr->m_value);
+        } else {
+            return nullptr;
         }
     }
 
@@ -374,20 +370,6 @@ public:
         return find(v);
     }
 
-    /**
-        \brief Similar to \c find, but the splay tree is reorganized.
-        If <tt>find(v)</tt> is invoked after <tt>splay_find(v)</tt>, then the cost will be O(1).
-        The idea is to move recently accessed elements close to the root.
-    */
-    T const * splay_find(T const & v) {
-        if (pull(v)) {
-            lean_assert(cmp(m_ptr->m_value, v) == 0);
-            return &(m_ptr->m_value);
-        } else {
-            return nullptr;
-        }
-    }
-
     /** \brief Remove \c v from this splay tree. Actually, it removes an element that is equal to \c v. */
     void erase(T const & v) {
         if (pull(v)) {