From 9a1a9f3b5a47fc00198ddcf5607263b94dd78f80 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 6 Jan 2016 17:29:22 -0800
Subject: [PATCH] refactor(library/fun_info_manager): use expr_unsigned_map

---
 src/library/fun_info_manager.cpp | 23 ++++++++++++++---------
 src/library/fun_info_manager.h   | 15 ++++-----------
 2 files changed, 18 insertions(+), 20 deletions(-)

diff --git a/src/library/fun_info_manager.cpp b/src/library/fun_info_manager.cpp
index d078d3aa0..62156cec4 100644
--- a/src/library/fun_info_manager.cpp
+++ b/src/library/fun_info_manager.cpp
@@ -65,22 +65,25 @@ list<unsigned> fun_info_manager::get_core(expr const & fn, buffer<param_info> &
 }
 
 fun_info fun_info_manager::get(expr const & e) {
-    if (auto r = m_cache_get.find(e))
-        return *r;
+    auto it = m_cache_get.find(e);
+    if (it != m_cache_get.end())
+        return it->second;
     buffer<param_info> pinfos;
     auto result_deps = get_core(e, pinfos, std::numeric_limits<unsigned>::max());
     fun_info r(pinfos.size(), to_list(pinfos), result_deps);
-    m_cache_get.insert(e, r);
+    m_cache_get.insert(mk_pair(e, r));
     return r;
 }
 
 fun_info fun_info_manager::get(expr const & e, unsigned nargs) {
-    if (auto r = m_cache_get_nargs.find(mk_pair(nargs, e)))
-        return *r;
+    expr_unsigned key(e, nargs);
+    auto it = m_cache_get_nargs.find(key);
+    if (it != m_cache_get_nargs.end())
+        return it->second;
     buffer<param_info> pinfos;
     auto result_deps = get_core(e, pinfos, nargs);
     fun_info r(pinfos.size(), to_list(pinfos), result_deps);
-    m_cache_get_nargs.insert(mk_pair(nargs, e), r);
+    m_cache_get_nargs.insert(mk_pair(key, r));
     return r;
 }
 
@@ -191,13 +194,15 @@ fun_info fun_info_manager::get_specialization(expr const & a) {
         expr g = a;
         for (unsigned i = 0; i < num_rest_args; i++)
             g = app_fn(g);
-        if (auto r = m_cache_get_spec.find(mk_pair(num_rest_args, g)))
-            return *r;
+        expr_unsigned key(g, num_rest_args);
+        auto it = m_cache_get_spec.find(key);
+        if (it != m_cache_get_spec.end())
+            return it->second;
         buffer<param_info> new_pinfos;
         copy_prefix(prefix_sz, pinfos, new_pinfos);
         auto result_deps = get_core(g, new_pinfos, num_rest_args);
         fun_info r(new_pinfos.size(), to_list(new_pinfos), result_deps);
-        m_cache_get_spec.insert(mk_pair(num_rest_args, g), r);
+        m_cache_get_spec.insert(mk_pair(key, r));
         return r;
     }
 }
diff --git a/src/library/fun_info_manager.h b/src/library/fun_info_manager.h
index 6a4f3a3ab..72f248865 100644
--- a/src/library/fun_info_manager.h
+++ b/src/library/fun_info_manager.h
@@ -5,7 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "library/expr_lt.h"
+#include "kernel/expr_maps.h"
+#include "library/expr_unsigned_map.h"
 #include "library/type_context.h"
 
 namespace lean {
@@ -82,16 +83,8 @@ public:
     dependencies, implicit binder info, etc. */
 class fun_info_manager {
     type_context &                         m_ctx;
-    struct unsigned_expr_cmp {
-        int operator()(pair<unsigned, expr> const & p1, pair<unsigned, expr> const & p2) const {
-            if (p1.first != p2.first)
-                return p1.first < p2.first ? -1 : 1;
-            else
-                return expr_quick_cmp()(p1.second, p2.second);
-        }
-    };
-    typedef rb_map<expr, fun_info, expr_quick_cmp>                    cache;
-    typedef rb_map<pair<unsigned, expr>, fun_info, unsigned_expr_cmp> narg_cache;
+    typedef expr_map<fun_info>          cache;
+    typedef expr_unsigned_map<fun_info> narg_cache;
     cache      m_cache_get;
     narg_cache m_cache_get_nargs;
     narg_cache m_cache_get_spec;