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

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

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

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