This module provides the iterator combinator IterM.take.

@[unbox]

structure Std.Iterators.Take (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] : Type w

The internal state of the IterM.take iterator combinator.

• countdown : Nat

  Internal implementation detail of the iterator library. Caution: For take n, countdown is n + 1. If countdown is zero, the combinator only terminates when inner terminates.

• inner : IterM m β

  Internal implementation detail of the iterator library

• finite : self.countdown > 0 ∨ Finite α m

  Internal implementation detail of the iterator library. This proof term ensures that a take always produces a finite iterator from a productive one.

@[inline]

def Std.Iterators.IterM.take {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] (n : Nat) (it : IterM m β) : IterM m β

Given an iterator it and a natural number n, it.take n is an iterator that outputs up to the first n of it's values in order and then terminates.

Marble diagram:

it          ---a----b---c--d-e--⊥
it.take 3   ---a----b---c⊥

it          ---a--⊥
it.take 3   ---a--⊥

Termination properties:

• Finite instance: only if it is productive
• Productive instance: only if it is productive

Performance:

This combinator incurs an additional O(1) cost with each output of it.

Equations

• Std.Iterators.IterM.take n it = Std.Iterators.toIterM { countdown := n + 1, inner := it, finite := ⋯ } m β

@[inline]

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

This combinator is only useful for advanced use cases.

Given a finite iterator it, returns an iterator that behaves exactly like it but is of the same type as it.take n.

Marble diagram:

it          ---a----b---c--d-e--⊥
it.toTake   ---a----b---c--d-e--⊥

Termination properties:

• Finite instance: always
• Productive instance: always

Performance:

This combinator incurs an additional O(1) cost with each output of it.

Equations

• it.toTake = Std.Iterators.toIterM { countdown := 0, inner := it, finite := ⋯ } m β

theorem Std.Iterators.IterM.take.surjective_of_zero_lt {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] (it : IterM m β) (h : 0 < it.internalState.countdown) : ∃ (it₀ : IterM m β), ∃ (k : Nat), it = take k it₀

inductive Std.Iterators.Take.PlausibleStep {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] (it : IterM m β) (step : IterStep (IterM m β) β) : Prop

• yield {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {it : IterM m β} {it' : IterM m β} {out : β} : it.internalState.inner.IsPlausibleStep (IterStep.yield it' out) → ∀ (h : it.internalState.countdown ≠ 1), PlausibleStep it (IterStep.yield { internalState := { countdown := it.internalState.countdown - 1, inner := it', finite := ⋯ } } out)
• skip {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {it : IterM m β} {it' : IterM m β} : it.internalState.inner.IsPlausibleStep (IterStep.skip it') → it.internalState.countdown ≠ 1 → PlausibleStep it (IterStep.skip { internalState := { countdown := it.internalState.countdown, inner := it', finite := ⋯ } })
• done {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {it : IterM m β} : it.internalState.inner.IsPlausibleStep IterStep.done → PlausibleStep it IterStep.done
• depleted {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {it : IterM m β} : it.internalState.countdown = 1 → PlausibleStep it IterStep.done

@[inline]

instance Std.Iterators.Take.instIterator {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α m β] : Iterator (Take α m) m β

Equations

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

def Std.Iterators.Take.Rel {α β : Type w} (m : Type w → Type w') [Monad m] [Iterator α m β] [Productive α m] : IterM m β → IterM m β → Prop

Equations

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

theorem Std.Iterators.Take.rel_of_countdown {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α m β] [Productive α m] {it it' : IterM m β} (h : it'.internalState.countdown < it.internalState.countdown) : Rel m it' it

theorem Std.Iterators.Take.rel_of_inner {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α m β] [Productive α m] {remaining : Nat} {it it' : IterM m β} (h : it'.finitelyManySkips.Rel it.finitelyManySkips) : Rel m (IterM.take remaining it') (IterM.take remaining it)

theorem Std.Iterators.Take.rel_of_zero_of_inner {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α m β] {it it' : IterM m β} (h : it.internalState.countdown = 0) (h' : it'.internalState.countdown = 0) (h'' : it'.internalState.inner.finitelyManySteps.Rel it.internalState.inner.finitelyManySteps) : Rel m it' it

instance Std.Iterators.Take.instFinite {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α m β] [Productive α m] : Finite (Take α m) m

instance Std.Iterators.Take.instIteratorCollect {α : Type w} {m : Type w → Type w'} {β : Type w} {n : Type w → Type w'} [Monad m] [Monad n] [Iterator α m β] : IteratorCollect (Take α m) m n

Equations

• Std.Iterators.Take.instIteratorCollect = Std.Iterators.IteratorCollect.defaultImplementation

instance Std.Iterators.Take.instIteratorCollectPartial {α : Type w} {m : Type w → Type w'} {β : Type w} {n : Type w → Type w'} [Monad m] [Monad n] [Iterator α m β] : IteratorCollectPartial (Take α m) m n

Equations

• Std.Iterators.Take.instIteratorCollectPartial = Std.Iterators.IteratorCollectPartial.defaultImplementation

instance Std.Iterators.Take.instIteratorLoop {α : Type w} {m : Type w → Type w'} {β : Type w} {n : Type x → Type x'} [Monad m] [Monad n] [Iterator α m β] : IteratorLoop (Take α m) m n

Equations

• Std.Iterators.Take.instIteratorLoop = Std.Iterators.IteratorLoop.defaultImplementation

instance Std.Iterators.Take.instIteratorLoopPartial {α : Type w} {m : Type w → Type w'} {β : Type w} {n : Type u_1 → Type u_2} [Monad m] [Monad n] [Iterator α m β] : IteratorLoopPartial (Take α m) m n

Equations

• Std.Iterators.Take.instIteratorLoopPartial = Std.Iterators.IteratorLoopPartial.defaultImplementation