# Functions for splitting monadic lazy lists. #

partial def MLList.getUpToFirstM {α : Type u} {m : Type u → Type u} [] (L : MLList m α) (p : αm ()) :
m (List α × MLList m α)

Extract the prefix of a lazy list consisting of elements up to and including the first element satisfying a monadic predicate. Return (in the monad) the prefix as a List, along with the remaining elements as a MLList.

def MLList.getUpToFirst {α : Type u} {m : Type u → Type u} [] (L : MLList m α) (p : αBool) :
m (List α × MLList m α)

Extract the prefix of a lazy list consisting of elements up to and including the first element satisfying a predicate. Return (in the monad) the prefix as a List, along with the remaining elements as a MLList.

Equations
• L.getUpToFirst p = L.getUpToFirstM fun (a : α) => pure { down := p a }
Instances For
partial def MLList.splitWhileM {α : Type u} {m : Type u → Type u} [] (L : MLList m α) (p : αm ()) :
m (List α × MLList m α)

Extract a maximal prefix of a lazy list consisting of elements satisfying a monadic predicate. Return (in the monad) the prefix as a List, along with the remaining elements as a MLList.

(Note that the first element not satisfying the predicate will be generated, and pushed back on to the remaining lazy list.)

def MLList.splitWhile {α : Type u} {m : Type u → Type u} [] (L : MLList m α) (p : αBool) :
m (List α × MLList m α)

Extract a maximal prefix of a lazy list consisting of elements satisfying a predicate. Return (in the monad) the prefix as a List, along with the remaining elements as a MLList.

(Note that the first element not satisfying the predicate will be generated, and pushed back on to the remaining lazy list.)

Equations
• L.splitWhile p = L.splitWhileM fun (a : α) => pure { down := p a }
Instances For
partial def MLList.groupByM {α : Type u} {β : Type u} {m : Type u → Type u} [] [] (L : MLList m α) (f : αm β) :
MLList m (β × List α)

Splits a lazy list into contiguous sublists of elements with the same value under a monadic function. Return a lazy lists of pairs, consisting of a value under that function, and a maximal list of elements having that value.

def MLList.groupBy {α : Type u} {β : Type u} {m : Type u → Type u} [] [] (L : MLList m α) (f : αβ) :
MLList m (β × List α)

Splits a lazy list into contiguous sublists of elements with the same value under a function. Return a lazy lists of pairs, consisting of a value under that function, and a maximal list of elements having that value.

Equations
• L.groupBy f = L.groupByM fun (a : α) => pure (f a)
Instances For
def MLList.splitAtBecomesTrueM {α : Type u} {m : Type u → Type u} [] (L : MLList m α) (p : αm ()) :
MLList m (List α)

Split a lazy list into contiguous sublists, starting a new sublist each time a monadic predicate changes from false to true.

Equations
Instances For
partial def MLList.splitAtBecomesTrueM.aux {α : Type u} {m : Type u → Type u} [] (M : MLList m ( × List α)) :
MLList m (List α)
def MLList.splitAtBecomesTrue {α : Type u} {m : Type u → Type u} [] (L : MLList m α) (p : αBool) :
MLList m (List α)

Split a lazy list into contiguous sublists, starting a new sublist each time a predicate changes from false to true.

Equations
• L.splitAtBecomesTrue p = L.splitAtBecomesTrueM fun (a : α) => pure { down := p a }
Instances For