Functions for splitting monadic lazy lists.

partial def MLList.getUpToFirstM {α : Type u} {m : Type u → Type u} [Monad m] (L : MLList m α) (p : α → m (ULift.{u, 0} Bool)) : 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} [Monad m] (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

• MLList.getUpToFirst L p = MLList.getUpToFirstM L fun (a : α) => pure { down := p a }

partial def MLList.splitWhileM {α : Type u} {m : Type u → Type u} [Monad m] (L : MLList m α) (p : α → m (ULift.{u, 0} Bool)) : 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} [Monad m] (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

• MLList.splitWhile L p = MLList.splitWhileM L fun (a : α) => pure { down := p a }

partial def MLList.groupByM {α : Type u} {β : Type u} {m : Type u → Type u} [Monad m] [DecidableEq β] (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} [Monad m] [DecidableEq β] (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

• MLList.groupBy L f = MLList.groupByM L fun (a : α) => pure (f a)

def MLList.splitAtBecomesTrueM {α : Type u} {m : Type u → Type u} [Monad m] (L : MLList m α) (p : α → m (ULift.{u, 0} Bool)) : 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

• MLList.splitAtBecomesTrueM L p = MLList.splitAtBecomesTrueM.aux (MLList.groupByM L p)

partial def MLList.splitAtBecomesTrueM.aux {α : Type u} {m : Type u → Type u} [Monad m] (M : MLList m (ULift.{u, 0} Bool × List α)) : MLList m (List α)

def MLList.splitAtBecomesTrue {α : Type u} {m : Type u → Type u} [Monad m] (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

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