Skip to content

stdlib.array

Fixed-Size Array Operations

Generated from v0.65.7. 3 source files, 45 documented symbols.

array.xi

fn len[T, N](arr: &[N]T) -> Int

Number of elements in the fixed-size array.

  • Postcondition: result == N

fn is_empty[T, N](arr: &[N]T) -> Bool

True when the array has zero length.

  • Postcondition: (N == 0) => (result == true)
  • Postcondition: (N > 0) => (result == false)

fn first[T, N](arr: &[N]T) -> Option[T]

First element, or None for an empty array.

  • Postcondition: N == 0 => result is None

fn last[T, N](arr: &[N]T) -> Option[T]

Last element, or None for an empty array.

  • Postcondition: N == 0 => result is None

fn get[T, N](arr: &[N]T, index: Int) -> Option[T]

Element at index, or None when out of bounds.

  • Postcondition: index < 0 || index >= N => result is None

fn get_mut[T, N](arr: &mut [N]T, index: Int) -> Option[T]

Value-returning read (like Vec.get). The Option<&T> reference form is not representable on this compiler: the mono'd body boxes the element VALUE into the Option payload while call sites auto-deref the payload as a pointer (inttoptr of the value -> AV). All consumers must use the value form.

  • Postcondition: index < 0 || index >= N => result is None

fn map[T, U, N](arr: [N]T, f: fn(T) -> U) -> [N]U

Apply f to every element, returning a new array.

  • Postcondition: result.len() == N

fn zip[T, U, N](a: [N]T, b: [N]U) -> [N](T, U)

Pair the elements of two arrays positionally.

  • Postcondition: result.len() == N

fn fold[T, B, N](arr: [N]T, init: B, f: fn(B, T) -> B) -> B

Fold the elements with f, starting from init.

  • Postcondition: (N == 0) => (result == init)

fn as_slice[T, N](arr: &[N]T) -> Slice[T]

Borrow the array as a Slice.

  • Precondition: N > 0
  • Postcondition: result.len == N

fn as_mut_slice[T, N](arr: &mut [N]T) -> Slice[T]

Mutably borrow the array as a Slice.

  • Precondition: N > 0
  • Postcondition: result.len == N

fn each_ref[T, N](arr: &[N]T) -> [N]&T

Array of shared references to each element.

  • Postcondition: result.len() == N

fn each_mut[T, N](arr: &mut [N]T) -> [N]&mut T

Array of mutable references to each element.

  • Postcondition: result.len() == N

fn fill[T, N](arr: &mut [N]T, value: T)

Set every element to a clone of value.

  • Postcondition: true

fn swap[T, N](arr: &mut [N]T, a: Int, b: Int)

Swap the elements at a and b.

  • Precondition: a >= 0 && a < N
  • Precondition: b >= 0 && b < N

fn reverse[T, N](arr: &mut [N]T)

Reverse the elements in place.

  • Postcondition: true

fn rotate_left[T, N](arr: &mut [N]T, mid: Int)

Rotate the elements left by mid positions.

  • Precondition: mid >= 0
  • Precondition: mid <= N

fn rotate_right[T, N](arr: &mut [N]T, k: Int)

Rotate the elements right by k positions.

  • Precondition: k >= 0

fn sort[T, N](arr: &mut [N]T)

Sort the elements in place (ascending).

  • Postcondition: arr.is_sorted()

fn is_sorted_by[T, N](arr: &[N]T, compare: fn(&T, &T) -> Ordering) -> Bool

Whether arr is sorted according to compare (non-decreasing: no adjacent pair compares as Greater). O(N).

  • Postcondition: arr.len() < 2 => result == true

fn sort_by[T, N](arr: &mut [N]T, compare: fn(&T, &T) -> Ordering)

Sort with a comparator returning an Ordering.

  • Postcondition: is_sorted_by(arr, compare)

fn binary_search[T, N](arr: &[N]T, x: &T) -> Result[Int, Int]

Binary search in a sorted array: Ok(index) or Err(insertion point).

  • Precondition: N >= 0
  • Precondition: arr.is_sorted()

fn contains[T, N](arr: &[N]T, x: &T) -> Bool

True when the array contains x.

  • Postcondition: result == true => arr.contains(x)

fn array_sum[N](arr: &[N]Int) -> Int

Sum of all elements in an integer array. O(N).

  • Postcondition: (N == 0) => (result == 0)

fn array_max[T, N](arr: &[N]T) -> Option[T]

Maximum element in an array, or None if N == 0. O(N).

  • Postcondition: (N == 0) => (result.is_none == true)

fn array_min[T, N](arr: &[N]T) -> Option[T]

Minimum element in an array, or None if N == 0. O(N).

  • Postcondition: (N == 0) => (result.is_none == true)

fn array_count[T, N](arr: &[N]T, value: T) -> Int

Count occurrences of value in the array. O(N).

  • Postcondition: (N == 0) => (result == 0)

fn array_find[T, N](arr: &[N]T, value: T) -> Option[Int]

Find the index of the first occurrence of value, or None. O(N).

  • Postcondition: (N == 0) => (result.is_none == true)

fn array_equal[T, N](a: &[N]T, b: &[N]T) -> Bool

Deep equality check between two arrays. O(N).

  • Postcondition: (N == 0) => (result == true)

dynamic.xi

fn array_push(a: &mut Vec[Int], value: Int)

Append value to the end of a. O(1) amortized.

  • Postcondition: a.len() == a.len()@pre + 1
fn array_pop(a: &mut Vec[Int]) -> Option[Int]

Remove and return the last element, or None if a is empty. O(1).

  • Postcondition: (result.is_none == true) => (a.len() == 0)
fn array_insert(a: &mut Vec[Int], idx: Int, value: Int)

Insert value at idx, shifting later elements right. O(n). No-op when idx is outside [0, len].

  • Postcondition: idx < 0 || idx > a.len()@pre => a.len() == a.len()@pre
  • Postcondition: idx >= 0 && idx <= a.len()@pre => a.len() == a.len()@pre + 1
fn array_remove(a: &mut Vec[Int], idx: Int) -> Option[Int]

Remove and return the element at idx, or None if out of bounds. O(n).

  • Postcondition: idx < 0 || idx >= a.len()@pre => result is None
  • Postcondition: result is None => a.len() == a.len()@pre
  • Postcondition: result is Some(_) => a.len() == a.len()@pre - 1
fn array_resize(a: &mut Vec[Int], n: Int, fill: Int)

Resize a to n elements, padding new slots with fill. O(n). Negative n is a no-op; shrinking drops trailing elements.

  • Postcondition: (n >= 0) => (a.len() == n)
fn array_concat(a: &Vec[Int], b: &Vec[Int]) -> Vec[Int]

New vector with a followed by b. O(a.len() + b.len()).

  • Postcondition: result.len() == a.len() + b.len()
fn array_extend(a: &mut Vec[Int], b: &Vec[Int])

Append all elements of b to a. O(b.len()).

  • Postcondition: a.len() == a.len()@pre + b.len()
fn array_sort(a: &mut Vec[Int])

Sort a in place. O(n log n), stable, O(n) space.

  • Postcondition: a.len() == a.len()@pre
fn array_search(a: &Vec[Int], item: Int) -> Option[Int]

Index of the first occurrence of item, or None. O(n).

  • Postcondition: (a.len() == 0) => (result.is_none == true)
fn array_is_empty(a: &Vec[Int]) -> Bool

True if the vector has no elements. O(1).

  • Postcondition: (a.len() == 0) => (result == true)
  • Postcondition: (a.len() != 0) => (result == false)

fixed.xi

fn array_len[N](a: &[N]Int) -> Int

Compile-time length N of a fixed-size array. O(1).

  • Postcondition: result == N
fn array_get[N](a: &[N]Int, idx: Int) -> Option[Int]

Element at idx, or None if out of bounds. O(1). Returns a value copy.

  • Postcondition: (idx < 0 || idx >= N) => (result.is_none == true)
fn array_first[N](a: &[N]Int) -> Option[Int]

First element, or None if N == 0. O(1).

  • Postcondition: (N == 0) => (result.is_none == true)
fn array_last[N](a: &[N]Int) -> Option[Int]

Last element, or None if N == 0. O(1).

  • Postcondition: (N == 0) => (result.is_none == true)
fn array_slice[N](a: &[N]Int, start: Int, end: Int) -> Vec[Int]

Copy of a[start..end) as a Vec[Int]. Bounds are clamped to [0, N]. O(n).

  • Postcondition: (start >= end) => (result.len() == 0)
  • Postcondition: (start >= 0 && end <= N && end > start) => (result.len() == end - start)
  • Postcondition: (N == 0) => (result.len() == 0)
fn array_zip[N, M](a: &[N]Int, b: &[N]Int) -> Vec[(Int, Int)]

(a[i], b[i]) pairs, truncated to the shorter array. O(min(N, M)). Returns Vec[(Int, Int)]. Both truncation directions are claimed now that the const-generic truncate is fixed (compiler m237, verified on v0.64.2).

  • Postcondition: (N <= M) => (result.len() == N)
  • Postcondition: (M <= N) => (result.len() == M)