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

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

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

Computes the size of the subarray.

Equations

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

theorem Subarray.size_le_array_size {α : Type u_1} {s : Subarray α} : s.size ≤ s.array.size

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]

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⟩ }

@[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₀

@[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

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

• s.popFront = if h : s.start < s.stop then { array := s.array, start := s.start + 1, stop := s.stop, start_le_stop := ⋯, stop_le_array_size := ⋯ } else s

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

The empty subarray.

This empty subarray is backed by an empty array.

Equations

• Subarray.empty = { array := #[], start := 0, stop := 0, start_le_stop := Subarray.empty._proof_1, stop_le_array_size := Subarray.empty._proof_1 }

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

Equations

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

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

Equations

• Subarray.instInhabited = { default := ∅ }

@[inline]

unsafe def Subarray.forInUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (s : Subarray α) (b : β) (f : α → β → m (ForInStep β)) : m β

The run-time implementation of ForIn.forIn for Subarray, which allows it to be used with for loops in do-notation.

This definition replaces Subarray.forIn.

Equations

• s.forInUnsafe b f = Subarray.forInUnsafe.loop s f (USize.ofNat s.stop) (USize.ofNat s.start) b

@[specialize #[]]

unsafe def Subarray.forInUnsafe.loop {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (s : Subarray α) (f : α → β → m (ForInStep β)) (sz i : USize) (b : β) : m β

Equations

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

@[implemented_by Subarray.forInUnsafe]

opaque Subarray.forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (s : Subarray α) (b : β) (f : α → β → m (ForInStep β)) : m β

The implementation of ForIn.forIn for Subarray, which allows it to be used with for loops in do-notation.

instance Subarray.instForIn {m : Type u_1 → Type u_2} {α : Type u_3} : ForIn m (Subarray α) α

Equations

• Subarray.instForIn = { forIn := fun {β : Type ?u.15} [Monad m] => Subarray.forIn }

@[inline]

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

Folds a monadic operation from left to right 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. The monad in question may permit early termination or repetition.

Examples:

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

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

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

none

Equations

• Subarray.foldlM f init as = Array.foldlM f init as.array as.start as.stop

@[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

@[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

@[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

@[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

@[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

@[inline]

def Subarray.foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Subarray α) : β

Folds an operation from left to right 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.

Examples:

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

Equations

• Subarray.foldl f init as = (Subarray.foldlM (fun (x1 : β) (x2 : α) => pure (f x1 x2)) init as).run

@[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:

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

Equations

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

@[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

@[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

@[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 ⋯

@[specialize #[]]

def Subarray.findSomeRevM?.find {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Subarray α) (f : α → m (Option β)) (i : Nat) : i ≤ as.size → m (Option β)

Equations

• Subarray.findSomeRevM?.find as f 0 x_2 = pure none
• Subarray.findSomeRevM?.find as f i.succ h = do let r ← f as[i] match r with | some val => pure r | none => have this := ⋯; Subarray.findSomeRevM?.find as f i this

@[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)

@[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

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.

def Array.ofSubarray {α : Type u} (s : Subarray α) : Array α

Allocates a new array that contains the contents of the subarray.

Equations

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

instance Array.instCoeSubarray {α : Type u} : Coe (Subarray α) (Array α)

Equations

• Array.instCoeSubarray = { coe := Array.ofSubarray }

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

A subarray with the provided bounds.

Equations

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

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.

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.

def Subarray.toArray {α : Type u_1} (s : Subarray α) : Array α

Allocates a new array that contains the contents of the subarray.

Equations

• s.toArray = ↑s

instance instAppendSubarray {α : Type u_1} : Append (Subarray α)

Equations

• instAppendSubarray = { append := fun (x y : Subarray α) => let a := x.toArray ++ y.toArray; a.toSubarray }

def Subarray.repr {α : Type u_1} [Repr α] (s : Subarray α) : Std.Format

Subarray representation.

Equations

• s.repr = repr s.toArray ++ Std.Format.text ".toSubarray"

instance instReprSubarray {α : Type u_1} [Repr α] : Repr (Subarray α)

Equations

• instReprSubarray = { reprPrec := fun (s : Subarray α) (x : Nat) => s.repr }

instance instToStringSubarray {α : Type u_1} [ToString α] : ToString (Subarray α)

Equations

• instToStringSubarray = { toString := fun (s : Subarray α) => toString s.toArray }