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

chore(library/vm): fix warning

Browse source
This commit is contained in:
Leonardo de Moura 2016-12-20 10:19:20 -08:00
parent f9a61b2b29
commit 5f72e37501
3 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -389,10 +389,10 @@ static environment vm_compile(environment const & env, buffer<procedure> const &
unsigned arity;
std::tie(arity, args_info) = gen(p.m_code);
lean_trace(name({"compiler", "code_gen"}), tout() << " " << p.m_name << " " << arity << "\n";
display_vm_code(tout().get_stream(), new_env, code.size(), code.data()););
display_vm_code(tout().get_stream(), code.size(), code.data()););
optimize(new_env, code);
lean_trace(name({"compiler", "optimize_bytecode"}), tout() << " " << p.m_name << " " << arity << "\n";
display_vm_code(tout().get_stream(), new_env, code.size(), code.data()););
display_vm_code(tout().get_stream(), code.size(), code.data()););
new_env = update_vm_code(new_env, p.m_name, code.size(), code.data(), args_info, p.m_pos);
}
return new_env;

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

@ -3180,7 +3180,7 @@ void vm_state::profiler::snapshots::display(std::ostream & out) const {
}
}
void display_vm_code(std::ostream & out, environment const & env, unsigned code_sz, vm_instr const * code) {
void display_vm_code(std::ostream & out, unsigned code_sz, vm_instr const * code) {
for (unsigned i = 0; i < code_sz; i++) {
out << i << ": ";
code[i].display(out);

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

@ -896,7 +896,7 @@ vm_obj invoke(vm_obj const & fn, unsigned nargs, vm_obj const * args);
vm_obj invoke(unsigned fn_idx, unsigned nargs, vm_obj const * args);
vm_obj invoke(unsigned fn_idx, vm_obj const & arg);
void display_vm_code(std::ostream & out, environment const & env, unsigned code_sz, vm_instr const * code);
void display_vm_code(std::ostream & out, unsigned code_sz, vm_instr const * code);
environment vm_monitor_register(environment const & env, name const & d);