perf: Replacement.apply

Avoid potentially expensive `e.replace` if it is not applicable.

src/Init/Util.lean

@@ -45,13 +45,6 @@ def dbgSleep {α : Type u} (ms : UInt32) (f : Unit → α) : α := f ()
 @[extern "lean_ptr_addr"]
 unsafe opaque ptrAddrUnsafe {α : Type u} (a : @& α) : USize
 
-/--
-Returns `true` if `a` is an exclusive object.
-We say an object is exclusive if it is single-threaded and its reference counter is 1.
--/
-@[extern "lean_is_exclusive_obj"]
-unsafe opaque isExclusiveUnsafe {α : Type u} (a : @& α) : Bool
-
 set_option linter.unusedVariables.funArgs false in
 @[inline] unsafe def withPtrAddrUnsafe {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β :=
   k (ptrAddrUnsafe a)

src/include/lean/lean.h

@@ -481,10 +481,6 @@ static inline bool lean_is_exclusive(lean_object * o) {
     }
 }
 
-static inline uint8_t lean_is_exclusive_obj(lean_object * o) {
-    return lean_is_exclusive(o);
-}
-
 static inline bool lean_is_shared(lean_object * o) {
     if (LEAN_LIKELY(lean_is_st(o))) {
         return o->m_rc > 1;
@@ -1137,17 +1133,6 @@ static inline void * lean_get_external_data(lean_object * o) {
     return lean_to_external(o)->m_data;
 }
 
-static inline lean_object * lean_set_external_data(lean_object * o, void * data) {
-    if (lean_is_exclusive(o)) {
-        lean_to_external(o)->m_data = data;
-        return o;
-    } else {
-        lean_object * o_new = lean_alloc_external(lean_get_external_class(o), data);
-        lean_dec_ref(o);
-        return o_new;
-    }
-}
-
 /* Natural numbers */
 
 #define LEAN_MAX_SMALL_NAT (SIZE_MAX >> 1)

src/runtime/sharecommon.cpp

@@ -358,16 +358,30 @@ class sharecommon_quick_fn {
         return result;
     }
 
-    // `sarray` and `string`
-    lean_object * visit_terminal(lean_object * a) {
-        auto it = m_set.find(a);
-        if (it == m_set.end()) {
-            m_set.insert(a);
-        } else {
-            a = *it;
-        }
-        lean_inc_ref(a);
-        return a;
+    lean_object * visit_sarray(lean_object * a) {
+        lean_object * r = check_cache(a);
+        if (r != nullptr) { lean_assert(r->m_rc > 1); return r; }
+
+        size_t sz        = lean_sarray_size(a);
+        unsigned elem_sz = lean_sarray_elem_size(a);
+        lean_sarray_object * new_a = (lean_sarray_object*)lean_alloc_sarray(elem_sz, sz, sz);
+        memcpy(new_a->m_data, lean_to_sarray(a)->m_data, elem_sz*sz);
+        return save(a, (lean_object*)new_a);
+    }
+
+    lean_object * visit_string(lean_object * a) {
+        lean_object * r = check_cache(a);
+        if (r != nullptr) { lean_assert(r->m_rc > 1); return r; }
+
+        size_t sz     = lean_string_size(a);
+        size_t len    = lean_string_len(a);
+        lean_string_object * new_a = (lean_string_object*)lean_alloc_string(sz, sz, len);
+        lean_set_st_header((lean_object*)new_a, LeanString, 0);
+        new_a->m_size     = sz;
+        new_a->m_capacity = sz;
+        new_a->m_length   = len;
+        memcpy(new_a->m_data, lean_to_string(a)->m_data, sz);
+        return save(a, (lean_object*)new_a);
     }
 
     lean_object * visit_array(lean_object * a) {
@@ -385,6 +399,7 @@ class sharecommon_quick_fn {
     lean_object * visit_ctor(lean_object * a) {
         lean_object * r = check_cache(a);
         if (r != nullptr) { lean_assert(r->m_rc > 1); return r; }
+
         unsigned num_objs      = lean_ctor_num_objs(a);
         unsigned tag           = lean_ptr_tag(a);
         unsigned sz            = lean_object_byte_size(a);
@@ -427,9 +442,9 @@ public:
         case LeanRef:             lean_inc_ref(a); return a;
         case LeanExternal:        lean_inc_ref(a); return a;
         case LeanReserved:        lean_inc_ref(a); return a;
-        case LeanScalarArray:     return visit_terminal(a);
-        case LeanString:          return visit_terminal(a);
         case LeanArray:           return visit_array(a);
+        case LeanScalarArray:     return visit_sarray(a);
+        case LeanString:          return visit_string(a);
         default:                  return visit_ctor(a);
         }
     }