# Monadic `filterMap`, `filter` and `map` combinators #

This file provides iterator combinators for filtering and mapping.

- `IterM.filterMap` either modifies or drops each value based on an option-valued mapping function.
- `IterM.filter` drops some elements based on a predicate.
- `IterM.map` modifies each value based on a mapping function

Several variants of these combinators are provided:

- `M` suffix: Instead of a pure function, these variants take a monadic function. Given a suitable `MonadLiftT` instance, they also allow lifting the iterator to another monad first and then applying the mapping function in this monad.
- `WithPostcondition` suffix: These variants take a monadic function where the return type in the monad is a subtype. This variant is in rare cases necessary for the intrinsic verification of an iterator, and particularly for specialized termination proofs. If possible, avoid this.

source
@[unbox]
structure Std.Iterators.FilterMap (α : Type w) {β γ : Type w} (m : Type w → Type w') (n : Type w → Type w'') (lift : ⦃α : Type w⦄ → m α → n α) (f : β → PostconditionT n (Option γ)) :
Type w

Internal state of the `filterMap` combinator. Do not depend on its internals.

- inner : IterM m β

  Internal implementation detail of the iterator library.

Instances For

source
theorem Std.Iterators.FilterMap.ext_iff {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} {x y : FilterMap α m n lift f} :
x = y ↔ x.inner = y.inner
source
theorem Std.Iterators.FilterMap.ext {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} {x y : FilterMap α m n lift f} (inner : x.inner = y.inner) :
x = y
source
def Std.Iterators.Map (α : Type w) {β γ : Type w} (m : Type w → Type w') (n : Type w → Type w'') (lift : ⦃α : Type w⦄ → m α → n α) [Functor n] (f : β → PostconditionT n γ) :
Type w

Internal state of the `map` combinator. Do not depend on its internals.

Equations

- Std.Iterators.Map α m n lift f = Std.Iterators.FilterMap α m n lift fun (b : β) => Std.Iterators.PostconditionT.map some (f b)

Instances For

source
@[inline]
def Std.Iterators.IterM.InternalCombinators.filterMap {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} (lift : ⦃α : Type w⦄ → m α → n α) [Iterator α m β] (f : β → PostconditionT n (Option γ)) (it : IterM m β) :
IterM n γ
Equations

- Std.Iterators.IterM.InternalCombinators.filterMap lift f it = Std.Iterators.toIterM { inner := it } n γ

Instances For

source
@[inline]
def Std.Iterators.IterM.InternalCombinators.map {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] (lift : ⦃α : Type w⦄ → m α → n α) [Iterator α m β] (f : β → PostconditionT n γ) (it : IterM m β) :
IterM n γ
Equations

- Std.Iterators.IterM.InternalCombinators.map lift f it = Std.Iterators.toIterM { inner := it } n γ

Instances For

source
@[inline]
def Std.Iterators.IterM.filterMapWithPostcondition {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [MonadLiftT m n] [Iterator α m β] (f : β → PostconditionT n (Option γ)) (it : IterM m β) :
IterM n γ

Note: This is a very general combinator that requires an advanced understanding of monads, dependent types and termination proofs. The variants `filterMap` and `filterMapM` are easier to use and sufficient for most use cases.

If `it` is an iterator, then `it.filterMapWithPostcondition f` is another iterator that applies a monadic function `f` to all values emitted by `it`. `f` is expected to return an `Option` inside the monad. If `f` returns `none`, then nothing is emitted; if it returns `some x`, then `x` is emitted.

`f` is expected to return `PostconditionT n (Option _)`. The base iterator `it` being monadic in `m`, `n` can be different from `m`, but `it.filterMapWithPostcondition f` expects a `MonadLiftT m n` instance. The `PostconditionT` transformer allows the caller to intrinsically prove properties about `f`'s return value in the monad `n`, enabling termination proofs depending on the specific behavior of `f`.

Marble diagram (without monadic effects):

    it                                ---a --b--c --d-e--⊥
    it.filterMapWithPostcondition     ---a'-----c'-------⊥

(given that `f a = pure (some a)'`, `f c = pure (some c')` and `f b = f d = d e = pure none`)

Termination properties:

- `Finite` instance: only if `it` is finite
- `Productive` instance: only if `it` is finite`

For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though no `Finite` (or `Productive`) instance is provided. For example, if `f` never returns `none`, then this combinator will preserve productiveness. If `f` is an `ExceptT` monad and will always fail, then `it.filterMapWithPostcondition` will be finite even if `it` isn't. In the first case, consider using the `map`/`mapM`/`mapWithPostcondition` combinators instead, which provide more instances out of the box.

In such situations, the missing instances can be proved manually if the postcondition bundled in the `PostconditionT n` monad is strong enough. If `f` always returns `some _`, a suitable postcondition is `fun x => x.isSome`; if `f` always fails, a suitable postcondition might be `fun _ => False`.

Performance:

For each value emitted by the base iterator `it`, this combinator calls `f` and matches on the returned `Option` value.

Equations

- Std.Iterators.IterM.filterMapWithPostcondition f it = Std.Iterators.IterM.InternalCombinators.filterMap (fun ⦃x : Type ?u.26⦄ => monadLift) f it

Instances For

source
inductive Std.Iterators.FilterMap.PlausibleStep {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} [Iterator α m β] (it : IterM n γ) :
IterStep (IterM n γ) γ → Prop

`it.PlausibleStep step` is the proposition that `step` is a possible next step from the `filterMap` iterator `it`. This is mostly internally relevant, except if one needs to manually prove termination (`Finite` or `Productive` instances, for example) of a `filterMap` iterator.

- yieldNone {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} [Iterator α m β] {it : IterM n γ} {it' : IterM m β} {out : β} : it.internalState.inner.IsPlausibleStep (IterStep.yield it' out) → (f out).Property none → PlausibleStep it (IterStep.skip (IterM.InternalCombinators.filterMap lift f it'))
- yieldSome {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} [Iterator α m β] {it : IterM n γ} {it' : IterM m β} {out : β} {out' : γ} : it.internalState.inner.IsPlausibleStep (IterStep.yield it' out) → (f out).Property (some out') → PlausibleStep it (IterStep.yield (IterM.InternalCombinators.filterMap lift f it') out')
- skip {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} [Iterator α m β] {it : IterM n γ} {it' : IterM m β} : it.internalState.inner.IsPlausibleStep (IterStep.skip it') → PlausibleStep it (IterStep.skip (IterM.InternalCombinators.filterMap lift f it'))
- done {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} [Iterator α m β] {it : IterM n γ} : it.internalState.inner.IsPlausibleStep IterStep.done → PlausibleStep it IterStep.done

Instances For

source
instance Std.Iterators.FilterMap.instIterator {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} [Iterator α m β] [Monad n] :
Iterator (FilterMap α m n lift f) n γ
Equations

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

source
instance Std.Iterators.instIteratorMap {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n γ} :
Iterator (Map α m n lift f) n γ
Equations

- Std.Iterators.instIteratorMap = inferInstanceAs (Std.Iterators.Iterator (Std.Iterators.FilterMap α m n lift fun (b : β) => Std.Iterators.PostconditionT.map some (f b)) n γ)

source
instance Std.Iterators.FilterMap.instFinite {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} [Finite α m] :
Finite (FilterMap α m n lift f) n
source
instance Std.Iterators.instFiniteMap {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n γ} [Finite α m] :
Finite (Map α m n lift f) n
source
instance Std.Iterators.Map.instProductive {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n γ} [Productive α m] :
Productive (Map α m n lift f) n
source
instance Std.Iterators.instIteratorCollectFilterMapOfMonad {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type x} [Monad n] [Monad o] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} :
IteratorCollect (FilterMap α m n lift f) n o
Equations

- Std.Iterators.instIteratorCollectFilterMapOfMonad = Std.Iterators.IteratorCollect.defaultImplementation

source
instance Std.Iterators.instIteratorCollectPartialFilterMapOfMonadOfFinite {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type x} [Monad n] [Monad o] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} [Finite α m] :
IteratorCollectPartial (FilterMap α m n lift f) n o
Equations

- Std.Iterators.instIteratorCollectPartialFilterMapOfMonadOfFinite = Std.Iterators.IteratorCollectPartial.defaultImplementation

source
instance Std.Iterators.FilterMap.instIteratorLoop {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type x → Type x'} [Monad n] [Monad o] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} [Finite α m] :
IteratorLoop (FilterMap α m n lift f) n o
Equations

- Std.Iterators.FilterMap.instIteratorLoop = Std.Iterators.IteratorLoop.defaultImplementation

source
instance Std.Iterators.FilterMap.instIteratorLoopPartial {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type x → Type x'} [Monad n] [Monad o] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} :
IteratorLoopPartial (FilterMap α m n lift f) n o
Equations

- Std.Iterators.FilterMap.instIteratorLoopPartial = Std.Iterators.IteratorLoopPartial.defaultImplementation

source
instance Std.Iterators.Map.instIteratorCollect {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type x} [Monad n] [Monad o] [Iterator α m β] {lift₁ : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n γ} [IteratorCollect α m o] [Finite α m] :
IteratorCollect (Map α m n lift₁ f) n o

`map` operations allow for a more efficient implementation of `toArray`. For example, `array.iter.map f |>.toArray happens in-place if possible.

Equations

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

source
instance Std.Iterators.Map.instIteratorCollectPartial {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type x} [Monad n] [Monad o] [Iterator α m β] {lift₁ : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n γ} [IteratorCollectPartial α m o] :
IteratorCollectPartial (Map α m n lift₁ f) n o
Equations

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

source
instance Std.Iterators.Map.instIteratorLoop {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type x → Type x'} [Monad n] [Monad o] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n γ} :
IteratorLoop (Map α m n lift f) n o
Equations

- Std.Iterators.Map.instIteratorLoop = Std.Iterators.IteratorLoop.defaultImplementation

source
instance Std.Iterators.Map.instIteratorLoopPartial {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type x → Type x'} [Monad n] [Monad o] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n γ} :
IteratorLoopPartial (Map α m n lift f) n o
Equations

- Std.Iterators.Map.instIteratorLoopPartial = Std.Iterators.IteratorLoopPartial.defaultImplementation

source
@[inline]
def Std.Iterators.IterM.mapWithPostcondition {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [MonadLiftT m n] [Iterator α m β] (f : β → PostconditionT n γ) (it : IterM m β) :
IterM n γ

Note: This is a very general combinator that requires an advanced understanding of monads, dependent types and termination proofs. The variants `map` and `mapM` are easier to use and sufficient for most use cases.

If `it` is an iterator, then `it.mapWithPostcondition f` is another iterator that applies a monadic function `f` to all values emitted by `it` and emits the result.

`f` is expected to return `PostconditionT n _`. The base iterator `it` being monadic in `m`, `n` can be different from `m`, but `it.mapWithPostcondition f` expects a `MonadLiftT m n` instance. The `PostconditionT` transformer allows the caller to intrinsically prove properties about `f`'s return value in the monad `n`, enabling termination proofs depending on the specific behavior of `f`.

Marble diagram (without monadic effects):

    it                          ---a --b --c --d -e ----⊥
    it.mapWithPostcondition     ---a'--b'--c'--d'-e'----⊥

(given that `f a = pure a'`, `f b = pure b'` etc.)

Termination properties:

- `Finite` instance: only if `it` is finite
- `Productive` instance: only if `it` is productive

For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though no `Finite` (or `Productive`) instance is provided. For example, if `f` is an `ExceptT` monad and will always fail, then `it.mapWithPostcondition` will be finite even if `it` isn't.

In such situations, the missing instances can be proved manually if the postcondition bundled in the `PostconditionT n` monad is strong enough. In the given example, a suitable postcondition might be `fun _ => False`.

Performance:

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

Equations

- Std.Iterators.IterM.mapWithPostcondition f it = Std.Iterators.IterM.InternalCombinators.map (fun {x : Type ?u.27} => monadLift) f it

Instances For

source
@[inline]
def Std.Iterators.IterM.filterWithPostcondition {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [MonadLiftT m n] [Iterator α m β] (f : β → PostconditionT n (ULift Bool)) (it : IterM m β) :
IterM n β

Note: This is a very general combinator that requires an advanced understanding of monads, dependent types and termination proofs. The variants `filter` and `filterM` are easier to use and sufficient for most use cases.

If `it` is an iterator, then `it.filterWithPostcondition f` is another iterator that applies a monadic predicate `f` to all values emitted by `it` and emits them only if they are accepted by `f`.

`f` is expected to return `PostconditionT n (ULift Bool)`. The base iterator `it` being monadic in `m`, `n` can be different from `m`, but `it.filterWithPostcondition f` expects a `MonadLiftT m n` instance. The `PostconditionT` transformer allows the caller to intrinsically prove properties about `f`'s return value in the monad `n`, enabling termination proofs depending on the specific behavior of `f`.

Marble diagram (without monadic effects):

    it                             ---a--b--c--d-e--⊥
    it.filterWithPostcondition     ---a-----c-------⊥

(given that `f a = f c = pure true` and `f b = f d = d e = pure false`)

Termination properties:

- `Finite` instance: only if `it` is finite
- `Productive` instance: only if `it` is finite`

For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though no `Finite` (or `Productive`) instance is provided. For example, if `f` is an `ExceptT` monad and will always fail, then `it.filterWithPostcondition` will be finite -- and productive -- even if `it` isn't.

In such situations, the missing instances can be proved manually if the postcondition bundled in the `PostconditionT n` monad is strong enough. In the given example, a suitable postcondition might be `fun _ => False`.

Performance:

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

Equations

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

Instances For

source
@[inline]
def Std.Iterators.IterM.filterMapM {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] [Monad n] [MonadLiftT m n] (f : β → n (Option γ)) (it : IterM m β) :
IterM n γ

If `it` is an iterator, then `it.filterMapM f` is another iterator that applies a monadic function `f` to all values emitted by `it`. `f` is expected to return an `Option` inside the monad. If `f` returns `none`, then nothing is emitted; if it returns `some x`, then `x` is emitted.

The base iterator `it` being monadic in `m`, `f` can return values in any monad `n` for which a `MonadLiftT m n` instance is available.

If `f` is pure, then the simpler variant `it.filterMap` can be used instead.

Marble diagram (without monadic effects):

    it                ---a --b--c --d-e--⊥
    it.filterMapM     ---a'-----c'-------⊥

(given that `f a = pure (some a)'`, `f c = pure (some c')` and `f b = f d = d e = pure none`)

Termination properties:

- `Finite` instance: only if `it` is finite
- `Productive` instance: only if `it` is finite`

For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though no `Finite` (or `Productive`) instance is provided. For example, if `f` never returns `none`, then this combinator will preserve productiveness. If `f` is an `ExceptT` monad and will always fail, then `it.filterMapM` will be finite even if `it` isn't. In the first case, consider using the `map`/`mapM`/`mapWithPostcondition` combinators instead, which provide more instances out of the box.

If that does not help, the more general combinator `it.filterMapWithPostcondition f` makes it possible to manually prove `Finite` and `Productive` instances depending on the concrete choice of `f`.

Performance:

For each value emitted by the base iterator `it`, this combinator calls `f` and matches on the returned `Option` value.

Equations

- Std.Iterators.IterM.filterMapM f it = Std.Iterators.IterM.filterMapWithPostcondition (fun (b : β) => Std.Iterators.PostconditionT.lift (f b)) it

Instances For

source
@[inline]
def Std.Iterators.IterM.mapM {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] [Monad n] [MonadLiftT m n] (f : β → n γ) (it : IterM m β) :
IterM n γ

If `it` is an iterator, then `it.mapM f` is another iterator that applies a monadic function `f` to all values emitted by `it` and emits the result.

The base iterator `it` being monadic in `m`, `f` can return values in any monad `n` for which a `MonadLiftT m n` instance is available.

If `f` is pure, then the simpler variant `it.map` can be used instead.

Marble diagram (without monadic effects):

    it          ---a --b --c --d -e ----⊥
    it.mapM     ---a'--b'--c'--d'-e'----⊥

(given that `f a = pure a'`, `f b = pure b'` etc.)

Termination properties:

- `Finite` instance: only if `it` is finite
- `Productive` instance: only if `it` is productive

For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though no `Finite` (or `Productive`) instance is provided. For example, if `f` is an `ExceptT` monad and will always fail, then `it.mapM` will be finite even if `it` isn't.

If that does not help, the more general combinator `it.mapWithPostcondition f` makes it possible to manually prove `Finite` and `Productive` instances depending on the concrete choice of `f`.

Performance:

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

Equations

- Std.Iterators.IterM.mapM f it = Std.Iterators.IterM.mapWithPostcondition (fun (b : β) => Std.Iterators.PostconditionT.lift (f b)) it

Instances For

source
@[inline]
def Std.Iterators.IterM.filterM {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] [Monad n] [MonadLiftT m n] (f : β → n (ULift Bool)) (it : IterM m β) :
IterM n β

If `it` is an iterator, then `it.filterM f` is another iterator that applies a monadic predicate `f` to all values emitted by `it` and emits them only if they are accepted by `f`.

The base iterator `it` being monadic in `m`, `f` can return values in any monad `n` for which a `MonadLiftT m n` instance is available.

If `f` is pure, then the simpler variant `it.filter` can be used instead.

Marble diagram (without monadic effects):

    it             ---a--b--c--d-e--⊥
    it.filterM     ---a-----c-------⊥

(given that `f a = f c = pure true` and `f b = f d = d e = pure false`)

Termination properties:

- `Finite` instance: only if `it` is finite
- `Productive` instance: only if `it` is finite`

For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though no `Finite` (or `Productive`) instance is provided. For example, if `f` is an `ExceptT` monad and will always fail, then `it.filterWithPostcondition` will be finite -- and productive -- even if `it` isn't.

In such situations, the more general combinator `it.filterWithPostcondition f` makes it possible to manually prove `Finite` and `Productive` instances depending on the concrete choice of `f`.

Performance:

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

Equations

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

Instances For

source
@[inline]
def Std.Iterators.IterM.filterMap {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Monad m] (f : β → Option γ) (it : IterM m β) :
IterM m γ

If `it` is an iterator, then `it.filterMap f` is another iterator that applies a function `f` to all values emitted by `it`. `f` is expected to return an `Option`. If it returns `none`, then nothing is emitted; if it returns `some x`, then `x` is emitted.

In situations where `f` is monadic, use `filterMapM` instead.

Marble diagram:

    it               ---a --b--c --d-e--⊥
    it.filterMap     ---a'-----c'-------⊥

(given that `f a = some a'`, `f c = c'` and `f b = f d = d e = none`)

Termination properties:

- `Finite` instance: only if `it` is finite
- `Productive` instance: only if `it` is finite`

For certain mapping functions `f`, the resulting iterator will be productive even though no `Productive` instance is provided. For example, if `f` never returns `none`, then this combinator will preserve productiveness. In such situations, the missing instance needs to be proved manually.

Performance:

For each value emitted by the base iterator `it`, this combinator calls `f` and matches on the returned `Option` value.

Equations

- Std.Iterators.IterM.filterMap f it = Std.Iterators.IterM.filterMapWithPostcondition (fun (b : β) => pure (f b)) it

Instances For

source
@[inline]
def Std.Iterators.IterM.map {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Monad m] (f : β → γ) (it : IterM m β) :
IterM m γ

If `it` is an iterator, then `it.map f` is another iterator that applies a function `f` to all values emitted by `it` and emits the result.

In situations where `f` is monadic, use `mapM` instead.

Marble diagram:

    it         ---a --b --c --d -e ----⊥
    it.map     ---a'--b'--c'--d'-e'----⊥

(given that `f a = a'`, `f b = b'` etc.)

Termination properties:

- `Finite` instance: only if `it` is finite
- `Productive` instance: only if `it` is productive

Performance:

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

Equations

- Std.Iterators.IterM.map f it = Std.Iterators.IterM.mapWithPostcondition (fun (b : β) => pure (f b)) it

Instances For

source
@[inline]
def Std.Iterators.IterM.filter {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Monad m] (f : β → Bool) (it : IterM m β) :
IterM m β

If `it` is an iterator, then `it.filter f` is another iterator that applies a predicate `f` to all values emitted by `it` and emits them only if they are accepted by `f`.

In situations where `f` is monadic, use `filterM` instead.

Marble diagram (without monadic effects):

    it            ---a--b--c--d-e--⊥
    it.filter     ---a-----c-------⊥

(given that `f a = f c = true` and `f b = f d = d e = false`)

Termination properties:

- `Finite` instance: only if `it` is finite
- `Productive` instance: only if `it` is finite`

For certain mapping functions `f`, the resulting iterator will be productive even though no `Productive` instance is provided. For example, if `f` always returns `True`, the resulting iterator will be productive as long as `it` is. In such situations, the missing instance needs to be proved manually.

Performance:

For each value emitted by the base iterator `it`, this combinator calls `f` and matches on the returned value.

Equations

- Std.Iterators.IterM.filter f it = Std.Iterators.IterM.filterMap (fun (b : β) => if f b = true then some b else none) it

Instances For

source
instance Std.Iterators.instIteratorSizeFilterMapOfFinite {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} [Finite α m] :
IteratorSize (FilterMap α m n lift f) n
Equations

- Std.Iterators.instIteratorSizeFilterMapOfFinite = Std.Iterators.IteratorSize.defaultImplementation

source
instance Std.Iterators.instIteratorSizePartialFilterMap {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n (Option γ)} :
IteratorSizePartial (FilterMap α m n lift f) n
Equations

- Std.Iterators.instIteratorSizePartialFilterMap = Std.Iterators.IteratorSizePartial.defaultImplementation

source
instance Std.Iterators.instIteratorSizeMap {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n γ} [IteratorSize α m] :
IteratorSize (Map α m n lift f) n
Equations

- Std.Iterators.instIteratorSizeMap = { size := fun (it : Std.IterM n γ) => lift (Std.Iterators.IteratorSize.size it.internalState.inner) }

source
instance Std.Iterators.instIteratorSizePartialMap {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n γ} [IteratorSizePartial α m] :
IteratorSizePartial (Map α m n lift f) n
Equations

- Std.Iterators.instIteratorSizePartialMap = { size := fun (it : Std.IterM n γ) => lift (Std.Iterators.IteratorSizePartial.size it.internalState.inner) }