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

feat(library/compiler/emit_cpp): "merge" the case with most occurrences as default:

Browse source
This commit is contained in:
Leonardo de Moura 2019-02-16 12:27:25 -08:00
parent 54985b5a0e
commit e98acc86b8
1 changed files with 25 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -674,6 +674,25 @@ struct emit_fn_fn {
}
}
expr find_max_occs(unsigned sz, expr const * es) {
lean_assert(sz > 0);
expr r = es[sz-1];
unsigned r_noccs = 1;
for (unsigned i = 0; i < sz; i++) {
expr curr = es[i];
unsigned curr_noccs = 1;
for (unsigned j = i+1; j < sz; j++) {
if (es[j] == curr)
curr_noccs++;
}
if (curr_noccs > r_noccs) {
r = curr;
r_noccs = curr_noccs;
}
}
return r;
}
void emit_cases(expr const & e) {
lean_assert(is_cases_on_app(m_env, e));
buffer<expr> args;
@ -695,13 +714,15 @@ struct emit_fn_fn {
} else {
m_out << "switch ("; emit_fvar(x); m_out << ") {\n";
}
expr def = find_max_occs(args.size() - 1, args.data() + 1);
for (unsigned i = 1; i < args.size(); i++) {
if (i == args.size() - 1)
m_out << "default:\n";
else
if (args[i] != def) {
m_out << "case " << (i-1) << ":\n";
emit(args[i]);
emit(args[i]);
}
}
m_out << "default:\n";
emit(def);
m_out << "}\n";
}
}