From 7a9384c46db1480cb562117372977ebca16f9dcb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 3 Oct 2024 12:46:53 +0100
Subject: [PATCH] perf: remove List.redLength

---
 src/Init/Data/Array/Basic.lean  |  1 +
 src/Init/Data/List.lean         |  1 +
 src/Init/Data/List/ToArray.lean | 23 +++++++++++++++++++++++
 src/Init/Prelude.lean           | 22 ----------------------
 4 files changed, 25 insertions(+), 22 deletions(-)
 create mode 100644 src/Init/Data/List/ToArray.lean

diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 509343f11f03..69418da8d64a 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -11,6 +11,7 @@ import Init.Data.UInt.Basic
 import Init.Data.Repr
 import Init.Data.ToString.Basic
 import Init.GetElem
+import Init.Data.List.ToArray
 universe u v w
 
 /-! ### Array literal syntax -/
diff --git a/src/Init/Data/List.lean b/src/Init/Data/List.lean
index 94e8c22a6e47..e00a18706fbb 100644
--- a/src/Init/Data/List.lean
+++ b/src/Init/Data/List.lean
@@ -23,3 +23,4 @@ import Init.Data.List.TakeDrop
 import Init.Data.List.Zip
 import Init.Data.List.Perm
 import Init.Data.List.Sort
+import Init.Data.List.ToArray
diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean
new file mode 100644
index 000000000000..214364b5bb88
--- /dev/null
+++ b/src/Init/Data/List/ToArray.lean
@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Init.Data.List.Basic
+
+/--
+Auxiliary definition for `List.toArray`.
+`List.toArrayAux as r = r ++ as.toArray`
+-/
+@[inline_if_reduce]
+def List.toArrayAux : List α → Array α → Array α
+  | nil,       r => r
+  | cons a as, r => toArrayAux as (r.push a)
+
+/-- Convert a `List α` into an `Array α`. This is O(n) in the length of the list.  -/
+-- This function is exported to C, where it is called by `Array.mk`
+-- (the constructor) to implement this functionality.
+@[inline, match_pattern, pp_nodot, export lean_list_to_array]
+def List.toArrayImpl (as : List α) : Array α :=
+  as.toArrayAux (Array.mkEmpty as.length)
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 36be316832e6..b8e8472c081c 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -2716,28 +2716,6 @@ def Array.extract (as : Array α) (start stop : Nat) : Array α :=
   let sz' := Nat.sub (min stop as.size) start
   loop sz' start (mkEmpty sz')
 
-/--
-Auxiliary definition for `List.toArray`.
-`List.toArrayAux as r = r ++ as.toArray`
--/
-@[inline_if_reduce]
-def List.toArrayAux : List α → Array α → Array α
-  | nil,       r => r
-  | cons a as, r => toArrayAux as (r.push a)
-
-/-- A non-tail-recursive version of `List.length`, used for `List.toArray`. -/
-@[inline_if_reduce]
-def List.redLength : List α → Nat
-  | nil       => 0
-  | cons _ as => as.redLength.succ
-
-/-- Convert a `List α` into an `Array α`. This is O(n) in the length of the list.  -/
--- This function is exported to C, where it is called by `Array.mk`
--- (the constructor) to implement this functionality.
-@[inline, match_pattern, pp_nodot, export lean_list_to_array]
-def List.toArrayImpl (as : List α) : Array α :=
-  as.toArrayAux (Array.mkEmpty as.redLength)
-
 /-- The typeclass which supplies the `>>=` "bind" function. See `Monad`. -/
 class Bind (m : Type u → Type v) where
   /-- If `x : m α` and `f : α → m β`, then `x >>= f : m β` represents the