From 232443371bd7f4c1cef5c64aff6cbdd945afeef5 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 1 Jul 2025 13:39:12 +0100 Subject: [PATCH] perf: add missing `std::move`s (#9107) Continues from #4700. This will save a handful of refcounts here and there. --- src/kernel/environment.h | 6 +++--- src/library/elab_environment.h | 4 ++-- src/runtime/pair_ref.h | 4 ++-- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 88ff149699..7a7073be32 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -29,7 +29,7 @@ namespace lean { class diagnostics : public object_ref { public: diagnostics(diagnostics const & other):object_ref(other) {} - diagnostics(diagnostics && other):object_ref(other) {} + diagnostics(diagnostics && other):object_ref(std::move(other)) {} explicit diagnostics(b_obj_arg o, bool b):object_ref(o, b) {} explicit diagnostics(obj_arg o):object_ref(o) {} ~diagnostics() {} @@ -74,13 +74,13 @@ class LEAN_EXPORT environment : public object_ref { environment add_inductive(declaration const & d) const; public: environment(environment const & other):object_ref(other) {} - environment(environment && other):object_ref(other) {} + environment(environment && other):object_ref(std::move(other)) {} explicit environment(b_obj_arg o, bool b):object_ref(o, b) {} explicit environment(obj_arg o):object_ref(o) {} ~environment() {} environment & operator=(environment const & other) { object_ref::operator=(other); return *this; } - environment & operator=(environment && other) { object_ref::operator=(other); return *this; } + environment & operator=(environment && other) { object_ref::operator=(std::move(other)); return *this; } diagnostics get_diag() const; environment set_diag(diagnostics const & diag) const; diff --git a/src/library/elab_environment.h b/src/library/elab_environment.h index 12b35167df..8aa95e6016 100644 --- a/src/library/elab_environment.h +++ b/src/library/elab_environment.h @@ -12,13 +12,13 @@ namespace lean { class LEAN_EXPORT elab_environment : public object_ref { public: elab_environment(elab_environment const & other):object_ref(other) {} - elab_environment(elab_environment && other):object_ref(other) {} + elab_environment(elab_environment && other):object_ref(std::move(other)) {} explicit elab_environment(b_obj_arg o, bool b):object_ref(o, b) {} explicit elab_environment(obj_arg o):object_ref(o) {} ~elab_environment() {} elab_environment & operator=(elab_environment const & other) { object_ref::operator=(other); return *this; } - elab_environment & operator=(elab_environment && other) { object_ref::operator=(other); return *this; } + elab_environment & operator=(elab_environment && other) { object_ref::operator=(std::move(other)); return *this; } /** \brief Return information for the constant with name \c n (if it is defined in this environment). */ optional find(name const & n) const { return to_kernel_env().find(n); }; diff --git a/src/runtime/pair_ref.h b/src/runtime/pair_ref.h index d20bcc4db6..d09929930a 100644 --- a/src/runtime/pair_ref.h +++ b/src/runtime/pair_ref.h @@ -16,9 +16,9 @@ public: explicit pair_ref(b_obj_arg o, bool b):object_ref(o, b) {} pair_ref(T1 const & a, T2 const & b):object_ref(mk_cnstr(0, a.raw(), b.raw())) { inc(a.raw()); inc(b.raw()); } pair_ref(pair_ref const & other):object_ref(other) {} - pair_ref(pair_ref && other):object_ref(other) {} + pair_ref(pair_ref && other):object_ref(std::move(other)) {} pair_ref & operator=(pair_ref const & other) { object_ref::operator=(other); return *this; } - pair_ref & operator=(pair_ref && other) { object_ref::operator=(other); return *this; } + pair_ref & operator=(pair_ref && other) { object_ref::operator=(std::move(other)); return *this; } T1 const & fst() const { return static_cast(cnstr_get_ref(*this, 0)); } T2 const & snd() const { return static_cast(cnstr_get_ref(*this, 1)); }