michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(emplace_back): use emplace_back when appropriate

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-10 11:09:04 -08:00
parent 8c140ff86f
commit 7683188ab0
8 changed files with 33 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/parser.cpp
View file

@ -681,7 +681,7 @@ class parser::imp {
*/ */
void parse_names(buffer<std::pair<pos_info, name>> & result) { void parse_names(buffer<std::pair<pos_info, name>> & result) {
while (curr_is_identifier()) { while (curr_is_identifier()) {
result.push_back(mk_pair(pos(), curr_name())); result.emplace_back(pos(), curr_name());
next(); next();
} }
} }
@ -873,7 +873,7 @@ class parser::imp {
check_assign_next("invalid let expression, ':=' expected"); check_assign_next("invalid let expression, ':=' expected");
expr val = parse_expr(); expr val = parse_expr();
register_binding(id); register_binding(id);
bindings.push_back(std::make_tuple(p, id, type, val)); bindings.emplace_back(p, id, type, val);
if (curr_is_in()) { if (curr_is_in()) {
next(); next();
expr r = parse_expr(); expr r = parse_expr();

8
src/frontends/lean/pp.cpp
View file

@ -312,7 +312,7 @@ class pp_fn {
expr lambda = arg(e, 2); expr lambda = arg(e, 2);
name n1 = get_unused_name(lambda); name n1 = get_unused_name(lambda);
m_local_names.insert(n1); m_local_names.insert(n1);
r.push_back(mk_pair(n1, abst_domain(lambda))); r.emplace_back(n1, abst_domain(lambda));
expr b = replace_var_with_name(abst_body(lambda), n1); expr b = replace_var_with_name(abst_body(lambda), n1);
if (is_quant_expr(b, is_forall)) if (is_quant_expr(b, is_forall))
return collect_nested_quantifiers(b, is_forall, r); return collect_nested_quantifiers(b, is_forall, r);
@ -730,7 +730,7 @@ class pp_fn {
if (e.kind() == k && (!T || is_abstraction(T))) { if (e.kind() == k && (!T || is_abstraction(T))) {
name n1 = get_unused_name(e); name n1 = get_unused_name(e);
m_local_names.insert(n1); m_local_names.insert(n1);
r.push_back(mk_pair(n1, abst_domain(e))); r.emplace_back(n1, abst_domain(e));
expr b = replace_var_with_name(abst_body(e), n1); expr b = replace_var_with_name(abst_body(e), n1);
if (T) if (T)
T = replace_var_with_name(abst_body(T), n1); T = replace_var_with_name(abst_body(T), n1);
@ -965,7 +965,7 @@ class pp_fn {
if (is_let(e)) { if (is_let(e)) {
name n1 = get_unused_name(e); name n1 = get_unused_name(e);
m_local_names.insert(n1); m_local_names.insert(n1);
bindings.push_back(std::make_tuple(n1, let_type(e), let_value(e))); bindings.emplace_back(n1, let_type(e), let_value(e));
expr b = replace_var_with_name(let_body(e), n1); expr b = replace_var_with_name(let_body(e), n1);
return collect_nested_let(b, bindings); return collect_nested_let(b, bindings);
} else { } else {
@ -1102,7 +1102,7 @@ class pp_fn {
if (!main && m_extra_lets && is_shared(e) && r.second > m_alias_min_weight) { if (!main && m_extra_lets && is_shared(e) && r.second > m_alias_min_weight) {
name new_aux = name(m_aux, m_aliases_defs.size()+1); name new_aux = name(m_aux, m_aliases_defs.size()+1);
m_aliases.insert(e, new_aux); m_aliases.insert(e, new_aux);
m_aliases_defs.push_back(mk_pair(new_aux, r.first)); m_aliases_defs.emplace_back(new_aux, r.first);
return mk_result(format(new_aux), 1); return mk_result(format(new_aux), 1);
} }
return r; return r;

6
src/kernel/environment.cpp
View file

@ -217,10 +217,10 @@ struct environment::imp {
level const & l3 = std::get<1>(c); level const & l3 = std::get<1>(c);
int u_l3_d = safe_add(d, std::get<2>(c)); int u_l3_d = safe_add(d, std::get<2>(c));
if (!is_implied(u, l3, u_l3_d)) if (!is_implied(u, l3, u_l3_d))
to_add.push_back(constraint(u, l3, u_l3_d)); to_add.emplace_back(u, l3, u_l3_d);
} }
} }
m_constraints.push_back(constraint(u, v, d)); m_constraints.emplace_back(u, v, d);
for (constraint const & c : to_add) { for (constraint const & c : to_add) {
m_constraints.push_back(c); m_constraints.push_back(c);
} }
@ -275,7 +275,7 @@ struct environment::imp {
\brief Initialize the set of universe variables with bottom \brief Initialize the set of universe variables with bottom
*/ */
void init_uvars() { void init_uvars() {
m_uvars.push_back(level()); m_uvars.emplace_back();
} }
/** /**

16
src/tests/kernel/expr.cpp
View file

@ -96,7 +96,7 @@ unsigned depth2(expr const & e) {
unsigned depth3(expr const & e) { unsigned depth3(expr const & e) {
static std::vector<std::pair<expr const *, unsigned>> todo; static std::vector<std::pair<expr const *, unsigned>> todo;
unsigned m = 0; unsigned m = 0;
todo.push_back(std::make_pair(&e, 0)); todo.emplace_back(&e, 0);
while (!todo.empty()) { while (!todo.empty()) {
auto const & p = todo.back(); auto const & p = todo.back();
expr const & e = *(p.first); expr const & e = *(p.first);
@ -110,20 +110,20 @@ unsigned depth3(expr const & e) {
case expr_kind::App: { case expr_kind::App: {
unsigned num = num_args(e); unsigned num = num_args(e);
for (unsigned i = 0; i < num; i++) for (unsigned i = 0; i < num; i++)
todo.push_back(std::make_pair(&arg(e, i), c)); todo.emplace_back(&arg(e, i), c);
break; break;
} }
case expr_kind::Eq: case expr_kind::Eq:
todo.push_back(std::make_pair(&eq_lhs(e), c)); todo.emplace_back(&eq_lhs(e), c);
todo.push_back(std::make_pair(&eq_rhs(e), c)); todo.emplace_back(&eq_rhs(e), c);
break; break;
case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Lambda: case expr_kind::Pi:
todo.push_back(std::make_pair(&abst_domain(e), c)); todo.emplace_back(&abst_domain(e), c);
todo.push_back(std::make_pair(&abst_body(e), c)); todo.emplace_back(&abst_body(e), c);
break; break;
case expr_kind::Let: case expr_kind::Let:
todo.push_back(std::make_pair(&let_value(e), c)); todo.emplace_back(&let_value(e), c);
todo.push_back(std::make_pair(&let_body(e), c)); todo.emplace_back(&let_body(e), c);
break; break;
} }
} }

8
src/util/buffer.h
View file

@ -110,6 +110,14 @@ public:
m_pos++; m_pos++;
} }
template<typename... Args>
void emplace_back(Args&&... args) {
if (m_pos >= m_capacity)
expand();
new (m_buffer + m_pos) T(args...);
m_pos++;
}
void pop_back() { void pop_back() {
back().~T(); back().~T();
m_pos--; m_pos--;

6
src/util/scoped_map.h
View file

@ -108,11 +108,11 @@ public:
auto it = m_map.find(k); auto it = m_map.find(k);
if (it == m_map.end()) { if (it == m_map.end()) {
if (!at_base_lvl()) if (!at_base_lvl())
m_actions.push_back(std::make_pair(action_kind::Insert, value_type(k, T()))); m_actions.emplace_back(action_kind::Insert, value_type(k, T()));
m_map.insert(value_type(k, v)); m_map.insert(value_type(k, v));
} else { } else {
if (!at_base_lvl()) if (!at_base_lvl())
m_actions.push_back(std::make_pair(action_kind::Replace, *it)); m_actions.emplace_back(action_kind::Replace, *it);
it->second = v; it->second = v;
} }
} }
@ -126,7 +126,7 @@ public:
if (!at_base_lvl()) { if (!at_base_lvl()) {
auto it = m_map.find(k); auto it = m_map.find(k);
if (m_map.find(k) != m_map.end()) if (m_map.find(k) != m_map.end())
m_actions.push_back(std::make_pair(action_kind::Erase, *it)); m_actions.emplace_back(action_kind::Erase, *it);
} }
m_map.erase(k); m_map.erase(k);
} }

4
src/util/scoped_set.h
View file

@ -91,7 +91,7 @@ public:
void insert(Key const & k) { void insert(Key const & k) {
if (!at_base_lvl()) { if (!at_base_lvl()) {
if (m_set.find(k) == m_set.end()) if (m_set.find(k) == m_set.end())
m_actions.push_back(std::make_pair(action_kind::Insert, k)); m_actions.emplace_back(action_kind::Insert, k);
} }
m_set.insert(k); m_set.insert(k);
} }
@ -100,7 +100,7 @@ public:
void erase(Key const & k) { void erase(Key const & k) {
if (!at_base_lvl()) { if (!at_base_lvl()) {
if (m_set.find(k) != m_set.end()) if (m_set.find(k) != m_set.end())
m_actions.push_back(std::make_pair(action_kind::Erase, k)); m_actions.emplace_back(action_kind::Erase, k);
} }
m_set.erase(k); m_set.erase(k);
} }

6
src/util/splay_tree.h
View file

@ -246,10 +246,10 @@ class splay_tree : public CMP {
lean_assert(!n->is_shared()); lean_assert(!n->is_shared());
int c = cmp(v, n->m_value); int c = cmp(v, n->m_value);
if (c < 0) { if (c < 0) {
path.push_back(entry(false, n)); path.emplace_back(false, n);
n = n->m_left; n = n->m_left;
} else if (c > 0) { } else if (c > 0) {
path.push_back(entry(true, n)); path.emplace_back(true, n);
n = n->m_right; n = n->m_right;
} else { } else {
if (is_insert) if (is_insert)
@ -280,7 +280,7 @@ class splay_tree : public CMP {
update_parent(path, n); update_parent(path, n);
} }
if (n->m_right) { if (n->m_right) {
path.push_back(entry(true, n)); path.emplace_back(true, n);
n = n->m_right; n = n->m_right;
} else { } else {
splay_to_top(path, n); splay_to_top(path, n);