Range iterator

This module implements an iterator for ranges (Std.PRange).

This iterator is publicly available via PRange.iter after importing Std.Data.Iterators and it internally powers many functions on ranges such as PRange.toList.

@[unbox]

structure Std.PRange.RangeIterator (shape : BoundShape) (α : Type u) : Type u

Internal state of the range iterators. Do not depend on its internals.

• next : Option α
• upperBound : Bound shape α

@[inline]

def Std.PRange.RangeIterator.Monadic.step {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] (it : IterM Id α) : Iterators.IterStep (IterM Id α) α

The pure function mapping a range iterator of type IterM to the next step of the iterator.

This function is prefixed with Monadic in order to disambiguate it from the version for iterators of type Iter.

Equations

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

@[inline]

def Std.PRange.RangeIterator.step {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] (it : Iter α) : Iterators.IterStep (Iter α) α

The pure function mapping a range iterator of type Iter to the next step of the iterator.

Equations

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

theorem Std.PRange.RangeIterator.step_eq_monadicStep {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] {it : Iter α} : step it = Iterators.IterStep.mapIterator Iterators.IterM.toIter (Monadic.step it.toIterM)

@[inline]

instance Std.PRange.instIteratorRangeIteratorIdOfUpwardEnumerableOfSupportsUpperBound {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] : Iterators.Iterator (RangeIterator su α) Id α

Equations

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

theorem Std.PRange.RangeIterator.Monadic.isPlausibleStep_iff {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] {it : IterM Id α} {step : Iterators.IterStep (IterM Id α) α} : it.IsPlausibleStep step ↔ step = Monadic.step it

theorem Std.PRange.RangeIterator.Monadic.step_eq_step {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] {it : IterM Id α} : it.step = pure ⟨step it, ⋯⟩

theorem Std.PRange.RangeIterator.isPlausibleStep_iff {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] {it : Iter α} {step : Iterators.IterStep (Iter α) α} : it.IsPlausibleStep step ↔ step = RangeIterator.step it

theorem Std.PRange.RangeIterator.step_eq_step {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] {it : Iter α} : it.step = ⟨step it, ⋯⟩

instance Std.PRange.RangeIterator.instIteratorCollect {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] {n : Type u → Type w} [Monad n] : Iterators.IteratorCollect (RangeIterator su α) Id n

Equations

• Std.PRange.RangeIterator.instIteratorCollect = Std.Iterators.IteratorCollect.defaultImplementation

instance Std.PRange.RangeIterator.instIteratorCollectPartial {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] {n : Type u → Type w} [Monad n] : Iterators.IteratorCollectPartial (RangeIterator su α) Id n

Equations

• Std.PRange.RangeIterator.instIteratorCollectPartial = Std.Iterators.IteratorCollectPartial.defaultImplementation

theorem Std.PRange.RangeIterator.Monadic.isPlausibleOutput_next {α : Type u} {su : BoundShape} {a : α} [UpwardEnumerable α] [SupportsUpperBound su α] {it : IterM Id α} (h : it.internalState.next = some a) (hP : SupportsUpperBound.IsSatisfied it.internalState.upperBound a) : it.IsPlausibleOutput a

theorem Std.PRange.RangeIterator.Monadic.isPlausibleOutput_iff {α : Type u} {su : BoundShape} {a : α} [UpwardEnumerable α] [SupportsUpperBound su α] {it : IterM Id α} : it.IsPlausibleOutput a ↔ it.internalState.next = some a ∧ SupportsUpperBound.IsSatisfied it.internalState.upperBound a

theorem Std.PRange.RangeIterator.isPlausibleOutput_next {α : Type u} {su : BoundShape} {a : α} [UpwardEnumerable α] [SupportsUpperBound su α] {it : Iter α} (h : it.internalState.next = some a) (hP : SupportsUpperBound.IsSatisfied it.internalState.upperBound a) : it.IsPlausibleOutput a

theorem Std.PRange.RangeIterator.isPlausibleOutput_iff {α : Type u} {su : BoundShape} {a : α} [UpwardEnumerable α] [SupportsUpperBound su α] {it : Iter α} : it.IsPlausibleOutput a ↔ it.internalState.next = some a ∧ SupportsUpperBound.IsSatisfied it.internalState.upperBound a

theorem Std.PRange.RangeIterator.Monadic.isPlausibleSuccessorOf_iff {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] {it' it : IterM Id α} : it'.IsPlausibleSuccessorOf it ↔ ∃ (a : α), it.internalState.next = some a ∧ SupportsUpperBound.IsSatisfied it.internalState.upperBound a ∧ UpwardEnumerable.succ? a = it'.internalState.next ∧ it'.internalState.upperBound = it.internalState.upperBound

theorem Std.PRange.RangeIterator.isPlausibleSuccessorOf_iff {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] {it' it : Iter α} : it'.IsPlausibleSuccessorOf it ↔ ∃ (a : α), it.internalState.next = some a ∧ SupportsUpperBound.IsSatisfied it.internalState.upperBound a ∧ UpwardEnumerable.succ? a = it'.internalState.next ∧ it'.internalState.upperBound = it.internalState.upperBound

theorem Std.PRange.RangeIterator.isSome_next_of_isPlausibleIndirectOutput {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] {it : Iter α} {out : α} (h : it.IsPlausibleIndirectOutput out) : it.internalState.next.isSome = true

instance Std.PRange.RangeIterator.instFinite {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] [LawfulUpwardEnumerable α] [HasFiniteRanges su α] : Iterators.Finite (RangeIterator su α) Id

instance Std.PRange.RangeIterator.instProductive {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] [LawfulUpwardEnumerable α] : Iterators.Productive (RangeIterator su α) Id

instance Std.PRange.RangeIterator.instIteratorAccess {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableUpperBound su α] : Iterators.IteratorAccess (RangeIterator su α) Id

Equations

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

instance Std.PRange.RangeIterator.instLawfulDeterministicIterator {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] : Iterators.LawfulDeterministicIterator (RangeIterator su α) Id

theorem Std.PRange.RangeIterator.Monadic.isPlausibleIndirectOutput_iff {su : BoundShape} {α : Type u_1} [UpwardEnumerable α] [SupportsUpperBound su α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableUpperBound su α] {it : IterM Id α} {out : α} : it.IsPlausibleIndirectOutput out ↔ ∃ (n : Nat), (it.internalState.next.bind fun (x : α) => UpwardEnumerable.succMany? n x) = some out ∧ SupportsUpperBound.IsSatisfied it.internalState.upperBound out

theorem Std.PRange.RangeIterator.isPlausibleIndirectOutput_iff {su : BoundShape} {α : Type u_1} [UpwardEnumerable α] [SupportsUpperBound su α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableUpperBound su α] {it : Iter α} {out : α} : it.IsPlausibleIndirectOutput out ↔ ∃ (n : Nat), (it.internalState.next.bind fun (x : α) => UpwardEnumerable.succMany? n x) = some out ∧ SupportsUpperBound.IsSatisfied it.internalState.upperBound out

Efficient IteratorLoop instance

As long as the compiler cannot optimize away the Option in the internal state, we use a special loop implementation.

@[inline]

instance Std.PRange.RangeIterator.instIteratorLoop {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableUpperBound su α] {n : Type u → Type w} [Monad n] : Iterators.IteratorLoop (RangeIterator su α) Id n

Equations

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

@[irreducible, specialize #[]]

def Std.PRange.RangeIterator.instIteratorLoop.loop {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] [LawfulUpwardEnumerable α] {n : Type u → Type w} [Monad n] (γ : Type u) (Pl : α → γ → ForInStep γ → Prop) (wf : Iterators.IteratorLoop.WellFounded (RangeIterator su α) Id Pl) (upperBound : Bound su α) (least : α) (acc : γ) (f : (out : α) → UpwardEnumerable.LE least out → SupportsUpperBound.IsSatisfied upperBound out → (c : γ) → n { s : ForInStep γ // Pl out c s }) (next : α) (hl : UpwardEnumerable.LE least next) (hu : SupportsUpperBound.IsSatisfied upperBound next) : n γ

Equations

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

instance Std.PRange.RepeatIterator.instIteratorLoopPartial {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableUpperBound su α] {n : Type u → Type w} [Monad n] : Iterators.IteratorLoopPartial (RangeIterator su α) Id n

Equations

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

@[specialize #[]]

partial def Std.PRange.RepeatIterator.instIteratorLoopPartial.loop {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] [LawfulUpwardEnumerable α] {n : Type u → Type w} [Monad n] (γ : Type u) (upperBound : Bound su α) (least : α) (acc : γ) (f : (out : α) → UpwardEnumerable.LE least out → SupportsUpperBound.IsSatisfied upperBound out → γ → n (ForInStep γ)) (next : α) (hl : UpwardEnumerable.LE least next) (hu : SupportsUpperBound.IsSatisfied upperBound next) : n γ

@[irreducible]

theorem Std.PRange.RangeIterator.instIteratorLoop.loop_eq {α : Type u} {least : α} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableUpperBound su α] {n : Type u → Type w} [Monad n] [LawfulMonad n] {γ : Type u} {lift : (γ δ : Type u) → (γ → n δ) → Id γ → n δ} [Internal.LawfulMonadLiftBindFunction lift] {PlausibleForInStep : α → γ → ForInStep γ → Prop} {upperBound : Bound su α} {next : α} {hl : UpwardEnumerable.LE least next} {hu : SupportsUpperBound.IsSatisfied upperBound next} {f : (out : α) → UpwardEnumerable.LE least out → SupportsUpperBound.IsSatisfied upperBound out → (c : γ) → n { s : ForInStep γ // PlausibleForInStep out c s }} {acc : γ} {wf : Iterators.IteratorLoop.WellFounded (RangeIterator su α) Id PlausibleForInStep} : loop γ PlausibleForInStep wf upperBound least acc f next hl hu = do let __do_lift ← f next hl hu acc match __do_lift with | ⟨ForInStep.yield c, property⟩ => Iterators.IterM.DefaultConsumers.forIn' lift γ PlausibleForInStep wf { internalState := { next := UpwardEnumerable.succ? next, upperBound := upperBound } } c { internalState := { next := UpwardEnumerable.succ? next, upperBound := upperBound } }.IsPlausibleIndirectOutput ⋯ fun (b : α) (h : { internalState := { next := UpwardEnumerable.succ? next, upperBound := upperBound } }.IsPlausibleIndirectOutput b) (c : γ) => f b ⋯ ⋯ c | ⟨ForInStep.done c, property⟩ => pure c

instance Std.PRange.RangeIterator.instLawfulIteratorLoop {α : Type u} {su : BoundShape} [UpwardEnumerable α] [SupportsUpperBound su α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableUpperBound su α] {n : Type u → Type w} [Monad n] [LawfulMonad n] : Iterators.LawfulIteratorLoop (RangeIterator su α) Id n