Data.ArrayVect

Definitions

data ArrayVect : Nat -> Type -> Type

  A fixed-length vector.
  
  The constructors are the source-level specification. The exported
  operations below are transformed during code generation so transformed
  producers and consumers use `IArray` as their runtime representation.
  Complexity notes on operations describe that transformed runtime path.

Totality: total
Visibility: export
Constructors:

Nil : ArrayVect 0 a

(::) : a -> ArrayVect n a -> ArrayVect (S n) a

Hints:

Applicative (ArrayVect n)

Eq a => Eq (ArrayVect n a)

Foldable (ArrayVect n)

Functor (ArrayVect n)

Ord a => Ord (ArrayVect n a)

Show a => Show (ArrayVect n a)

fromVect : Vect n a -> ArrayVect n a

  Runtime after transform: O(n). Allocates n array elements.

Totality: total
Visibility: export

toVect : ArrayVect n a -> Vect n a

  Runtime after transform: O(n). Allocates an n-element `Vect`.

Totality: total
Visibility: export

fromList : (xs : List a) -> ArrayVect (length xs) a

  Runtime after transform: O(n). Allocates n array elements.

Totality: total
Visibility: export

toList : ArrayVect n a -> List a

  Runtime after transform: O(n). Allocates n list cons cells.

Totality: total
Visibility: export

empty : ArrayVect 0 a

  Runtime after transform: O(1). Allocates an empty array.

Totality: total
Visibility: export

singleton : a -> ArrayVect 1 a

  Runtime after transform: O(1). Allocates a one-element array.

Totality: total
Visibility: export

replicate : (n : Nat) -> a -> ArrayVect n a

  Runtime after transform: O(n). Allocates n array elements.

Totality: total
Visibility: export

generate : (n : Nat) -> (Fin n -> a) -> ArrayVect n a

  Runtime after transform: O(n), plus callback cost. Allocates n array elements.

Totality: total
Visibility: export

iterate : (n : Nat) -> (a -> a) -> a -> ArrayVect n a

  Runtime after transform: O(n), plus callback cost. Allocates n array elements.

Totality: total
Visibility: export

length : ArrayVect n a -> Nat

  Runtime after transform: O(1). Allocates nothing.

Totality: total
Visibility: export

null : ArrayVect n a -> Bool

  Runtime after transform: O(1). Allocates nothing.

Totality: total
Visibility: export

index : Fin n -> ArrayVect n a -> a

  Runtime after transform: O(1). Allocates nothing.

Totality: total
Visibility: export

head : ArrayVect (S n) a -> a

  Runtime after transform: O(1). Allocates nothing.

Totality: total
Visibility: export

tail : ArrayVect (S n) a -> ArrayVect n a

  Runtime after transform: O(n) for a tail of length n.
  Allocates n array elements.

Totality: total
Visibility: export

map : (a -> b) -> ArrayVect n a -> ArrayVect n b

  Runtime after transform: O(n), plus callback cost. Allocates n array elements.

Totality: total
Visibility: export

mapWithIndex : (Fin n -> a -> b) -> ArrayVect n a -> ArrayVect n b

  Runtime after transform: O(n), plus callback cost. Allocates n array elements.

Totality: total
Visibility: export

updateAt : Fin n -> (a -> a) -> ArrayVect n a -> ArrayVect n a

  Runtime after transform: O(n), plus callback cost.
  Copies the whole array and allocates n array elements.

Totality: total
Visibility: export

replaceAt : Fin n -> a -> ArrayVect n a -> ArrayVect n a

  Runtime after transform: O(n).
  Copies the whole array and allocates n array elements.

Totality: total
Visibility: export

(++) : ArrayVect m a -> ArrayVect n a -> ArrayVect (m + n) a

  Runtime after transform: O(m + n). Allocates m + n array elements.

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 7

take : (m : Nat) -> ArrayVect (m + n) a -> ArrayVect m a

  Runtime after transform: O(1). Allocates nothing and reuses the array prefix.

Totality: total
Visibility: export

drop : (m : Nat) -> ArrayVect n a -> ArrayVect (minus n m) a

  Runtime after transform: O(n `minus` m). Allocates n `minus` m array elements.

Totality: total
Visibility: export

zipWith : (a -> b -> c) -> ArrayVect n a -> ArrayVect n b -> ArrayVect n c

  Runtime after transform: O(n), plus callback cost. Allocates n array elements.

Totality: total
Visibility: export

foldr : (a -> acc -> acc) -> acc -> ArrayVect n a -> acc

  Runtime after transform: O(n), plus callback cost. Allocates nothing.

Totality: total
Visibility: export

foldl : (acc -> a -> acc) -> acc -> ArrayVect n a -> acc

  Runtime after transform: O(n), plus callback cost. Allocates nothing.

Totality: total
Visibility: export

filter : (a -> Bool) -> ArrayVect n a -> (m : Nat ** ArrayVect m a)

  Runtime after transform: O(n), plus predicate cost.
  Allocates an n-slot result buffer; the returned vector length is the number retained.

Totality: total
Visibility: export

mapMaybe : (a -> Maybe b) -> ArrayVect n a -> (m : Nat ** ArrayVect m b)

  Runtime after transform: O(n), plus callback cost.
  Allocates an n-slot result buffer; the returned vector length is the number produced.

Totality: total
Visibility: export

equals : Eq a => ArrayVect n a -> ArrayVect n a -> Bool

  Runtime after transform: O(n) worst case. Allocates nothing.

Totality: total
Visibility: export

compare : Ord a => ArrayVect n a -> ArrayVect n a -> Ordering

  Runtime after transform: O(n) worst case. Allocates nothing.

Totality: total
Visibility: export