feat: add List.toArrayMap (#1090)

Batteries/Data/List.lean

@@ -1,3 +1,4 @@
+import Batteries.Data.List.ArrayMap
 import Batteries.Data.List.Basic
 import Batteries.Data.List.Count
 import Batteries.Data.List.EraseIdx

Batteries/Data/List/ArrayMap.lean

@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2024 Michael Rothgang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Rothgang
+-/
+
+universe u v w
+variable {α : Type u} {β : Type v}
+
+namespace List
+
+/--
+This function is provided as a more efficient runtime alternative to `(l.map f).toArray`.
+(It avoids the intermediate memory allocation of creating an intermediate list first.)
+For verification purposes, we immediately simplify it to that form.
+-/
+def toArrayMap (l : List α) (f : α → β) : Array β :=
+  l.foldl (init := #[]) fun acc x => acc.push (f x)
+
+-- Future: a toArrayMapM version could be useful (e.g. in mathlib's DeriveToExpr)
+-- def toArrayMapM {m : Type v → Type w} [Monad m] (l : List α) (f : α → m β) : m (Array β) :=
+--   l.foldlM (init := #[]) fun acc x => acc.push (f x)
+
+theorem toArrayMap_toList (l : List α) (f : α → β ) : (l.toArrayMap f).toList = l.map f := by
+  suffices ∀ arr : Array β, (l.foldl (init := arr) fun acc x => acc.push (f x)).toList
+      = arr.toList ++ l.map f from
+    this #[]
+  induction l with
+  | nil => simp
+  | cons head tail tail_ih =>
+    intro arr
+    have : arr.toList ++ f head :: map f tail = (arr.push (f head)).toList ++ map f tail := by simp
+    rw [List.foldl_cons, List.map_cons, this, ← tail_ih]
+
+
+@[simp]
+theorem toArrayMap_eq_toArray_map (l : List α) (f : α → β) : l.toArrayMap f = (l.map f).toArray :=
+  Array.ext' (by simpa using toArrayMap_toList l f)
+
+end List

BatteriesTest/ArrayMap.lean

@@ -0,0 +1,11 @@
+import Batteries.Data.List.ArrayMap
+
+open List
+
+/-- info: #[3, 4, 5, 6] -/
+#guard_msgs in
+#eval List.toArrayMap [0, 1, 2, 3] (fun n => n + 3)
+
+/-- info: #[7, 9, 15, 25] -/
+#guard_msgs in
+#eval toArrayMap [0, 1, 2, 3] (fun n => 2 * n ^ 2 + 7)

scripts/test.lean

@@ -3,8 +3,9 @@ Copyright (c) 2024 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
-open IO.Process
-open System
+import Batteries.Data.List.ArrayMap
+
+open IO.Process System
 
 /--
 Run tests.
@@ -26,7 +27,7 @@ def main (args : List String) : IO Unit := do
   let allowNoisy := args.contains "--allow-noisy"
   let targets ← match args.erase "--allow-noisy" with
   | [] => System.FilePath.walkDir "./test"
-  | _ => pure <| (args.map fun t => mkFilePath [".", "test", t] |>.withExtension "lean") |>.toArray
+  | _ => pure <| args.toArrayMap fun t => mkFilePath [".", "test", t] |>.withExtension "lean"
   let existing ← targets.filterM fun t => do pure <| (← t.pathExists) && !(← t.isDir)
   -- Generate a `lake env lean` task for each test target.
   let tasks ← existing.mapM fun t => do