From ac93582e969ed92415f8d3a002e6f73161667185 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Tue, 28 Jan 2025 09:48:11 -0500
Subject: [PATCH] Add permutations and LazyList.length to Util

---
 src/Util.md | 154 +++++++++++++++++++++++++++++++++++++---------------
 1 file changed, 111 insertions(+), 43 deletions(-)

diff --git a/src/Util.md b/src/Util.md
index 4e8de44..c2979cb 100644
--- a/src/Util.md
+++ b/src/Util.md
@@ -10,6 +10,7 @@ import Data.SortedSet
 import Data.String
 import Data.List.Lazy
 import Data.List1
+import Data.Vect
 
 %default total
 ```
@@ -56,13 +57,13 @@ namespace List
 Returns `True` if the list contains the given value
 
 ```idris
-export
-contains : Eq a => a -> List a -> Bool
-contains x [] = False
-contains x (y :: xs) = 
-  if x == y 
-    then True
-    else contains x xs
+  export
+  contains : Eq a => a -> List a -> Bool
+  contains x [] = False
+  contains x (y :: xs) = 
+    if x == y 
+      then True
+      else contains x xs
 ```
 
 ### rotations
@@ -76,16 +77,64 @@ rotations [1, 2, 3] == [[1, 2, 3], [3, 1, 2], [2, 3, 1]]
 ```
 
 ```idris
-export
-rotations : List a -> List (List a) 
-rotations xs = rotations' (length xs) xs []
-  where
-    rotations' : Nat -> List a -> (acc : List (List a)) -> List (List a)
-    rotations' 0 xs acc = acc
-    rotations' (S k) [] acc = acc
-    rotations' (S k) (x :: xs) acc = 
-      let next = xs ++ [x]
-      in rotations' k next (next :: acc)
+  export
+  rotations : List a -> List (List a) 
+  rotations xs = rotations' (length xs) xs []
+    where
+      rotations' : Nat -> List a -> (acc : List (List a)) -> List (List a)
+      rotations' 0 xs acc = acc
+      rotations' (S k) [] acc = acc
+      rotations' (S k) (x :: xs) acc = 
+        let next = xs ++ [x]
+        in rotations' k next (next :: acc)
+```
+
+### permutations
+
+Lazily generate all of the permutations of a list
+
+```idris
+  export
+  permutations : List a -> LazyList (List a)
+  permutations [] = pure []
+  permutations xs = do
+    (head, tail) <- select xs
+    tail <- permutations (assert_smaller xs tail)
+    pure $ head :: tail
+    where 
+      consSnd : a -> (a, List a) -> (a, List a)
+      consSnd x (y, xs) = (y, x :: xs)
+      select : List a -> LazyList (a, List a)
+      select [] = []
+      select (x :: xs) = (x, xs) :: map (consSnd x) (select xs)
+```
+
+## Vect
+
+```idris hide
+namespace Vect
+```
+
+### permutations
+
+Lazily generate all the permutations of a Vect
+
+```idris
+  export
+  permutations : Vect n a -> LazyList (Vect n a)
+  permutations [] = []
+  permutations [x] = [[x]]
+  permutations (x :: xs) = do
+    (head, tail) <- select (x :: xs)
+    tail <- permutations tail
+    pure $ head :: tail
+    where
+      consSnd : a -> (a, Vect m a) -> (a, Vect (S m) a)
+      consSnd x (y, xs) = (y, x :: xs)
+      select : Vect (S m) a -> LazyList (a, Vect m a)
+      select [y] = [(y, [])]
+      select (y :: (z :: ys)) = 
+        (y, z :: ys) :: map (consSnd y) (select (z :: ys))
 ```
 
 ## Vectors
@@ -166,20 +215,24 @@ off of the string at a time, checking if the needle is a prefix at each step.
 
 ### Cartesian product
 
+```idris hide
+namespace LazyList
+```
+
 Lazily take the cartesian product of two foldables
 
 ```idris
-export
-cartProd : Foldable a => Foldable b => a e -> b f -> LazyList (e, f)
-cartProd x y = 
-  let y = foldToLazy y
-  in foldr (\e, acc => combine e y acc) [] x
-  where
-    foldToLazy : Foldable a' => a' e' -> LazyList e'
-    foldToLazy x = foldr (\e, acc => e :: acc) [] x
-    combine : e -> LazyList f -> LazyList (e, f) -> LazyList (e, f)
-    combine x [] rest = rest
-    combine x (y :: ys) rest = (x, y) :: combine x ys rest
+  export
+  cartProd : Foldable a => Foldable b => a e -> b f -> LazyList (e, f)
+  cartProd x y = 
+    let y = foldToLazy y
+    in foldr (\e, acc => combine e y acc) [] x
+    where
+      foldToLazy : Foldable a' => a' e' -> LazyList e'
+      foldToLazy x = foldr (\e, acc => e :: acc) [] x
+      combine : e -> LazyList f -> LazyList (e, f) -> LazyList (e, f)
+      combine x [] rest = rest
+      combine x (y :: ys) rest = (x, y) :: combine x ys rest
 ```
 
 ### Concat
@@ -187,10 +240,10 @@ cartProd x y =
 Lazily concatenate a LazyList of LazyLists
 
 ```idris
-export
-lazyConcat : LazyList (LazyList a) -> LazyList a
-lazyConcat [] = []
-lazyConcat (x :: xs) = x ++ lazyConcat xs
+  export
+  lazyConcat : LazyList (LazyList a) -> LazyList a
+  lazyConcat [] = []
+  lazyConcat (x :: xs) = x ++ lazyConcat xs
 ```
 
 ### Group
@@ -198,15 +251,30 @@ lazyConcat (x :: xs) = x ++ lazyConcat xs
 Lazily group a LazyList
 
 ```idris
-export
-lazyGroup : Eq a => LazyList a -> LazyList (List1 a)
-lazyGroup [] = []
-lazyGroup (x :: xs) = lazyGroup' xs x (x ::: [])
-  where
-    lazyGroup' : LazyList a -> (current : a) -> (acc : List1 a) -> LazyList (List1 a)
-    lazyGroup' [] current acc = [acc]
-    lazyGroup' (y :: ys) current acc@(head ::: tail) = 
-      if y == current
-        then lazyGroup' ys current (head ::: (y :: tail))
-        else acc :: lazyGroup (y :: ys)
+  export
+  lazyGroup : Eq a => LazyList a -> LazyList (List1 a)
+  lazyGroup [] = []
+  lazyGroup (x :: xs) = lazyGroup' xs x (x ::: [])
+    where
+      lazyGroup' : LazyList a -> (current : a) -> (acc : List1 a)
+        -> LazyList (List1 a)
+      lazyGroup' [] current acc = [acc]
+      lazyGroup' (y :: ys) current acc@(head ::: tail) = 
+        if y == current
+          then lazyGroup' ys current (head ::: (y :: tail))
+          else acc :: lazyGroup (y :: ys)
+```
+
+### length
+
+Calculate the length of a LazyList
+
+```idris
+  export
+  length : LazyList a -> Nat
+  length = length' 0
+    where
+      length' : Nat -> LazyList a -> Nat
+      length' k [] = k
+      length' k (x :: xs) = length' (S k) xs
 ```