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 suitableMonadLiftT
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.
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 ifit
is finiteProductive
instance: only ifit
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
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 ifit
is finiteProductive
instance: only ifit
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
Instances For
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 ifit
is finiteProductive
instance: only ifit
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
Instances For
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
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.