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)

Equations

• (_ : Nonempty (MLList.Spec m)) = (_ : Nonempty (MLList.Spec m))

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

A monadic lazy list, controlled by an arbitrary monad.

Equations

• MLList m α = (MLList.spec m).listM α

@[inline]

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

The empty MLList.

Equations

• MLList.nil = (MLList.spec m).nil

@[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.

Equations

• MLList.cons = (MLList.spec m).cons

@[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.

Equations

• MLList.thunk = (MLList.spec m).thunk

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.

Equations

• MLList.squash = (MLList.spec m).squash

@[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.

Equations

• MLList.uncons = (MLList.spec m).uncons

@[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.

Equations

• MLList.uncons? = (MLList.spec m).uncons?

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

Equations

• MLList.instEmptyCollectionMLList = { emptyCollection := MLList.nil }

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

Equations

• MLList.instInhabitedMLList = { default := MLList.nil }

@[specialize #[]]

partial def MLList.forIn {m : Type u_1 → Type u_1} {n : Type u_1 → Type u_2} {α : Type u_1} {δ : 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.instForInMLList {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 α) α

Equations

• MLList.instForInMLList = { forIn := fun {β : Type u_1} [Monad n] => MLList.forIn }

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.

Equations

• MLList.singletonM x = MLList.squash fun (x_1 : Unit) => do let __do_lift ← x pure (MLList.cons __do_lift MLList.nil)

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.

Equations

• MLList.singleton x = MLList.singletonM (pure x)

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} {β : 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} {β : 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.

Equations

• MLList.fixl f s = MLList.fixlWith f s []

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.

Equations

• MLList.isEmpty xs = (ULift.up ∘ Option.isSome) <$> MLList.uncons xs

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

Convert a List to a MLList.

Equations

• MLList.ofList [] = MLList.nil
• MLList.ofList (h :: t) = MLList.cons h (MLList.thunk fun (x : Unit) => MLList.ofList t)

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.

Equations

• MLList.ofListM [] = MLList.nil
• MLList.ofListM (h :: t) = MLList.squash fun (x : Unit) => do let __do_lift ← h pure (MLList.cons __do_lift (MLList.ofListM t))

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.

Equations

• One or more equations did not get rendered due to their size.

@[specialize #[]]

def MLList.casesM {m : Type u_1 → 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.

Equations

• MLList.casesM xs hnil hcons = MLList.squash fun (x : Unit) => do let __do_lift ← MLList.uncons xs match __do_lift with | none => hnil () | some (x, xs) => hcons x xs

@[specialize #[]]

def MLList.cases {m : Type u_1 → 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.)

Equations

• One or more equations did not get rendered due to their size.

partial def MLList.foldsM {m : Type u_1 → 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} {α : 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₁, ...].

Equations

• MLList.folds f init L = MLList.foldsM (fun (b : β) (a : α) => pure (f b a)) init L

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.

Equations

• MLList.takeAsList xs n = MLList.takeAsList.go n [] xs

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.

Equations

• MLList.takeAsArray xs n = MLList.takeAsArray.go n #[] xs

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.

Equations

• MLList.drop xs 0 = xs
• MLList.drop xs (Nat.succ r_1) = MLList.cases xs (fun (x : Unit) => MLList.nil) fun (x : α) (l : MLList m α) => MLList.drop l r_1

partial def MLList.mapM {m : Type u_1 → 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} {β : Type u_1} [Monad m] (f : α → β) (L : MLList m α) : MLList m β

Apply a function to every element of a MLList.

Equations

• MLList.map f L = MLList.mapM (fun (a : α) => pure (f a)) L

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.

Equations

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

partial def MLList.filterMapM {m : Type u_1 → 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} {β : Type u_1} [Monad m] (f : α → Option β) : MLList m α → MLList m β

Filter and transform a MLList using an Option valued function.

Equations

• MLList.filterMap f = MLList.filterMapM fun (a : α) => pure (f a)

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.

Equations

• MLList.takeWhile f = MLList.takeWhileM fun (a : α) => pure { down := f a }

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.

Equations

• MLList.enum = MLList.enumFrom 0

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

The infinite monadic lazy list of natural numbers.

Equations

• MLList.range = MLList.fix (fun (n : Nat) => pure (n + 1)) 0

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

Iterate through the elements of Fin n.

Equations

• MLList.fin n = MLList.fin.go n 0

partial def MLList.fin.go {m : Type → Type} (n : Nat) (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.

Equations

• MLList.ofArray L = MLList.ofArray.go L 0

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).

Equations

• MLList.chunk L n = MLList.chunk.go n n #[] L

partial def MLList.chunk.go {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (n : Nat) (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.

Equations

• MLList.concat L a = MLList.append L fun (x : Unit) => MLList.cons a MLList.nil

partial def MLList.zip {m : Type u → 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} {β : 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.

Equations

• MLList.monadLift x = MLList.squash fun (x_1 : Unit) => do let __do_lift ← x pure (MLList.cons __do_lift MLList.nil)

partial def MLList.liftM {m : Type u_1 → Type u_1} {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} {α : 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} {α : 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.

Equations

• MLList.runState' L s = MLList.map (fun (x : α × σ) => x.fst) (MLList.runState L s)

partial def MLList.runReader {m : Type u → 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} {σ : 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.

Equations

• MLList.head? L = do let __do_lift ← MLList.uncons L pure (Option.map (fun (x : α × MLList m α) => x.fst) __do_lift)

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.

Equations

• MLList.takeUpToFirst L f = MLList.takeUpToFirstM L fun (a : α) => pure { down := f a }

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.

Equations

• MLList.getLast? L = do let __do_lift ← MLList.uncons L match __do_lift with | none => pure none | some (x, xs) => MLList.getLast?.aux x xs

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.

Equations

• MLList.getLast! L = Option.get! <$> MLList.getLast? L

def MLList.foldM {m : Type u_1 → 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.

Equations

• MLList.foldM f init L = do let __do_lift ← MLList.getLast? (MLList.foldsM f init L) pure (Option.getD __do_lift init)

def MLList.fold {m : Type u_1 → 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.

Equations

• MLList.fold f init L = MLList.foldM (fun (b : β) (a : α) => pure (f b a)) init L

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.

Equations

• MLList.head L = do let __discr ← MLList.uncons L match __discr with | some (r, snd) => pure r | x => failure

def MLList.firstM {m : Type u_1 → 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.

Equations

• MLList.firstM L f = MLList.head (MLList.filterMapM f L)

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.

Equations

• MLList.first L p = MLList.head (MLList.filter p L)

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

Equations

• MLList.instMonadMLList = Monad.mk

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

Equations

• MLList.instAlternativeMLList = Alternative.mk (fun {α : Type u_1} => MLList.nil) fun {α : Type u_1} => MLList.append

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

Equations

• MLList.instMonadLiftMLList = { monadLift := fun {α : Type u_1} => MLList.monadLift }