This module provides the iterator combinator IterM.take.

@[unbox]

structure Std.Iterators.Types.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.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.

@[inline]

def Std.IterM.toTake {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [Iterators.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.

theorem Std.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.Types.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.Types.Take.instIterator {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α m β] : Iterator (Take α m) m β

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

theorem Std.Iterators.Types.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.Types.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.Types.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.Types.Take.instFinite {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α m β] [Productive α m] : Finite (Take α m) m

instance Std.Iterators.Types.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