From 87e860f87155751bd8a088206f60df4dc4ebf7fe Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 16 Dec 2021 15:06:51 +0100 Subject: [PATCH] perf: Array.push: move elements directly when source is unique --- src/runtime/object.cpp | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index e2878c57a1..0fcf649cb8 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -2064,11 +2064,17 @@ extern "C" LEAN_EXPORT obj_res lean_copy_expand_array(obj_arg a, bool expand) { object ** it = lean_array_cptr(a); object ** end = it + sz; object ** dest = lean_array_cptr(r); - for (; it != end; ++it, ++dest) { - *dest = *it; - lean_inc(*it); + if (lean_is_exclusive(a)) { + // transfer ownership of elements directly instead of inc+dec + memcpy(dest, it, sz * sizeof(object *)); + lean_dealloc(a, lean_array_byte_size(a)); + } else { + for (; it != end; ++it, ++dest) { + *dest = *it; + lean_inc(*it); + } + lean_dec(a); } - lean_dec(a); return r; }