perf: empty array

src/include/lean/lean.h

@@ -1011,13 +1011,13 @@ static inline lean_object * lean_array_get_size(b_lean_obj_arg a) {
     return lean_box(lean_array_size(a));
 }
 
-static inline lean_object * lean_mk_empty_array() {
-    return lean_alloc_array(0, 0);
-}
+LEAN_EXPORT lean_object * lean_mk_empty_array(void);
 
 static inline lean_object * lean_mk_empty_array_with_capacity(b_lean_obj_arg capacity) {
     if (!lean_is_scalar(capacity)) lean_internal_panic_out_of_memory();
-    return lean_alloc_array(0, lean_unbox(capacity));
+    size_t c = lean_unbox(capacity);
+    if (c == 0) return lean_mk_empty_array();
+    return lean_alloc_array(0, c);
 }
 
 static inline lean_object * lean_array_uget(b_lean_obj_arg a, size_t i) {

src/runtime/object.cpp

@@ -495,6 +495,10 @@ static obj_res mk_closure_3_2(lean_cfun3 fn, obj_arg a1, obj_arg a2) {
 static object * g_array_empty = nullptr;
 
 object * array_mk_empty() {
+    return lean_mk_empty_array();
+}
+
+extern "C" LEAN_EXPORT object * lean_mk_empty_array() {
     return g_array_empty;
 }
 

tests/compile/array_empty_cached.lean

@@ -0,0 +1,29 @@
+module
+
+import Init.Data.Array.Basic
+import Init.Util
+
+/-!
+Tests that zero-capacity arrays reuse the runtime's cached empty array.
+-/
+
+set_option compiler.extract_closed false
+
+@[noinline] def empty : Unit → Array Nat := fun _ => Array.empty
+
+@[noinline] def emptyLiteral : Unit → Array Nat := fun _ => #[]
+
+@[noinline] def emptyWithCapacity : Unit → Array Nat := fun _ => Array.emptyWithCapacity 0
+
+@[noinline] def mkEmpty : Unit → Array Nat := fun _ => Array.mkEmpty 0
+
+@[noinline] def emptyWithPositiveCapacity : Unit → Array Nat := fun _ => Array.emptyWithCapacity 1
+
+public unsafe def main : IO Unit := do
+  let xs := empty ()
+  IO.println (ptrEq xs (emptyLiteral ()))
+  IO.println (ptrEq xs (emptyWithCapacity ()))
+  IO.println (ptrEq xs (mkEmpty ()))
+  IO.println (isExclusiveUnsafe (emptyWithPositiveCapacity ()))
+  let ys := xs.push 42
+  IO.println (xs.isEmpty && ys == #[42])

tests/compile/array_empty_cached.lean.no_interpret

@@ -0,0 +1 @@
+The interpreter does not model native reference-count exclusivity.

tests/compile/array_empty_cached.lean.out.expected

@@ -0,0 +1,5 @@
+true
+true
+true
+true
+true