michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/fun_info_manager): use expr_unsigned_map

Browse source
This commit is contained in:
Leonardo de Moura 2016-01-06 17:29:22 -08:00
parent 7312dd77b8
commit 9a1a9f3b5a
2 changed files with 18 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/library/fun_info_manager.cpp
View file

@ -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;
}
}

15
src/library/fun_info_manager.h
View file

@ -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;