source
structure Std.Slice.Internal.SubarrayData (α : Type u) :
Type u

Internal representation of `Subarray`, which is an abbreviation for `Slice SubarrayData`.

- array : Array α

  The underlying array.

- start : Nat

  The starting index of the region of interest (inclusive).

- stop : Nat

  The ending index of the region of interest (exclusive).

- start_le_stop : self.start ≤ self.stop

  The starting index is no later than the ending index.

  The ending index is exclusive. If the starting and ending indices are equal, then the subarray is empty.

- stop_le_array_size : self.stop ≤ self.array.size

  The stopping index is no later than the end of the array.

  The ending index is exclusive. If it is equal to the size of the array, then the last element of the array is in the subarray.

Instances For

source
@[reducible, inline]
abbrev Subarray (α : Type u) :
Type u

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`.

Equations

- Subarray α = Std.Slice (Std.Slice.Internal.SubarrayData α)

Instances For

source
instance instSelfSliceSubarrayDataSubarray {α : Type u} :
Std.Slice.Self (Std.Slice (Std.Slice.Internal.SubarrayData α)) (Subarray α)
source
@[inline]
def Subarray.array {α : Type u_1} (xs : Subarray α) :
Array α

The underlying array.

Equations

- xs.array = xs.internalRepresentation.array

Instances For

source
@[inline]
def Subarray.start {α : Type u_1} (xs : Subarray α) :
Nat

The starting index of the region of interest (inclusive).

Equations

- xs.start = xs.internalRepresentation.start

Instances For

source
@[inline]
def Subarray.stop {α : Type u_1} (xs : Subarray α) :
Nat

The ending index of the region of interest (exclusive).

Equations

- xs.stop = xs.internalRepresentation.stop

Instances For

source
@[inline]
def Subarray.start_le_stop {α : Type u_1} (xs : Subarray α) :
xs.start ≤ xs.stop

The starting index is no later than the ending index.

The ending index is exclusive. If the starting and ending indices are equal, then the subarray is empty.

Equations

- ⋯ = ⋯

Instances For

source
@[inline]
def Subarray.stop_le_array_size {α : Type u_1} (xs : Subarray α) :
xs.stop ≤ xs.array.size

The stopping index is no later than the end of the array.

The ending index is exclusive. If it is equal to the size of the array, then the last element of the array is in the subarray.

Equations

- ⋯ = ⋯

Instances For

source
def Subarray.size {α : Type u_1} (s : Subarray α) :
Nat

Computes the size of the subarray.

Equations

- s.size = s.stop - s.start

Instances For

source
theorem Subarray.size_le_array_size {α : Type u_1} {s : Subarray α} :
s.size ≤ s.array.size
source
def Subarray.get {α : Type u_1} (s : Subarray α) (i : Fin s.size) :
α

Extracts an element from the subarray.

The index is relative to the start of the subarray, rather than the underlying array.

Equations

- s.get i = s.array[s.start + ↑i]

Instances For

source
instance Subarray.instGetElemNatLtSize {α : Type u_1} :
GetElem (Subarray α) Nat α fun (xs : Subarray α) (i : Nat) => i < xs.size
Equations

- Subarray.instGetElemNatLtSize = { getElem := fun (xs : Subarray α) (i : Nat) (h : i < xs.size) => xs.get ⟨i, h⟩ }

source
@[inline]
def Subarray.getD {α : Type u_1} (s : Subarray α) (i : Nat) (v₀ : α) :
α

Extracts an element from the subarray, or returns a default value `v₀` when the index is out of bounds.

The index is relative to the start and end of the subarray, rather than the underlying array.

Equations

- s.getD i v₀ = if h : i < s.size then s[i] else v₀

Instances For

source
@[reducible, inline]
abbrev Subarray.get! {α : Type u_1} [Inhabited α] (s : Subarray α) (i : Nat) :
α

Extracts an element from the subarray, or returns a default value when the index is out of bounds.

The index is relative to the start and end of the subarray, rather than the underlying array. The default value is that provided by the `Inhabited α` instance.

Equations

- s.get! i = s.getD i default

Instances For

source
def Subarray.popFront {α : Type u_1} (s : Subarray α) :
Subarray α

Shrinks the subarray by incrementing its starting index if possible, returning it unchanged if not.

Examples:

- `#[1,2,3].toSubarray.popFront.toArray = #[2, 3]`
- `#[1,2,3].toSubarray.popFront.popFront.toArray = #[3]`
- `#[1,2,3].toSubarray.popFront.popFront.popFront.toArray = #[]`
- `#[1,2,3].toSubarray.popFront.popFront.popFront.popFront.toArray = #[]`

Equations

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

Instances For

source
def Subarray.empty {α : Type u_1} :
Subarray α

The empty subarray.

This empty subarray is backed by an empty array.

Equations

- Subarray.empty = { internalRepresentation := { array := #[], start := 0, stop := 0, start_le_stop := Subarray.empty._proof_1✝, stop_le_array_size := Subarray.empty._proof_1✝¹ } }

Instances For

source
instance Subarray.instEmptyCollection {α : Type u_1} :
EmptyCollection (Subarray α)
Equations

- Subarray.instEmptyCollection = { emptyCollection := Subarray.empty }

source
instance Subarray.instInhabited {α : Type u_1} :
Inhabited (Subarray α)
Equations

- Subarray.instInhabited = { default := ∅ }

`ForIn`, `foldlM`, `foldl` and other operations are implemented in `Init.Data.Slice.Array.Iterator` using the slice iterator.

source
@[inline]
def Subarray.foldrM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → β → m β) (init : β) (as : Subarray α) :
m β

Folds a monadic operation from right to left over the elements in a subarray.

An accumulator of type `β` is constructed by starting with `init` and monadically combining each element of the subarray with the current accumulator value in turn, moving from the end to the start. The monad in question may permit early termination or repetition.

Examples:

    #eval #["red", "green", "blue"].toSubarray.foldrM (init := "") fun x acc => do
      let l ← Option.guard (· ≠ 0) x.length
      return s!"{acc}({l}){x} "

    some "(4)blue (5)green (3)red "

    #eval #["red", "green", "blue"].toSubarray.foldrM (init := 0) fun x acc => do
      let l ← Option.guard (· ≠ 5) x.length
      return s!"{acc}({l}){x} "

    none

Equations

- Subarray.foldrM f init as = Array.foldrM f init as.array as.stop as.start

Instances For

source
@[inline]
def Subarray.anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Subarray α) :
m Bool

Checks whether any of the elements in a subarray satisfy a monadic Boolean predicate.

The elements are tested starting at the lowest index and moving up. The search terminates as soon as an element that satisfies the predicate is found.

Example:

    #eval #["red", "green", "blue", "orange"].toSubarray.popFront.anyM fun x => do
      IO.println x
      pure (x == "blue")

    green
    blue

    true

Equations

- Subarray.anyM p as = Array.anyM p as.array as.start as.stop

Instances For

source
@[inline]
def Subarray.allM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Subarray α) :
m Bool

Checks whether all of the elements in a subarray satisfy a monadic Boolean predicate.

The elements are tested starting at the lowest index and moving up. The search terminates as soon as an element that does not satisfy the predicate is found.

Example:

    #eval #["red", "green", "blue", "orange"].toSubarray.popFront.allM fun x => do
      IO.println x
      pure (x.length == 5)

    green
    blue

    false

Equations

- Subarray.allM p as = Array.allM p as.array as.start as.stop

Instances For

source
@[inline]
def Subarray.forM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Subarray α) :
m PUnit

Runs a monadic action on each element of a subarray.

The elements are processed starting at the lowest index and moving up.

Equations

- Subarray.forM f as = Array.forM f as.array as.start as.stop

Instances For

source
@[inline]
def Subarray.forRevM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Subarray α) :
m PUnit

Runs a monadic action on each element of a subarray, in reverse order.

The elements are processed starting at the highest index and moving down.

Equations

- Subarray.forRevM f as = Array.forRevM f as.array as.stop as.start

Instances For

source
@[inline]
def Subarray.foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : Subarray α) :
β

Folds an operation from right to left over the elements in a subarray.

An accumulator of type `β` is constructed by starting with `init` and combining each element of the subarray with the current accumulator value in turn, moving from the end to the start.

Examples:

- `#["red", "green", "blue"].toSubarray.foldr (·.length + ·) 0 = 12`
- `#["red", "green", "blue"].toSubarray.popFront.foldr (·.length + ·) 0 = 9`

Equations

- Subarray.foldr f init as = (Subarray.foldrM (fun (x1 : α) (x2 : β) => pure (f x1 x2)) init as).run

Instances For

source
@[inline]
def Subarray.any {α : Type u} (p : α → Bool) (as : Subarray α) :
Bool

Checks whether any of the elements in a subarray satisfy a Boolean predicate.

The elements are tested starting at the lowest index and moving up. The search terminates as soon as an element that satisfies the predicate is found.

Equations

- Subarray.any p as = (Subarray.anyM (fun (x : α) => pure (p x)) as).run

Instances For

source
@[inline]
def Subarray.all {α : Type u} (p : α → Bool) (as : Subarray α) :
Bool

Checks whether all of the elements in a subarray satisfy a Boolean predicate.

The elements are tested starting at the lowest index and moving up. The search terminates as soon as an element that does not satisfy the predicate is found.

Equations

- Subarray.all p as = (Subarray.allM (fun (x : α) => pure (p x)) as).run

Instances For

source
@[inline]
def Subarray.findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Subarray α) (f : α → m (Option β)) :
m (Option β)

Applies a monadic function to each element in a subarray in reverse order, stopping at the first element for which the function succeeds by returning a value other than `none`. The succeeding value is returned, or `none` if there is no success.

Example:

    #eval #["red", "green", "blue"].toSubarray.findSomeRevM? fun x => do
      IO.println x
      return Option.guard (· = 5) x.length

    blue
    green

    some 5

Equations

- as.findSomeRevM? f = Subarray.findSomeRevM?.find✝ as f as.size ⋯

Instances For

source
@[inline]
def Subarray.findRevM? {α : Type} {m : Type → Type w} [Monad m] (as : Subarray α) (p : α → m Bool) :
m (Option α)

Applies a monadic Boolean predicate to each element in a subarray in reverse order, stopping at the first element that satisfies the predicate. The element that satisfies the predicate is returned, or `none` if no element satisfies it.

Example:

    #eval #["red", "green", "blue"].toSubarray.findRevM? fun x => do
      IO.println x
      return (x.length = 5)

    blue
    green

    some 5

Equations

- as.findRevM? p = as.findSomeRevM? fun (a : α) => do let __do_lift ← p a pure (if __do_lift = true then some a else none)

Instances For

source
@[inline]
def Subarray.findRev? {α : Type} (as : Subarray α) (p : α → Bool) :
Option α

Tests each element in a subarray with a Boolean predicate in reverse order, stopping at the first element that satisfies the predicate. The element that satisfies the predicate is returned, or `none` if no element satisfies the predicate.

Examples:

- `#["red", "green", "blue"].toSubarray.findRev? (·.length ≠ 4) = some "green"`
- `#["red", "green", "blue"].toSubarray.findRev? (fun _ => true) = some "blue"`
- `#["red", "green", "blue"].toSubarray 0 0 |>.findRev? (fun _ => true) = none`

Equations

- as.findRev? p = (as.findRevM? fun (x : α) => pure (p x)).run

Instances For

source
def Array.toSubarray {α : Type u} (as : Array α) (start : Nat := 0) (stop : Nat := as.size) :
Subarray α

Returns a subarray of an array, with the given bounds.

If `start` or `stop` are not valid bounds for a subarray, then they are clamped to array's size. Additionally, the starting index is clamped to the ending index.

Equations

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

Instances For

source
def Array.«term__[_:_]» :
Lean.TrailingParserDescr

A subarray with the provided bounds.

Equations

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

Instances For

source
def Array.«term__[_:]» :
Lean.TrailingParserDescr

A subarray with the provided lower bound that extends to the rest of the array.

Equations

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

Instances For

source
def Array.«term__[:_]» :
Lean.TrailingParserDescr

A subarray with the provided upper bound, starting at the index 0.

Equations

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

Instances For