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

perf: add missing std::moves (#9107)

Browse source 
Continues from #4700.

This will save a handful of refcounts here and there.
This commit is contained in:
Eric Wieser 2025-07-01 13:39:12 +01:00 • committed by GitHub
parent c231b742ca
commit 232443371b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/kernel/environment.h
View file

@ -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;

4
src/library/elab_environment.h
View file

@ -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<constant_info> find(name const & n) const { return to_kernel_env().find(n); };

4
src/runtime/pair_ref.h
View file

@ -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<T1 const &>(cnstr_get_ref(*this, 0)); }
T2 const & snd() const { return static_cast<T2 const &>(cnstr_get_ref(*this, 1)); }