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 list
• IterM.toListRev, collecting the values in a list in reverse order but more efficiently
• IterM.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.

class Std.Iterators.IteratorCollect (α : Type w) (m : Type w → Type w') (n : Type w → Type w'') {β : Type w} [Iterator α m β] : Type (max (max (w + 1) w') w'')

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.

• toArrayMapped [Finite α m] (lift : ⦃δ : Type w⦄ → m δ → n δ) {γ : Type w} : (β → n γ) → IterM m β → n (Array γ)

  Maps the emitted values of an iterator using the given function and collects the results in an Array. This is an internal implementation detail. Consider using it.map f |>.toArray instead.

class Std.Iterators.IteratorCollectPartial (α : Type w) (m : Type w → Type w') (n : Type w → Type w'') {β : Type w} [Iterator α m β] : Type (max (max (w + 1) w') w'')

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.

• toArrayMappedPartial (lift : ⦃δ : Type w⦄ → m δ → n δ) {γ : Type w} : (β → n γ) → IterM m β → n (Array γ)

  Maps the emitted values of an iterator using the given function and collects the results in an Array. This is an internal implementation detail. Consider using it.map f |>.allowNontermination.toArray instead.

@[inline]

def Std.Iterators.IterM.DefaultConsumers.toArrayMapped {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Iterator α m β] [Finite α m] (lift : ⦃α : Type w⦄ → m α → n α) {γ : Type w} (f : β → n γ) (it : IterM m β) : n (Array γ)

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

• Std.Iterators.IterM.DefaultConsumers.toArrayMapped lift f it = Std.Iterators.IterM.DefaultConsumers.toArrayMapped.go lift f it #[]

@[irreducible, specialize #[]]

def Std.Iterators.IterM.DefaultConsumers.toArrayMapped.go {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] (lift : ⦃α : Type w⦄ → m α → n α) {γ : Type w} (f : β → n γ) [Monad n] [Finite α m] (it : IterM m β) (a : Array γ) : n (Array γ)

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.Iterators.IteratorCollect.defaultImplementation {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Iterator α m β] : IteratorCollect α m n

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

• Std.Iterators.IteratorCollect.defaultImplementation = { toArrayMapped := fun [Std.Iterators.Finite α m] => Std.Iterators.IterM.DefaultConsumers.toArrayMapped }

class Std.Iterators.LawfulIteratorCollect (α : Type w) (m : Type w → Type w') (n : Type w → Type w'') {β : Type w} [Monad m] [Monad n] [Iterator α m β] [i : IteratorCollect α m n] : Prop

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

theorem Std.Iterators.LawfulIteratorCollect.toArrayMapped_eq {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [Monad n] [Iterator α m β] [Finite α m] [IteratorCollect α m n] [hl : LawfulIteratorCollect α m n] {lift : ⦃δ : Type w⦄ → m δ → n δ} [Internal.LawfulMonadLiftFunction lift] {f : β → n γ} {it : IterM m β} : IteratorCollect.toArrayMapped lift f it = IterM.DefaultConsumers.toArrayMapped lift f it

instance Std.Iterators.instLawfulIteratorCollectOfIteratorOfFinite (α β : Type w) (m : Type w → Type w') (n : Type w → Type w'') [Monad n] [Iterator α m β] [Monad m] [Iterator α m β] [Finite α m] : LawfulIteratorCollect α m n

@[inline]

def Std.Iterators.IterM.DefaultConsumers.toArrayMappedPartial {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Iterator α m β] (lift : {α : Type w} → m α → n α) {γ : Type w} (f : β → n γ) (it : IterM m β) : n (Array γ)

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

• Std.Iterators.IterM.DefaultConsumers.toArrayMappedPartial lift f it = Std.Iterators.IterM.DefaultConsumers.toArrayMappedPartial.go lift f it #[]

@[specialize #[]]

partial def Std.Iterators.IterM.DefaultConsumers.toArrayMappedPartial.go {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β] (lift : {α : Type w} → m α → n α) {γ : Type w} (f : β → n γ) [Monad n] (it : IterM m β) (a : Array γ) : n (Array γ)

@[inline]

def Std.Iterators.IteratorCollectPartial.defaultImplementation {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Iterator α m β] : IteratorCollectPartial α m n

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

• Std.Iterators.IteratorCollectPartial.defaultImplementation = { toArrayMappedPartial := Std.Iterators.IterM.DefaultConsumers.toArrayMappedPartial }

@[inline]

def Std.Iterators.IterM.toArray {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Finite α m] [IteratorCollect α m m] (it : IterM m β) : m (Array β)

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

• it.toArray = Std.Iterators.IteratorCollect.toArrayMapped (fun ⦃x : Type ?u.35⦄ => id) pure it

@[inline]

def Std.Iterators.IterM.Partial.toArray {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α m β] (it : Partial m β) [IteratorCollectPartial α m m] : m (Array β)

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

• it.toArray = Std.Iterators.IteratorCollectPartial.toArrayMappedPartial (fun ⦃x : Type ?u.52⦄ => id) pure it.it

@[inline]

def Std.Iterators.IterM.toListRev {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w} [Iterator α m β] [Finite α m] (it : IterM m β) : m (List β)

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

• it.toListRev = Std.Iterators.IterM.toListRev.go it []

@[irreducible]

def Std.Iterators.IterM.toListRev.go {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w} [Iterator α m β] [Finite α m] (it : IterM m β) (bs : List β) : m (List β)

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.Iterators.IterM.Partial.toListRev {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w} [Iterator α m β] (it : Partial m β) : m (List β)

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

• it.toListRev = Std.Iterators.IterM.Partial.toListRev.go it.it []

@[specialize #[]]

partial def Std.Iterators.IterM.Partial.toListRev.go {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w} [Iterator α m β] (it : IterM m β) (bs : List β) : m (List β)

@[inline]

def Std.Iterators.IterM.toList {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w} [Iterator α m β] [Finite α m] [IteratorCollect α m m] (it : IterM m β) : m (List β)

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

• it.toList = Array.toList <$> it.toArray

@[inline]

def Std.Iterators.IterM.Partial.toList {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w} [Iterator α m β] (it : Partial m β) [IteratorCollectPartial α m m] : m (List β)

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.

Equations

• it.toList = Array.toList <$> it.toArray