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

fix(library/compiler/vm_compiler): missing case

Browse source
This commit is contained in:
Leonardo de Moura 2018-06-05 11:03:49 -07:00
parent 0dd25b0a24
commit 8ae42417eb
2 changed files with 2 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -211,6 +211,8 @@ class vm_compiler_fn {
} else if (is_constant(fn)) {
if (is_neutral_expr(fn)) {
emit(mk_sconstructor_instr(0));
} else if (is_unreachable_expr(fn)) {
emit(mk_unreachable_instr());
} else if (optional<vm_decl> decl = get_vm_decl(m_env, const_name(fn))) {
compile_global(*decl, args.size(), args.data(), bpz, m);
} else {

4
tests/lean/macro1.lean.expected.out
View file

@ -1,7 +1,3 @@
macro1.lean:8:4: warning: failed to generate bytecode for 'lambda_macro'
code generation failed, VM does not have code for '_unreachable_'
macro1.lean:23:4: warning: failed to generate bytecode for 'ref_macro'
code generation failed, VM does not have code for '_unreachable_'
(0: node lambda (1: ident x) (2: node ref (3: ident x)))
((0: node lambda (1: ident x) (2: node ref (3: ident x))), ⟨3 ← ((inl 1), x)⟩)
(0: node lambda (1: ident x) (5: node lambda (6: ident x from 0) (2: node ref (3: ident x))))