max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(kernel/expr): compress expr_macro representation

Browse source
This commit is contained in:
Leonardo de Moura 2016-12-28 09:01:21 -08:00
parent 80670abb8f
commit caf92bbcc0
2 changed files with 18 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/kernel/expr.cpp
View file

@ -315,17 +315,17 @@ expr_macro::expr_macro(macro_definition const & m, unsigned num, expr const * ar
g),
m_definition(m),
m_num_args(num) {
m_args = new expr[num];
for (unsigned i = 0; i < m_num_args; i++)
m_args[i] = args[i];
expr * data = get_args_ptr();
std::uninitialized_copy(args, args + num, data);
}
void expr_macro::dealloc(buffer<expr_cell*> & todelete) {
for (unsigned i = 0; i < m_num_args; i++) dec_ref(m_args[i], todelete);
delete(this);
}
expr_macro::~expr_macro() {
delete[] m_args;
expr * args = get_args_ptr();
for (unsigned i = 0; i < m_num_args; i++) dec_ref(args[i], todelete);
this->~expr_macro();
char * mem = reinterpret_cast<char*>(this);
delete[] mem;
}
expr_macro::~expr_macro() {}
// =======================================
// Constructors
@ -374,7 +374,8 @@ expr mk_constant(name const & n, levels const & ls, tag g) {
return cache(expr(new (get_const_allocator().allocate()) expr_const(n, ls, g)));
}
expr mk_macro(macro_definition const & m, unsigned num, expr const * args, tag g) {
return cache(expr(new expr_macro(m, num, args, g)));
char * mem = new char[sizeof(expr_macro) + num*sizeof(expr const *)];
return cache(expr(new (mem) expr_macro(m, num, args, g)));
}
expr mk_metavar(name const & n, expr const & t, tag g) {
return cache(expr(new (get_mlocal_allocator().allocate()) expr_mlocal(true, n, t, g)));

11
src/kernel/expr.h
View file

@ -389,18 +389,23 @@ public:
class expr_macro : public expr_composite {
macro_definition m_definition;
unsigned m_num_args;
expr * m_args;
friend class expr_cell;
friend expr copy(expr const & a);
friend expr update_macro(expr const & e, unsigned num, expr const * args);
void dealloc(buffer<expr_cell*> & todelete);
expr * get_args_ptr() {
return reinterpret_cast<expr *>(reinterpret_cast<char *>(this)+sizeof(expr_macro));
}
expr const * get_args_ptr() const {
return reinterpret_cast<expr const *>(reinterpret_cast<char const *>(this)+sizeof(expr_macro));
}
public:
expr_macro(macro_definition const & v, unsigned num, expr const * args, tag g);
~expr_macro();
macro_definition const & get_def() const { return m_definition; }
expr const * get_args() const { return m_args; }
expr const & get_arg(unsigned idx) const { lean_assert(idx < m_num_args); return m_args[idx]; }
expr const * get_args() const { return get_args_ptr(); }
expr const & get_arg(unsigned idx) const { lean_assert(idx < m_num_args); return get_args_ptr()[idx]; }
unsigned get_num_args() const { return m_num_args; }
};