Module Indexing.Vector

The submodule Vector allows safely manipulating indices into a vector.

type ('n, 'a) t = ('n, 'a) vector
val length : ('n, 'a) t -> 'n cardinal

length is analogous to Array.length, but returns a cardinal instead of an ordinary integer.

val get : ('n, 'a) t -> 'n index -> 'a

get is Array.get, but expects an index instead of an ordinary integer. This guarantees that the index is within bounds.

val set : ('n, 'a) t -> 'n index -> 'a -> unit

set is Array.set, but expects an index instead of an ordinary integer. This guarantees that the index is within bounds.

val set_cons : ('n, 'a list) t -> 'n index -> 'a -> unit

set_cons t i x is short for set t i (x :: get t i).

val empty : (_, _) t

empty is the empty vector.

val make : 'n cardinal -> 'a -> ('n, 'a) t

make is analogous to Array.make. Invoking make n x fixes the cardinal n.

val make' : 'n cardinal -> (unit -> 'a) -> ('n, 'a) t

make' n f is roughly analogous to make n (f()), but removes the need to exhibit a value of type 'a when n is zero. The function call f() takes place only if n is greater than zero. It takes place at most once. Invoking make' n f fixes the cardinal n.

val init : 'n cardinal -> ('n index -> 'a) -> ('n, 'a) t

init is analogous to Array.init. Invoking init n f fixes the cardinal n.

val map : ('a -> 'b) -> ('n, 'a) t -> ('n, 'b) t

map is analogous to Array.map.