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

feat(library/compiler/emit_cpp): use if statement when cases has only 2 cases

Browse source
This commit is contained in:
Leonardo de Moura 2019-01-29 16:32:23 -08:00
parent e4c4eab48e
commit 38172c8f1c
1 changed files with 24 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -363,16 +363,32 @@ struct emit_fn_fn {
buffer<expr> args;
get_app_args(e, args);
expr const & x = args[0];
if (is_obj(x)) {
m_out << "switch (lean::obj_tag("; emit_fvar(x); m_out << ")) {\n";
if (args.size() == 3) {
// use if-statement
if (is_obj(x)) {
m_out << "if (lean::obj_tag("; emit_fvar(x); m_out << ") == 0)\n";
} else {
m_out << "if ("; emit_fvar(x); m_out << " == 0)\n";
}
emit(args[1]);
m_out << "else\n";
emit(args[2]);
} else {
m_out << "switch ("; emit_fvar(x); m_out << ") {\n";
if (is_obj(x)) {
m_out << "switch (lean::obj_tag("; emit_fvar(x); m_out << ")) {\n";
} else {
m_out << "switch ("; emit_fvar(x); m_out << ") {\n";
}
for (unsigned i = 1; i < args.size(); i++) {
if (i == args.size() - 1)
m_out << "default:\n";
else
m_out << "case " << (i-1) << ":\n";
emit(args[i]);
}
m_out << "}\n";
}
for (unsigned i = 1; i < args.size(); i++) {
m_out << "case " << (i-1) << ":\n";
emit(args[i]);
}
m_out << "}\n";
}
void emit_jmp(expr const & e) {