From 6b3da2daf457f69b110cd11482773eff1bdf93e6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 8 Nov 2016 15:50:38 -0800 Subject: [PATCH] feat(library/compiler/vm_compiler): save local_info for let-expressions --- src/library/compiler/vm_compiler.cpp | 14 +++++++++----- src/library/vm/vm.cpp | 29 ++++++++++++++++++++++++++++ src/library/vm/vm.h | 23 +++++++++++++++++++--- 3 files changed, 58 insertions(+), 8 deletions(-) diff --git a/src/library/compiler/vm_compiler.cpp b/src/library/compiler/vm_compiler.cpp index 84822b7b08..b7a6aa00a8 100644 --- a/src/library/compiler/vm_compiler.cpp +++ b/src/library/compiler/vm_compiler.cpp @@ -235,6 +235,13 @@ class vm_compiler_fn { } } + optional to_type_info(expr const & t) { + if (!is_neutral_expr(t) && closed(t)) + return some_expr(t); + else + return none_expr(); + } + void compile_let(expr e, unsigned bpz, name_map const & m) { unsigned counter = 0; buffer locals; @@ -242,6 +249,7 @@ class vm_compiler_fn { while (is_let(e)) { counter++; compile(instantiate_rev(let_value(e), locals.size(), locals.data()), bpz, new_m); + emit(mk_local_info_instr(bpz, let_name(e), to_type_info(let_type(e)))); name n = mk_fresh_name(); new_m.insert(n, bpz); locals.push_back(mk_local(n)); @@ -307,11 +315,7 @@ public: m.insert(n, i); locals.push_back(mk_local(n)); bpz++; - if (!is_neutral_expr(binding_domain(e)) && closed(binding_domain(e))) { - args_info = cons(vm_local_info(binding_name(e), some_expr(binding_domain(e))), args_info); - } else { - args_info = cons(vm_local_info(binding_name(e), none_expr()), args_info); - } + args_info = cons(vm_local_info(binding_name(e), to_type_info(binding_domain(e))), args_info); e = binding_body(e); } e = instantiate_rev(e, locals.size(), locals.data()); diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index dad5382877..31d2c56b27 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -246,6 +246,8 @@ void vm_instr::display(std::ostream & out, break; case opcode::Pexpr: out << "pexpr " << *m_expr; break; + case opcode::LocalInfo: + out << "localinfo " << m_local_info->first << " @ " << m_local_idx; break; } } @@ -349,6 +351,13 @@ vm_instr mk_pexpr_instr(expr const & v) { return r; } +vm_instr mk_local_info_instr(unsigned idx, name const & n, optional const & e) { + vm_instr r(opcode::LocalInfo); + r.m_local_idx = idx; + r.m_local_info = new vm_local_info(n, e); + return r; +} + vm_instr mk_ret_instr() { return vm_instr(opcode::Ret); } vm_instr mk_destruct_instr() { return vm_instr(opcode::Destruct); } @@ -459,6 +468,10 @@ void vm_instr::copy_args(vm_instr const & i) { case opcode::Pexpr: m_expr = new expr(*i.m_expr); break; + case opcode::LocalInfo: + m_local_idx = i.m_local_idx; + m_local_info = new vm_local_info(*i.m_local_info); + break; case opcode::Ret: case opcode::Destruct: case opcode::Unreachable: case opcode::Apply: break; @@ -499,6 +512,9 @@ vm_instr::~vm_instr() { case opcode::Pexpr: delete m_expr; break; + case opcode::LocalInfo: + delete m_local_info; + break; default: break; } @@ -571,6 +587,9 @@ void vm_instr::serialize(serializer & s, std::function const & i case opcode::Pexpr: s << *m_expr; break; + case opcode::LocalInfo: + s << m_local_idx << m_local_info->first << m_local_info->second; + break; case opcode::Ret: case opcode::Destruct: case opcode::Unreachable: case opcode::Apply: break; @@ -639,6 +658,12 @@ static vm_instr read_vm_instr(deserializer & d, name_map const & name2 return mk_num_instr(read_mpz(d)); case opcode::Pexpr: return mk_pexpr_instr(read_expr(d)); + case opcode::LocalInfo: { + unsigned idx = d.read_unsigned(); + name n; optional t; + d >> n >> t; + return mk_local_info_instr(idx, n, t); + } case opcode::Ret: return mk_ret_instr(); case opcode::Destruct: @@ -1915,6 +1940,10 @@ void vm_state::run() { m_stack.push_back(to_obj(instr.get_expr())); m_pc++; goto main_loop; + case opcode::LocalInfo: + /* TODO(Leo): debug mode */ + m_pc++; + goto main_loop; case opcode::Destruct: { /** Instruction: destruct diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h index 4efc15b9cb..6e08156411 100644 --- a/src/library/vm/vm.h +++ b/src/library/vm/vm.h @@ -224,13 +224,15 @@ typedef vm_obj (*vm_cfunction_N)(unsigned n, vm_obj const *); the data stored in the object in the buffer \c data. */ typedef unsigned (*vm_cases_function)(vm_obj const & o, buffer & data); +typedef pair> vm_local_info; + /** \brief VM instruction opcode */ enum class opcode { Push, Ret, Drop, Goto, SConstructor, Constructor, Num, Destruct, Cases2, CasesN, NatCases, BuiltinCases, Proj, Apply, InvokeGlobal, InvokeBuiltin, InvokeCFun, - Closure, Unreachable, Pexpr + Closure, Unreachable, Pexpr, LocalInfo }; /** \brief VM instructions */ @@ -263,6 +265,11 @@ class vm_instr { mpz * m_mpz; /* Pexpr */ expr * m_expr; + /* LocalInfo */ + struct { + unsigned m_local_idx; + vm_local_info * m_local_info; + }; }; /* Apply, Ret, Destruct and Unreachable do not have arguments */ friend vm_instr mk_push_instr(unsigned idx); @@ -285,6 +292,7 @@ class vm_instr { friend vm_instr mk_invoke_builtin_instr(unsigned fn_idx); friend vm_instr mk_closure_instr(unsigned fn_idx, unsigned n); friend vm_instr mk_pexpr_instr(expr const & e); + friend vm_instr mk_local_info_instr(unsigned idx, name const & n, optional const & e); void copy_args(vm_instr const & i); public: @@ -384,6 +392,16 @@ public: return *m_expr; } + unsigned get_local_idx() const { + lean_assert(m_op == opcode::LocalInfo); + return m_local_idx; + } + + vm_local_info const & get_local_info() const { + lean_assert(m_op == opcode::LocalInfo); + return *m_local_info; + } + unsigned get_num_pcs() const; unsigned get_pc(unsigned i) const; void set_pc(unsigned i, unsigned pc); @@ -416,14 +434,13 @@ vm_instr mk_invoke_cfun_instr(unsigned fn_idx); vm_instr mk_invoke_builtin_instr(unsigned fn_idx); vm_instr mk_closure_instr(unsigned fn_idx, unsigned n); vm_instr mk_pexpr_instr(expr const & e); +vm_instr mk_local_info_instr(unsigned idx, name const & n, optional const & e); class vm_state; class vm_instr; enum class vm_decl_kind { Bytecode, Builtin, CFun }; -typedef pair> vm_local_info; - /** \brief VM function/constant declaration cell */ struct vm_decl_cell { MK_LEAN_RC();