From 7caa88b61eb495af0cf6ff27f28886676748da29 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 26 Oct 2017 16:23:06 -0700 Subject: [PATCH] refactor(library/vm/vm): remove unnecessary field from vm_decl_cell --- src/library/vm/vm.cpp | 31 ++++++++++++++++++------------- src/library/vm/vm.h | 8 +++----- 2 files changed, 21 insertions(+), 18 deletions(-) diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index 0e5b5a4d64..bfe7328086 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -1009,23 +1009,28 @@ static vm_instr read_vm_instr(deserializer & d) { lean_unreachable(); } +static unsigned get_num_lambdas(expr const & e) { + unsigned r = 0; + expr it = e; + while (is_lambda(it)) { + r++; + it = binding_body(it); + } + return r; +} + vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_function fn): m_rc(0), m_kind(vm_decl_kind::Builtin), m_name(n), m_idx(idx), m_arity(arity), m_fn(fn) {} vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_cfunction fn): m_rc(0), m_kind(vm_decl_kind::CFun), m_name(n), m_idx(idx), m_arity(arity), m_cfn(fn) {} -vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, expr const & e, unsigned code_sz, vm_instr const * code, +vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, unsigned arity, unsigned code_sz, vm_instr const * code, list const & args_info, optional const & pos, optional const & olean): - m_rc(0), m_kind(vm_decl_kind::Bytecode), m_name(n), m_idx(idx), m_expr(e), m_arity(0), + m_rc(0), m_kind(vm_decl_kind::Bytecode), m_name(n), m_idx(idx), m_arity(arity), m_args_info(args_info), m_pos(pos), m_olean(olean), m_code_size(code_sz) { - expr it = e; - while (is_lambda(it)) { - m_arity++; - it = binding_body(it); - } m_code = new vm_instr[code_sz]; for (unsigned i = 0; i < code_sz; i++) m_code[i] = code[i]; @@ -1146,7 +1151,7 @@ struct vm_decls : public environment_extension { unsigned idx = get_vm_index(n); if (m_decls.contains(idx)) throw exception(sstream() << "VM already contains code for '" << n << "'"); - m_decls.insert(idx, vm_decl(n, idx, e, 0, nullptr, list(), optional())); + m_decls.insert(idx, vm_decl(n, idx, get_num_lambdas(e), 0, nullptr, list(), optional())); return idx; } @@ -1284,7 +1289,7 @@ struct vm_code_modification : public modification { void serialize(serializer & s) const override { unsigned code_sz = m_decl.get_code_size(); - s << m_decl.get_name() << m_decl.get_expr() << code_sz << m_decl.get_pos_info(); + s << m_decl.get_name() << m_decl.get_arity() << code_sz << m_decl.get_pos_info(); write_list(s, m_decl.get_args_info()); auto c = m_decl.get_code(); for (unsigned i = 0; i < code_sz; i++) @@ -1292,15 +1297,15 @@ struct vm_code_modification : public modification { } static std::shared_ptr deserialize(deserializer & d) { - name fn; unsigned code_sz; expr e; optional pos; - d >> fn >> e >> code_sz >> pos; + name fn; unsigned arity; unsigned code_sz; optional pos; + d >> fn >> arity >> code_sz >> pos; auto args_info = read_list(d); buffer code; for (unsigned i = 0; i < code_sz; i++) code.emplace_back(read_vm_instr(d)); optional file_name; // TODO(gabriel) return std::make_shared( - vm_decl(fn, get_vm_index(fn), e, code_sz, code.data(), args_info, pos, file_name)); + vm_decl(fn, get_vm_index(fn), arity, code_sz, code.data(), args_info, pos, file_name)); } }; @@ -1335,7 +1340,7 @@ environment reserve_vm_index(environment const & env, name const & fn, expr cons environment update_vm_code(environment const & env, name const & fn, unsigned code_sz, vm_instr const * code, list const & args_info, optional const & pos) { - vm_decl decl(fn, get_vm_index(fn), get_vm_decl(env, fn)->get_expr(), code_sz, code, args_info, pos); + vm_decl decl(fn, get_vm_index(fn), get_vm_decl(env, fn)->get_arity(), code_sz, code, args_info, pos); return module::add_and_perform(env, std::make_shared(decl)); } diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h index 40bd2d2de8..bdd05b41e7 100644 --- a/src/library/vm/vm.h +++ b/src/library/vm/vm.h @@ -534,7 +534,6 @@ struct vm_decl_cell { vm_decl_kind m_kind; name m_name; unsigned m_idx; - expr m_expr; unsigned m_arity; list m_args_info; optional m_pos; @@ -549,7 +548,7 @@ struct vm_decl_cell { }; vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_function fn); vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_cfunction fn); - vm_decl_cell(name const & n, unsigned idx, expr const & e, unsigned code_sz, vm_instr const * code, + vm_decl_cell(name const & n, unsigned idx, unsigned arity, unsigned code_sz, vm_instr const * code, list const & args_info, optional const & pos, optional const & olean); ~vm_decl_cell(); @@ -566,10 +565,10 @@ public: vm_decl(new vm_decl_cell(n, idx, arity, fn)) {} vm_decl(name const & n, unsigned idx, unsigned arity, vm_cfunction 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(name const & n, unsigned idx, unsigned arity, unsigned code_sz, vm_instr const * code, list const & args_info, optional const & pos, optional const & olean = optional()): - vm_decl(new vm_decl_cell(n, idx, e, code_sz, code, args_info, pos, olean)) {} + vm_decl(new vm_decl_cell(n, idx, arity, code_sz, code, args_info, pos, olean)) {} 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(); } @@ -592,7 +591,6 @@ public: vm_instr const * get_code() const { lean_assert(is_bytecode()); return m_ptr->m_code; } vm_function get_fn() const { lean_assert(is_builtin()); return m_ptr->m_fn; } vm_cfunction get_cfn() const { lean_assert(is_cfun()); return m_ptr->m_cfn; } - expr const & get_expr() const { lean_assert(is_bytecode()); return m_ptr->m_expr; } list const & get_args_info() const { lean_assert(is_bytecode()); return m_ptr->m_args_info; } optional const & get_pos_info() const { lean_assert(is_bytecode()); return m_ptr->m_pos; } optional const & get_olean() const { lean_assert(is_bytecode()); return m_ptr->m_olean; }