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

chore(library/compiler/emit_cpp): unnecessary line break

Browse source
This commit is contained in:
Leonardo de Moura 2019-02-03 19:19:01 -08:00
parent 79e8358f9c
commit 67f4fb603d
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -703,6 +703,7 @@ struct emit_fn_fn {
buffer<expr> jps;
buffer<expr> locals;
buffer<expr> instrs;
bool declared_vars = false;
while (is_let(e)) {
expr v = instantiate_rev(let_value(e), locals.size(), locals.data());
if (is_join_point_name(let_name(e))) {
@ -712,6 +713,7 @@ struct emit_fn_fn {
jp_vars.push_back(y);
/* Declare join point parameter, we need them to implement join point calls in this block. */
m_out << to_cpp_type(binding_domain(v)) << " "; emit_fvar(y); m_out << "; ";
declared_vars = true;
v = binding_body(v);
}
v = instantiate_rev(v, jp_vars.size(), jp_vars.data());
@ -730,6 +732,7 @@ struct emit_fn_fn {
Remark: variables of type `_void` are used to store instructions that do
not return any value. */
m_out << to_cpp_type(let_type(e)) << " "; emit_fvar(x); m_out << "; ";
declared_vars = true;
}
instrs.push_back(x);
}
@ -737,7 +740,8 @@ struct emit_fn_fn {
e = let_body(e);
}
e = instantiate_rev(e, locals.size(), locals.data());
m_out << "\n";
if (declared_vars)
m_out << "\n";
/* emit instructions */
for (expr const & x : instrs) {
local_decl d = m_lctx.get_local_decl(x);