diff --git a/src/Util.md b/src/Util.md index 62d4a83..c7a9bbc 100644 --- a/src/Util.md +++ b/src/Util.md @@ -9,6 +9,7 @@ module Util import Data.SortedSet import Data.String import Data.List.Lazy +import Data.List1 %default total ``` @@ -180,3 +181,32 @@ cartProd x y = combine x [] rest = rest combine x (y :: ys) rest = (x, y) :: combine x ys rest ``` + +### Concat + +Lazily concatenate a LazyList of LazyLists + +```idris +export +lazyConcat : LazyList (LazyList a) -> LazyList a +lazyConcat [] = [] +lazyConcat (x :: xs) = x ++ lazyConcat xs +``` + +### Group + +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) +```