Monadic lazy lists.

Lazy lists with "laziness" controlled by an arbitrary monad.

In an initial section we describe the specification of MLList, and provide a private unsafe implementation, and then a public opaque wrapper of this implementation, satisfying the specification.

instance MLList.instNonemptySpec {m : Type u_1 → Type u_1} : Nonempty (MLList.Spec✝ m)

def MLList (m : Type u → Type u) (α : Type u) : Type u

A monadic lazy list, controlled by an arbitrary monad.

@[inline]

def MLList.nil {m : Type u_1 → Type u_1} {α : Type u_1} : MLList m α

The empty MLList.

@[inline]

def MLList.cons {α : Type u_1} {m : Type u_1 → Type u_1} : α → MLList m α → MLList m α

Constructs a MLList from head and tail.

@[inline]

def MLList.thunk {m : Type u_1 → Type u_1} {α : Type u_1} : (Unit → MLList m α) → MLList m α

Embed a non-monadic thunk as a lazy list.

def MLList.squash {m : Type u_1 → Type u_1} {α : Type u_1} : (Unit → m (MLList m α)) → MLList m α

Lift a monadic lazy list inside the monad to a monadic lazy list.

@[inline]

def MLList.uncons {m : Type u → Type u} {α : Type u} [Monad m] : MLList m α → m (Option (α × MLList m α))

Deconstruct a MLList, returning inside the monad an optional pair α × MLList m α representing the head and tail of the list.

@[inline]

def MLList.uncons? {m : Type u → Type u} {α : Type u} : MLList m α → Option (Option (α × MLList m α))

Try to deconstruct a MLList, returning an optional pair α × MLList m α representing the head and tail of the list if it is already evaluated, and none otherwise.

instance MLList.instEmptyCollection {m : Type u_1 → Type u_1} {α : Type u_1} : EmptyCollection (MLList m α)

instance MLList.instInhabited {m : Type u_1 → Type u_1} {α : Type u_1} : Inhabited (MLList m α)

@[specialize #[]]

partial def MLList.forIn {m : Type u_1 → Type u_1} {n : Type u_1 → Type u_2} {α δ : Type u_1} [Monad m] [Monad n] [MonadLiftT m n] (as : MLList m α) (init : δ) (f : α → δ → n (ForInStep δ)) : n δ

The implementation of ForIn, which enables for a in L do ... notation.

instance MLList.instForInOfMonadOfMonadLiftT {m : Type u_1 → Type u_1} {n : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [MonadLiftT m n] : ForIn n (MLList m α) α

def MLList.singletonM {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (x : m α) : MLList m α

Construct a singleton monadic lazy list from a single monadic value.

def MLList.singleton {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (x : α) : MLList m α

Construct a singleton monadic lazy list from a single value.

partial def MLList.fix {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (f : α → m α) (x : α) : MLList m α

Construct a MLList recursively. Failures from f will result in uncons failing.

partial def MLList.fix?' {m : Type (max u_1 u_2) → Type (max u_1 u_2)} {α : Type u_2} {β : Type (max u_1 u_2)} [Monad m] (f : α → m (Option (β × α))) (init : α) : MLList m β

Constructs an MLList recursively, with state in α, recording terms from β. If f returns none the list will terminate.

Variant of MLList.fix? that allows returning values of a different type.

partial def MLList.fix? {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (f : α → m (Option α)) (x : α) : MLList m α

Constructs an MLList recursively. If f returns none the list will terminate.

Returns the initial value as the first element.

partial def MLList.iterate {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (f : m α) : MLList m α

Construct a MLList by iteration. (m must be a stateful monad for this to be useful.)

partial def MLList.fixlWith {m : Type u → Type u} [Monad m] {α β : Type u} (f : α → m (α × List β)) (s : α) (l : List β) : MLList m β

Repeatedly apply a function f : α → m (α × List β) to an initial a : α, accumulating the elements of the resulting List β as a single monadic lazy list.

(This variant allows starting with a specified List β of elements, as well. )

def MLList.fixl {m : Type u → Type u} [Monad m] {α β : Type u} (f : α → m (α × List β)) (s : α) : MLList m β

Repeatedly apply a function f : α → m (α × List β) to an initial a : α, accumulating the elements of the resulting List β as a single monadic lazy list.

def MLList.isEmpty {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (xs : MLList m α) : m (ULift Bool)

Compute, inside the monad, whether a MLList is empty.

def MLList.ofList {α : Type u_1} {m : Type u_1 → Type u_1} : List α → MLList m α

Convert a List to a MLList.

def MLList.ofListM {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] : List (m α) → MLList m α

Convert a List of values inside the monad into a MLList.

partial def MLList.force {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (L : MLList m α) : m (List α)

Extract a list inside the monad from a MLList.

def MLList.asArray {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (L : MLList m α) : m (Array α)

Extract an array inside the monad from a MLList.

@[specialize #[]]

def MLList.casesM {m : Type u_1 → Type u_1} {α β : Type u_1} [Monad m] (xs : MLList m α) (hnil : Unit → m (MLList m β)) (hcons : α → MLList m α → m (MLList m β)) : MLList m β

Performs a monadic case distinction on a MLList when the motive is a MLList as well.

@[specialize #[]]

def MLList.cases {m : Type u_1 → Type u_1} {α β : Type u_1} [Monad m] (xs : MLList m α) (hnil : Unit → MLList m β) (hcons : α → MLList m α → MLList m β) : MLList m β

Performs a case distinction on a MLList when the motive is a MLList as well. (We need to be in a monadic context to distinguish a nil from a cons.)

partial def MLList.foldsM {m : Type u_1 → Type u_1} {β α : Type u_1} [Monad m] (f : β → α → m β) (init : β) (L : MLList m α) : MLList m β

Gives the monadic lazy list consisting all of folds of a function on a given initial element. Thus [a₀, a₁, ...].foldsM f b will give [b, ← f b a₀, ← f (← f b a₀) a₁, ...].

def MLList.folds {m : Type u_1 → Type u_1} {β α : Type u_1} [Monad m] (f : β → α → β) (init : β) (L : MLList m α) : MLList m β

Gives the monadic lazy list consisting all of folds of a function on a given initial element. Thus [a₀, a₁, ...].foldsM f b will give [b, f b a₀, f (f b a₀) a₁, ...].

def MLList.takeAsList {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (xs : MLList m α) (n : Nat) : m (List α)

Take the first n elements, as a list inside the monad.

partial def MLList.takeAsList.go {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (r : Nat) (acc : List α) (xs : MLList m α) : m (List α)

Implementation of MLList.takeAsList.

def MLList.takeAsArray {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (xs : MLList m α) (n : Nat) : m (Array α)

Take the first n elements, as an array inside the monad.

partial def MLList.takeAsArray.go {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (r : Nat) (acc : Array α) (xs : MLList m α) : m (Array α)

Implementation of MLList.takeAsArray.

partial def MLList.take {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (xs : MLList m α) : Nat → MLList m α

Take the first n elements.

def MLList.drop {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (xs : MLList m α) : Nat → MLList m α

Drop the first n elements.

partial def MLList.mapM {m : Type u_1 → Type u_1} {α β : Type u_1} [Monad m] (f : α → m β) (xs : MLList m α) : MLList m β

Apply a function which returns values in the monad to every element of a MLList.

def MLList.map {m : Type u_1 → Type u_1} {α β : Type u_1} [Monad m] (f : α → β) (L : MLList m α) : MLList m β

Apply a function to every element of a MLList.

partial def MLList.filterM {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (p : α → m (ULift Bool)) (L : MLList m α) : MLList m α

Filter a MLList using a monadic function.

def MLList.filter {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (p : α → Bool) (L : MLList m α) : MLList m α

Filter a MLList.

partial def MLList.filterMapM {m : Type u_1 → Type u_1} {α β : Type u_1} [Monad m] (f : α → m (Option β)) (xs : MLList m α) : MLList m β

Filter and transform a MLList using a function that returns values inside the monad.

def MLList.filterMap {m : Type u_1 → Type u_1} {α β : Type u_1} [Monad m] (f : α → Option β) : MLList m α → MLList m β

Filter and transform a MLList using an Option valued function.

partial def MLList.takeWhileM {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (f : α → m (ULift Bool)) (L : MLList m α) : MLList m α

Take the initial segment of the lazy list, until the function f first returns false.

def MLList.takeWhile {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (f : α → Bool) : MLList m α → MLList m α

Take the initial segment of the lazy list, until the function f first returns false.

partial def MLList.append {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (xs : MLList m α) (ys : Unit → MLList m α) : MLList m α

Concatenate two monadic lazy lists.

partial def MLList.join {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (xs : MLList m (MLList m α)) : MLList m α

Join a monadic lazy list of monadic lazy lists into a single monadic lazy list.

partial def MLList.enumFrom {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (n : Nat) (xs : MLList m α) : MLList m (Nat × α)

Enumerate the elements of a monadic lazy list, starting at a specified offset.

def MLList.enum {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] : MLList m α → MLList m (Nat × α)

Enumerate the elements of a monadic lazy list.

def MLList.range {m : Type → Type} [Monad m] : MLList m Nat

The infinite monadic lazy list of natural numbers.

def MLList.fin {m : Type → Type} (n : Nat) : MLList m (Fin n)

Iterate through the elements of Fin n.

partial def MLList.fin.go {m : Type → Type} (n i : Nat) : MLList m (Fin n)

Implementation of MLList.fin.

def MLList.ofArray {m : Type → Type} {α : Type} (L : Array α) : MLList m α

Convert an array to a monadic lazy list.

partial def MLList.ofArray.go {m : Type → Type} {α : Type} (L : Array α) (i : Nat) : MLList m α

Implementation of MLList.ofArray.

def MLList.chunk {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (L : MLList m α) (n : Nat) : MLList m (Array α)

Group the elements of a lazy list into chunks of a given size. If the lazy list is finite, the last chunk may be smaller (possibly even length 0).

partial def MLList.chunk.go {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (n r : Nat) (acc : Array α) (M : MLList m α) : MLList m (Array α)

Implementation of MLList.chunk.

def MLList.concat {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (L : MLList m α) (a : α) : MLList m α

Add one element to the end of a monadic lazy list.

partial def MLList.zip {m : Type u → Type u} {α β : Type u} [Monad m] (L : MLList m α) (M : MLList m β) : MLList m (α × β)

Take the product of two monadic lazy lists.

partial def MLList.bind {m : Type u_1 → Type u_1} {α β : Type u_1} [Monad m] (xs : MLList m α) (f : α → MLList m β) : MLList m β

Apply a function returning a monadic lazy list to each element of a monadic lazy list, joining the results.

def MLList.monadLift {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (x : m α) : MLList m α

Convert any value in the monad to the singleton monadic lazy list.

partial def MLList.liftM {m n : Type u_1 → Type u_1} {α : Type u_1} [Monad m] [Monad n] [MonadLiftT m n] (L : MLList m α) : MLList n α

Lift the monad of a lazy list.

partial def MLList.runState {m : Type u → Type u} {σ α : Type u} [Monad m] (L : MLList (StateT σ m) α) (s : σ) : MLList m (α × σ)

Given a lazy list in a state monad, run it on some initial state, recording the states.

def MLList.runState' {m : Type u → Type u} {σ α : Type u} [Monad m] (L : MLList (StateT σ m) α) (s : σ) : MLList m α

Given a lazy list in a state monad, run it on some initial state.

partial def MLList.runReader {m : Type u → Type u} {ρ α : Type u} [Monad m] (L : MLList (ReaderT ρ m) α) (r : ρ) : MLList m α

Run a lazy list in a ReaderT monad on some fixed state.

partial def MLList.runStateRef {m : Type → Type} {ω σ α : Type} [Monad m] [MonadLiftT (ST ω) m] (L : MLList (StateRefT' ω σ m) α) (s : σ) : MLList m α

Run a lazy list in a StateRefT' monad on some initial state.

def MLList.head? {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (L : MLList m α) : m (Option α)

Return the head of a monadic lazy list if it exists, as an Option in the monad.

partial def MLList.takeUpToFirstM {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (L : MLList m α) (f : α → m (ULift Bool)) : MLList m α

Take the initial segment of the lazy list, up to and including the first place where f gives true.

def MLList.takeUpToFirst {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (L : MLList m α) (f : α → Bool) : MLList m α

Take the initial segment of the lazy list, up to and including the first place where f gives true.

def MLList.getLast? {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (L : MLList m α) : m (Option α)

Gets the last element of a monadic lazy list, as an option in the monad. This will run forever if the list is infinite.

partial def MLList.getLast?.aux {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (x : α) (L : MLList m α) : m (Option α)

Implementation of MLList.aux.

def MLList.getLast! {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] [Inhabited α] (L : MLList m α) : m α

Gets the last element of a monadic lazy list, or the default value if the list is empty. This will run forever if the list is infinite.

def MLList.foldM {m : Type u_1 → Type u_1} {β α : Type u_1} [Monad m] (f : β → α → m β) (init : β) (L : MLList m α) : m β

Folds a binary function across a monadic lazy list, from an initial starting value. This will run forever if the list is infinite.

def MLList.fold {m : Type u_1 → Type u_1} {β α : Type u_1} [Monad m] (f : β → α → β) (init : β) (L : MLList m α) : m β

Folds a binary function across a monadic lazy list, from an initial starting value. This will run forever if the list is infinite.

def MLList.head {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] [Alternative m] (L : MLList m α) : m α

Return the head of a monadic lazy list, as a value in the monad. Fails if the list is empty.

def MLList.firstM {m : Type u_1 → Type u_1} {α β : Type u_1} [Monad m] [Alternative m] (L : MLList m α) (f : α → m (Option β)) : m β

Apply a function returning values inside the monad to a monadic lazy list, returning only the first successful result.

def MLList.first {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] [Alternative m] (L : MLList m α) (p : α → Bool) : m α

Return the first value on which a predicate returns true.

instance MLList.instMonad {m : Type u_1 → Type u_1} [Monad m] : Monad (MLList m)

instance MLList.instAlternativeOfMonad {m : Type u_1 → Type u_1} [Monad m] : Alternative (MLList m)

instance MLList.instMonadLiftOfMonad {m : Type u_1 → Type u_1} [Monad m] : MonadLift m (MLList m)