source
@[always_inline]
def Std.Iterators.Iter.flatMapAfterM {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β] [Iterator α₂ m γ] (f : β → m (IterM m γ)) (it₁ : Iter β) (it₂ : Option (IterM m γ)) :
IterM m γ

Let `it₁` and `it₂` be iterators and `f` a monadic function mapping `it₁`'s outputs to iterators of the same type as `it₂`. Then `it₁.flatMapAfterM f it₂` first goes over `it₂` and then over `it₁.flatMap f it₂`, emitting all their values.

The main purpose of this combinator is to represent the intermediate state of a `flatMap` iterator that is currently iterating over one of the inner iterators.

Marble diagram (without monadic effects):

    it₁                            --b      c    --d -⊥
    it₂                      a1-a2⊥
    f b                               b1-b2⊥
    f c                                      c1-c2⊥
    f d                                             ⊥
    it.flatMapAfterM f it₂   a1-a2----b1-b2--c1-c2----⊥

Termination properties:

- `Finite` instance: only if `it₁`, `it₂` and the inner iterators are finite
- `Productive` instance: only if `it₁` is finite and `it₂` and the inner iterators are productive

For certain functions `f`, the resulting iterator will be finite (or productive) even though no `Finite` (or `Productive`) instance is provided out of the box. For example, if the outer iterator is productive and the inner iterators are productive and provably never empty, then the resulting iterator is also productive.

Performance:

This combinator incurs an additional O(1) cost with each output of `it₁`, `it₂` or an internal iterator.

For each value emitted by the outer iterator `it₁`, this combinator calls `f`.

Equations

- Std.Iterators.Iter.flatMapAfterM f it₁ it₂ = Std.Iterators.IterM.flatMapAfterM f (Std.Iterators.Iter.mapM pure it₁) it₂

Instances For

source
@[always_inline]
def Std.Iterators.Iter.flatMapM {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β] [Iterator α₂ m γ] (f : β → m (IterM m γ)) (it : Iter β) :
IterM m γ

Let `it` be an iterator and `f` a monadic function mapping `it`'s outputs to iterators. Then `it.flatMapM f` is an iterator that goes over `it` and for each output, it applies `f` and iterates over the resulting iterator. `it.flatMapM f` emits all values obtained from the inner iterators -- first, all of the first inner iterator, then all of the second one, and so on.

Marble diagram (without monadic effects):

    it                 ---a      --b      c    --d -⊥
    f a                    a1-a2⊥
    f b                             b1-b2⊥
    f c                                    c1-c2⊥
    f d                                           ⊥
    it.flatMapM        ----a1-a2----b1-b2--c1-c2----⊥

Termination properties:

- `Finite` instance: only if `it` and the inner iterators are finite
- `Productive` instance: only if `it` is finite and the inner iterators are productive

For certain functions `f`, the resulting iterator will be finite (or productive) even though no `Finite` (or `Productive`) instance is provided out of the box. For example, if the outer iterator is productive and the inner iterators are productive and provably never empty, then the resulting iterator is also productive.

Performance:

This combinator incurs an additional O(1) cost with each output of `it` or an internal iterator.

For each value emitted by the outer iterator `it`, this combinator calls `f`.

Equations

- Std.Iterators.Iter.flatMapM f it = Std.Iterators.Iter.flatMapAfterM f it none

Instances For

source
@[always_inline]
def Std.Iterators.Iter.flatMapAfter {α β α₂ γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ] (f : β → Iter γ) (it₁ : Iter β) (it₂ : Option (Iter γ)) :
Iter γ

Let `it₁` and `it₂` be iterators and `f` a function mapping `it₁`'s outputs to iterators of the same type as `it₂`. Then `it₁.flatMapAfter f it₂` first goes over `it₂` and then over `it₁.flatMap f it₂`, emitting all their values.

The main purpose of this combinator is to represent the intermediate state of a `flatMap` iterator that is currently iterating over one of the inner iterators.

Marble diagram:

    it₁                            --b      c    --d -⊥
    it₂                      a1-a2⊥
    f b                               b1-b2⊥
    f c                                      c1-c2⊥
    f d                                             ⊥
    it.flatMapAfter  f it₂   a1-a2----b1-b2--c1-c2----⊥

Termination properties:

- `Finite` instance: only if `it₁`, `it₂` and the inner iterators are finite
- `Productive` instance: only if `it₁` is finite and `it₂` and the inner iterators are productive

For certain functions `f`, the resulting iterator will be finite (or productive) even though no `Finite` (or `Productive`) instance is provided out of the box. For example, if the outer iterator is productive and the inner iterators are productive and provably never empty, then the resulting iterator is also productive.

Performance:

This combinator incurs an additional O(1) cost with each output of `it₁`, `it₂` or an internal iterator.

For each value emitted by the outer iterator `it₁`, this combinator calls `f`.

Equations

- Std.Iterators.Iter.flatMapAfter f it₁ it₂ = (Std.Iterators.IterM.flatMapAfter (fun (b : β) => (f b).toIterM) it₁.toIterM (Std.Iterators.Iter.toIterM <$> it₂)).toIter

Instances For

source
@[always_inline]
def Std.Iterators.Iter.flatMap {α β α₂ γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ] (f : β → Iter γ) (it : Iter β) :
Iter γ

Let `it` be an iterator and `f` a function mapping `it`'s outputs to iterators. Then `it.flatMap f` is an iterator that goes over `it` and for each output, it applies `f` and iterates over the resulting iterator. `it.flatMap f` emits all values obtained from the inner iterators -- first, all of the first inner iterator, then all of the second one, and so on.

Marble diagram:

    it                 ---a      --b      c    --d -⊥
    f a                    a1-a2⊥
    f b                             b1-b2⊥
    f c                                    c1-c2⊥
    f d                                           ⊥
    it.flatMap         ----a1-a2----b1-b2--c1-c2----⊥

Termination properties:

- `Finite` instance: only if `it` and the inner iterators are finite
- `Productive` instance: only if `it` is finite and the inner iterators are productive

For certain functions `f`, the resulting iterator will be finite (or productive) even though no `Finite` (or `Productive`) instance is provided out of the box. For example, if the outer iterator is productive and the inner iterators are productive and provably never empty, then the resulting iterator is also productive.

Performance:

This combinator incurs an additional O(1) cost with each output of `it` or an internal iterator.

For each value emitted by the outer iterator `it`, this combinator calls `f`.

Equations

- Std.Iterators.Iter.flatMap f it = Std.Iterators.Iter.flatMapAfter f it none

Instances For