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

feat(library/compiler/vm_compiler): save local_info for let-expressions

Browse source
This commit is contained in:
Leonardo de Moura 2016-11-08 15:50:38 -08:00
parent d66584f390
commit 6b3da2daf4
3 changed files with 58 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/library/compiler/vm_compiler.cpp
View file

@ -235,6 +235,13 @@ class vm_compiler_fn {
}
}
optional<expr> 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<unsigned> const & m) {
unsigned counter = 0;
buffer<expr> 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());

29
src/library/vm/vm.cpp
View file

@ -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<expr> 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<name(unsigned)> 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<unsigned> 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<expr> 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

23
src/library/vm/vm.h
View file

@ -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<vm_obj> & data);
typedef pair<name, optional<expr>> 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<expr> 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<expr> const & e);
class vm_state;
class vm_instr;
enum class vm_decl_kind { Bytecode, Builtin, CFun };
typedef pair<name, optional<expr>> vm_local_info;
/** \brief VM function/constant declaration cell */
struct vm_decl_cell {
MK_LEAN_RC();