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

fix(library/compiler/emit_cpp): bug handling 0-ary _cnstr

Browse source
This commit is contained in:
Leonardo de Moura 2019-02-01 14:35:40 -08:00
parent d461833fcd
commit d12667fb6b
1 changed files with 3 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/library/compiler/emit_cpp.cpp
View file

@ -430,7 +430,6 @@ struct emit_fn_fn {
}
void emit_cnstr(expr const & x, expr const & fn, buffer<expr> const & args) {
lean_assert(!args.empty());
unsigned cidx, num_usizes, num_bytes;
lean_verify(is_llnf_cnstr(fn, cidx, num_usizes, num_bytes));
emit_alloc_cnstr(x, cidx, args.size(), num_usizes, num_bytes);
@ -544,13 +543,9 @@ struct emit_fn_fn {
if (is_lit(val)) {
emit_lit(x, val);
} else if (is_constant(val)) {
unsigned cidx, d1, d2;
if (is_llnf_cnstr(val, cidx, d1, d2)) {
emit_lhs(x);
if (is_obj(x))
m_out << "lean::box(" << cidx << ")";
else
m_out << cidx;
if (is_llnf_cnstr(val)) {
buffer<expr> args;
emit_cnstr(x, val, args);
} else if (is_enf_unreachable(val)) {
m_out << "lean_unreachable();\n";
emit_lhs(x); emit_unit();