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 fime. 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.

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

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

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

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

@[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 addictional O(1) cost for each value emitted by it.

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

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

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'))

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

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

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

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

instance Std.Iterators.DropWhile.instIteratorLoop {α : Type w} {m : Type w → Type w'} {β : Type w} {n : Type w → Type u_1} [Monad m] [Monad n] [Iterator α m β] : IteratorLoop α m n

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