Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

perf: avoid expr copies in replace_rec_fn::apply #4702

Merged
merged 3 commits into from
Aug 2, 2024
Merged

perf: avoid expr copies in replace_rec_fn::apply #4702

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
c3c46b2
perf: fix implementation of move constructors and move assignment ope…
legrosbuffle Jul 9, 2024
59e4228
perf: avoid `expr` copies in `replace_rec_fn::apply`
legrosbuffle Jul 9, 2024
7fca1c9
Merge branch 'master' into fewer-expr-copies
leodemoura Aug 2, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
56 changes: 28 additions & 28 deletions src/kernel/declaration.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<name const &>(cnstr_get_ref(*this, 0)); }
names const & get_lparams() const { return static_cast<names const &>(cnstr_get_ref(*this, 1)); }
expr const & get_type() const { return static_cast<expr const &>(cnstr_get_ref(*this, 2)); }
Expand All @@ -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<constant_val const &>(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(); }
Expand All @@ -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<constant_val const &>(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(); }
Expand All @@ -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<constant_val const &>(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(); }
Expand All @@ -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<constant_val const &>(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(); }
Expand Down Expand Up @@ -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<name const &>(cnstr_get_ref(*this, 0)); }
expr const & get_type() const { return static_cast<expr const &>(cnstr_get_ref(*this, 1)); }
constructors const & get_cnstrs() const { return static_cast<constructors const &>(cnstr_get_ref(*this, 2)); }
Expand All @@ -205,15 +205,15 @@ 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) {}
explicit declaration(object_ref const & o):object_ref(o) {}
declaration_kind kind() const { return static_cast<declaration_kind>(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(); }

Expand Down Expand Up @@ -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<names const &>(cnstr_get_ref(raw(), 0)); }
nat const & get_nparams() const { return static_cast<nat const &>(cnstr_get_ref(raw(), 1)); }
inductive_types const & get_types() const { return static_cast<inductive_types const &>(cnstr_get_ref(raw(), 2)); }
Expand All @@ -290,9 +290,9 @@ class inductive_val : public object_ref {
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<constant_val const &>(cnstr_get_ref(*this, 0)); }
unsigned get_nparams() const { return static_cast<nat const &>(cnstr_get_ref(*this, 1)).get_small_value(); }
unsigned get_nindices() const { return static_cast<nat const &>(cnstr_get_ref(*this, 2)).get_small_value(); }
Expand All @@ -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<constant_val const &>(cnstr_get_ref(*this, 0)); }
name const & get_induct() const { return static_cast<name const &>(cnstr_get_ref(*this, 1)); }
unsigned get_cidx() const { return static_cast<nat const &>(cnstr_get_ref(*this, 2)).get_small_value(); }
Expand All @@ -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<name const &>(cnstr_get_ref(*this, 0)); }
unsigned get_nfields() const { return static_cast<nat const &>(cnstr_get_ref(*this, 1)).get_small_value(); }
expr const & get_rhs() const { return static_cast<expr const &>(cnstr_get_ref(*this, 2)); }
Expand All @@ -365,9 +365,9 @@ class recursor_val : public object_ref {
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<constant_val const &>(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(); }
Expand Down Expand Up @@ -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<constant_val const &>(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(); }
Expand Down Expand Up @@ -434,14 +434,14 @@ class constant_info : public object_ref {
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<constant_info_kind>(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(); }

Expand Down
8 changes: 4 additions & 4 deletions src/kernel/expr.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,9 +50,9 @@ class literal : public object_ref {
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<literal_kind>(cnstr_tag(o)); }
literal_kind kind() const { return kind(raw()); }
Expand Down Expand Up @@ -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<expr_kind>(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(); }
};
Expand Down
4 changes: 2 additions & 2 deletions src/kernel/level.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,14 +43,14 @@ class level : public object_ref {
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<level_kind>(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(); }

Expand Down
8 changes: 4 additions & 4 deletions src/kernel/local_ctx.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<nat const &>(cnstr_get_ref(raw(), 0)).get_small_value(); }
name const & get_name() const { return static_cast<name const &>(cnstr_get_ref(raw(), 1)); }
Expand All @@ -54,9 +54,9 @@ class local_ctx : public object_ref {
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;

Expand Down
5 changes: 3 additions & 2 deletions src/kernel/replace_fn.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/
#include <vector>
#include <memory>
#include <utility>
#include <unordered_map>
#include "kernel/replace_fn.h"

Expand All @@ -21,7 +22,7 @@ class replace_rec_fn {
std::function<optional<expr>(expr const &, unsigned)> m_f;
bool m_use_cache;

expr save_result(expr const & e, unsigned offset, expr const & r, bool shared) {
expr save_result(expr const & e, unsigned offset, expr r, bool shared) {
if (shared)
m_cache.insert(mk_pair(mk_pair(e.raw(), offset), r));
return r;
Expand All @@ -36,7 +37,7 @@ class replace_rec_fn {
shared = true;
}
if (optional<expr> r = m_f(e, offset)) {
return save_result(e, offset, *r, shared);
return save_result(e, offset, std::move(*r), shared);
} else {
switch (e.kind()) {
case expr_kind::Const: case expr_kind::Sort:
Expand Down
4 changes: 2 additions & 2 deletions src/library/compiler/specialize.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -92,10 +92,10 @@ class spec_info : public object_ref {
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<names const &>(cnstr_get_ref(*this, 0)); }
spec_arg_kinds const & get_arg_kinds() const { return static_cast<spec_arg_kinds const &>(cnstr_get_ref(*this, 1)); }
};
Expand Down
Loading
Loading