From d12667fb6b365dc11e3a826e6d409addcd785ea8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 1 Feb 2019 14:35:40 -0800 Subject: [PATCH] fix(library/compiler/emit_cpp): bug handling 0-ary `_cnstr` --- src/library/compiler/emit_cpp.cpp | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/src/library/compiler/emit_cpp.cpp b/src/library/compiler/emit_cpp.cpp index 2966b67336..d10582522c 100644 --- a/src/library/compiler/emit_cpp.cpp +++ b/src/library/compiler/emit_cpp.cpp @@ -430,7 +430,6 @@ struct emit_fn_fn { } void emit_cnstr(expr const & x, expr const & fn, buffer 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 args; + emit_cnstr(x, val, args); } else if (is_enf_unreachable(val)) { m_out << "lean_unreachable();\n"; emit_lhs(x); emit_unit();