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

refactor(util): rename fixed_size_allocator to memory_pool

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-22 07:49:40 -07:00
parent b7838f5db7
commit c8b6f0c7fb
2 changed files with 12 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/kernel/expr.cpp
View file

@ -15,7 +15,7 @@ Author: Leonardo de Moura
#include "util/buffer.h"
#include "util/object_serializer.h"
#include "util/lru_cache.h"
#include "util/fixed_size_allocator.h"
#include "util/memory_pool.h"
#include "kernel/expr.h"
#include "kernel/expr_eq_fn.h"
#include "kernel/free_vars.h"
@ -94,7 +94,7 @@ bool is_meta(expr const & e) {
}
// Expr variables
typedef fixed_size_allocator<sizeof(expr_var)> var_allocator;
typedef memory_pool<sizeof(expr_var)> var_allocator;
MK_THREAD_LOCAL_GET_DEF(var_allocator, get_var_allocator);
expr_var::expr_var(unsigned idx):
expr_cell(expr_kind::Var, idx, false, false, false, false),
@ -108,7 +108,7 @@ void expr_var::dealloc() {
}
// Expr constants
typedef fixed_size_allocator<sizeof(expr_const)> const_allocator;
typedef memory_pool<sizeof(expr_const)> const_allocator;
MK_THREAD_LOCAL_GET_DEF(const_allocator, get_const_allocator);
expr_const::expr_const(name const & n, levels const & ls):
expr_cell(expr_kind::Constant, ::lean::hash(n.hash(), hash_levels(ls)), false, has_meta(ls), false, has_param(ls)),
@ -121,7 +121,7 @@ void expr_const::dealloc() {
}
// Expr metavariables and local variables
typedef fixed_size_allocator<sizeof(expr_mlocal)> mlocal_allocator;
typedef memory_pool<sizeof(expr_mlocal)> mlocal_allocator;
MK_THREAD_LOCAL_GET_DEF(mlocal_allocator, get_mlocal_allocator);
expr_mlocal::expr_mlocal(bool is_meta, name const & n, expr const & t):
expr_composite(is_meta ? expr_kind::Meta : expr_kind::Local, n.hash(), is_meta || t.has_expr_metavar(), t.has_univ_metavar(),
@ -135,7 +135,7 @@ void expr_mlocal::dealloc(buffer<expr_cell*> & todelete) {
get_mlocal_allocator().recyle(this);
}
typedef fixed_size_allocator<sizeof(expr_local)> local_allocator;
typedef memory_pool<sizeof(expr_local)> local_allocator;
MK_THREAD_LOCAL_GET_DEF(local_allocator, get_local_allocator);
expr_local::expr_local(name const & n, name const & pp_name, expr const & t, binder_info const & bi):
expr_mlocal(false, n, t),
@ -155,7 +155,7 @@ expr_composite::expr_composite(expr_kind k, unsigned h, bool has_expr_mv, bool h
m_free_var_range(fv_range) {}
// Expr applications
typedef fixed_size_allocator<sizeof(expr_app)> app_allocator;
typedef memory_pool<sizeof(expr_app)> app_allocator;
MK_THREAD_LOCAL_GET_DEF(app_allocator, get_app_allocator);
expr_app::expr_app(expr const & fn, expr const & arg):
expr_composite(expr_kind::App, ::lean::hash(fn.hash(), arg.hash()),
@ -186,7 +186,7 @@ bool operator==(binder_info const & i1, binder_info const & i2) {
}
// Expr binders (Lambda, Pi)
typedef fixed_size_allocator<sizeof(expr_binding)> binding_allocator;
typedef memory_pool<sizeof(expr_binding)> binding_allocator;
MK_THREAD_LOCAL_GET_DEF(binding_allocator, get_binding_allocator);
expr_binding::expr_binding(expr_kind k, name const & n, expr const & t, expr const & b, binder_info const & i):
expr_composite(k, ::lean::hash(t.hash(), b.hash()),
@ -209,7 +209,7 @@ void expr_binding::dealloc(buffer<expr_cell*> & todelete) {
}
// Expr Sort
typedef fixed_size_allocator<sizeof(expr_sort)> sort_allocator;
typedef memory_pool<sizeof(expr_sort)> sort_allocator;
MK_THREAD_LOCAL_GET_DEF(sort_allocator, get_sort_allocator);
expr_sort::expr_sort(level const & l):
expr_cell(expr_kind::Sort, ::lean::hash(l), false, has_meta(l), false, has_param(l)),

7
src/util/fixed_size_allocator.h → src/util/memory_pool.h
View file

@ -8,12 +8,13 @@ Author: Leonardo de Moura
#include "util/memory.h"
namespace lean {
/** \brief Auxiliary object for "recycling" allocated memory of fixed size */
template<unsigned Size>
class fixed_size_allocator {
class memory_pool {
void * m_free_list;
public:
fixed_size_allocator():m_free_list(nullptr) {}
~fixed_size_allocator() {
memory_pool():m_free_list(nullptr) {}
~memory_pool() {
while (m_free_list != nullptr) {
void * r = m_free_list;
m_free_list = *(reinterpret_cast<void **>(r));