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

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

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

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

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

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

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

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

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

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

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

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

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