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 fun_info_manager::get_core(expr const & fn, buffer & } 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 pinfos; auto result_deps = get_core(e, pinfos, std::numeric_limits::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 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 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 const & p1, pair 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 cache; - typedef rb_map, fun_info, unsigned_expr_cmp> narg_cache; + typedef expr_map cache; + typedef expr_unsigned_map narg_cache; cache m_cache_get; narg_cache m_cache_get_nargs; narg_cache m_cache_get_spec;