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

fix(library/compiler/vm_compiler): bytecode generation error

Browse source 
This bug was introduced by commit 2bd400964c
when we decided to store arguments in reverse order.
This commit is contained in:
Leonardo de Moura 2017-01-12 08:44:37 -08:00
parent 1f2b8745dc
commit 1977b4ff3f
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -219,8 +219,8 @@ class vm_compiler_fn {
buffer<expr> args;
expr fn = get_app_args(e, args);
if (!is_constant(fn)) {
compile_rev_args(args.size(), args.data(), bpz+1, m);
compile(fn, bpz, m);
compile_rev_args(args.size(), args.data(), bpz, m);
compile(fn, bpz + args.size(), m);
emit_apply_instr(args.size());
return;
} else if (is_constant(fn)) {