From d2c738c4bd798b484f474d4d7ac5d3fb5ee8ee95 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Mon, 9 Feb 2026 08:45:42 +0100 Subject: [PATCH] feat: vector iterator (#12363) This PR introduces iterators for vectors via `Vector.iter` and `Vector.iterM`, together with the usual lemmas. --- .../Iterators/Lemmas/Consumers/Collect.lean | 6 + src/Std/Data/Iterators/Lemmas/Producers.lean | 1 + .../Iterators/Lemmas/Producers/Array.lean | 16 +- .../Iterators/Lemmas/Producers/Monadic.lean | 1 + .../Lemmas/Producers/Monadic/Array.lean | 14 +- .../Lemmas/Producers/Monadic/Vector.lean | 148 +++++++++++++++++ .../Iterators/Lemmas/Producers/Vector.lean | 153 ++++++++++++++++++ src/Std/Data/Iterators/Producers.lean | 1 + src/Std/Data/Iterators/Producers/Monadic.lean | 1 + .../Iterators/Producers/Monadic/Vector.lean | 57 +++++++ src/Std/Data/Iterators/Producers/Vector.lean | 55 +++++++ 11 files changed, 449 insertions(+), 4 deletions(-) create mode 100644 src/Std/Data/Iterators/Lemmas/Producers/Monadic/Vector.lean create mode 100644 src/Std/Data/Iterators/Lemmas/Producers/Vector.lean create mode 100644 src/Std/Data/Iterators/Producers/Monadic/Vector.lean create mode 100644 src/Std/Data/Iterators/Producers/Vector.lean diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean index a4accb2e54..ca40328bec 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean @@ -59,6 +59,12 @@ theorem Iter.toListRev_ensureTermination_eq_toListRev {α β} [Iterator α Id β {it : Iter (α := α) β} : it.ensureTermination.toListRev = it.toListRev := (rfl) +@[simp] +theorem IterM.toArray_toIter {α β} [Iterator α Id β] [Finite α Id] + {it : IterM (α := α) Id β} : + it.toIter.toArray = it.toArray.run := + (rfl) + @[simp] theorem IterM.toList_toIter {α β} [Iterator α Id β] [Finite α Id] {it : IterM (α := α) Id β} : diff --git a/src/Std/Data/Iterators/Lemmas/Producers.lean b/src/Std/Data/Iterators/Lemmas/Producers.lean index 5819f96e04..3492264c5c 100644 --- a/src/Std/Data/Iterators/Lemmas/Producers.lean +++ b/src/Std/Data/Iterators/Lemmas/Producers.lean @@ -8,6 +8,7 @@ module prelude public import Std.Data.Iterators.Lemmas.Producers.Monadic public import Std.Data.Iterators.Lemmas.Producers.Array +public import Std.Data.Iterators.Lemmas.Producers.Vector public import Std.Data.Iterators.Lemmas.Producers.Empty public import Std.Data.Iterators.Lemmas.Producers.Repeat public import Std.Data.Iterators.Lemmas.Producers.Range diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Array.lean b/src/Std/Data/Iterators/Lemmas/Producers/Array.lean index 79d4f7f6b9..7e2061c31d 100644 --- a/src/Std/Data/Iterators/Lemmas/Producers/Array.lean +++ b/src/Std/Data/Iterators/Lemmas/Producers/Array.lean @@ -7,6 +7,8 @@ module prelude public import Std.Data.Iterators.Lemmas.Consumers.Collect +import Std.Data.Iterators.Lemmas.Consumers.Loop +import Init.Data.List.TakeDrop public import Std.Data.Iterators.Producers.Array public import Init.Data.Iterators.Producers.List public import Std.Data.Iterators.Lemmas.Producers.Monadic.Array @@ -76,7 +78,7 @@ theorem Array.toArray_iterFromIdx {array : Array β} {pos : Nat} : simp [iterFromIdx_eq_toIter_iterFromIdxM, Iter.toArray] @[simp, grind =] -theorem Array.toArray_toIter {array : Array β} : +theorem Array.toArray_iter {array : Array β} : array.iter.toArray = array := by simp [Array.iter_eq_iterFromIdx] @@ -86,10 +88,20 @@ theorem Array.toListRev_iterFromIdx {array : Array β} {pos : Nat} : simp [Iter.toListRev_eq, Array.toList_iterFromIdx] @[simp, grind =] -theorem Array.toListRev_toIter {array : Array β} : +theorem Array.toListRev_iter {array : Array β} : array.iter.toListRev = array.toListRev := by simp [Array.iter_eq_iterFromIdx] +@[simp, grind =] +theorem Array.length_iterFromIdx {array : Array β} {pos : Nat} : + (array.iterFromIdx pos).length = array.size - pos := by + simp [← Iter.length_toList_eq_length] + +@[simp, grind =] +theorem Array.length_iter {array : Array β} : + array.iter.length = array.size := by + simp [← Iter.length_toList_eq_length] + section Equivalence theorem Array.iterFromIdx_equiv_iter_drop_toList {α : Type w} {array : Array α} diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Monadic.lean b/src/Std/Data/Iterators/Lemmas/Producers/Monadic.lean index 50904ce584..d50a7d860c 100644 --- a/src/Std/Data/Iterators/Lemmas/Producers/Monadic.lean +++ b/src/Std/Data/Iterators/Lemmas/Producers/Monadic.lean @@ -7,5 +7,6 @@ module prelude public import Std.Data.Iterators.Lemmas.Producers.Monadic.Array +public import Std.Data.Iterators.Lemmas.Producers.Monadic.Vector public import Std.Data.Iterators.Lemmas.Producers.Monadic.Empty public import Std.Data.Iterators.Lemmas.Producers.Monadic.List diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean index bb2bfb6859..de64c028ea 100644 --- a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean +++ b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean @@ -145,7 +145,7 @@ theorem Array.toArray_iterFromIdxM [LawfulMonad m] {array : Array β} {pos : Nat rw [← List.toArray_drop] @[simp, grind =] -theorem Array.toArray_toIterM [LawfulMonad m] {array : Array β} : +theorem Array.toArray_iterM [LawfulMonad m] {array : Array β} : (array.iterM m).toArray = pure array := by simp [Array.iterM_eq_iterFromIdxM, Array.toArray_iterFromIdxM] @@ -155,6 +155,16 @@ theorem Array.toListRev_iterFromIdxM [LawfulMonad m] {array : Array β} {pos : N simp [IterM.toListRev_eq, Array.toList_iterFromIdxM] @[simp, grind =] -theorem Array.toListRev_toIterM [LawfulMonad m] {array : Array β} : +theorem Array.toListRev_iterM [LawfulMonad m] {array : Array β} : (array.iterM m).toListRev = pure array.toListRev := by simp [Array.iterM_eq_iterFromIdxM, Array.toListRev_iterFromIdxM] + +@[simp, grind =] +theorem Array.length_iterFromIdxM [LawfulMonad m] {array : Array β} {pos : Nat} : + (array.iterFromIdxM m pos).length = pure (.up (array.size - pos)) := by + simp [← IterM.up_length_toList_eq_length] + +@[simp, grind =] +theorem Array.length_iterM [LawfulMonad m] {array : Array β} : + (array.iterM m).length = pure (.up array.size) := by + simp [← IterM.up_length_toList_eq_length] diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Vector.lean b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Vector.lean new file mode 100644 index 0000000000..a341f29b6e --- /dev/null +++ b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Vector.lean @@ -0,0 +1,148 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +module + +prelude +public import Std.Data.Iterators.Lemmas.Producers.Monadic.Array +public import Std.Data.Iterators.Producers.Monadic.Vector +public import Std.Data.Iterators.Lemmas.Consumers.Monadic +public import Std.Data.Iterators.Lemmas.Producers.Monadic.List +public import Init.Data.Array.Lemmas +import Init.Data.List.Nat.TakeDrop +import Init.Data.List.TakeDrop +import Init.Omega +import Init.Data.Vector.Lemmas + +set_option doc.verso true + +open Std Std.Iterators + +@[expose] public section + +/-! +# Lemmas about vector iterators + +This module provides lemmas about the interactions of {name}`Vector.iterM` with {name}`IterM.step` +and various +collectors. +-/ + +variable {m : Type w → Type w'} [Monad m] {β : Type w} {n : Nat} + +theorem Vector.iterM_eq_iterFromIdxM {xs : Vector β n} : + xs.iterM m = xs.iterFromIdxM m 0 := + rfl + +theorem Std.Iterators.Vector.isPlausibleStep_iterFromIdxM_of_lt {xs : Vector β n} {pos : Nat} + (h : pos < n) : + (xs.iterFromIdxM m pos).IsPlausibleStep (.yield (xs.iterFromIdxM m (pos + 1)) xs[pos]) := by + simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep] + refine ⟨rfl, rfl, ?_, rfl⟩ + simpa [Vector.iterFromIdxM, Array.iterFromIdxM] using h + +theorem Std.Iterators.Vector.isPlausibleStep_iterFromIdxM_of_not_lt {xs : Vector β n} {pos : Nat} + (h : ¬ pos < n) : + (xs.iterFromIdxM m pos).IsPlausibleStep .done := by + simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep] + simpa [Vector.iterFromIdxM, Array.iterFromIdxM, Nat.not_lt] using h + +theorem Std.Iterators.Vector.isPlausibleStep_iterM_of_pos {xs : Vector β n} + (h : 0 < n) : + (xs.iterM m).IsPlausibleStep (.yield (xs.iterFromIdxM m 1) xs[0]) := by + simp only [Vector.iterM_eq_iterFromIdxM] + exact isPlausibleStep_iterFromIdxM_of_lt h + +theorem Std.Iterators.Vector.isPlausibleStep_iterM_of_not_pos {xs : Vector β n} + (h : ¬ 0 < n) : + (xs.iterM m).IsPlausibleStep .done := by + simp only [Vector.iterM_eq_iterFromIdxM] + exact isPlausibleStep_iterFromIdxM_of_not_lt h + +@[simp, grind =] +theorem Vector.iterFromIdxM_toArray {xs : Vector β n} {pos : Nat} : + xs.toArray.iterFromIdxM m pos = xs.iterFromIdxM m pos := + rfl + +@[simp, grind =] +theorem Vector.iterM_toArray {xs : Vector β n} : + xs.toArray.iterM m = xs.iterM m := + rfl + +theorem Vector.step_iterFromIdxM {xs : Vector β n} {pos : Nat} : + (xs.iterFromIdxM m pos).step = (pure <| .deflate <| if h : pos < n then + .yield + (xs.iterFromIdxM m (pos + 1)) + xs[pos] + (Vector.isPlausibleStep_iterFromIdxM_of_lt h) + else + .done (Vector.isPlausibleStep_iterFromIdxM_of_not_lt h)) := by + simp [← Vector.iterFromIdxM_toArray, Array.step_iterFromIdxM] + +theorem Vector.step_iterM {xs : Vector β n} : + (xs.iterM m).step = (pure <| .deflate <| if h : 0 < n then + .yield + (xs.iterFromIdxM m 1) + xs[0] + (Vector.isPlausibleStep_iterM_of_pos h) + else + .done (Vector.isPlausibleStep_iterM_of_not_pos h)) := by + simp [← Vector.iterFromIdxM_toArray, ← Vector.iterM_toArray, Array.step_iterM] + +section Equivalence + +theorem Vector.iterFromIdxM_equiv_iterM_drop_toList {α : Type w} {xs : Vector α n} + {m : Type w → Type w'} [Monad m] [LawfulMonad m] {pos : Nat} : + (xs.iterFromIdxM m pos).Equiv ((xs.toList.drop pos).iterM m) := by + simp only [← Vector.iterFromIdxM_toArray] + apply Array.iterFromIdxM_equiv_iterM_drop_toList + +theorem Vector.iterM_equiv_iterM_toList {α : Type w} {xs : Vector α n} {m : Type w → Type w'} + [Monad m] [LawfulMonad m] : + (xs.iterM m).Equiv (xs.toList.iterM m) := by + simp only [← Vector.iterM_toArray] + apply Array.iterM_equiv_iterM_toList + +end Equivalence + +@[simp, grind =] +theorem Vector.toList_iterFromIdxM [LawfulMonad m] {xs : Vector β n} {pos : Nat} : + (xs.iterFromIdxM m pos).toList = pure (xs.toList.drop pos) := by + simp [← Vector.iterFromIdxM_toArray, Vector.toList_toArray] + +@[simp, grind =] +theorem Vector.toList_iterM [LawfulMonad m] {xs : Vector β n} : + (xs.iterM m).toList = pure xs.toList := by + simp [← Vector.iterM_toArray, Vector.toList_toArray] + +@[simp, grind =] +theorem Vector.toArray_iterFromIdxM [LawfulMonad m] {xs : Vector β n} {pos : Nat} : + (xs.iterFromIdxM m pos).toArray = pure (xs.toArray.extract pos n) := by + simp [← Vector.iterFromIdxM_toArray] + +@[simp, grind =] +theorem Vector.toArray_iterM [LawfulMonad m] {xs : Vector β n} : + (xs.iterM m).toArray = pure xs.toArray := by + simp [← Vector.iterM_toArray] + +@[simp, grind =] +theorem Vector.toListRev_iterFromIdxM [LawfulMonad m] {xs : Vector β n} {pos : Nat} : + (xs.iterFromIdxM m pos).toListRev = pure (xs.toList.drop pos).reverse := by + simp [← Vector.iterFromIdxM_toArray, Vector.toList_toArray] + +@[simp, grind =] +theorem Vector.toListRev_iterM [LawfulMonad m] {xs : Vector β n} : + (xs.iterM m).toListRev = pure xs.toList.reverse := by + simp [← Vector.iterM_toArray, Vector.toList_toArray] + +@[simp, grind =] +theorem Vector.length_iterFromIdxM [LawfulMonad m] {xs : Vector β n} {pos : Nat} : + (xs.iterFromIdxM m pos).length = pure (.up (n - pos)) := by + simp [← IterM.up_length_toList_eq_length] + +@[simp, grind =] +theorem Vector.length_iterM [LawfulMonad m] {xs : Vector β n} : + (xs.iterM m).length = pure (.up n) := by + simp [← IterM.up_length_toList_eq_length] diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Vector.lean b/src/Std/Data/Iterators/Lemmas/Producers/Vector.lean new file mode 100644 index 0000000000..1b3442e322 --- /dev/null +++ b/src/Std/Data/Iterators/Lemmas/Producers/Vector.lean @@ -0,0 +1,153 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +module + +prelude +public import Std.Data.Iterators.Lemmas.Producers.Array +public import Std.Data.Iterators.Producers.Vector +public import Std.Data.Iterators.Producers.Monadic.Vector +import Init.Data.Vector.Lemmas +import Std.Data.Iterators.Lemmas.Consumers.Collect +import Std.Data.Iterators.Lemmas.Consumers.Loop +import Init.Data.List.TakeDrop +import Std.Data.Iterators.Lemmas.Producers.Monadic.Vector + +set_option doc.verso true + +open Std Std.Iterators + +@[expose] public section + +/-! +# Lemmas about vector iterators + +This module provides lemmas about the interactions of {name}`Vector.iter` with {name}`Iter.step` and +various collectors. +-/ + +variable {β : Type w} {n : Nat} + +theorem Vector.iter_eq_toIter_iterM {xs : Vector β n} : + xs.iter = (xs.iterM Id).toIter := + rfl + +theorem Vector.iter_eq_iterFromIdx {xs : Vector β n} : + xs.iter = xs.iterFromIdx 0 := + rfl + +theorem Vector.iterFromIdx_eq_toIter_iterFromIdxM {xs : Vector β n} {pos : Nat} : + xs.iterFromIdx pos = (xs.iterFromIdxM Id pos).toIter := + rfl + +theorem Std.Iterators.Vector.isPlausibleStep_iterFromIdx_of_lt {xs : Vector β n} {pos : Nat} + (h : pos < n) : + (xs.iterFromIdx pos).IsPlausibleStep (.yield (xs.iterFromIdx (pos + 1)) xs[pos]) := by + simp only [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep] + refine ⟨rfl, rfl, ?_, rfl⟩ + simpa [Vector.iterFromIdx, Array.iterFromIdxM, Array.iterFromIdx] using h + +theorem Std.Iterators.Vector.isPlausibleStep_iterFromIdx_of_not_lt {xs : Vector β n} {pos : Nat} + (h : ¬ pos < n) : + (xs.iterFromIdx pos).IsPlausibleStep .done := by + simp only [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep] + simpa [Vector.iterFromIdx, Array.iterFromIdxM, Array.iterFromIdx, Nat.not_lt] using h + +theorem Std.Iterators.Vector.isPlausibleStep_iter_of_pos {xs : Vector β n} + (h : 0 < n) : + (xs.iter).IsPlausibleStep (.yield (xs.iterFromIdx 1) xs[0]) := by + simp only [Vector.iter_eq_iterFromIdx] + exact isPlausibleStep_iterFromIdx_of_lt h + +theorem Std.Iterators.Vector.isPlausibleStep_iter_of_not_pos {xs : Vector β n} + (h : ¬ 0 < n) : + (xs.iter).IsPlausibleStep .done := by + simp only [Vector.iter_eq_iterFromIdx] + exact isPlausibleStep_iterFromIdx_of_not_lt h + +@[simp, grind =] +theorem Vector.iterFromIdx_toArray {xs : Vector β n} {pos : Nat} : + xs.toArray.iterFromIdx pos = xs.iterFromIdx pos := + rfl + +@[simp, grind =] +theorem Vector.iter_toArray {xs : Vector β n} : + xs.toArray.iter = xs.iter := + rfl + +theorem Vector.step_iterFromIdx {xs : Vector β n} {pos : Nat} : + (xs.iterFromIdx pos).step = if h : pos < n then + .yield + (xs.iterFromIdx (pos + 1)) + xs[pos] + (Vector.isPlausibleStep_iterFromIdx_of_lt h) + else + .done (Vector.isPlausibleStep_iterFromIdx_of_not_lt h) := by + split <;> simp [Vector.iterFromIdx_eq_toIter_iterFromIdxM, Iter.step, Vector.step_iterFromIdxM, *] + +theorem Vector.step_iter {xs : Vector β n} : + xs.iter.step = if h : 0 < n then + .yield + (xs.iterFromIdx 1) + xs[0] + (Vector.isPlausibleStep_iter_of_pos h) + else + .done (Vector.isPlausibleStep_iter_of_not_pos h) := by + simp [iter_eq_iterFromIdx, step_iterFromIdx] + +@[simp, grind =] +theorem Vector.toList_iterFromIdx {xs : Vector β n} {pos : Nat} : + (xs.iterFromIdx pos).toList = xs.toList.drop pos := by + simp [Iter.toList, Vector.iterFromIdx_eq_toIter_iterFromIdxM, Iter.toIterM_toIter, + Vector.toList_iterFromIdxM] + +@[simp, grind =] +theorem Vector.toList_iter {xs : Vector β n} : + xs.iter.toList = xs.toList := by + simp [← iter_toArray, Vector.toList_toArray] + +@[simp, grind =] +theorem Vector.toArray_iterFromIdx {xs : Vector β n} {pos : Nat} : + (xs.iterFromIdx pos).toArray = xs.toArray.extract pos n := by + simp [← iterFromIdx_toArray] + +@[simp, grind =] +theorem Vector.toArray_iter {xs : Vector β n} : + xs.iter.toArray = xs.toArray := by + simp [← iter_toArray] + +@[simp, grind =] +theorem Vector.toListRev_iterFromIdx {xs : Vector β n} {pos : Nat} : + (xs.iterFromIdx pos).toListRev = (xs.toList.drop pos).reverse := by + simp [Iter.toListRev_eq, Vector.toList_iterFromIdx] + +@[simp, grind =] +theorem Vector.toListRev_toIter {xs : Vector β n} : + xs.iter.toListRev = xs.toList.reverse := by + simp [Vector.iter_eq_iterFromIdx] + +@[simp, grind =] +theorem Vector.length_iterFromIdx {xs : Vector β n} {pos : Nat} : + (xs.iterFromIdx pos).length = n - pos := by + simp [← Iter.length_toList_eq_length] + +@[simp, grind =] +theorem Vector.length_iter {xs : Vector β n} : + xs.iter.length = n := by + simp [← Iter.length_toList_eq_length] + +section Equivalence + +theorem Vector.iterFromIdx_equiv_iter_drop_toList {α : Type w} {xs : Vector α n} + {pos : Nat} : (xs.iterFromIdx pos).Equiv (xs.toList.drop pos).iter := by + apply IterM.Equiv.toIter + exact Vector.iterFromIdxM_equiv_iterM_drop_toList + +theorem Vector.iter_equiv_iter_toList {α : Type w} {xs : Vector α n} : + xs.iter.Equiv xs.toList.iter := by + rw [Vector.iter_eq_iterFromIdx] + simpa using iterFromIdx_equiv_iter_drop_toList + +end Equivalence diff --git a/src/Std/Data/Iterators/Producers.lean b/src/Std/Data/Iterators/Producers.lean index 61f764266d..7158628705 100644 --- a/src/Std/Data/Iterators/Producers.lean +++ b/src/Std/Data/Iterators/Producers.lean @@ -8,6 +8,7 @@ module prelude public import Std.Data.Iterators.Producers.Monadic public import Std.Data.Iterators.Producers.Array +public import Std.Data.Iterators.Producers.Vector public import Std.Data.Iterators.Producers.Empty public import Std.Data.Iterators.Producers.Range public import Std.Data.Iterators.Producers.Repeat diff --git a/src/Std/Data/Iterators/Producers/Monadic.lean b/src/Std/Data/Iterators/Producers/Monadic.lean index 6737b0fc97..8fce647f20 100644 --- a/src/Std/Data/Iterators/Producers/Monadic.lean +++ b/src/Std/Data/Iterators/Producers/Monadic.lean @@ -7,4 +7,5 @@ module prelude public import Std.Data.Iterators.Producers.Monadic.Array +public import Std.Data.Iterators.Producers.Monadic.Vector public import Std.Data.Iterators.Producers.Monadic.Empty diff --git a/src/Std/Data/Iterators/Producers/Monadic/Vector.lean b/src/Std/Data/Iterators/Producers/Monadic/Vector.lean new file mode 100644 index 0000000000..a04e479900 --- /dev/null +++ b/src/Std/Data/Iterators/Producers/Monadic/Vector.lean @@ -0,0 +1,57 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +module + +prelude +public import Init.Data.Vector.Basic +public import Std.Data.Iterators.Producers.Monadic.Array + +set_option doc.verso true + +/-! +# Vector iterator + +This module provides an iterator for vectors that is accessible via +{name (scope := "Std.Data.Iterators.Producers.Monadic.Vector")}`Vector.iterM`. +-/ + +@[expose] public section + +open Std Std.Iterators + +/-- +Returns a finite monadic iterator for the given vector starting at the given index. +The iterator yields the elements of the vector in order and then terminates. + +The pure version of this iterator is +{name (scope := "Std.Data.Iterators.Producers.Vector")}`Vector.iterFromIdx`. + +**Termination properties:** + +* {name}`Finite` instance: always +* {name}`Productive` instance: always +-/ +@[always_inline, inline, match_pattern] +def _root_.Vector.iterFromIdxM (xs : Vector α n) (m : Type w → Type w') + (pos : Nat) [Pure m] := + (xs.toArray.iterFromIdxM m pos : IterM m α) + +/-- +Returns a finite monadic iterator for the given vector. +The iterator yields the elements of the vector in order and then terminates. There are no side +effects. + +The pure version of this iterator is +{name (scope := "Std.Data.Iterators.Producers.Vector")}`Vector.iter`. + +**Termination properties:** + +* {name}`Finite` instance: always +* {name}`Productive` instance: always +-/ +@[inline] +def Vector.iterM (xs : Vector α n) (m : _) [Pure m] := + (xs.toArray.iterM m : IterM m α) diff --git a/src/Std/Data/Iterators/Producers/Vector.lean b/src/Std/Data/Iterators/Producers/Vector.lean new file mode 100644 index 0000000000..a610228357 --- /dev/null +++ b/src/Std/Data/Iterators/Producers/Vector.lean @@ -0,0 +1,55 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +module + +prelude +public import Init.Data.Vector.Basic +public import Std.Data.Iterators.Producers.Array + +set_option doc.verso true + +/-! +# Vector iterator + +This module provides an iterator for vectors that is accessible via +{name (scope := "Std.Data.Iterators.Producers.Vector")}`Vector.iter`. +-/ + +@[expose] public section + +open Std Std.Iterators + +/-- +Returns a finite iterator for the given vector starting at the given index. +The iterator yields the elements of the vector in order and then terminates. + +The monadic version of this iterator is +{name (scope := "Std.Data.Iterators.Producers.Monadic.Vector")}`Vector.iterFromIdxM`. + +**Termination properties:** + +* {name}`Finite` instance: always +* {name}`Productive` instance: always +-/ +@[always_inline, inline] +def Vector.iterFromIdx {α : Type w} (xs : Vector α n) (pos : Nat) := + (xs.toArray.iterFromIdx pos : Iter α) + +/-- +Returns a finite iterator for the given vector. +The iterator yields the elements of the vector in order and then terminates. + +The monadic version of this iterator is +{name (scope := "Std.Data.Iterators.Producers.Monadic.Vector")}`Vector.iterM`. + +**Termination properties:** + +* {name}`Finite` instance: always +* {name}`Productive` instance: always +-/ +@[always_inline, inline] +def Vector.iter {α : Type w} (xs : Vector α n) := + (xs.toArray.iter : Iter α)