# Monadic `dropWhile` iterator combinator #

This module provides the iterator combinator `IterM.dropWhile` that will drop all values emitted by a given iterator until a given predicate on these values becomes false the first time. Beginning with that moment, the combinator will forward all emitted values.

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.DropWhile (α : Type w) (m : Type w → Type w') (β : Type w) (P : β → PostconditionT m (ULift Bool)) :
Type w

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

- dropping : Bool

  Internal implementation detail of the iterator library.

- inner : IterM m β

  Internal implementation detail of the iterator library.

Instances For

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

Constructs intermediate states of an iterator created with the combinator `IterM.dropWhileWithPostcondition`. When `it.dropWhileWithPostcondition P` has stopped dropping elements, its new state cannot be created directly with `IterM.dropWhileWithPostcondition` but only with `Intermediate.dropWhileWithPostcondition`.

`Intermediate.dropWhileWithPostcondition` is meant to be used only for internally or for verification purposes.

Equations

- Std.Iterators.IterM.Intermediate.dropWhileWithPostcondition P dropping it = Std.Iterators.toIterM { dropping := dropping, inner := it } m β

Instances For

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

Constructs intermediate states of an iterator created with the combinator `IterM.dropWhileM`. When `it.dropWhileM P` has stopped dropping elements, its new state cannot be created directly with `IterM.dropWhileM` but only with `Intermediate.dropWhileM`.

`Intermediate.dropWhileM` is meant to be used only for internally or for verification purposes.

Equations

- Std.Iterators.IterM.Intermediate.dropWhileM P dropping it = Std.Iterators.IterM.Intermediate.dropWhileWithPostcondition (Std.Iterators.PostconditionT.lift ∘ P) dropping it

Instances For

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

Constructs intermediate states of an iterator created with the combinator `IterM.dropWhile`. When `it.dropWhile P` has stopped dropping elements, its new state cannot be created directly with `IterM.dropWhile` but only with `Intermediate.dropWhile`.

`Intermediate.dropWhile` is meant to be used only for internally or for verification purposes.

Equations

- Std.Iterators.IterM.Intermediate.dropWhile P dropping it = Std.Iterators.IterM.Intermediate.dropWhileM (pure ∘ ULift.up ∘ P) dropping it

Instances For

source
@[inline]
def Std.Iterators.IterM.dropWhileWithPostcondition {α : 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 `dropWhile` and `dropWhileM` are easier to use and sufficient for most use cases.

Given an iterator `it` and a monadic predicate `P`, `it.dropWhileWithPostcondition P` is an iterator that emits the values emitted by `it` starting from the first value that is rejected by `P`. The elements before are dropped.

`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.dropWhileWithPostcondition P   ------------c--d-e--⊥

    it                                ---a----⊥
    it.dropWhileWithPostcondition P   --------⊥

Termination properties:

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

Depending on `P`, it is possible that `it.dropWhileWithPostcondition 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. After that, the combinator incurs an additional O(1) cost for each value emitted by `it`.

Equations

- Std.Iterators.IterM.dropWhileWithPostcondition P it = Std.Iterators.IterM.Intermediate.dropWhileWithPostcondition P true it

Instances For

source
@[inline]
def Std.Iterators.IterM.dropWhileM {α : 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.dropWhileM P` is an iterator that emits the values emitted by `it` starting from the first value that is rejected by `P`. The elements before are dropped.

If `P` is pure, then the simpler variant `dropWhile` 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.dropWhileM P   ------------c--d-e--⊥

    it                ---a----⊥
    it.dropWhileM P   --------⊥

Termination properties:

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

Depending on `P`, it is possible that `it.dropWhileM P` is finite (or productive) although `it` is not. In this case, the `Finite` (or `Productive`) instance needs to be proved manually. Use `dropWhileWithPostcondition` if the termination behavior depends on `P`'s behavior.

Performance:

This combinator calls `P` on each output of `it` until the predicate evaluates to false. After that, the combinator incurs an addictional O(1) cost for each value emitted by `it`.

Equations

- Std.Iterators.IterM.dropWhileM P it = Std.Iterators.IterM.Intermediate.dropWhileM P true it

Instances For

source
@[inline]
def Std.Iterators.IterM.dropWhile {α : 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.dropWhile P` is an iterator that emits the values emitted by `it` starting from the first value that is rejected by `P`. The elements before are dropped.

In situations where `P` is monadic, use `dropWhileM` 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.dropWhile P   ------------c--d-e--⊥

    it               ---a----⊥
    it.dropWhile P   --------⊥

Termination properties:

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

Depending on `P`, it is possible that `it.dropWhileM P` is productive although `it` is not. In this case, the `Productive` instance needs to be proved manually.

Performance:

This combinator calls `P` on each output of `it` until the predicate evaluates to false. After that, the combinator incurs an addictional O(1) cost for each value emitted by `it`.

Equations

- Std.Iterators.IterM.dropWhile P it = Std.Iterators.IterM.Intermediate.dropWhile P true it

Instances For

source
inductive Std.Iterators.DropWhile.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 `dropWhile` iterator `it`. This is mostly internally relevant, except if one needs to manually prove termination (`Finite` or `Productive` instances, for example) of a `dropWhile` 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) → it.internalState.dropping = false → PlausibleStep it (IterStep.yield (IterM.Intermediate.dropWhileWithPostcondition P false 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.Intermediate.dropWhileWithPostcondition P it.internalState.dropping 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
- start {α : 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) → it.internalState.dropping = true → (P out).Property { down := false } → PlausibleStep it (IterStep.yield (IterM.Intermediate.dropWhileWithPostcondition P false it') out)
- dropped {α : 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) → it.internalState.dropping = true → (P out).Property { down := true } → PlausibleStep it (IterStep.skip (IterM.Intermediate.dropWhileWithPostcondition P true it'))

Instances For

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

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

source
instance Std.Iterators.DropWhile.instFinite {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α m β] [Finite α m] {P : β → PostconditionT m (ULift Bool)} :
Finite (DropWhile α m β P) m
source
instance Std.Iterators.DropWhile.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 (DropWhile α m β P) m n
Equations

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

source
instance Std.Iterators.DropWhile.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 (DropWhile α m β P) m n
Equations

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

source
instance Std.Iterators.DropWhile.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 (DropWhile α m β P) m n
Equations

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

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

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

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

- Std.Iterators.instIteratorSizeDropWhileOfFiniteOfIteratorLoop = Std.Iterators.IteratorSize.defaultImplementation

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

- Std.Iterators.instIteratorSizePartialDropWhileOfIteratorLoopPartial = Std.Iterators.IteratorSizePartial.defaultImplementation