feat: introduce slices (#8947)

This PR introduces polymorphic slices in their most basic form. They
come with a notation similar to the new range notation. `Subarray` is
now also a slice and can produce an iterator now. It is intended to
migrate more operations of `Subarray` to the `Slice` wrapper type to
make them available for slices of other types, too.

The PR also moves the `filterMap` combinators into `Init` because they
are used internally to implement iterators on array slices.

Author: datokrat

src/Init/Data.lean

@@ -48,3 +48,4 @@ import Init.Data.RArray
 import Init.Data.Vector
 import Init.Data.Iterators
 import Init.Data.Range.Polymorphic
+import Init.Data.Slice

src/Init/Data/Array/Subarray.lean

@@ -7,21 +7,17 @@ module
 
 prelude
 import Init.Data.Array.Basic
+import Init.Data.Slice.Basic
 
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 set_option linter.missingDocs true
 
 universe u v w
 
 /--
-A region of some underlying array.
-
-A subarray contains an array together with the start and end indices of a region of interest.
-Subarrays can be used to avoid copying or allocating space, while being more convenient than
-tracking the bounds by hand. The region of interest consists of every index that is both greater
-than or equal to `start` and strictly less than `stop`.
+Internal representation of `Subarray`, which is an abbreviation for `Slice SubarrayData`.
 -/
-structure Subarray (α : Type u) where
+structure Std.Slice.Internal.SubarrayData (α : Type u) where
   /-- The underlying array. -/
   array : Array α
   /-- The starting index of the region of interest (inclusive). -/
@@ -42,6 +38,40 @@ structure Subarray (α : Type u) where
   -/
   stop_le_array_size : stop ≤ array.size
 
+open Std.Slice
+
+/--
+A region of some underlying array.
+
+A subarray contains an array together with the start and end indices of a region of interest.
+Subarrays can be used to avoid copying or allocating space, while being more convenient than
+tracking the bounds by hand. The region of interest consists of every index that is both greater
+than or equal to `start` and strictly less than `stop`.
+-/
+abbrev Subarray (α : Type u) := Std.Slice (Internal.SubarrayData α)
+
+instance {α : Type u} : Self (Std.Slice (Internal.SubarrayData α)) (Subarray α) where
+
+@[always_inline, inline, expose, inherit_doc Internal.SubarrayData.array]
+def Subarray.array (xs : Subarray α) : Array α :=
+  xs.internalRepresentation.array
+
+@[always_inline, inline, expose, inherit_doc Internal.SubarrayData.start]
+def Subarray.start (xs : Subarray α) : Nat :=
+  xs.internalRepresentation.start
+
+@[always_inline, inline, expose, inherit_doc Internal.SubarrayData.stop]
+def Subarray.stop (xs : Subarray α) : Nat :=
+  xs.internalRepresentation.stop
+
+@[always_inline, inline, expose, inherit_doc Internal.SubarrayData.start_le_stop]
+def Subarray.start_le_stop (xs : Subarray α) : xs.start ≤ xs.stop :=
+  xs.internalRepresentation.start_le_stop
+
+@[always_inline, inline, expose, inherit_doc Internal.SubarrayData.stop_le_array_size]
+def Subarray.stop_le_array_size (xs : Subarray α) : xs.stop ≤ xs.array.size :=
+  xs.internalRepresentation.stop_le_array_size
+
 namespace Subarray
 
 /--
@@ -51,7 +81,7 @@ def size (s : Subarray α) : Nat :=
   s.stop - s.start
 
 theorem size_le_array_size {s : Subarray α} : s.size ≤ s.array.size := by
-  let {array, start, stop, start_le_stop, stop_le_array_size} := s
+  let ⟨{array, start, stop, start_le_stop, stop_le_array_size}⟩ := s
   simp [size]
   apply Nat.le_trans (Nat.sub_le stop start)
   assumption
@@ -102,7 +132,9 @@ Examples:
 -/
 def popFront (s : Subarray α) : Subarray α :=
   if h : s.start < s.stop then
-    { s with start := s.start + 1, start_le_stop := Nat.le_of_lt_succ (Nat.add_lt_add_right h 1) }
+    ⟨{ s.internalRepresentation with
+        start := s.start + 1,
+        start_le_stop := Nat.le_of_lt_succ (Nat.add_lt_add_right h 1) }⟩
   else
     s
 
@@ -111,12 +143,13 @@ The empty subarray.
 
 This empty subarray is backed by an empty array.
 -/
-protected def empty : Subarray α where
-  array := #[]
-  start := 0
-  stop := 0
-  start_le_stop := Nat.le_refl 0
-  stop_le_array_size := Nat.le_refl 0
+protected def empty : Subarray α := ⟨{
+    array := #[]
+    start := 0
+    stop := 0
+    start_le_stop := Nat.le_refl 0
+    stop_le_array_size := Nat.le_refl 0
+  }⟩
 
 instance : EmptyCollection (Subarray α) :=
   ⟨Subarray.empty⟩
@@ -410,24 +443,24 @@ Additionally, the starting index is clamped to the ending index.
 def toSubarray (as : Array α) (start : Nat := 0) (stop : Nat := as.size) : Subarray α :=
   if h₂ : stop ≤ as.size then
     if h₁ : start ≤ stop then
-      { array := as, start := start, stop := stop,
-        start_le_stop := h₁, stop_le_array_size := h₂ }
+      ⟨{ array := as, start := start, stop := stop,
+         start_le_stop := h₁, stop_le_array_size := h₂ }⟩
     else
-      { array := as, start := stop, stop := stop,
-        start_le_stop := Nat.le_refl _, stop_le_array_size := h₂ }
+      ⟨{ array := as, start := stop, stop := stop,
+         start_le_stop := Nat.le_refl _, stop_le_array_size := h₂ }⟩
   else
     if h₁ : start ≤ as.size then
-      { array := as,
-        start := start,
-        stop := as.size,
-        start_le_stop := h₁,
-        stop_le_array_size := Nat.le_refl _ }
+      ⟨{ array := as,
+         start := start,
+         stop := as.size,
+         start_le_stop := h₁,
+         stop_le_array_size := Nat.le_refl _ }⟩
     else
-      { array := as,
-        start := as.size,
-        stop := as.size,
-        start_le_stop := Nat.le_refl _,
-        stop_le_array_size := Nat.le_refl _ }
+      ⟨{ array := as,
+         start := as.size,
+         stop := as.size,
+         start_le_stop := Nat.le_refl _,
+         stop_le_array_size := Nat.le_refl _ }⟩
 
 /--
 Allocates a new array that contains the contents of the subarray.

src/Init/Data/Array/Subarray/Split.lean

@@ -21,44 +21,24 @@ set_option linter.listVariables true -- Enforce naming conventions for `List`/`A
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Subarray
-/--
-Splits a subarray into two parts, the first of which contains the first `i` elements and the second
-of which contains the remainder.
--/
-def split (s : Subarray α) (i : Fin s.size.succ) : (Subarray α × Subarray α) :=
-  let ⟨i', isLt⟩ := i
-  have := s.start_le_stop
-  have := s.stop_le_array_size
-  have : s.start + i' ≤ s.stop := by
-    simp only [size] at isLt
-    omega
-  let pre := {s with
-    stop := s.start + i',
-    start_le_stop := by omega,
-    stop_le_array_size := by omega
-  }
-  let post := {s with
-    start := s.start + i'
-    start_le_stop := by assumption
-  }
-  (pre, post)
 
 /--
 Removes the first `i` elements of the subarray. If there are `i` or fewer elements, the resulting
 subarray is empty.
 -/
-def drop (arr : Subarray α) (i : Nat) : Subarray α where
+def drop (arr : Subarray α) (i : Nat) : Subarray α := ⟨{
   array := arr.array
   start := min (arr.start + i) arr.stop
   stop := arr.stop
   start_le_stop := by omega
   stop_le_array_size := arr.stop_le_array_size
+}⟩
 
 /--
 Keeps only the first `i` elements of the subarray. If there are `i` or fewer elements, the resulting
 subarray is empty.
 -/
-def take (arr : Subarray α) (i : Nat) : Subarray α where
+def take (arr : Subarray α) (i : Nat) : Subarray α := ⟨{
   array := arr.array
   start := arr.start
   stop := min (arr.start + i) arr.stop
@@ -68,3 +48,11 @@ def take (arr : Subarray α) (i : Nat) : Subarray α where
   stop_le_array_size := by
     have := arr.stop_le_array_size
     omega
+}⟩
+
+/--
+Splits a subarray into two parts, the first of which contains the first `i` elements and the second
+of which contains the remainder.
+-/
+def split (s : Subarray α) (i : Fin s.size.succ) : (Subarray α × Subarray α) :=
+  (s.take i, s.drop i)

src/Init/Data/Iterators.lean

@@ -9,7 +9,9 @@ prelude
 import Init.Data.Iterators.Basic
 import Init.Data.Iterators.PostconditionMonad
 import Init.Data.Iterators.Consumers
+import Init.Data.Iterators.Combinators
 import Init.Data.Iterators.Lemmas
+import Init.Data.Iterators.ToIterator
 import Init.Data.Iterators.Internal
 
 /-!

src/Init/Data/Iterators/Basic.lean

@@ -401,6 +401,20 @@ theorem IterM.IsPlausibleIndirectSuccessorOf.trans {α β : Type w} {m : Type w
   case refl => exact h'
   case cons_right ih => exact IsPlausibleIndirectSuccessorOf.cons_right ih ‹_›
 
+theorem IterM.IsPlausibleIndirectSuccessorOf.single {α β : Type w} {m : Type w → Type w'}
+    [Iterator α m β] {it' it : IterM (α := α) m β}
+    (h : it'.IsPlausibleSuccessorOf it) :
+    it'.IsPlausibleIndirectSuccessorOf it :=
+  .cons_right (.refl _) h
+
+theorem IterM.IsPlausibleIndirectOutput.trans {α β : Type w} {m : Type w → Type w'}
+    [Iterator α m β]
+    {it' it : IterM (α := α) m β} {out : β} (h : it'.IsPlausibleIndirectSuccessorOf it)
+    (h' : it'.IsPlausibleIndirectOutput out) : it.IsPlausibleIndirectOutput out := by
+  induction h
+  case refl => exact h'
+  case cons_right ih => exact IsPlausibleIndirectOutput.indirect ‹_› ih
+
 /--
 The type of the step object returned by `Iter.step`, containing an `IterStep`
 and a proof that this is a plausible step for the given iterator.

src/Init/Data/Iterators/Combinators.lean

@@ -0,0 +1,10 @@
+/-
+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
+import Init.Data.Iterators.Combinators.Monadic
+import Init.Data.Iterators.Combinators.FilterMap

src/Init/Data/Iterators/Combinators/Attach.lean

@@ -0,0 +1,25 @@
+/-
+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
+import Init.Data.Iterators.Combinators.Monadic.Attach
+import Init.Data.Iterators.Combinators.FilterMap
+
+namespace Std.Iterators
+
+@[always_inline, inline, inherit_doc IterM.attachWith]
+def Iter.attachWith {α β : Type w}
+    [Iterator α Id β]
+    (it : Iter (α := α) β) (P : β → Prop) (h : ∀ out, it.IsPlausibleIndirectOutput out → P out) :
+  Iter (α := Types.Attach α Id P) { out : β // P out } :=
+  (it.toIterM.attachWith P ?h).toIter
+where finally
+  case h =>
+    simp only [← isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM]
+    exact h
+
+end Std.Iterators

src/Std/Data/Iterators/Combinators/FilterMap.lean renamed to src/Init/Data/Iterators/Combinators/FilterMap.lean

@@ -3,8 +3,10 @@ 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
-import Std.Data.Iterators.Combinators.Monadic.FilterMap
+import Init.Data.Iterators.Combinators.Monadic.FilterMap
 
 /-!
 
@@ -75,7 +77,7 @@ postcondition is `fun x => x.isSome`; if `f` always fails, a suitable postcondit
 For each value emitted by the base iterator `it`, this combinator calls `f` and matches on the
 returned `Option` value.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 def Iter.filterMapWithPostcondition {α β γ : Type w} [Iterator α Id β] {m : Type w → Type w'}
     [Monad m] (f : β → PostconditionT m (Option γ)) (it : Iter (α := α) β) :=
   (letI : MonadLift Id m := ⟨pure⟩; it.toIterM.filterMapWithPostcondition f : IterM m γ)
@@ -120,7 +122,7 @@ be `fun _ => False`.
 
 For each value emitted by the base iterator `it`, this combinator calls `f`.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 def Iter.filterWithPostcondition {α β : Type w} [Iterator α Id β] {m : Type w → Type w'}
     [Monad m] (f : β → PostconditionT m (ULift Bool)) (it : Iter (α := α) β) :=
   (letI : MonadLift Id m := ⟨pure⟩; it.toIterM.filterWithPostcondition f : IterM m β)
@@ -164,7 +166,7 @@ be `fun _ => False`.
 
 For each value emitted by the base iterator `it`, this combinator calls `f`.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 def Iter.mapWithPostcondition {α β γ : Type w} [Iterator α Id β] {m : Type w → Type w'}
     [Monad m] (f : β → PostconditionT m γ) (it : Iter (α := α) β) :=
   (letI : MonadLift Id m := ⟨pure⟩; it.toIterM.mapWithPostcondition f : IterM m γ)
@@ -205,7 +207,7 @@ possible to manually prove `Finite` and `Productive` instances depending on the
 For each value emitted by the base iterator `it`, this combinator calls `f` and matches on the
 returned `Option` value.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 def Iter.filterMapM {α β γ : Type w} [Iterator α Id β] {m : Type w → Type w'}
     [Monad m] (f : β → m (Option γ)) (it : Iter (α := α) β) :=
   (letI : MonadLift Id m := ⟨pure⟩; it.toIterM.filterMapM f : IterM m γ)
@@ -242,7 +244,7 @@ manually prove `Finite` and `Productive` instances depending on the concrete cho
 
 For each value emitted by the base iterator `it`, this combinator calls `f`.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 def Iter.filterM {α β : Type w} [Iterator α Id β] {m : Type w → Type w'}
     [Monad m] (f : β → m (ULift Bool)) (it : Iter (α := α) β) :=
   (letI : MonadLift Id m := ⟨pure⟩; it.toIterM.filterM f : IterM m β)
@@ -281,22 +283,22 @@ manually prove `Finite` and `Productive` instances depending on the concrete cho
 
 For each value emitted by the base iterator `it`, this combinator calls `f`.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 def Iter.mapM {α β γ : Type w} [Iterator α Id β] {m : Type w → Type w'}
     [Monad m] (f : β → m γ) (it : Iter (α := α) β) :=
   (letI : MonadLift Id m := ⟨pure⟩; it.toIterM.mapM f : IterM m γ)
 
-@[always_inline, inline, inherit_doc IterM.filterMap]
+@[always_inline, inline, inherit_doc IterM.filterMap, expose]
 def Iter.filterMap {α : Type w} {β : Type w} {γ : Type w} [Iterator α Id β]
     (f : β → Option γ) (it : Iter (α := α) β) :=
   ((it.toIterM.filterMap f).toIter : Iter γ)
 
-@[always_inline, inline, inherit_doc IterM.filter]
+@[always_inline, inline, inherit_doc IterM.filter, expose]
 def Iter.filter {α : Type w} {β : Type w} [Iterator α Id β]
     (f : β → Bool) (it : Iter (α := α) β) :=
   ((it.toIterM.filter f).toIter : Iter β)
 
-@[always_inline, inline, inherit_doc IterM.map]
+@[always_inline, inline, inherit_doc IterM.map, expose]
 def Iter.map {α : Type w} {β : Type w} {γ : Type w} [Iterator α Id β]
     (f : β → γ) (it : Iter (α := α) β) :=
   ((it.toIterM.map f).toIter : Iter γ)

src/Init/Data/Iterators/Combinators/Monadic.lean

@@ -0,0 +1,9 @@
+/-
+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
+import Init.Data.Iterators.Combinators.Monadic.FilterMap