From 2c002718e067bbf3060a33ced19fe952994a4a35 Mon Sep 17 00:00:00 2001 From: Clement Courbet Date: Fri, 2 Aug 2024 19:55:03 +0200 Subject: [PATCH] =?UTF-8?q?perf:=20fix=20implementation=20of=20move=20cons?= =?UTF-8?q?tructors=20and=20move=20assignment=20ope=E2=80=A6=20(#4700)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit …rators Right now those constructors result in a copy instead of the desired move. We've measured that expr copying and assignment by itself uses around 10% of total runtime on our workloads. See #4698 for details. --- src/kernel/declaration.h | 56 ++++++++++++++--------------- src/kernel/expr.h | 8 ++--- src/kernel/level.h | 4 +-- src/kernel/local_ctx.h | 8 ++--- src/library/compiler/specialize.cpp | 4 +-- src/library/projection.h | 4 +-- src/runtime/array_ref.h | 4 +-- src/runtime/list_ref.h | 4 +-- src/runtime/option_ref.h | 4 +-- src/runtime/optional.h | 16 ++++----- src/runtime/string_ref.h | 4 +-- src/util/kvmap.h | 4 +-- src/util/name.h | 4 +-- src/util/nat.h | 4 +-- 14 files changed, 64 insertions(+), 64 deletions(-) diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h index cf45393b43..9b636ae0a8 100644 --- a/src/kernel/declaration.h +++ b/src/kernel/declaration.h @@ -63,9 +63,9 @@ class constant_val : public object_ref { public: constant_val(name const & n, names const & lparams, expr const & type); constant_val(constant_val const & other):object_ref(other) {} - constant_val(constant_val && other):object_ref(other) {} + constant_val(constant_val && other):object_ref(std::move(other)) {} constant_val & operator=(constant_val const & other) { object_ref::operator=(other); return *this; } - constant_val & operator=(constant_val && other) { object_ref::operator=(other); return *this; } + constant_val & operator=(constant_val && other) { object_ref::operator=(std::move(other)); return *this; } name const & get_name() const { return static_cast(cnstr_get_ref(*this, 0)); } names const & get_lparams() const { return static_cast(cnstr_get_ref(*this, 1)); } expr const & get_type() const { return static_cast(cnstr_get_ref(*this, 2)); } @@ -79,9 +79,9 @@ class axiom_val : public object_ref { public: axiom_val(name const & n, names const & lparams, expr const & type, bool is_unsafe); axiom_val(axiom_val const & other):object_ref(other) {} - axiom_val(axiom_val && other):object_ref(other) {} + axiom_val(axiom_val && other):object_ref(std::move(other)) {} axiom_val & operator=(axiom_val const & other) { object_ref::operator=(other); return *this; } - axiom_val & operator=(axiom_val && other) { object_ref::operator=(other); return *this; } + axiom_val & operator=(axiom_val && other) { object_ref::operator=(std::move(other)); return *this; } constant_val const & to_constant_val() const { return static_cast(cnstr_get_ref(*this, 0)); } name const & get_name() const { return to_constant_val().get_name(); } names const & get_lparams() const { return to_constant_val().get_lparams(); } @@ -105,9 +105,9 @@ class definition_val : public object_ref { public: definition_val(name const & n, names const & lparams, expr const & type, expr const & val, reducibility_hints const & hints, definition_safety safety, names const & all); definition_val(definition_val const & other):object_ref(other) {} - definition_val(definition_val && other):object_ref(other) {} + definition_val(definition_val && other):object_ref(std::move(other)) {} definition_val & operator=(definition_val const & other) { object_ref::operator=(other); return *this; } - definition_val & operator=(definition_val && other) { object_ref::operator=(other); return *this; } + definition_val & operator=(definition_val && other) { object_ref::operator=(std::move(other)); return *this; } constant_val const & to_constant_val() const { return static_cast(cnstr_get_ref(*this, 0)); } name const & get_name() const { return to_constant_val().get_name(); } names const & get_lparams() const { return to_constant_val().get_lparams(); } @@ -128,9 +128,9 @@ class theorem_val : public object_ref { public: theorem_val(name const & n, names const & lparams, expr const & type, expr const & val, names const & all); theorem_val(theorem_val const & other):object_ref(other) {} - theorem_val(theorem_val && other):object_ref(other) {} + theorem_val(theorem_val && other):object_ref(std::move(other)) {} theorem_val & operator=(theorem_val const & other) { object_ref::operator=(other); return *this; } - theorem_val & operator=(theorem_val && other) { object_ref::operator=(other); return *this; } + theorem_val & operator=(theorem_val && other) { object_ref::operator=(std::move(other)); return *this; } constant_val const & to_constant_val() const { return static_cast(cnstr_get_ref(*this, 0)); } name const & get_name() const { return to_constant_val().get_name(); } names const & get_lparams() const { return to_constant_val().get_lparams(); } @@ -148,9 +148,9 @@ class opaque_val : public object_ref { public: opaque_val(name const & n, names const & lparams, expr const & type, expr const & val, bool is_unsafe, names const & all); opaque_val(opaque_val const & other):object_ref(other) {} - opaque_val(opaque_val && other):object_ref(other) {} + opaque_val(opaque_val && other):object_ref(std::move(other)) {} opaque_val & operator=(opaque_val const & other) { object_ref::operator=(other); return *this; } - opaque_val & operator=(opaque_val && other) { object_ref::operator=(other); return *this; } + opaque_val & operator=(opaque_val && other) { object_ref::operator=(std::move(other)); return *this; } constant_val const & to_constant_val() const { return static_cast(cnstr_get_ref(*this, 0)); } name const & get_name() const { return to_constant_val().get_name(); } names const & get_lparams() const { return to_constant_val().get_lparams(); } @@ -179,9 +179,9 @@ class inductive_type : public object_ref { public: inductive_type(name const & id, expr const & type, constructors const & cnstrs); inductive_type(inductive_type const & other):object_ref(other) {} - inductive_type(inductive_type && other):object_ref(other) {} + inductive_type(inductive_type && other):object_ref(std::move(other)) {} inductive_type & operator=(inductive_type const & other) { object_ref::operator=(other); return *this; } - inductive_type & operator=(inductive_type && other) { object_ref::operator=(other); return *this; } + inductive_type & operator=(inductive_type && other) { object_ref::operator=(std::move(other)); return *this; } name const & get_name() const { return static_cast(cnstr_get_ref(*this, 0)); } expr const & get_type() const { return static_cast(cnstr_get_ref(*this, 1)); } constructors const & get_cnstrs() const { return static_cast(cnstr_get_ref(*this, 2)); } @@ -205,7 +205,7 @@ class declaration : public object_ref { public: declaration(); declaration(declaration const & other):object_ref(other) {} - declaration(declaration && other):object_ref(other) {} + declaration(declaration && other):object_ref(std::move(other)) {} /* low-level constructors */ explicit declaration(object * o):object_ref(o) {} explicit declaration(b_obj_arg o, bool b):object_ref(o, b) {} @@ -213,7 +213,7 @@ public: declaration_kind kind() const { return static_cast(obj_tag(raw())); } declaration & operator=(declaration const & other) { object_ref::operator=(other); return *this; } - declaration & operator=(declaration && other) { object_ref::operator=(other); return *this; } + declaration & operator=(declaration && other) { object_ref::operator=(std::move(other)); return *this; } friend bool is_eqp(declaration const & d1, declaration const & d2) { return d1.raw() == d2.raw(); } @@ -263,10 +263,10 @@ declaration mk_axiom_inferring_unsafe(environment const & env, name const & n, class inductive_decl : public object_ref { public: inductive_decl(inductive_decl const & other):object_ref(other) {} - inductive_decl(inductive_decl && other):object_ref(other) {} + inductive_decl(inductive_decl && other):object_ref(std::move(other)) {} inductive_decl(declaration const & d):object_ref(d) { lean_assert(d.is_inductive()); } inductive_decl & operator=(inductive_decl const & other) { object_ref::operator=(other); return *this; } - inductive_decl & operator=(inductive_decl && other) { object_ref::operator=(other); return *this; } + inductive_decl & operator=(inductive_decl && other) { object_ref::operator=(std::move(other)); return *this; } names const & get_lparams() const { return static_cast(cnstr_get_ref(raw(), 0)); } nat const & get_nparams() const { return static_cast(cnstr_get_ref(raw(), 1)); } inductive_types const & get_types() const { return static_cast(cnstr_get_ref(raw(), 2)); } @@ -290,9 +290,9 @@ public: inductive_val(name const & n, names const & lparams, expr const & type, unsigned nparams, unsigned nindices, names const & all, names const & cnstrs, unsigned nnested, bool is_rec, bool is_unsafe, bool is_reflexive); inductive_val(inductive_val const & other):object_ref(other) {} - inductive_val(inductive_val && other):object_ref(other) {} + inductive_val(inductive_val && other):object_ref(std::move(other)) {} inductive_val & operator=(inductive_val const & other) { object_ref::operator=(other); return *this; } - inductive_val & operator=(inductive_val && other) { object_ref::operator=(other); return *this; } + inductive_val & operator=(inductive_val && other) { object_ref::operator=(std::move(other)); return *this; } constant_val const & to_constant_val() const { return static_cast(cnstr_get_ref(*this, 0)); } unsigned get_nparams() const { return static_cast(cnstr_get_ref(*this, 1)).get_small_value(); } unsigned get_nindices() const { return static_cast(cnstr_get_ref(*this, 2)).get_small_value(); } @@ -317,9 +317,9 @@ class constructor_val : public object_ref { public: constructor_val(name const & n, names const & lparams, expr const & type, name const & induct, unsigned cidx, unsigned nparams, unsigned nfields, bool is_unsafe); constructor_val(constructor_val const & other):object_ref(other) {} - constructor_val(constructor_val && other):object_ref(other) {} + constructor_val(constructor_val && other):object_ref(std::move(other)) {} constructor_val & operator=(constructor_val const & other) { object_ref::operator=(other); return *this; } - constructor_val & operator=(constructor_val && other) { object_ref::operator=(other); return *this; } + constructor_val & operator=(constructor_val && other) { object_ref::operator=(std::move(other)); return *this; } constant_val const & to_constant_val() const { return static_cast(cnstr_get_ref(*this, 0)); } name const & get_induct() const { return static_cast(cnstr_get_ref(*this, 1)); } unsigned get_cidx() const { return static_cast(cnstr_get_ref(*this, 2)).get_small_value(); } @@ -338,9 +338,9 @@ class recursor_rule : public object_ref { public: recursor_rule(name const & cnstr, unsigned nfields, expr const & rhs); recursor_rule(recursor_rule const & other):object_ref(other) {} - recursor_rule(recursor_rule && other):object_ref(other) {} + recursor_rule(recursor_rule && other):object_ref(std::move(other)) {} recursor_rule & operator=(recursor_rule const & other) { object_ref::operator=(other); return *this; } - recursor_rule & operator=(recursor_rule && other) { object_ref::operator=(other); return *this; } + recursor_rule & operator=(recursor_rule && other) { object_ref::operator=(std::move(other)); return *this; } name const & get_cnstr() const { return static_cast(cnstr_get_ref(*this, 0)); } unsigned get_nfields() const { return static_cast(cnstr_get_ref(*this, 1)).get_small_value(); } expr const & get_rhs() const { return static_cast(cnstr_get_ref(*this, 2)); } @@ -365,9 +365,9 @@ public: names const & all, unsigned nparams, unsigned nindices, unsigned nmotives, unsigned nminors, recursor_rules const & rules, bool k, bool is_unsafe); recursor_val(recursor_val const & other):object_ref(other) {} - recursor_val(recursor_val && other):object_ref(other) {} + recursor_val(recursor_val && other):object_ref(std::move(other)) {} recursor_val & operator=(recursor_val const & other) { object_ref::operator=(other); return *this; } - recursor_val & operator=(recursor_val && other) { object_ref::operator=(other); return *this; } + recursor_val & operator=(recursor_val && other) { object_ref::operator=(std::move(other)); return *this; } constant_val const & to_constant_val() const { return static_cast(cnstr_get_ref(*this, 0)); } name const & get_name() const { return to_constant_val().get_name(); } name const & get_induct() const { return get_name().get_prefix(); } @@ -398,9 +398,9 @@ class quot_val : public object_ref { public: quot_val(name const & n, names const & lparams, expr const & type, quot_kind k); quot_val(quot_val const & other):object_ref(other) {} - quot_val(quot_val && other):object_ref(other) {} + quot_val(quot_val && other):object_ref(std::move(other)) {} quot_val & operator=(quot_val const & other) { object_ref::operator=(other); return *this; } - quot_val & operator=(quot_val && other) { object_ref::operator=(other); return *this; } + quot_val & operator=(quot_val && other) { object_ref::operator=(std::move(other)); return *this; } constant_val const & to_constant_val() const { return static_cast(cnstr_get_ref(*this, 0)); } name const & get_name() const { return to_constant_val().get_name(); } names const & get_lparams() const { return to_constant_val().get_lparams(); } @@ -434,14 +434,14 @@ public: constant_info(constructor_val const & v); constant_info(recursor_val const & v); constant_info(constant_info const & other):object_ref(other) {} - constant_info(constant_info && other):object_ref(other) {} + constant_info(constant_info && other):object_ref(std::move(other)) {} explicit constant_info(b_obj_arg o, bool b):object_ref(o, b) {} explicit constant_info(obj_arg o):object_ref(o) {} constant_info_kind kind() const { return static_cast(cnstr_tag(raw())); } constant_info & operator=(constant_info const & other) { object_ref::operator=(other); return *this; } - constant_info & operator=(constant_info && other) { object_ref::operator=(other); return *this; } + constant_info & operator=(constant_info && other) { object_ref::operator=(std::move(other)); return *this; } friend bool is_eqp(constant_info const & d1, constant_info const & d2) { return d1.raw() == d2.raw(); } diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 0371110d33..d1771e73a3 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -50,9 +50,9 @@ public: explicit literal(nat const & v); literal():literal(0u) {} literal(literal const & other):object_ref(other) {} - literal(literal && other):object_ref(other) {} + literal(literal && other):object_ref(std::move(other)) {} literal & operator=(literal const & other) { object_ref::operator=(other); return *this; } - literal & operator=(literal && other) { object_ref::operator=(other); return *this; } + literal & operator=(literal && other) { object_ref::operator=(std::move(other)); return *this; } static literal_kind kind(object * o) { return static_cast(cnstr_tag(o)); } literal_kind kind() const { return kind(raw()); } @@ -100,14 +100,14 @@ class expr : public object_ref { public: expr(); expr(expr const & other):object_ref(other) {} - expr(expr && other):object_ref(other) {} + expr(expr && other):object_ref(std::move(other)) {} explicit expr(b_obj_arg o, bool b):object_ref(o, b) {} explicit expr(obj_arg o):object_ref(o) {} static expr_kind kind(object * o) { return static_cast(cnstr_tag(o)); } expr_kind kind() const { return kind(raw()); } expr & operator=(expr const & other) { object_ref::operator=(other); return *this; } - expr & operator=(expr && other) { object_ref::operator=(other); return *this; } + expr & operator=(expr && other) { object_ref::operator=(std::move(other)); return *this; } friend bool is_eqp(expr const & e1, expr const & e2) { return e1.raw() == e2.raw(); } }; diff --git a/src/kernel/level.h b/src/kernel/level.h index b01240747e..32bfade7c2 100644 --- a/src/kernel/level.h +++ b/src/kernel/level.h @@ -43,14 +43,14 @@ public: explicit level(obj_arg o):object_ref(o) {} explicit level(b_obj_arg o, bool b):object_ref(o, b) {} level(level const & other):object_ref(other) {} - level(level && other):object_ref(other) {} + level(level && other):object_ref(std::move(other)) {} level_kind kind() const { return lean_is_scalar(raw()) ? level_kind::Zero : static_cast(lean_ptr_tag(raw())); } unsigned hash() const; level & operator=(level const & other) { object_ref::operator=(other); return *this; } - level & operator=(level && other) { object_ref::operator=(other); return *this; } + level & operator=(level && other) { object_ref::operator=(std::move(other)); return *this; } friend bool is_eqp(level const & l1, level const & l2) { return l1.raw() == l2.raw(); } diff --git a/src/kernel/local_ctx.h b/src/kernel/local_ctx.h index 8338316a4a..500d62a03c 100644 --- a/src/kernel/local_ctx.h +++ b/src/kernel/local_ctx.h @@ -27,11 +27,11 @@ class local_decl : public object_ref { public: local_decl(); local_decl(local_decl const & other):object_ref(other) {} - local_decl(local_decl && other):object_ref(other) {} + local_decl(local_decl && other):object_ref(std::move(other)) {} local_decl(obj_arg o):object_ref(o) {} local_decl(b_obj_arg o, bool):object_ref(o, true) {} local_decl & operator=(local_decl const & other) { object_ref::operator=(other); return *this; } - local_decl & operator=(local_decl && other) { object_ref::operator=(other); return *this; } + local_decl & operator=(local_decl && other) { object_ref::operator=(std::move(other)); return *this; } friend bool is_eqp(local_decl const & d1, local_decl const & d2) { return d1.raw() == d2.raw(); } unsigned get_idx() const { return static_cast(cnstr_get_ref(raw(), 0)).get_small_value(); } name const & get_name() const { return static_cast(cnstr_get_ref(raw(), 1)); } @@ -54,9 +54,9 @@ public: explicit local_ctx(obj_arg o):object_ref(o) {} local_ctx(b_obj_arg o, bool):object_ref(o, true) {} local_ctx(local_ctx const & other):object_ref(other) {} - local_ctx(local_ctx && other):object_ref(other) {} + local_ctx(local_ctx && other):object_ref(std::move(other)) {} local_ctx & operator=(local_ctx const & other) { object_ref::operator=(other); return *this; } - local_ctx & operator=(local_ctx && other) { object_ref::operator=(other); return *this; } + local_ctx & operator=(local_ctx && other) { object_ref::operator=(std::move(other)); return *this; } bool empty() const; diff --git a/src/library/compiler/specialize.cpp b/src/library/compiler/specialize.cpp index e6aa59c715..6874412c89 100644 --- a/src/library/compiler/specialize.cpp +++ b/src/library/compiler/specialize.cpp @@ -92,10 +92,10 @@ public: object_ref(mk_cnstr(0, ns, ks)) {} spec_info():spec_info(names(), spec_arg_kinds()) {} spec_info(spec_info const & other):object_ref(other) {} - spec_info(spec_info && other):object_ref(other) {} + spec_info(spec_info && other):object_ref(std::move(other)) {} spec_info(b_obj_arg o, bool b):object_ref(o, b) {} spec_info & operator=(spec_info const & other) { object_ref::operator=(other); return *this; } - spec_info & operator=(spec_info && other) { object_ref::operator=(other); return *this; } + spec_info & operator=(spec_info && other) { object_ref::operator=(std::move(other)); return *this; } names const & get_mutual_decls() const { return static_cast(cnstr_get_ref(*this, 0)); } spec_arg_kinds const & get_arg_kinds() const { return static_cast(cnstr_get_ref(*this, 1)); } }; diff --git a/src/library/projection.h b/src/library/projection.h index 11e1abb2c8..3ade6827e6 100644 --- a/src/library/projection.h +++ b/src/library/projection.h @@ -24,13 +24,13 @@ public: projection_info(name const & c, unsigned nparams, unsigned i, bool inst_implicit); projection_info():projection_info(name(), 0, 0, false) {} projection_info(projection_info const & other):object_ref(other) {} - projection_info(projection_info && other):object_ref(other) {} + projection_info(projection_info && other):object_ref(std::move(other)) {} /* low-level constructors */ explicit projection_info(object * o):object_ref(o) {} explicit projection_info(b_obj_arg o, bool b):object_ref(o, b) {} explicit projection_info(object_ref const & o):object_ref(o) {} projection_info & operator=(projection_info const & other) { object_ref::operator=(other); return *this; } - projection_info & operator=(projection_info && other) { object_ref::operator=(other); return *this; } + projection_info & operator=(projection_info && other) { object_ref::operator=(std::move(other)); return *this; } name const & get_constructor() const { return static_cast(cnstr_get_ref(*this, 0)); } unsigned get_nparams() const { return static_cast(cnstr_get_ref(*this, 1)).get_small_value(); } unsigned get_i() const { return static_cast(cnstr_get_ref(*this, 2)).get_small_value(); } diff --git a/src/runtime/array_ref.h b/src/runtime/array_ref.h index a0f4db4450..468ca77340 100644 --- a/src/runtime/array_ref.h +++ b/src/runtime/array_ref.h @@ -28,12 +28,12 @@ public: array_ref(b_obj_arg o, bool b):object_ref(o, b) {} array_ref():object_ref(array_mk_empty()) {} array_ref(array_ref const & other):object_ref(other) {} - array_ref(array_ref && other):object_ref(other) {} + array_ref(array_ref && other):object_ref(std::move(other)) {} array_ref(std::initializer_list const & elems):object_ref(to_array(elems)) {} array_ref(buffer const & elems):object_ref(to_array(elems)) {} array_ref & operator=(array_ref const & other) { object_ref::operator=(other); return *this; } - array_ref & operator=(array_ref && other) { object_ref::operator=(other); return *this; } + array_ref & operator=(array_ref && other) { object_ref::operator=(std::move(other)); return *this; } size_t size() const { return array_size(raw()); } diff --git a/src/runtime/list_ref.h b/src/runtime/list_ref.h index 19aa342a6f..1b5f163c56 100644 --- a/src/runtime/list_ref.h +++ b/src/runtime/list_ref.h @@ -23,7 +23,7 @@ public: explicit list_ref(list_ref const * l) { if (l) *this = *l; } list_ref(T const & h, list_ref const & t):object_ref(mk_cnstr(1, h.raw(), t.raw())) { inc(h.raw()); inc(t.raw()); } list_ref(list_ref const & other):object_ref(other) {} - list_ref(list_ref && other):object_ref(other) {} + list_ref(list_ref && other):object_ref(std::move(other)) {} template list_ref(It const & begin, It const & end):list_ref() { auto it = end; while (it != begin) { @@ -35,7 +35,7 @@ public: list_ref(buffer const & b):list_ref(b.begin(), b.end()) {} list_ref & operator=(list_ref const & other) { object_ref::operator=(other); return *this; } - list_ref & operator=(list_ref && other) { object_ref::operator=(other); return *this; } + list_ref & operator=(list_ref && other) { object_ref::operator=(std::move(other)); return *this; } explicit operator bool() const { return !is_scalar(raw()); } friend bool is_nil(list_ref const & l) { return is_scalar(l.raw()); } diff --git a/src/runtime/option_ref.h b/src/runtime/option_ref.h index 187616e6c9..18c3f915ec 100644 --- a/src/runtime/option_ref.h +++ b/src/runtime/option_ref.h @@ -16,14 +16,14 @@ public: option_ref(b_obj_arg o, bool b):object_ref(o, b) {} option_ref():object_ref(box(0)) {} option_ref(option_ref const & other):object_ref(other) {} - option_ref(option_ref && other):object_ref(other) {} + option_ref(option_ref && other):object_ref(std::move(other)) {} explicit option_ref(T const & a):object_ref(mk_cnstr(1, a.raw())) { inc(a.raw()); } explicit option_ref(T const * a) { if (a) *this = option_ref(*a); } explicit option_ref(option_ref const * o) { if (o) *this = *o; } explicit option_ref(optional const & o):option_ref(o ? &*o : nullptr) {} option_ref & operator=(option_ref const & other) { object_ref::operator=(other); return *this; } - option_ref & operator=(option_ref && other) { object_ref::operator=(other); return *this; } + option_ref & operator=(option_ref && other) { object_ref::operator=(std::move(other)); return *this; } explicit operator bool() const { return !is_scalar(raw()); } optional get() const { return *this ? some(static_cast(cnstr_get_ref(*this, 0))) : optional(); } diff --git a/src/runtime/optional.h b/src/runtime/optional.h index cf3455fc54..995fb31859 100644 --- a/src/runtime/optional.h +++ b/src/runtime/optional.h @@ -31,13 +31,13 @@ public: } optional(optional && other):m_some(other.m_some) { if (other.m_some) - new (&m_value) T(std::forward(other.m_value)); + new (&m_value) T(std::move(other.m_value)); } explicit optional(T const & v):m_some(true) { new (&m_value) T(v); } explicit optional(T && v):m_some(true) { - new (&m_value) T(std::forward(v)); + new (&m_value) T(std::move(v)); } template explicit optional(Args&&... args):m_some(true) { @@ -84,7 +84,7 @@ public: m_value.~T(); m_some = other.m_some; if (m_some) - new (&m_value) T(std::forward(other.m_value)); + new (&m_value) T(std::move(other.m_value)); return *this; } optional& operator=(T const & other) { @@ -98,7 +98,7 @@ public: if (m_some) m_value.~T(); m_some = true; - new (&m_value) T(std::forward(other)); + new (&m_value) T(std::move(other)); return *this; } @@ -130,9 +130,9 @@ template<> class optional

{ \ public: \ optional():m_value(nullptr) {} \ optional(optional const & other):m_value(other.m_value) {} \ - optional(optional && other):m_value(std::forward

(other.m_value)) {} \ + optional(optional && other):m_value(std::move(other.m_value)) {} \ explicit optional(P const & v):m_value(v) {} \ - explicit optional(P && v):m_value(std::forward

(v)) {} \ + explicit optional(P && v):m_value(std::move(v)) {} \ \ explicit operator bool() const { return m_value.m_ptr != nullptr; } \ P const * operator->() const { lean_assert(m_value.m_ptr); return &m_value; } \ @@ -142,9 +142,9 @@ public: \ P const & value() const { lean_assert(m_value.m_ptr); return m_value; } \ P & value() { lean_assert(m_value.m_ptr); return m_value; } \ optional & operator=(optional const & other) { m_value = other.m_value; return *this; } \ - optional& operator=(optional && other) { m_value = std::forward

(other.m_value); return *this; } \ + optional& operator=(optional && other) { m_value = std::move(other.m_value); return *this; } \ optional& operator=(P const & other) { m_value = other; return *this; } \ - optional& operator=(P && other) { m_value = std::forward

(other); return *this; } \ + optional& operator=(P && other) { m_value = std::move(other); return *this; } \ friend bool operator==(optional const & o1, optional const & o2) { \ return static_cast(o1) == static_cast(o2) && (!o1 || o1.m_value == o2.m_value); \ } \ diff --git a/src/runtime/string_ref.h b/src/runtime/string_ref.h index a510ee8375..dd9fb726cb 100644 --- a/src/runtime/string_ref.h +++ b/src/runtime/string_ref.h @@ -17,11 +17,11 @@ public: explicit string_ref(std::string const & s):object_ref(mk_string(s)) {} explicit string_ref(sstream const & strm):string_ref(strm.str()) {} string_ref(string_ref const & other):object_ref(other) {} - string_ref(string_ref && other):object_ref(other) {} + string_ref(string_ref && other):object_ref(std::move(other)) {} explicit string_ref(obj_arg o):object_ref(o) {} string_ref(b_obj_arg o, bool b):object_ref(o, b) {} string_ref & operator=(string_ref const & other) { object_ref::operator=(other); return *this; } - string_ref & operator=(string_ref && other) { object_ref::operator=(other); return *this; } + string_ref & operator=(string_ref && other) { object_ref::operator=(std::move(other)); return *this; } /* Number of bytes used to store the string in UTF8. Remark: it does not include the null character added in the end to make it efficient to convert to C string. */ diff --git a/src/util/kvmap.h b/src/util/kvmap.h index 172c441472..ff16d98328 100644 --- a/src/util/kvmap.h +++ b/src/util/kvmap.h @@ -30,9 +30,9 @@ public: explicit data_value(name const & v):object_ref(mk_cnstr(static_cast(data_value_kind::Name), v.raw())) { inc(v.raw()); } data_value():data_value(false) {} data_value(data_value const & other):object_ref(other) {} - data_value(data_value && other):object_ref(other) {} + data_value(data_value && other):object_ref(std::move(other)) {} data_value & operator=(data_value const & other) { object_ref::operator=(other); return *this; } - data_value & operator=(data_value && other) { object_ref::operator=(other); return *this; } + data_value & operator=(data_value && other) { object_ref::operator=(std::move(other)); return *this; } data_value_kind kind() const { return static_cast(cnstr_tag(raw())); } string_ref const & get_string() const { lean_assert(kind() == data_value_kind::String); return static_cast(cnstr_get_ref(*this, 0)); } diff --git a/src/util/name.h b/src/util/name.h index 9c1d70e575..f15fa1e29d 100644 --- a/src/util/name.h +++ b/src/util/name.h @@ -74,7 +74,7 @@ public: name(std::string const & s):name(name(), string_ref(s)) {} name(string_ref const & s):name(name(), s) {} name(name const & other):object_ref(other) {} - name(name && other):object_ref(other) {} + name(name && other):object_ref(std::move(other)) {} /** \brief Create a hierarchical name using the given strings. Example: name{"foo", "bla", "tst"} creates the hierarchical @@ -97,7 +97,7 @@ public: */ static name mk_internal_unique_name(); name & operator=(name const & other) { object_ref::operator=(other); return *this; } - name & operator=(name && other) { object_ref::operator=(other); return *this; } + name & operator=(name && other) { object_ref::operator=(std::move(other)); return *this; } static uint64_t hash(b_obj_arg n) { lean_assert(lean_name_hash(n) == lean_name_hash_exported_b(n)); return lean_name_hash(n); diff --git a/src/util/nat.h b/src/util/nat.h index e0bae8429a..8035a9cd5f 100644 --- a/src/util/nat.h +++ b/src/util/nat.h @@ -27,10 +27,10 @@ public: static nat of_size_t(size_t v) { return nat(lean_usize_to_nat(v)); } nat(nat const & other):object_ref(other) {} - nat(nat && other):object_ref(other) {} + nat(nat && other):object_ref(std::move(other)) {} nat & operator=(nat const & other) { object_ref::operator=(other); return *this; } - nat & operator=(nat && other) { object_ref::operator=(other); return *this; } + nat & operator=(nat && other) { object_ref::operator=(std::move(other)); return *this; } bool is_small() const { return is_scalar(raw()); } size_t get_small_value() const { lean_assert(is_small()); return unbox(raw()); } bool is_zero() const { return is_small() && get_small_value() == 0; }