From da66610fda6c03f73ffbc1465fb61c9477fa7eee Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 19 Jul 2021 19:28:27 -0700
Subject: [PATCH] chore: cleanup

---
 src/include/lean/lean.h   | 12 +++---------
 src/include/lean/object.h |  1 -
 src/runtime/object.cpp    | 22 +++++++++++++++++-----
 3 files changed, 20 insertions(+), 15 deletions(-)

diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
index daeb371ce8..bb41a8f261 100644
--- a/src/include/lean/lean.h
+++ b/src/include/lean/lean.h
@@ -402,21 +402,15 @@ static inline void lean_inc_ref_n(lean_object * o, size_t n) {
     }
 }
 
-bool lean_dec_ref_core_cold(lean_object * o);
+void lean_dec_ref_cold(lean_object * o);
 
-static inline bool lean_dec_ref_core(lean_object * o) {
+static inline void lean_dec_ref(lean_object * o) {
     if (LEAN_LIKELY(o->m_rc > 1)) {
         o->m_rc--;
-        return false;
     } else {
-        return lean_dec_ref_core_cold(o);
+        lean_dec_ref_cold(o);
     }
 }
-
-/* Generic Lean object delete operation. */
-void lean_del(lean_object * o);
-
-static inline void lean_dec_ref(lean_object * o) { if (lean_dec_ref_core(o)) lean_del(o); }
 static inline void lean_inc(lean_object * o) { if (!lean_is_scalar(o)) lean_inc_ref(o); }
 static inline void lean_inc_n(lean_object * o, size_t n) { if (!lean_is_scalar(o)) lean_inc_ref_n(o, n); }
 static inline void lean_dec(lean_object * o) { if (!lean_is_scalar(o)) lean_dec_ref(o); }
diff --git a/src/include/lean/object.h b/src/include/lean/object.h
index 30a4a5d472..210fefeb38 100644
--- a/src/include/lean/object.h
+++ b/src/include/lean/object.h
@@ -50,7 +50,6 @@ inline bool is_shared(object * o) { return lean_is_shared(o); }
 inline bool is_exclusive(object * o) { return lean_is_exclusive(o); }
 inline void inc_ref(object * o) { lean_inc_ref(o); }
 inline void inc_ref(object * o, size_t n) { lean_inc_ref_n(o, n); }
-inline bool dec_ref_core(object * o) { return lean_dec_ref_core(o); }
 inline void dec_ref(object * o) { lean_dec_ref(o); }
 inline void inc(object * o) { lean_inc(o); }
 inline void inc(object * o, size_t n) { lean_inc_n(o, n); }
diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
index b09e84e6a7..5d43862335 100644
--- a/src/runtime/object.cpp
+++ b/src/runtime/object.cpp
@@ -81,10 +81,15 @@ extern "C" void lean_inc_ref_n_cold(lean_object * o, unsigned n) {
     atomic_fetch_sub_explicit(lean_get_rc_mt_addr(o), n, memory_order_relaxed);
 }
 
-extern "C" bool lean_dec_ref_core_cold(lean_object * o) {
-    if (o->m_rc == 1) return true;
-    if (o->m_rc == 0) return false;
-    return atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), 1, memory_order_acq_rel) == -1;
+static inline bool lean_dec_ref_core(lean_object * o) {
+    if (LEAN_LIKELY(o->m_rc >= 1)) {
+        o->m_rc--;
+        return o->m_rc == 0;
+    } else if (o->m_rc == 0) {
+        return false;
+    } else {
+        return atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), 1, memory_order_acq_rel) == -1;
+    }
 }
 
 extern "C" size_t lean_object_byte_size(lean_object * o) {
@@ -247,7 +252,7 @@ static void lean_del_core(object * o, object * & todo) {
     }
 }
 
-extern "C" void lean_del(object * o) {
+static inline void lean_del(object * o) {
 #ifdef LEAN_LAZY_RC
     push_back(g_to_free, o);
 #else
@@ -261,6 +266,13 @@ extern "C" void lean_del(object * o) {
 #endif
 }
 
+extern "C" void lean_dec_ref_cold(lean_object * o) {
+  if (o->m_rc == 1) lean_del(o);
+  else if (o->m_rc == 0) return;
+  else if (atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), 1, memory_order_acq_rel) == -1) lean_del(o);
+}
+
+
 // =======================================
 // Closures