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

refactor(kernel): move instantiate_univ_cache to separate .h file

Browse source
This commit is contained in:
Leonardo de Moura 2015-09-21 16:08:34 -07:00
parent 9c09b0750b
commit 4cfebe7f1c
2 changed files with 45 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

33
src/kernel/instantiate.cpp
View file

@ -11,6 +11,7 @@ Author: Leonardo de Moura
#include "kernel/replace_fn.h"
#include "kernel/declaration.h"
#include "kernel/instantiate.h"
#include "kernel/instantiate_univ_cache.h"
#ifndef LEAN_INST_UNIV_CACHE_SIZE
#define LEAN_INST_UNIV_CACHE_SIZE 1023
@ -139,36 +140,8 @@ expr instantiate_univ_params(expr const & e, level_param_names const & ps, level
});
}
class instantiate_univ_cache {
typedef std::tuple<declaration, levels, expr> entry;
std::vector<optional<entry>> m_cache;
public:
instantiate_univ_cache() {
m_cache.resize(LEAN_INST_UNIV_CACHE_SIZE);
}
optional<expr> is_cached(declaration const & d, levels const & ls) {
unsigned idx = d.get_name().hash() % LEAN_INST_UNIV_CACHE_SIZE;
if (auto it = m_cache[idx]) {
declaration d_c; levels ls_c; expr r_c;
std::tie(d_c, ls_c, r_c) = *it;
if (!is_eqp(d_c, d))
return none_expr();
if (ls == ls_c)
return some_expr(r_c);
else
return none_expr();
}
return none_expr();
}
void save(declaration const & d, levels const & ls, expr const & r) {
unsigned idx = d.get_name().hash() % LEAN_INST_UNIV_CACHE_SIZE;
m_cache[idx] = entry(d, ls, r);
}
};
MK_THREAD_LOCAL_GET_DEF(instantiate_univ_cache, get_type_univ_cache);
MK_THREAD_LOCAL_GET_DEF(instantiate_univ_cache, get_value_univ_cache);
MK_THREAD_LOCAL_GET(instantiate_univ_cache, get_type_univ_cache, LEAN_INST_UNIV_CACHE_SIZE);
MK_THREAD_LOCAL_GET(instantiate_univ_cache, get_value_univ_cache, LEAN_INST_UNIV_CACHE_SIZE);
expr instantiate_type_univ_params(declaration const & d, levels const & ls) {
lean_assert(d.get_num_univ_params() == length(ls));

42
src/kernel/instantiate_univ_cache.h Normal file
View file

@ -0,0 +1,42 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <algorithm>
#include <limits>
#include <vector>
#include "kernel/declaration.h"
namespace lean {
class instantiate_univ_cache {
typedef std::tuple<declaration, levels, expr> entry;
std::vector<optional<entry>> m_cache;
public:
instantiate_univ_cache(unsigned capacity) {
m_cache.resize(capacity);
}
optional<expr> is_cached(declaration const & d, levels const & ls) {
unsigned idx = d.get_name().hash() % m_cache.size();
if (auto it = m_cache[idx]) {
declaration d_c; levels ls_c; expr r_c;
std::tie(d_c, ls_c, r_c) = *it;
if (!is_eqp(d_c, d))
return none_expr();
if (ls == ls_c)
return some_expr(r_c);
else
return none_expr();
}
return none_expr();
}
void save(declaration const & d, levels const & ls, expr const & r) {
unsigned idx = d.get_name().hash() % m_cache.size();
m_cache[idx] = entry(d, ls, r);
}
};
}