Abstract
Utility functions for arrays.
Synopsis
open import "/prelude/zip" | ||
val length | [n] 't : | [n]t -> i64 |
val null | [n] 't : | [n]t -> bool |
val head | [n] 't : | (x: [n]t) -> t |
val last | [n] 't : | (x: [n]t) -> t |
val tail | [n] 't : | (x: [n]t) -> [n - 1]t |
val init | [n] 't : | (x: [n]t) -> [n - 1]t |
val take | [n] 't : | (i: i64) -> (x: [n]t) -> [i]t |
val drop | [n] 't : | (i: i64) -> (x: [n]t) -> [n - i]t |
val sized | [m] 't : | (n: i64) -> (xs: [m]t) -> [n]t |
val split | [n] [m] 't : | (xs: [n + m]t) -> ([n]t, [m]t) |
val reverse | [n] 't : | (x: [n]t) -> [n]t |
val ++ | [n] [m] 't : | (xs: [n]t) -> (ys: [m]t) -> *[n + m]t |
val concat | [n] [m] 't : | (xs: [n]t) -> (ys: [m]t) -> *[n + m]t |
val iota | : | (n: i64) -> *[n]i64 |
val indices | [n] 't : | [n]t -> *[n]i64 |
val rotate | [n] 't : | (r: i64) -> (a: [n]t) -> *[n]t |
val replicate | 't : | (n: i64) -> (x: t) -> *[n]t |
val copy | 't : | (a: t) -> *t |
val manifest | 't : | (a: t) -> *t |
val flatten | [n] [m] 't : | (xs: [n][m]t) -> [n * m]t |
val flatten_3d | [n] [m] [l] 't : | (xs: [n][m][l]t) -> [n * m * l]t |
val flatten_4d | [n] [m] [l] [k] 't : | (xs: [n][m][l][k]t) -> [n * m * l * k]t |
val unflatten | 't [n] [m] : | (xs: [n * m]t) -> [n][m]t |
val unflatten_3d | 't [n] [m] [l] : | (xs: [n * m * l]t) -> [n][m][l]t |
val unflatten_4d | 't [n] [m] [l] [k] : | (xs: [n * m * l * k]t) -> [n][m][l][k]t |
val transpose | [n] [m] 't : | (a: [n][m]t) -> [m][n]t |
val and | [n] : | (xs: [n]bool) -> bool |
val or | [n] : | (xs: [n]bool) -> bool |
val foldl | [n] 'a 'b : | (f: a -> b -> a) -> (acc: a) -> (bs: [n]b) -> a |
val foldr | [n] 'a 'b : | (f: b -> a -> a) -> (acc: a) -> (bs: [n]b) -> a |
val tabulate | 'a : | (n: i64) -> (f: i64 -> a) -> *[n]a |
val tabulate_2d | 'a : | (n: i64) -> (m: i64) -> (f: i64 -> i64 -> a) -> *[n][m]a |
val tabulate_3d | 'a : | (n: i64) -> (m: i64) -> (o: i64) -> (f: i64 -> i64 -> i64 -> a) -> *[n][m][o]a |
Description
- ↑val tail [n] 't: (x: [n]t) -> [n - 1]t
Everything but the first element of the array.
Complexity: O(1).
- ↑val init [n] 't: (x: [n]t) -> [n - 1]t
Everything but the last element of the array.
Complexity: O(1).
- ↑val take [n] 't: (i: i64) -> (x: [n]t) -> [i]t
Take some number of elements from the head of the array.
Complexity: O(1).
- ↑val drop [n] 't: (i: i64) -> (x: [n]t) -> [n - i]t
Remove some number of elements from the head of the array.
Complexity: O(1).
- ↑val sized [m] 't: (n: i64) -> (xs: [m]t) -> [n]t
Statically change the size of an array. Fail at runtime if the imposed size does not match the actual size. Essentially syntactic sugar for a size coercion.
- ↑val split [n] [m] 't: (xs: [n + m]t) -> ([n]t, [m]t)
Split an array at a given position.
Complexity: O(1).
- ↑val reverse [n] 't: (x: [n]t) -> [n]t
Return the elements of the array in reverse order.
Complexity: O(1).
- ↑val ++ [n] [m] 't: (xs: [n]t) -> (ys: [m]t) -> *[n + m]t
Concatenate two arrays. Warning: never try to perform a reduction with this operator; it will not work.
Work: O(n).
Span: O(1).
- ↑val iota: (n: i64) -> *[n]i64
Construct an array of consecutive integers of the given length, starting at 0.
Work: O(n).
Span: O(1).
- ↑val indices [n] 't: [n]t -> *[n]i64
Construct an array comprising valid indexes into some other array, starting at 0.
Work: O(n).
Span: O(1).
- ↑val rotate [n] 't: (r: i64) -> (a: [n]t) -> *[n]t
Rotate an array some number of elements to the left. A negative rotation amount is also supported.
For example, if
b==rotate r a
, thenb[x] = a[x+r]
.Work: O(n).
Span: O(1).
Note: In most cases,
rotate
will be fused with subsequent operations such asmap
, in which case it is free.- ↑val replicate 't: (n: i64) -> (x: t) -> *[n]t
Construct an array of the given length containing the given value.
Work: O(n).
Span: O(1).
- ↑val manifest 't: (a: t) -> *t
Copy a value. The result will not alias anything. Additionally, there is a guarantee that the result will be laid out in row-major order in memory. This can be used for locality optimisations in cases where the compiler does not otherwise do the right thing.
Work: O(n).
Span: O(1).
- ↑val flatten [n] [m] 't: (xs: [n][m]t) -> [n * m]t
Combines the outer two dimensions of an array.
Complexity: O(1).
- ↑val flatten_3d [n] [m] [l] 't: (xs: [n][m][l]t) -> [n * m * l]t
Like
flatten
, but on the outer three dimensions of an array.- ↑val flatten_4d [n] [m] [l] [k] 't: (xs: [n][m][l][k]t) -> [n * m * l * k]t
Like
flatten
, but on the outer four dimensions of an array.- ↑val unflatten 't [n] [m]: (xs: [n * m]t) -> [n][m]t
Splits the outer dimension of an array in two.
Complexity: O(1).
- ↑val unflatten_3d 't [n] [m] [l]: (xs: [n * m * l]t) -> [n][m][l]t
Like
unflatten
, but produces three dimensions.- ↑val unflatten_4d 't [n] [m] [l] [k]: (xs: [n * m * l * k]t) -> [n][m][l][k]t
Like
unflatten
, but produces four dimensions.- ↑val and [n]: (xs: [n]bool) -> bool
True if all of the input elements are true. Produces true on an empty array.
Work: O(n).
Span: O(log(n)).
- ↑val or [n]: (xs: [n]bool) -> bool
True if any of the input elements are true. Produces false on an empty array.
Work: O(n).
Span: O(log(n)).
- ↑val foldl [n] 'a 'b: (f: a -> b -> a) -> (acc: a) -> (bs: [n]b) -> a
Perform a sequential left-fold of an array.
Work: O(n ✕ W(f))).
Span: O(n ✕ S(f)).
- ↑val foldr [n] 'a 'b: (f: b -> a -> a) -> (acc: a) -> (bs: [n]b) -> a
Perform a sequential right-fold of an array.
Work: O(n ✕ W(f))).
Span: O(n ✕ S(f)).
- ↑val tabulate 'a: (n: i64) -> (f: i64 -> a) -> *[n]a
Create a value for each point in a one-dimensional index space.
Work: O(n ✕ W(f))
Span: O(S(f))
- ↑val tabulate_2d 'a: (n: i64) -> (m: i64) -> (f: i64 -> i64 -> a) -> *[n][m]a
Create a value for each point in a two-dimensional index space.
Work: O(n ✕ m ✕ W(f))
Span: O(S(f))
- ↑val tabulate_3d 'a: (n: i64) -> (m: i64) -> (o: i64) -> (f: i64 -> i64 -> i64 -> a) -> *[n][m][o]a
Create a value for each point in a three-dimensional index space.
Work: O(n ✕ m ✕ o ✕ W(f))
Span: O(S(f))