Abstract

Utility functions for arrays.

Synopsis

open import "futlib/zip"
val length [n] t : [n]t -> i32
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) -> []t
val init [n] t : (x: [n]t) -> []t
val take [n] t : (i: i32) -> (x: [n]t) -> [i]t
val drop [n] t : (i: i32) -> (x: [n]t) -> []t
val split t : (n: i32) -> (xs: []t) -> ([n]t, []t)
val split2 t : (i: i32) -> (j: i32) -> (xs: []t) -> ([i]t, []t, []t)
val reverse [n] t : (x: [n]t) -> [n]t
val ++ t : (xs: []t) -> (ys: []t) -> *[]t
val concat t : (xs: []t) -> (ys: []t) -> *[]t
val rotate t : (r: i32) -> (xs: []t) -> []t
val update [n] t : (xs: *[n]t) -> (i: i32) -> (x: t) -> *[n]t
val iota : (n: i32) -> *[n]i32
val replicate t : (n: i32) -> (x: t) -> *[n]t
val copy t : (a: t) -> *t
val flatten [n] [m] t : (xs: [n][m]t) -> []t
val flatten_3d [n] [m] [l] t : (xs: [n][m][l]t) -> []t
val flatten_4d [n] [m] [l] [k] t : (xs: [n][m][l][k]t) -> []t
val unflatten t : (n: i32) -> (m: i32) -> (xs: []t) -> [n][m]t
val unflatten_3d t : (n: i32) -> (m: i32) -> (l: i32) -> (xs: []t) -> [n][m][l]t
val unflatten_4d t : (n: i32) -> (m: i32) -> (l: i32) -> (k: i32) -> (xs: []t) -> [n][m][l][k]t
val intersperse [n] t : (x: t) -> (xs: [n]t) -> *[]t
val intercalate [n] [m] t : (x: [m]t) -> (xs: [n][m]t) -> []t
val transpose [n] [m] t : (a: [n][m]t) -> [m][n]t
val steps : (start: i32) -> (num_steps: i32) -> (step: i32) -> [num_steps]i32
val range : (start: i32) -> (end: i32) -> (step: i32) -> []i32
val and : []bool -> bool
val or : []bool -> bool
val pick [n] t : (flags: [n]bool) -> (xs: [n]t) -> (ys: [n]t) -> *[n]t
val foldl a b : (f: a -> b -> a) -> (acc: a) -> (bs: []b) -> a
val foldr a b : (f: b -> a -> a) -> (acc: a) -> (bs: []b) -> a
val tabulate a : (n: i32) -> (f: i32 -> a) -> *[n]a
val tabulate_2d a : (n: i32) -> (m: i32) -> (f: i32 -> i32 -> a) -> *[n][m]a
val tabulate_3d a : (n: i32) -> (m: i32) -> (o: i32) -> (f: i32 -> i32 -> i32 -> a) -> *[n][m][o]a

Description

val length [n] t: [n]t -> i32

The size of the outer dimension of an array.

val null [n] t: [n]t -> bool

Is the array empty?

val head [n] t: (x: [n]t) -> t

The first element of the array.

val last [n] t: (x: [n]t) -> t

The last element of the array.

val tail [n] t: (x: [n]t) -> []t

Everything but the first element of the array.

val init [n] t: (x: [n]t) -> []t

Everything but the last element of the array.

val take [n] t: (i: i32) -> (x: [n]t) -> [i]t

Take some number of elements from the head of the array.

val drop [n] t: (i: i32) -> (x: [n]t) -> []t

Remove some number of elements from the head of the array.

val split t: (n: i32) -> (xs: []t) -> ([n]t, []t)

Split an array at a given position.

val split2 t: (i: i32) -> (j: i32) -> (xs: []t) -> ([i]t, []t, []t)

Split an array at two given positions.

val reverse [n] t: (x: [n]t) -> [n]t

Return the elements of the array in reverse order.

val ++ t: (xs: []t) -> (ys: []t) -> *[]t

Concatenate two arrays. Warning: never try to perform a reduction with this operator; it will not work.

val concat t: (xs: []t) -> (ys: []t) -> *[]t

An old-fashioned way of saying ++.

val rotate t: (r: i32) -> (xs: []t) -> []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, then b[x+r] = a[x].

val update [n] t: (xs: *[n]t) -> (i: i32) -> (x: t) -> *[n]t

Replace an element of the array with a new value.

val iota: (n: i32) -> *[n]i32

Construct an array of consecutive integers of the given length, starting at 0.

val replicate t: (n: i32) -> (x: t) -> *[n]t

Construct an array of the given length containing the given value.

val copy t: (a: t) -> *t

Copy a value. The result will not alias anything.

val flatten [n] [m] t: (xs: [n][m]t) -> []t

Combines the outer two dimensions of an array.

val flatten_3d [n] [m] [l] t: (xs: [n][m][l]t) -> []t

Combines the outer three dimensions of an array.

val flatten_4d [n] [m] [l] [k] t: (xs: [n][m][l][k]t) -> []t

Combines the outer four dimensions of an array.

val unflatten t: (n: i32) -> (m: i32) -> (xs: []t) -> [n][m]t

Splits the outer dimension of an array in two.

val unflatten_3d t: (n: i32) -> (m: i32) -> (l: i32) -> (xs: []t) -> [n][m][l]t

Splits the outer dimension of an array in three.

val unflatten_4d t: (n: i32) -> (m: i32) -> (l: i32) -> (k: i32) -> (xs: []t) -> [n][m][l][k]t

Splits the outer dimension of an array in four.

val intersperse [n] t: (x: t) -> (xs: [n]t) -> *[]t
val intercalate [n] [m] t: (x: [m]t) -> (xs: [n][m]t) -> []t
val transpose [n] [m] t: (a: [n][m]t) -> [m][n]t
val steps: (start: i32) -> (num_steps: i32) -> (step: i32) -> [num_steps]i32
val range: (start: i32) -> (end: i32) -> (step: i32) -> []i32
val and: []bool -> bool

True if all of the input elements are true. Produces true on an empty array.

val or: []bool -> bool

True if any of the input elements are true. Produces false on an empty array.

val pick [n] t: (flags: [n]bool) -> (xs: [n]t) -> (ys: [n]t) -> *[n]t
val foldl a b: (f: a -> b -> a) -> (acc: a) -> (bs: []b) -> a

Perform a sequential left-fold of an array.

val foldr a b: (f: b -> a -> a) -> (acc: a) -> (bs: []b) -> a

Perform a sequential right-fold of an array.

val tabulate a: (n: i32) -> (f: i32 -> a) -> *[n]a

Create a value for each point in a one-dimensional index space.

val tabulate_2d a: (n: i32) -> (m: i32) -> (f: i32 -> i32 -> a) -> *[n][m]a

Create a value for each point in a two-dimensional index space.

val tabulate_3d a: (n: i32) -> (m: i32) -> (o: i32) -> (f: i32 -> i32 -> i32 -> a) -> *[n][m][o]a

Create a value for each point in a three-dimensional index space.