Collectors #
This module provides consumers that collect the values emitted by an iterator in a data structure. Concretely, the following operations are provided:
IterM.toList
, collecting the values in a listIterM.toListRev
, collecting the values in a list in reverse order but more efficientlyIterM.toArray
, collecting the values in an array
Some producers and combinators provide specialized implementations. These are captured by the
IteratorCollect
and IteratorCollectPartial
typeclasses. They should be implemented by all
types of iterators. A default implementation is provided. The typeclass LawfulIteratorCollect
asserts that an IteratorCollect
instance equals the default implementation.
IteratorCollect α m
provides efficient implementations of collectors for α
-based
iterators. Right now, it is limited to a potentially optimized toArray
implementation.
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.
Note: For this to be compositional enough to be useful, toArrayMapped
would need to accept a
termination proof for the specific mapping function used instead of the blanket Finite α m
instance. Otherwise, most combinators like map
cannot implement their own instance relying on
the instance of their base iterators. However, fixing this is currently low priority.
Instances
IteratorCollectPartial α m
provides efficient implementations of collectors for α
-based
iterators. Right now, it is limited to a potentially optimized partial toArray
implementation.
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
This is an internal function used in IteratorCollect.defaultImplementation
.
It iterates over an iterator and applies f
whenever a value is emitted before inserting the result
of f
into an array.
Equations
Instances For
Equations
Instances For
This is the default implementation of the IteratorLoop
class.
It simply iterates through the iterator using IterM.step
, incrementally building up the desired
data structure. For certain iterators, more efficient implementations are possible and should be
used instead.
Equations
Instances For
Asserts that a given IteratorCollect
instance is equal to IteratorCollect.defaultImplementation
.
(Even though equal, the given instance might be vastly more efficient.)
- lawful_toArrayMapped {γ : Type w} (lift : ⦃α : Type w⦄ → m α → n α) [Internal.LawfulMonadLiftFunction lift] [Finite α m] : IteratorCollect.toArrayMapped lift = IteratorCollect.toArrayMapped lift
Instances
This is an internal function used in IteratorCollectPartial.defaultImplementation
.
It iterates over an iterator and applies f
whenever a value is emitted before inserting the result
of f
into an array.
Equations
Instances For
This is the default implementation of the IteratorLoopPartial
class.
It simply iterates through the iterator using IterM.step
, incrementally building up the desired
data structure. For certain iterators, more efficient implementations are possible and should be
used instead.
Equations
Instances For
Traverses the given iterator and stores the emitted values in an array.
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.toArray
instead of it.toArray
. However, it is not possible to formally
verify the behavior of the partial variant.
Equations
Instances For
Traverses the given iterator and stores the emitted values in an array.
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.toArray
instead.
Equations
Instances For
Traverses the given iterator and stores the emitted values in reverse order in a list. Because
lists are prepend-only, this toListRev
is usually more efficient that toList
.
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.toListRev
instead of it.toListRev
. However, it is not possible to
formally verify the behavior of the partial variant.
Equations
Instances For
Traverses the given iterator and stores the emitted values in reverse order in a list. Because
lists are prepend-only, this toListRev
is usually more efficient that toList
.
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.toListRev
instead.
Equations
Instances For
Traverses the given iterator and stores the emitted values in a list. Because
lists are prepend-only, toListRev
is usually more efficient that toList
.
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.toList
instead of it.toList
. However, it is not possible to
formally verify the behavior of the partial variant.
Equations
Instances For
Traverses the given iterator and stores the emitted values in a list. Because
lists are prepend-only, toListRev
is usually more efficient that toList
.
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.toList
instead.