# Loop consumers #

This module provides consumers that iterate over a given iterator, applying a certain user-supplied function in every iteration. Concretely, the following operations are provided:

- `ForIn` instances
- `Iter.fold`, the analogue of `List.foldl`
- `Iter.foldM`, the analogue of `List.foldlM`

These operations are implemented using the `IteratorLoop` and `IteratorLoopPartial` typeclasses.

source
@[inline]
def Std.Iterators.Iter.instForIn' {α β : Type w} {n : Type x → Type x'} [Monad n] [Iterator α Id β] [Finite α Id] [IteratorLoop α Id n] :
ForIn' n (Iter β) β { mem := fun (it : Iter β) (out : β) => it.IsPlausibleIndirectOutput out }

A `ForIn'` instance for iterators. Its generic membership relation is not easy to use, so this is not marked as `instance`. This way, more convenient instances can be built on top of it or future library improvements will make it more comfortable.

Equations

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

Instances For

source
instance Std.Iterators.instForInIterOfMonadOfFiniteOfIteratorLoopId (α β : Type w) (n : Type x → Type x') [Monad n] [Iterator α Id β] [Finite α Id] [IteratorLoop α Id n] :
ForIn n (Iter β) β
Equations

- Std.Iterators.instForInIterOfMonadOfFiniteOfIteratorLoopId α β n = instForInOfForIn'

source
@[inline]
def Std.Iterators.Iter.Partial.instForIn' {α β : Type w} {n : Type x → Type x'} [Monad n] [Iterator α Id β] [IteratorLoopPartial α Id n] :
ForIn' n (Partial β) β { mem := fun (it : Partial β) (out : β) => it.it.IsPlausibleIndirectOutput out }
Equations

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

Instances For

source
instance Std.Iterators.instForInPartialOfMonadOfIteratorLoopPartialId (α β : Type w) (n : Type x → Type x') [Monad n] [Iterator α Id β] [IteratorLoopPartial α Id n] :
ForIn n (Iter.Partial β) β
Equations

- Std.Iterators.instForInPartialOfMonadOfIteratorLoopPartialId α β n = instForInOfForIn'

source
instance Std.Iterators.instForMIterOfFiniteOfIteratorLoopId {m : Type x → Type x'} {α β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id m] :
ForM m (Iter β) β
Equations

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

source
instance Std.Iterators.instForMPartialOfFiniteOfIteratorLoopPartialId {m : Type x → Type x'} {α β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoopPartial α Id m] :
ForM m (Iter.Partial β) β
Equations

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

source
@[inline]
def Std.Iterators.Iter.foldM {m : Type x → Type x'} [Monad m] {α β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id m] (f : γ → β → m γ) (init : γ) (it : Iter β) :
m γ

Folds a monadic function over an iterator from the left, accumulating a value starting with `init`. The accumulated value is combined with the each element of the list in order, using `f`.

It is equivalent to `it.toList.foldlM`.

This function requires a `Finite` instance proving that the iterator will finish after a finite number of steps. If the iterator is not finite or such an instance is not available, consider using `it.allowNontermination.foldM` instead of `it.foldM`. However, it is not possible to formally verify the behavior of the partial variant.

Equations

- Std.Iterators.Iter.foldM f init it = forIn it init fun (x : β) (acc : γ) => ForInStep.yield <$> f acc x

Instances For

source
@[inline]
def Std.Iterators.Iter.Partial.foldM {m : Type x → Type x'} [Monad m] {α β : Type w} {γ : Type x} [Iterator α Id β] [IteratorLoopPartial α Id m] (f : γ → β → m γ) (init : γ) (it : Partial β) :
m γ

Folds a monadic function over an iterator from the left, accumulating a value starting with `init`. The accumulated value is combined with the each element of the list in order, using `f`.

It is equivalent to `it.toList.foldlM`.

This is a partial, potentially nonterminating, function. It is not possible to formally verify its behavior. If the iterator has a `Finite` instance, consider using `IterM.foldM` instead.

Equations

- Std.Iterators.Iter.Partial.foldM f init it = forIn it init fun (x : β) (acc : γ) => ForInStep.yield <$> f acc x

Instances For

source
@[inline]
def Std.Iterators.Iter.fold {α β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] (f : γ → β → γ) (init : γ) (it : Iter β) :
γ

Folds a function over an iterator from the left, accumulating a value starting with `init`. The accumulated value is combined with the each element of the list in order, using `f`.

It is equivalent to `it.toList.foldl`.

This function requires a `Finite` instance proving that the iterator will finish after a finite number of steps. If the iterator is not finite or such an instance is not available, consider using `it.allowNontermination.fold` instead of `it.fold`. However, it is not possible to formally verify the behavior of the partial variant.

Equations

- Std.Iterators.Iter.fold f init it = forIn it init fun (x : β) (acc : γ) => ForInStep.yield (f acc x)

Instances For

source
@[inline]
def Std.Iterators.Iter.Partial.fold {α β : Type w} {γ : Type x} [Iterator α Id β] [IteratorLoopPartial α Id Id] (f : γ → β → γ) (init : γ) (it : Partial β) :
γ

Folds a function over an iterator from the left, accumulating a value starting with `init`. The accumulated value is combined with the each element of the list in order, using `f`.

It is equivalent to `it.toList.foldl`.

This is a partial, potentially nonterminating, function. It is not possible to formally verify its behavior. If the iterator has a `Finite` instance, consider using `IterM.fold` instead.

Equations

- Std.Iterators.Iter.Partial.fold f init it = forIn it init fun (x : β) (acc : γ) => ForInStep.yield (f acc x)

Instances For

source
@[specialize #[]]
def Std.Iterators.Iter.anyM {α β : Type w} {m : Type → Type w'} [Monad m] [Iterator α Id β] [IteratorLoop α Id m] [Finite α Id] (p : β → m Bool) (it : Iter β) :
m Bool

Returns `true` if the monadic predicate `p` returns `true` for any element emitted by the iterator `it`.

`O(|xs|)`. Short-circuits upon encountering the first match. The elements in `it` are examined in order of iteration.

Equations

- Std.Iterators.Iter.anyM p it = forIn it false fun (x : β) (x_1 : Bool) => do let __do_lift ← p x if __do_lift = true then pure (ForInStep.done true) else pure (ForInStep.yield false)

Instances For

source
@[inline]
def Std.Iterators.Iter.any {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id] [Finite α Id] (p : β → Bool) (it : Iter β) :
Bool

Returns `true` if the pure predicate `p` returns `true` for any element emitted by the iterator `it`.

`O(|xs|)`. Short-circuits upon encountering the first match. The elements in `it` are examined in order of iteration.

Equations

- Std.Iterators.Iter.any p it = (Std.Iterators.Iter.anyM (fun (x : β) => pure (p x)) it).run

Instances For

source
@[specialize #[]]
def Std.Iterators.Iter.allM {α β : Type w} {m : Type → Type w'} [Monad m] [Iterator α Id β] [IteratorLoop α Id m] [Finite α Id] (p : β → m Bool) (it : Iter β) :
m Bool

Returns `true` if the monadic predicate `p` returns `true` for all elements emitted by the iterator `it`.

`O(|xs|)`. Short-circuits upon encountering the first mismatch. The elements in `it` are examined in order of iteration.

Equations

- Std.Iterators.Iter.allM p it = forIn it true fun (x : β) (x_1 : Bool) => do let __do_lift ← p x if __do_lift = true then pure (ForInStep.yield true) else pure (ForInStep.done false)

Instances For

source
@[inline]
def Std.Iterators.Iter.all {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id] [Finite α Id] (p : β → Bool) (it : Iter β) :
Bool

Returns `true` if the pure predicate `p` returns `true` for all elements emitted by the iterator `it`.

`O(|xs|)`. Short-circuits upon encountering the first mismatch. The elements in `it` are examined in order of iteration.

Equations

- Std.Iterators.Iter.all p it = (Std.Iterators.Iter.allM (fun (x : β) => pure (p x)) it).run

Instances For

source
@[inline]
def Std.Iterators.Iter.size {α β : Type w} [Iterator α Id β] [IteratorSize α Id] (it : Iter β) :
Nat

Computes how many elements the iterator returns. In monadic situations, it is unclear which effects are caused by calling `size`, and if the monad is nondeterministic, it is also unclear what the returned value should be. The reference implementation, `IteratorSize.defaultImplementation`, simply iterates over the whole iterator monadically, counting the number of emitted values. An `IteratorSize` instance is considered lawful if it is equal to the reference implementation.

Performance:

Default performance is linear in the number of steps taken by the iterator.

Equations

- it.size = (Std.Iterators.IteratorSize.size it.toIterM).run.down

Instances For

source
@[inline]
def Std.Iterators.Iter.Partial.size {α β : Type w} [Iterator α Id β] [IteratorSizePartial α Id] (it : Iter β) :
Nat

Computes how many elements the iterator emits.

With monadic iterators (`IterM`), it is unclear which effects are caused by calling `size`, and if the monad is nondeterministic, it is also unclear what the returned value should be. The reference implementation, `IteratorSize.defaultImplementation`, simply iterates over the whole iterator monadically, counting the number of emitted values. An `IteratorSize` instance is considered lawful if it is equal to the reference implementation.

This is the partial version of `size`. It does not require a proof of finiteness and might loop forever. It is not possible to verify the behavior in Lean because it uses `partial`.

Performance:

Default performance is linear in the number of steps taken by the iterator.

Equations

- Std.Iterators.Iter.Partial.size it = (Std.Iterators.IteratorSizePartial.size it.toIterM).run.down

Instances For

source
class Std.Iterators.LawfulIteratorSize (α : Type w) {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorSize α Id] :
Prop

`LawfulIteratorSize α m` ensures that the `size` function of an iterator behaves as if it iterated over the whole iterator, counting its elements and causing all the monadic side effects of the iterations. This is a fairly strong condition for monadic iterators and it will be false for many efficient implementations of `size` that compute the size without actually iterating.

This class is experimental and users of the iterator API should not explicitly depend on it.

- size_eq_size_toArray {it : Iter β} : it.size = it.toArray.size

Instances