From 25b812f1c905a07c850044c8332efe3ef0ab2ff9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 8 Dec 2013 10:17:29 -0800 Subject: [PATCH] feat(kernel/expr): no overhead optional template specialization Signed-off-by: Leonardo de Moura --- src/kernel/expr.cpp | 2 +- src/kernel/expr.h | 25 ++++++++++++++----------- src/tests/kernel/expr.cpp | 9 ++++++--- src/util/optional.h | 36 ++++++++++++++++++++++++++++++++++++ 4 files changed, 57 insertions(+), 15 deletions(-) diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 7f0c7292d..e22326fcd 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -38,7 +38,7 @@ expr_cell::expr_cell(expr_kind k, unsigned h, bool has_mv): m_kind(static_cast(k)), m_flags(has_mv ? 4 : 0), m_hash(h), - m_rc(1) { + m_rc(0) { // m_hash_alloc does not need to be a unique identifier. // We want diverse hash codes such that given expr_cell * c1 and expr_cell * c2, // if c1 != c2, then there is high probability c1->m_hash_alloc != c2->m_hash_alloc. diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 828bc0bca..1f8594cf9 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -100,9 +100,10 @@ public: class expr { private: expr_cell * m_ptr; - explicit expr(expr_cell * ptr):m_ptr(ptr) {} + explicit expr(expr_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); } friend class expr_cell; expr_cell * steal_ptr() { expr_cell * r = m_ptr; m_ptr = nullptr; return r; } + friend class optional; public: expr(); expr(expr const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } @@ -135,10 +136,6 @@ public: friend expr mk_metavar(name const & n, local_context const & ctx); friend bool is_eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; } - friend bool is_eqp(optional const & a, optional const & b) { - return static_cast(a) == static_cast(b) && (!a || is_eqp(*a, *b)); - } - // Overloaded operator() can be used to create applications expr operator()(expr const & a1) const; expr operator()(expr const & a1, expr const & a2) const; @@ -150,6 +147,18 @@ public: expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5, expr const & a6, expr const & a7, expr const & a8) const; }; +// ======================================= +// Structural equality + bool operator==(expr const & a, expr const & b); +inline bool operator!=(expr const & a, expr const & b) { return !operator==(a, b); } +// ======================================= + +SPECIALIZE_OPTIONAL_FOR_SMART_PTR(expr) + +inline bool is_eqp(optional const & a, optional const & b) { + return static_cast(a) == static_cast(b) && (!a || is_eqp(*a, *b)); +} + // ======================================= // Expr (internal) Representation /** \brief Free variables. They are encoded using de Bruijn's indices. */ @@ -513,12 +522,6 @@ inline bool has_metavar(expr const & e) { return e.has_metavar(); } bool is_eq(expr const & e, expr & lhs, expr & rhs); // ======================================= -// ======================================= -// Structural equality - bool operator==(expr const & a, expr const & b); -inline bool operator!=(expr const & a, expr const & b) { return !operator==(a, b); } -// ======================================= - // ======================================= // Expression+Offset typedef std::pair expr_offset; diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index f60223d86..fa83c7ea2 100644 --- a/src/tests/kernel/expr.cpp +++ b/src/tests/kernel/expr.cpp @@ -355,9 +355,7 @@ static void tst18() { int main() { save_stack_info(); - std::cout << "sizeof(expr): " << sizeof(expr) << "\n"; - std::cout << "sizeof(expr_app): " << sizeof(expr_app) << "\n"; - std::cout << "sizeof(expr_cell): " << sizeof(expr_cell) << "\n"; + lean_assert(sizeof(expr) == sizeof(optional)); tst1(); tst2(); tst3(); @@ -376,6 +374,11 @@ int main() { tst16(); tst17(); tst18(); + std::cout << "sizeof(expr): " << sizeof(expr) << "\n"; + std::cout << "sizeof(expr_app): " << sizeof(expr_app) << "\n"; + std::cout << "sizeof(expr_cell): " << sizeof(expr_cell) << "\n"; + std::cout << "sizeof(optional): " << sizeof(optional) << "\n"; + std::cout << "sizeof(optional): " << sizeof(optional) << "\n"; std::cout << "done" << "\n"; return has_violations() ? 1 : 0; } diff --git a/src/util/optional.h b/src/util/optional.h index 8e3513ab4..59e4324db 100644 --- a/src/util/optional.h +++ b/src/util/optional.h @@ -110,4 +110,40 @@ public: template optional some(T const & t) { return optional(t); } template optional some(T && t) { return optional(std::forward(t)); } + +// The following macro creates a template specialization optional

, where P +// is an intrusive smart pointer that does not let "customers" point to nullptr. +// That is, if a customer have 'P x', then x is not a pointer to nullptr. +// Requirements: +// - P must declare optional

as a friend. +// - P must handle the nullptr case even if it does not let "customers" point to nullptr +// - P must have a field m_ptr a pointer to the actual value. +#define SPECIALIZE_OPTIONAL_FOR_SMART_PTR(P) \ +template<> class optional

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

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

(v)) {} \ + \ + explicit operator bool() const { return m_value.m_ptr != nullptr; } \ + P const * operator->() const { lean_assert(m_value.m_ptr); return &m_value; } \ + P * operator->() { lean_assert(m_value.m_ptr); return &m_value; } \ + P const & operator*() const { lean_assert(m_value.m_ptr); return m_value; } \ + P & operator*() { lean_assert(m_value.m_ptr); return m_value; } \ + 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=(P const & other) { m_value = other; return *this; } \ + optional& operator=(P && other) { m_value = std::forward

(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); \ + } \ + friend bool operator!=(optional const & o1, optional const & o2) { \ + return !operator==(o1, o2); \ + } \ +}; }