Loop-based consumers #
This module provides consumers that iterate over a given iterator, applying a certain user-supplied function in every iteration. Concretely, the following operations are provided:
ForIn
instancesIterM.fold
, the analogue ofList.foldl
IterM.foldM
, the analogue ofList.foldlM
IterM.drain
, which iterates over the whole iterator and discards all emitted values. It can be used to apply the monadic effects of the iterator.
Some producers and combinators provide specialized implementations. These are captured by the
IteratorLoop
and IteratorLoopPartial
typeclasses. They should be implemented by all
types of iterators. A default implementation is provided. The typeclass LawfulIteratorLoop
asserts that an IteratorLoop
instance equals the default implementation.
Relation that needs to be well-formed in order for a loop over an iterator to terminate.
It is assumed that the plausible_forInStep
predicate relates the input and output of the
stepper function.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Asserts that IteratorLoop.rel
is well-founded.
Equations
- Std.Iterators.IteratorLoop.WellFounded α m plausible_forInStep = WellFounded (Std.Iterators.IteratorLoop.rel α m plausible_forInStep)
Instances For
IteratorLoop α m
provides efficient implementations of loop-based consumers for α
-based
iterators. The basis is a ForIn
-style loop construct with the complication that it can be used
for infinite iterators, too -- given a proof that the given loop will nevertheless terminate.
This class is experimental and users of the iterator API should not explicitly depend on it. They can, however, assume that consumers that require an instance will work for all iterators provided by the standard library.
Instances
IteratorLoopPartial α m
provides efficient implementations of loop-based consumers for α
-based
iterators. The basis is a partial, i.e. potentially nonterminating, ForIn
instance.
This class is experimental and users of the iterator API should not explicitly depend on it. They can, however, assume that consumers that require an instance will work for all iterators provided by the standard library.
Instances
Equations
- Std.Iterators.instWellFoundedRelationWFRel wf = { rel := Std.Iterators.IteratorLoop.rel α m plausible_forInStep, wf := wf }
This is the loop implementation of the default instance IteratorLoop.defaultImplementation
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
This is the default implementation of the IteratorLoop
class.
It simply iterates through the iterator using IterM.step
. For certain iterators, more efficient
implementations are possible and should be used instead.
Equations
- Std.Iterators.IteratorLoop.defaultImplementation = { forIn := fun (lift : (γ : Type ?u.41) → m γ → n γ) => Std.Iterators.IterM.DefaultConsumers.forIn lift }
Instances For
Asserts that a given IteratorLoop
instance is equal to IteratorLoop.defaultImplementation
.
(Even though equal, the given instance might be vastly more efficient.)
Instances
This is the loop implementation of the default instance IteratorLoopPartial.defaultImplementation
.
This is the default implementation of the IteratorLoopPartial
class.
It simply iterates through the iterator using IterM.step
. For certain iterators, more efficient
implementations are possible and should be used instead.
Equations
- One or more equations did not get rendered due to their size.
Instances For
This ForIn
-style loop construct traverses a finite iterator using an IteratorLoop
instance.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
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.
Equations
- One or more equations did not get rendered due to their size.
Folds a monadic function over an iterator from the left, accumulating a value starting with init
.
The accumulated value is combined with the each element of the list in order, using f
.
The monadic effects of f
are interleaved with potential effects caused by the iterator's step
function. Therefore, it may not be equivalent to (← it.toList).foldlM
.
This function requires a Finite
instance proving that the iterator will finish after a finite
number of steps. If the iterator is not finite or such an instance is not available, consider using
it.allowNontermination.foldM
instead of it.foldM
. However, it is not possible to formally
verify the behavior of the partial variant.
Equations
- Std.Iterators.IterM.foldM f init it = forIn it init fun (x : β) (acc : γ) => ForInStep.yield <$> f acc x
Instances For
Folds a monadic function over an iterator from the left, accumulating a value starting with init
.
The accumulated value is combined with the each element of the list in order, using f
.
The monadic effects of f
are interleaved with potential effects caused by the iterator's step
function. Therefore, it may not be equivalent to it.toList.foldlM
.
This is a partial, potentially nonterminating, function. It is not possible to formally verify
its behavior. If the iterator has a Finite
instance, consider using IterM.foldM
instead.
Equations
- Std.Iterators.IterM.Partial.foldM f init it = forIn it init fun (x : β) (acc : γ) => ForInStep.yield <$> f acc x
Instances For
Folds a function over an iterator from the left, accumulating a value starting with init
.
The accumulated value is combined with the each element of the list in order, using f
.
It is equivalent to it.toList.foldl
.
This function requires a Finite
instance proving that the iterator will finish after a finite
number of steps. If the iterator is not finite or such an instance is not available, consider using
it.allowNontermination.fold
instead of it.fold
. However, it is not possible to formally
verify the behavior of the partial variant.
Equations
- Std.Iterators.IterM.fold f init it = forIn it init fun (x : β) (acc : γ) => pure (ForInStep.yield (f acc x))
Instances For
Folds a function over an iterator from the left, accumulating a value starting with init
.
The accumulated value is combined with the each element of the list in order, using f
.
It is equivalent to it.toList.foldl
.
This is a partial, potentially nonterminating, function. It is not possible to formally verify
its behavior. If the iterator has a Finite
instance, consider using IterM.fold
instead.
Equations
- Std.Iterators.IterM.Partial.fold f init it = forIn it init fun (x : β) (acc : γ) => pure (ForInStep.yield (f acc x))
Instances For
Iterates over the whole iterator, applying the monadic effects of each step, discarding all emitted values.
This function requires a Finite
instance proving that the iterator will finish after a finite
number of steps. If the iterator is not finite or such an instance is not available, consider using
it.allowNontermination.drain
instead of it.drain
. However, it is not possible to formally
verify the behavior of the partial variant.
Equations
- it.drain = Std.Iterators.IterM.fold (fun (x : PUnit) (x : β) => PUnit.unit) PUnit.unit it
Instances For
Iterates over the whole iterator, applying the monadic effects of each step, discarding all emitted values.
This is a partial, potentially nonterminating, function. It is not possible to formally verify
its behavior. If the iterator has a Finite
instance, consider using IterM.drain
instead.
Equations
- it.drain = Std.Iterators.IterM.Partial.fold (fun (x : PUnit) (x : β) => PUnit.unit) PUnit.unit it