list slices

datokrat · datokrat · commit 1d395508d244 · 2025-10-30T14:17:12.000+01:00
diff --git a/src/Init/Data/Iterators.lean b/src/Init/Data/Iterators.lean
@@ -9,6 +9,7 @@ prelude
 public import Init.Data.Iterators.Basic
 public import Init.Data.Iterators.PostconditionMonad
 public import Init.Data.Iterators.Consumers
+public import Init.Data.Iterators.Producers
 public import Init.Data.Iterators.Combinators
 public import Init.Data.Iterators.Lemmas
 public import Init.Data.Iterators.ToIterator
diff --git a/src/Init/Data/Iterators/Combinators.lean b/src/Init/Data/Iterators/Combinators.lean
@@ -9,4 +9,5 @@ prelude
 public import Init.Data.Iterators.Combinators.Monadic
 public import Init.Data.Iterators.Combinators.FilterMap
 public import Init.Data.Iterators.Combinators.FlatMap
+public import Init.Data.Iterators.Combinators.Take
 public import Init.Data.Iterators.Combinators.ULift
diff --git a/src/Init/Data/Iterators/Combinators/Monadic.lean b/src/Init/Data/Iterators/Combinators/Monadic.lean
@@ -8,4 +8,5 @@ module
 prelude
 public import Init.Data.Iterators.Combinators.Monadic.FilterMap
 public import Init.Data.Iterators.Combinators.Monadic.FlatMap
+public import Init.Data.Iterators.Combinators.Monadic.Take
 public import Init.Data.Iterators.Combinators.Monadic.ULift
diff --git a/src/Init/Data/Iterators/Combinators/Monadic/Take.lean b/src/Init/Data/Iterators/Combinators/Monadic/Take.lean
@@ -144,8 +144,7 @@ instance Take.instIteratorLoop {n : Type x → Type x'} [Monad m] [Monad n] [Ite
     IteratorLoop (Take α m β) m n :=
   .defaultImplementation
 
-instance Take.instIteratorLoopPartial [Monad m] [Monad n] [Iterator α m β]
-    [MonadLiftT m n] :
+instance Take.instIteratorLoopPartial [Monad m] [Monad n] [Iterator α m β] :
     IteratorLoopPartial (Take α m β) m n :=
   .defaultImplementation
 
diff --git a/src/Init/Data/Iterators/Combinators/Take.lean b/src/Init/Data/Iterators/Combinators/Take.lean
@@ -6,7 +6,7 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Std.Data.Iterators.Combinators.Monadic.Take
+public import Init.Data.Iterators.Combinators.Monadic.Take
 
 @[expose] public section
 
diff --git a/src/Init/Data/Iterators/Lemmas.lean b/src/Init/Data/Iterators/Lemmas.lean
@@ -8,3 +8,4 @@ module
 prelude
 public import Init.Data.Iterators.Lemmas.Consumers
 public import Init.Data.Iterators.Lemmas.Combinators
+public import Init.Data.Iterators.Lemmas.Producers
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators.lean b/src/Init/Data/Iterators/Lemmas/Combinators.lean
@@ -10,4 +10,5 @@ public import Init.Data.Iterators.Lemmas.Combinators.Attach
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic
 public import Init.Data.Iterators.Lemmas.Combinators.FilterMap
 public import Init.Data.Iterators.Lemmas.Combinators.FlatMap
+public import Init.Data.Iterators.Lemmas.Combinators.Take
 public import Init.Data.Iterators.Lemmas.Combinators.ULift
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic.lean
@@ -9,4 +9,5 @@ prelude
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
+public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Take.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Take.lean
@@ -6,7 +6,7 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Std.Data.Iterators.Combinators.Monadic.Take
+public import Init.Data.Iterators.Combinators.Monadic.Take
 public import Init.Data.Iterators.Lemmas.Consumers.Monadic
 
 @[expose] public section
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Take.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Take.lean
@@ -6,8 +6,8 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Std.Data.Iterators.Combinators.Take
-public import Std.Data.Iterators.Lemmas.Combinators.Monadic.Take
+public import Init.Data.Iterators.Combinators.Take
+public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
 public import Init.Data.Iterators.Lemmas.Consumers
 
 @[expose] public section
diff --git a/src/Init/Data/Iterators/Lemmas/Producers.lean b/src/Init/Data/Iterators/Lemmas/Producers.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
+public import Init.Data.Iterators.Lemmas.Producers.Monadic
+public import Init.Data.Iterators.Lemmas.Producers.List
diff --git a/src/Init/Data/Iterators/Lemmas/Producers/List.lean b/src/Init/Data/Iterators/Lemmas/Producers/List.lean
@@ -7,8 +7,8 @@ module
 
 prelude
 public import Init.Data.Iterators.Lemmas.Consumers.Collect
-public import Std.Data.Iterators.Producers.List
-public import Std.Data.Iterators.Lemmas.Producers.Monadic.List
+public import Init.Data.Iterators.Producers.List
+public import Init.Data.Iterators.Lemmas.Producers.Monadic.List
 
 @[expose] public section
 
diff --git a/src/Init/Data/Iterators/Lemmas/Producers/Monadic.lean b/src/Init/Data/Iterators/Lemmas/Producers/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
+public import Init.Data.Iterators.Lemmas.Producers.Monadic.List
diff --git a/src/Init/Data/Iterators/Lemmas/Producers/Monadic/List.lean b/src/Init/Data/Iterators/Lemmas/Producers/Monadic/List.lean
@@ -7,7 +7,7 @@ module
 
 prelude
 public import Init.Data.Iterators.Lemmas.Consumers.Monadic
-public import Std.Data.Iterators.Producers.Monadic.List
+public import Init.Data.Iterators.Producers.Monadic.List
 public import Std.Data.Iterators.Lemmas.Equivalence.Basic
 
 @[expose] public section
diff --git a/src/Init/Data/Iterators/Producers.lean b/src/Init/Data/Iterators/Producers.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
+public import Init.Data.Iterators.Producers.Monadic
+public import Init.Data.Iterators.Producers.List
diff --git a/src/Init/Data/Iterators/Producers/List.lean b/src/Init/Data/Iterators/Producers/List.lean
@@ -6,7 +6,7 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Std.Data.Iterators.Producers.Monadic.List
+public import Init.Data.Iterators.Producers.Monadic.List
 
 @[expose] public section
 
diff --git a/src/Init/Data/Iterators/Producers/Monadic.lean b/src/Init/Data/Iterators/Producers/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
+public import Init.Data.Iterators.Producers.Monadic.List
diff --git a/src/Init/Data/Iterators/Producers/Monadic/List.lean b/src/Init/Data/Iterators/Producers/Monadic/List.lean
diff --git a/src/Init/Data/Slice.lean b/src/Init/Data/Slice.lean
@@ -10,6 +10,7 @@ public import Init.Data.Slice.Basic
 public import Init.Data.Slice.Notation
 public import Init.Data.Slice.Operations
 public import Init.Data.Slice.Array
+public import Init.Data.Slice.List
 public import Init.Data.Slice.Lemmas
 
 public section
diff --git a/src/Init/Data/Slice/Array/Iterator.lean b/src/Init/Data/Slice/Array/Iterator.lean
@@ -17,8 +17,7 @@ import Init.Omega
 public section
 
 /-!
-This module provides slice notation for array slices (a.k.a. `Subarray`) and implements an iterator
-for those slices.
+This module implements an iterator for array slices (`Subarray`).
 -/
 
 open Std Slice PRange Iterators
diff --git a/src/Init/Data/Slice/List.lean b/src/Init/Data/Slice/List.lean
@@ -0,0 +1,11 @@
+/-
+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 Init.Data.Slice.List.Basic
+public import Init.Data.Slice.List.Iterator
+public import Init.Data.Slice.List.Lemmas
diff --git a/src/Init/Data/Slice/List/Basic.lean b/src/Init/Data/Slice/List/Basic.lean
@@ -0,0 +1,77 @@
+/-
+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 Init.Data.Slice.Basic
+public import Init.Data.Slice.Notation
+public import Init.Data.Range.Polymorphic.Nat
+
+/-!
+This module provides slice notation for list slices (a.k.a. `Sublist`) and implements an iterator
+for those slices.
+-/
+
+open Std Std.Slice Std.PRange
+
+public class Std.Slice.Internal.ListSliceData (α : Type u) where
+  list : List α
+  stop : Nat
+
+public abbrev ListSlice (α : Type u) := Slice (Internal.ListSliceData α)
+
+variable {α : Type u}
+
+public def List.toSlice (as : List α) (start : Nat) (stop : Nat) : ListSlice α :=
+  if start ≤ stop then
+    ⟨{ list := as.drop start, stop := stop - start }⟩
+  else
+    ⟨{ list := [], stop := 0 }⟩
+
+public instance : Rcc.Sliceable (List α) Nat (ListSlice α) where
+  mkSlice xs range :=
+    let halfOpenRange := Rcc.HasRcoIntersection.intersection range 0...xs.length
+    (xs.toSlice halfOpenRange.lower halfOpenRange.upper)
+
+public instance : Rco.Sliceable (List α) Nat (ListSlice α) where
+  mkSlice xs range :=
+    let halfOpenRange := Rco.HasRcoIntersection.intersection range 0...xs.length
+    (xs.toSlice halfOpenRange.lower halfOpenRange.upper)
+
+public instance : Rci.Sliceable (List α) Nat (ListSlice α) where
+  mkSlice xs range :=
+    let halfOpenRange := Rci.HasRcoIntersection.intersection range 0...xs.length
+    (xs.toSlice halfOpenRange.lower halfOpenRange.upper)
+
+public instance : Roc.Sliceable (List α) Nat (ListSlice α) where
+  mkSlice xs range :=
+    let halfOpenRange := Roc.HasRcoIntersection.intersection range 0...xs.length
+    (xs.toSlice halfOpenRange.lower halfOpenRange.upper)
+
+public instance : Roo.Sliceable (List α) Nat (ListSlice α) where
+  mkSlice xs range :=
+    let halfOpenRange := Roo.HasRcoIntersection.intersection range 0...xs.length
+    (xs.toSlice halfOpenRange.lower halfOpenRange.upper)
+
+public instance : Roi.Sliceable (List α) Nat (ListSlice α) where
+  mkSlice xs range :=
+    let halfOpenRange := Roi.HasRcoIntersection.intersection range 0...xs.length
+    (xs.toSlice halfOpenRange.lower halfOpenRange.upper)
+
+public instance : Ric.Sliceable (List α) Nat (ListSlice α) where
+  mkSlice xs range :=
+    let halfOpenRange := Ric.HasRcoIntersection.intersection range 0...xs.length
+    (xs.toSlice halfOpenRange.lower halfOpenRange.upper)
+
+public instance : Rio.Sliceable (List α) Nat (ListSlice α) where
+  mkSlice xs range :=
+    let halfOpenRange := Rio.HasRcoIntersection.intersection range 0...xs.length
+    (xs.toSlice halfOpenRange.lower halfOpenRange.upper)
+
+public instance : Rii.Sliceable (List α) Nat (ListSlice α) where
+  mkSlice xs _ :=
+    let halfOpenRange := 0...<xs.length
+    (xs.toSlice halfOpenRange.lower halfOpenRange.upper)
diff --git a/src/Init/Data/Slice/List/Iterator.lean b/src/Init/Data/Slice/List/Iterator.lean
@@ -0,0 +1,77 @@
+/-
+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 Init.Data.Slice.List.Basic
+public import Init.Data.Iterators.Producers.List
+public import Init.Data.Iterators.Combinators.Take
+import all Init.Data.Range.Polymorphic.Basic
+public import Init.Data.Range.Polymorphic.Iterators
+public import Init.Data.Slice.Operations
+import Init.Omega
+
+public section
+
+/-!
+This module implements an iterator for list slices.
+-/
+
+open Std Slice PRange Iterators
+
+variable {shape : RangeShape} {α : Type u}
+
+instance {s : ListSlice α} : ToIterator s Id α :=
+  .of _ (s.internalRepresentation.list.iter.take s.internalRepresentation.stop)
+
+universe v w
+
+@[no_expose] instance {s : ListSlice α} : Iterator (ToIterator.State s Id) Id α := inferInstance
+@[no_expose] instance {s : ListSlice α} : Finite (ToIterator.State s Id) Id := inferInstance
+@[no_expose] instance {s : ListSlice α} : IteratorCollect (ToIterator.State s Id) Id Id := inferInstance
+@[no_expose] instance {s : ListSlice α} : IteratorCollectPartial (ToIterator.State s Id) Id Id := inferInstance
+@[no_expose] instance {s : ListSlice α} {m : Type v → Type w} [Monad m] :
+    IteratorLoop (ToIterator.State s Id) Id m := inferInstance
+@[no_expose] instance {s : ListSlice α} {m : Type v → Type w} [Monad m] :
+    IteratorLoopPartial (ToIterator.State s Id) Id m := inferInstance
+
+instance : SliceSize (Internal.ListSliceData α) where
+  size s := (Internal.iter s).count
+
+@[no_expose]
+instance {α : Type u} {m : Type v → Type w} :
+    ForIn m (ListSlice α) α where
+  forIn xs init f := forIn (Internal.iter xs) init f
+
+namespace List
+
+/--
+Allocates a new list that contains the contents of the slice.
+-/
+def ofSlice (s : ListSlice α) : List α :=
+  s.toList
+
+instance : Append (ListSlice α) where
+  append x y :=
+   let a := x.toList ++ y.toList
+   a.toSlice 0 a.length
+
+/-- `ListSlice` representation. -/
+protected def ListSlice.repr [Repr α] (s : ListSlice α) : Std.Format :=
+  let xs := s.toList
+  repr xs ++ ".toSlice 0 " ++ toString xs.length
+
+instance [Repr α] : Repr (ListSlice α) where
+  reprPrec s  _ := ListSlice.repr s
+
+instance [ToString α] : ToString (ListSlice α) where
+  toString s := toString s.toArray
+
+end List
+
+@[inherit_doc List.ofSlice]
+def ListSlice.toList (s : ListSlice α) : List α :=
+  List.ofSlice s
diff --git a/src/Init/Data/Slice/List/Lemmas.lean b/src/Init/Data/Slice/List/Lemmas.lean
@@ -0,0 +1,38 @@
+/-
+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 all Init.Data.Slice.List.Basic
+public import Init.Data.Slice.List.Iterator
+import all Init.Data.Slice.List.Iterator
+import all Init.Data.Slice.Operations
+import all Init.Data.Range.Polymorphic.Iterators
+import all Init.Data.Range.Polymorphic.Lemmas
+public import Init.Data.Slice.Lemmas
+public import Init.Data.Iterators.Lemmas
+
+open Std.Iterators Std.PRange
+
+namespace Std.Slice.List
+
+theorem internalIter_rco_eq {α : Type u} {s : ListSlice α} :
+    Internal.iter s = s.internalRepresentation.list.iter.take s.internalRepresentation.stop := by
+  simp [Internal.iter, ToIterator.iter_eq]
+
+theorem toList_internalIter {α : Type u} {s : ListSlice α} :
+    (Internal.iter s).toList = s.internalRepresentation.list.take s.internalRepresentation.stop := by
+  simp [internalIter_rco_eq]
+
+theorem internalIter_eq_toIteratorIter {α : Type u} {s : ListSlice α} :
+    Internal.iter s = ToIterator.iter s :=
+  rfl
+
+public instance : LawfulSliceSize (Internal.ListSliceData α) where
+  lawful s := by
+    simp [← internalIter_eq_toIteratorIter, SliceSize.size]
+
+end Std.Slice.List
diff --git a/src/Std/Data/Iterators/Combinators.lean b/src/Std/Data/Iterators/Combinators.lean
@@ -7,7 +7,6 @@ module
 
 prelude
 public import Std.Data.Iterators.Combinators.Monadic
-public import Std.Data.Iterators.Combinators.Take
 public import Std.Data.Iterators.Combinators.TakeWhile
 public import Std.Data.Iterators.Combinators.Drop
 public import Std.Data.Iterators.Combinators.DropWhile
diff --git a/src/Std/Data/Iterators/Combinators/Monadic.lean b/src/Std/Data/Iterators/Combinators/Monadic.lean
@@ -6,7 +6,6 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Std.Data.Iterators.Combinators.Monadic.Take
 public import Std.Data.Iterators.Combinators.Monadic.TakeWhile
 public import Std.Data.Iterators.Combinators.Monadic.Drop
 public import Std.Data.Iterators.Combinators.Monadic.DropWhile
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators.lean b/src/Std/Data/Iterators/Lemmas/Combinators.lean
@@ -7,7 +7,6 @@ module
 
 prelude
 public import Std.Data.Iterators.Lemmas.Combinators.Monadic
-public import Std.Data.Iterators.Lemmas.Combinators.Take
 public import Std.Data.Iterators.Lemmas.Combinators.TakeWhile
 public import Std.Data.Iterators.Lemmas.Combinators.Drop
 public import Std.Data.Iterators.Lemmas.Combinators.DropWhile
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic.lean
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean
diff --git a/src/Std/Data/Iterators/Lemmas/Producers.lean b/src/Std/Data/Iterators/Lemmas/Producers.lean
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Array.lean b/src/Std/Data/Iterators/Lemmas/Producers/Array.lean
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Monadic.lean b/src/Std/Data/Iterators/Lemmas/Producers/Monadic.lean
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Repeat.lean b/src/Std/Data/Iterators/Lemmas/Producers/Repeat.lean
diff --git a/src/Std/Data/Iterators/Producers.lean b/src/Std/Data/Iterators/Producers.lean
diff --git a/src/Std/Data/Iterators/Producers/Monadic.lean b/src/Std/Data/Iterators/Producers/Monadic.lean
diff --git a/tests/lean/run/slice.lean b/tests/lean/run/slice.lean
