From 7fbbb030df0cfd115e3f3e62b71479c3c44df571 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Stefan=20H=C3=B6ck?= <hock@zhaw.ch>
Date: Fri, 13 Oct 2023 14:48:15 +0200
Subject: [PATCH] [ new ] add Data.List.grouped function (#3089)

---
 CHANGELOG.md            |  2 ++
 libs/base/Data/List.idr | 18 ++++++++++++++++++
 2 files changed, 20 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 59f0fa6e3c..5f2a5ae4b8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -211,6 +211,8 @@
 
 * Adds updating functions to `SortedMap` and `SortedDMap`.
 
+* Adds `grouped` function to `Data.List` for splitting a list into equal-sized slices.
+
 * Implements `Ord` for `Count` from `Language.Reflection`.
 
 * Implements `MonadState` for `Data.Ref` with a named implementation requiring
diff --git a/libs/base/Data/List.idr b/libs/base/Data/List.idr
index 9e6c8d2f48..2ff1608b19 100644
--- a/libs/base/Data/List.idr
+++ b/libs/base/Data/List.idr
@@ -925,6 +925,24 @@ public export
 groupAllWith : Ord b => (a -> b) -> List a -> List (List1 a)
 groupAllWith f = groupWith f . sortBy (comparing f)
 
+||| Partitions a list into fixed sized sublists.
+|||
+||| Note: The last list in the result might be shorter than the rest if
+|||       the input cannot evenly be split into groups of the same size.
+|||
+||| ```idris example
+||| grouped 3 [1..10] === [[1,2,3],[4,5,6],[7,8,9],[10]]
+||| ```
+public export
+grouped : (n : Nat) -> {auto 0 p : IsSucc n} -> List a -> List (List a)
+grouped _     []      = []
+grouped (S m) (x::xs) = go [<] [<x] m xs
+  where
+    go : SnocList (List a) -> SnocList a -> Nat -> List a -> List (List a)
+    go sxs sx c     []        = sxs <>> [sx <>> []]
+    go sxs sx 0     (x :: xs) = go (sxs :< (sx <>> [])) [<x] m xs
+    go sxs sx (S k) (x :: xs) = go sxs (sx :< x) k xs
+
 --------------------------------------------------------------------------------
 -- Properties
 --------------------------------------------------------------------------------