Add permutations and LazyList.length to Util

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,10 +57,10 @@ namespace List
 Returns `True` if the list contains the given value
 
 ```idris
-export
+  export
-contains : Eq a => a -> List a -> Bool
+  contains : Eq a => a -> List a -> Bool
-contains x [] = False
+  contains x [] = False
-contains x (y :: xs) = 
+  contains x (y :: xs) = 
     if x == y 
       then True
       else contains x xs
@@ -76,9 +77,9 @@ rotations [1, 2, 3] == [[1, 2, 3], [3, 1, 2], [2, 3, 1]]
 ```
 
 ```idris
-export
+  export
-rotations : List a -> List (List a) 
+  rotations : List a -> List (List a) 
-rotations xs = rotations' (length xs) xs []
+  rotations xs = rotations' (length xs) xs []
     where
       rotations' : Nat -> List a -> (acc : List (List a)) -> List (List a)
       rotations' 0 xs acc = acc
@@ -88,6 +89,54 @@ rotations xs = rotations' (length xs) xs []
         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
 
 Define some operations for pairs of numbers, treating them roughly like vectors
@@ -166,12 +215,16 @@ 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
+  export
-cartProd : Foldable a => Foldable b => a e -> b f -> LazyList (e, f)
+  cartProd : Foldable a => Foldable b => a e -> b f -> LazyList (e, f)
-cartProd x y = 
+  cartProd x y = 
     let y = foldToLazy y
     in foldr (\e, acc => combine e y acc) [] x
     where
@@ -187,10 +240,10 @@ cartProd x y =
 Lazily concatenate a LazyList of LazyLists
 
 ```idris
-export
+  export
-lazyConcat : LazyList (LazyList a) -> LazyList a
+  lazyConcat : LazyList (LazyList a) -> LazyList a
-lazyConcat [] = []
+  lazyConcat [] = []
-lazyConcat (x :: xs) = x ++ lazyConcat xs
+  lazyConcat (x :: xs) = x ++ lazyConcat xs
 ```
 
 ### Group
@@ -198,15 +251,30 @@ lazyConcat (x :: xs) = x ++ lazyConcat xs
 Lazily group a LazyList
 
 ```idris
-export
+  export
-lazyGroup : Eq a => LazyList a -> LazyList (List1 a)
+  lazyGroup : Eq a => LazyList a -> LazyList (List1 a)
-lazyGroup [] = []
+  lazyGroup [] = []
-lazyGroup (x :: xs) = lazyGroup' xs x (x ::: [])
+  lazyGroup (x :: xs) = lazyGroup' xs x (x ::: [])
     where
-    lazyGroup' : LazyList a -> (current : a) -> (acc : List1 a) -> LazyList (List1 a)
+      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
+```