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

fix(library/compiler/emit_cpp): support for _unreachable

Browse source
This commit is contained in:
Leonardo de Moura 2019-01-31 17:05:52 -08:00
parent a1b65acf3d
commit 94d7b4e094
1 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -291,6 +291,7 @@ struct emit_fn_fn {
void emit_constant(expr const & c) {
lean_assert(is_constant(c));
lean_assert(!is_enf_unreachable(c));
if (optional<name> n = get_builtin_cname(const_name(c)))
m_out << *n;
else if (is_enf_neutral(c))
@ -538,15 +539,18 @@ struct emit_fn_fn {
if (is_lit(val)) {
emit_lit(x, val);
} else if (is_constant(val)) {
emit_lhs(x);
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;
} else if (is_enf_unreachable(val)) {
m_out << "lean_unreachable();\n";
emit_lhs(x); emit_unit(); m_out << ";\n";
} else {
emit_constant(val);
emit_lhs(x); emit_constant(val);
}
m_out << ";\n";
} else if (is_app(val)) {