From 7683188ab0bcc10befa75b59088a50312d12fa24 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 10 Nov 2013 11:09:04 -0800 Subject: [PATCH] chore(emplace_back): use emplace_back when appropriate Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser.cpp | 4 ++-- src/frontends/lean/pp.cpp | 8 ++++---- src/kernel/environment.cpp | 6 +++--- src/tests/kernel/expr.cpp | 16 ++++++++-------- src/util/buffer.h | 8 ++++++++ src/util/scoped_map.h | 6 +++--- src/util/scoped_set.h | 4 ++-- src/util/splay_tree.h | 6 +++--- 8 files changed, 33 insertions(+), 25 deletions(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 4167c8f26..d6ec2653f 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -681,7 +681,7 @@ class parser::imp { */ void parse_names(buffer> & result) { while (curr_is_identifier()) { - result.push_back(mk_pair(pos(), curr_name())); + result.emplace_back(pos(), curr_name()); next(); } } @@ -873,7 +873,7 @@ class parser::imp { check_assign_next("invalid let expression, ':=' expected"); expr val = parse_expr(); register_binding(id); - bindings.push_back(std::make_tuple(p, id, type, val)); + bindings.emplace_back(p, id, type, val); if (curr_is_in()) { next(); expr r = parse_expr(); diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 2c528bb0e..916537363 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -312,7 +312,7 @@ class pp_fn { expr lambda = arg(e, 2); name n1 = get_unused_name(lambda); 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); if (is_quant_expr(b, is_forall)) return collect_nested_quantifiers(b, is_forall, r); @@ -730,7 +730,7 @@ class pp_fn { if (e.kind() == k && (!T || is_abstraction(T))) { name n1 = get_unused_name(e); 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); if (T) T = replace_var_with_name(abst_body(T), n1); @@ -965,7 +965,7 @@ class pp_fn { if (is_let(e)) { name n1 = get_unused_name(e); 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); return collect_nested_let(b, bindings); } else { @@ -1102,7 +1102,7 @@ class pp_fn { 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); 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 r; diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 1dcb3ce01..c773beacc 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -217,10 +217,10 @@ struct environment::imp { level const & l3 = std::get<1>(c); int u_l3_d = safe_add(d, std::get<2>(c)); 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) { m_constraints.push_back(c); } @@ -275,7 +275,7 @@ struct environment::imp { \brief Initialize the set of universe variables with bottom */ void init_uvars() { - m_uvars.push_back(level()); + m_uvars.emplace_back(); } /** diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index 18e88b837..77a7c246f 100644 --- a/src/tests/kernel/expr.cpp +++ b/src/tests/kernel/expr.cpp @@ -96,7 +96,7 @@ unsigned depth2(expr const & e) { unsigned depth3(expr const & e) { static std::vector> todo; unsigned m = 0; - todo.push_back(std::make_pair(&e, 0)); + todo.emplace_back(&e, 0); while (!todo.empty()) { auto const & p = todo.back(); expr const & e = *(p.first); @@ -110,20 +110,20 @@ unsigned depth3(expr const & e) { case expr_kind::App: { unsigned num = num_args(e); 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; } case expr_kind::Eq: - todo.push_back(std::make_pair(&eq_lhs(e), c)); - todo.push_back(std::make_pair(&eq_rhs(e), c)); + todo.emplace_back(&eq_lhs(e), c); + todo.emplace_back(&eq_rhs(e), c); break; case expr_kind::Lambda: case expr_kind::Pi: - todo.push_back(std::make_pair(&abst_domain(e), c)); - todo.push_back(std::make_pair(&abst_body(e), c)); + todo.emplace_back(&abst_domain(e), c); + todo.emplace_back(&abst_body(e), c); break; case expr_kind::Let: - todo.push_back(std::make_pair(&let_value(e), c)); - todo.push_back(std::make_pair(&let_body(e), c)); + todo.emplace_back(&let_value(e), c); + todo.emplace_back(&let_body(e), c); break; } } diff --git a/src/util/buffer.h b/src/util/buffer.h index 124db7599..b9c110f78 100644 --- a/src/util/buffer.h +++ b/src/util/buffer.h @@ -110,6 +110,14 @@ public: m_pos++; } + template + void emplace_back(Args&&... args) { + if (m_pos >= m_capacity) + expand(); + new (m_buffer + m_pos) T(args...); + m_pos++; + } + void pop_back() { back().~T(); m_pos--; diff --git a/src/util/scoped_map.h b/src/util/scoped_map.h index 9dfa9bb40..618b81683 100644 --- a/src/util/scoped_map.h +++ b/src/util/scoped_map.h @@ -108,11 +108,11 @@ public: auto it = m_map.find(k); if (it == m_map.end()) { 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)); } else { 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; } } @@ -126,7 +126,7 @@ public: if (!at_base_lvl()) { auto it = m_map.find(k); 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); } diff --git a/src/util/scoped_set.h b/src/util/scoped_set.h index 9ec018e04..f9d9ce78e 100644 --- a/src/util/scoped_set.h +++ b/src/util/scoped_set.h @@ -91,7 +91,7 @@ public: void insert(Key const & k) { if (!at_base_lvl()) { 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); } @@ -100,7 +100,7 @@ public: void erase(Key const & k) { if (!at_base_lvl()) { 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); } diff --git a/src/util/splay_tree.h b/src/util/splay_tree.h index 2c65f2cb3..9e90d7362 100644 --- a/src/util/splay_tree.h +++ b/src/util/splay_tree.h @@ -246,10 +246,10 @@ class splay_tree : public CMP { lean_assert(!n->is_shared()); int c = cmp(v, n->m_value); if (c < 0) { - path.push_back(entry(false, n)); + path.emplace_back(false, n); n = n->m_left; } else if (c > 0) { - path.push_back(entry(true, n)); + path.emplace_back(true, n); n = n->m_right; } else { if (is_insert) @@ -280,7 +280,7 @@ class splay_tree : public CMP { update_parent(path, n); } if (n->m_right) { - path.push_back(entry(true, n)); + path.emplace_back(true, n); n = n->m_right; } else { splay_to_top(path, n);