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

feat(library/vm): store idx at vm_decl

Browse source
This commit is contained in:
Leonardo de Moura 2016-05-11 17:39:49 -07:00
parent 5189a83f57
commit 61471df3eb
2 changed files with 16 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/library/vm.cpp
View file

@ -354,11 +354,11 @@ vm_instr & vm_instr::operator=(vm_instr && s) {
}
vm_decl_cell::vm_decl_cell(name const & n, unsigned arity, vm_function fn):
m_rc(0), m_builtin(true), m_name(n), m_arity(arity), m_fn(fn) {}
vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_function fn):
m_rc(0), m_builtin(true), m_name(n), m_idx(idx), m_arity(arity), m_fn(fn) {}
vm_decl_cell::vm_decl_cell(name const & n, expr const & e, unsigned code_sz, vm_instr const * code):
m_rc(0), m_builtin(false), m_name(n), m_expr(e), m_arity(0),
vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, expr const & e, unsigned code_sz, vm_instr const * code):
m_rc(0), m_builtin(false), m_name(n), m_idx(idx), m_expr(e), m_arity(0),
m_code_size(code_sz) {
expr it = e;
while (is_lambda(it)) {
@ -398,8 +398,7 @@ struct vm_decls : public environment_extension {
void add(vm_decl const & d) {
lean_assert(!m_name2idx.contains(d.get_name()));
unsigned idx = m_decls.size();
m_name2idx.insert(d.get_name(), idx);
m_name2idx.insert(d.get_name(), d.get_idx());
m_decls.push_back(d);
}
@ -407,7 +406,7 @@ struct vm_decls : public environment_extension {
lean_assert(!m_name2idx.contains(n));
unsigned idx = m_decls.size();
m_name2idx.insert(n, idx);
m_decls.push_back(vm_decl(n, e, 0, nullptr));
m_decls.push_back(vm_decl(n, idx, e, 0, nullptr));
return idx;
}
@ -415,14 +414,14 @@ struct vm_decls : public environment_extension {
lean_assert(m_name2idx.contains(n));
unsigned idx = *m_name2idx.find(n);
vm_decl d = m_decls[idx];
m_decls.set(idx, vm_decl(n, d.get_expr(), code_sz, code));
m_decls.set(idx, vm_decl(n, idx, d.get_expr(), code_sz, code));
}
void initialize() {
if (!m_initialized) {
m_initialized = true;
g_vm_builtins->for_each([&](name const & n, pair<unsigned, vm_function> const & p) {
add(vm_decl(n, p.first, p.second));
add(vm_decl(n, m_decls.size(), p.first, p.second));
});
}
}

14
src/library/vm.h
View file

@ -314,6 +314,7 @@ struct vm_decl_cell {
MK_LEAN_RC();
bool m_builtin;
name m_name;
unsigned m_idx;
expr m_expr;
unsigned m_arity;
union {
@ -324,8 +325,8 @@ struct vm_decl_cell {
vm_function m_fn;
};
vm_decl_cell(name const & n, unsigned arity, vm_function fn);
vm_decl_cell(name const & n, expr const & e, unsigned code_sz, vm_instr const * code);
vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_function fn);
vm_decl_cell(name const & n, unsigned idx, expr const & e, unsigned code_sz, vm_instr const * code);
~vm_decl_cell();
void dealloc();
};
@ -336,10 +337,10 @@ class vm_decl {
explicit vm_decl(vm_decl_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); }
public:
vm_decl():m_ptr(nullptr) {}
vm_decl(name const & n, unsigned arity, vm_function fn):
vm_decl(new vm_decl_cell(n, arity, fn)) {}
vm_decl(name const & n, expr const & e, unsigned code_sz, vm_instr const * code):
vm_decl(new vm_decl_cell(n, e, code_sz, code)) {}
vm_decl(name const & n, unsigned idx, unsigned arity, vm_function fn):
vm_decl(new vm_decl_cell(n, idx, arity, fn)) {}
vm_decl(name const & n, unsigned idx, expr const & e, unsigned code_sz, vm_instr const * code):
vm_decl(new vm_decl_cell(n, idx, e, code_sz, code)) {}
vm_decl(vm_decl const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
vm_decl(vm_decl && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
~vm_decl() { if (m_ptr) m_ptr->dec_ref(); }
@ -350,6 +351,7 @@ public:
vm_decl & operator=(vm_decl && s) { LEAN_MOVE_REF(s); }
bool is_builtin() const { lean_assert(m_ptr); return m_ptr->m_builtin; }
unsigned get_idx() const { lean_assert(m_ptr); return m_ptr->m_idx; }
name get_name() const { lean_assert(m_ptr); return m_ptr->m_name; }
unsigned get_arity() const { lean_assert(m_ptr); return m_ptr->m_arity; }
unsigned get_code_size() const { lean_assert(!is_builtin()); return m_ptr->m_code_size; }