# Monadic `takeWhile` iterator combinator #

This module provides the iterator combinator `IterM.takeWhile` that will take all values emitted by a given iterator until a given predicate on these values becomes false the first time. Then the combinator will terminate.

Several variants of this combinator are provided:

- `M` suffix: Instead of a pure function, this variant takes a monadic function. Given a suitable `MonadLiftT` instance, it will also allow lifting the iterator to another monad first and then applying the mapping function in this monad.
- `WithPostcondition` suffix: This variant takes 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.TakeWhile (α : Type w) (m : Type w → Type w') (β : Type w) (P : β → PostconditionT m (ULift Bool)) :
Type w

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

- inner : IterM m β

  Internal implementation detail of the iterator library.

Instances For

source
@[inline]
def Std.Iterators.IterM.takeWhileWithPostcondition {α : Type w} {m : Type w → Type w'} {β : Type w} (P : β → PostconditionT m (ULift Bool)) (it : IterM m β) :
IterM m β

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

Given an iterator `it` and a monadic predicate `P`, `it.takeWhileWithPostcondition P` is an iterator that emits the values emitted by `it` until one of those values is rejected by `P`. If some emitted value is rejected by `P`, the value is dropped and the iterator terminates.

`P` is expected to return `PostconditionT m (ULift Bool)`. The `PostconditionT` transformer allows the caller to intrinsically prove properties about `P`'s return value in the monad `m`, enabling termination proofs depending on the specific behavior of `P`.

Marble diagram (ignoring monadic effects):

Assuming that the predicate `P` accepts `a` and `b` but rejects `c`:

    it                                ---a----b---c--d-e--⊥
    it.takeWhileWithPostcondition P   ---a----b---⊥

    it                                ---a----⊥
    it.takeWhileWithPostcondition P   ---a----⊥

Termination properties:

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

Depending on `P`, it is possible that `it.takeWhileWithPostcondition P` is finite (or productive) although `it` is not. In this case, the `Finite` (or `Productive`) instance needs to be proved manually.

Performance:

This combinator calls `P` on each output of `it` until the predicate evaluates to false. Then it terminates.

Equations

- Std.Iterators.IterM.takeWhileWithPostcondition P it = Std.Iterators.toIterM { inner := it } m β

Instances For

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

Given an iterator `it` and a monadic predicate `P`, `it.takeWhileM P` is an iterator that outputs the values emitted by `it` until one of those values is rejected by `P`. If some emitted value is rejected by `P`, the value is dropped and the iterator terminates.

If `P` is pure, then the simpler variant `takeWhile` can be used instead.

Marble diagram (ignoring monadic effects):

Assuming that the predicate `P` accepts `a` and `b` but rejects `c`:

    it                ---a----b---c--d-e--⊥
    it.takeWhileM P   ---a----b---⊥

    it                ---a----⊥
    it.takeWhileM P   ---a----⊥

Termination properties:

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

Depending on `P`, it is possible that `it.takeWhileM P` is finite (or productive) although `it` is not. In this case, the `Finite` (or `Productive`) instance needs to be proved manually.

Performance:

This combinator calls `P` on each output of `it` until the predicate evaluates to false. Then it terminates.

Equations

- Std.Iterators.IterM.takeWhileM P it = Std.Iterators.IterM.takeWhileWithPostcondition (Std.Iterators.PostconditionT.lift ∘ P) it

Instances For

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

Given an iterator `it` and a predicate `P`, `it.takeWhile P` is an iterator that outputs the values emitted by `it` until one of those values is rejected by `P`. If some emitted value is rejected by `P`, the value is dropped and the iterator terminates.

In situations where `P` is monadic, use `takeWhileM` instead.

Marble diagram (ignoring monadic effects):

Assuming that the predicate `P` accepts `a` and `b` but rejects `c`:

    it               ---a----b---c--d-e--⊥
    it.takeWhile P   ---a----b---⊥

    it               ---a----⊥
    it.takeWhile P   ---a----⊥

Termination properties:

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

Depending on `P`, it is possible that `it.takeWhile P` is finite (or productive) although `it` is not. In this case, the `Finite` (or `Productive`) instance needs to be proved manually.

Performance:

This combinator calls `P` on each output of `it` until the predicate evaluates to false. Then it terminates.

Equations

- Std.Iterators.IterM.takeWhile P it = Std.Iterators.IterM.takeWhileM (pure ∘ ULift.up ∘ P) it

Instances For

source
inductive Std.Iterators.TakeWhile.PlausibleStep {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {P : β → PostconditionT m (ULift Bool)} (it : IterM m β) (step : IterStep (IterM m β) β) :
Prop

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

- yield {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {P : β → PostconditionT m (ULift Bool)} {it : IterM m β} {it' : IterM m β} {out : β} : it.internalState.inner.IsPlausibleStep (IterStep.yield it' out) → (P out).Property { down := true } → PlausibleStep it (IterStep.yield (IterM.takeWhileWithPostcondition P it') out)
- skip {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {P : β → PostconditionT m (ULift Bool)} {it : IterM m β} {it' : IterM m β} : it.internalState.inner.IsPlausibleStep (IterStep.skip it') → PlausibleStep it (IterStep.skip (IterM.takeWhileWithPostcondition P it'))
- done {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {P : β → PostconditionT m (ULift Bool)} {it : IterM m β} : it.internalState.inner.IsPlausibleStep IterStep.done → PlausibleStep it IterStep.done
- rejected {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {P : β → PostconditionT m (ULift Bool)} {it : IterM m β} {it' : IterM m β} {out : β} : it.internalState.inner.IsPlausibleStep (IterStep.yield it' out) → (P out).Property { down := false } → PlausibleStep it IterStep.done

Instances For

source
@[inline]
instance Std.Iterators.TakeWhile.instIterator {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α m β] {P : β → PostconditionT m (ULift Bool)} :
Iterator (TakeWhile α m β P) m β
Equations

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

source
instance Std.Iterators.TakeWhile.instFinite {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α m β] [Finite α m] {P : β → PostconditionT m (ULift Bool)} :
Finite (TakeWhile α m β P) m
source
instance Std.Iterators.TakeWhile.instProductive {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α m β] [Productive α m] {P : β → PostconditionT m (ULift Bool)} :
Productive (TakeWhile α m β P) m
source
instance Std.Iterators.TakeWhile.instIteratorCollect {α : Type w} {m : Type w → Type w'} {β : Type w} {n : Type w → Type u_1} [Monad m] [Monad n] [Iterator α m β] [Productive α m] {P : β → PostconditionT m (ULift Bool)} :
IteratorCollect (TakeWhile α m β P) m n
Equations

- Std.Iterators.TakeWhile.instIteratorCollect = Std.Iterators.IteratorCollect.defaultImplementation

source
instance Std.Iterators.TakeWhile.instIteratorCollectPartial {α : Type w} {m : Type w → Type w'} {β : Type w} {n : Type w → Type u_1} [Monad m] [Monad n] [Iterator α m β] {P : β → PostconditionT m (ULift Bool)} :
IteratorCollectPartial (TakeWhile α m β P) m n
Equations

- Std.Iterators.TakeWhile.instIteratorCollectPartial = Std.Iterators.IteratorCollectPartial.defaultImplementation

source
instance Std.Iterators.TakeWhile.instIteratorLoop {α : Type w} {m : Type w → Type w'} {β : Type w} {n : Type u_1 → Type u_2} {P : β → PostconditionT m (ULift Bool)} [Monad m] [Monad n] [Iterator α m β] [IteratorLoop α m n] :
IteratorLoop (TakeWhile α m β P) m n
Equations

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

source
instance Std.Iterators.TakeWhile.instIteratorForPartial {α : Type w} {m : Type w → Type w'} {β : Type w} {n : Type u_1 → Type u_2} [Monad m] [Monad n] [Iterator α m β] [IteratorLoopPartial α m n] {P : β → PostconditionT m (ULift Bool)} :
IteratorLoopPartial (TakeWhile α m β P) m n
Equations

- Std.Iterators.TakeWhile.instIteratorForPartial = Std.Iterators.IteratorLoopPartial.defaultImplementation

source
instance Std.Iterators.instIteratorSizeTakeWhileOfFiniteOfIteratorLoop {m : Type w → Type w'} {β α : Type w} [Monad m] [Iterator α m β] [Finite α m] [IteratorLoop α m m] {P : β → PostconditionT m (ULift Bool)} :
IteratorSize (TakeWhile α m β P) m
Equations

- Std.Iterators.instIteratorSizeTakeWhileOfFiniteOfIteratorLoop = Std.Iterators.IteratorSize.defaultImplementation

source
instance Std.Iterators.instIteratorSizePartialTakeWhileOfIteratorLoopPartial {m : Type w → Type w'} {β α : Type w} [Monad m] [Iterator α m β] [IteratorLoopPartial α m m] {P : β → PostconditionT m (ULift Bool)} :
IteratorSizePartial (TakeWhile α m β P) m
Equations

- Std.Iterators.instIteratorSizePartialTakeWhileOfIteratorLoopPartial = Std.Iterators.IteratorSizePartial.defaultImplementation