Data.Vect

Reexports

import public Data.Fin
import public Data.Zippable

Definitions

data Vect : Nat -> Type -> Type

Totality: total
Visibility: public export
Constructors:

Nil : Vect 0 elem

  Empty vector

(::) : elem -> Vect len elem -> Vect (S len) elem

  A non-empty vector of length `S len`, consisting of a head element and
  the rest of the list, of length `len`.

Hints:

Applicative (Vect k)
Biinjective (::)
DecEq a => DecEq (Vect n a)
Eq a => Eq (Vect n a)
Foldable (Vect n)
Functor (Vect n)
Injective ((x ::))
Injective (\x => x :: xs)
Monad (Vect k)
Monoid a => Monoid (Vect k a)
Ord elem => Ord (Vect len elem)
Semigroup a => Semigroup (Vect k a)
Show elem => Show (Vect len elem)
Traversable (Vect k)
Zippable (Vect k)

length : Vect len elem -> Nat

Totality: total
Visibility: public export

lengthCorrect : (xs : Vect len elem) -> length xs = len

  Show that the length function on vectors in fact calculates the length

Totality: total
Visibility: export

invertVectZ : (xs : Vect 0 a) -> xs = []

Totality: total
Visibility: export

tail : Vect (S len) elem -> Vect len elem

  All but the first element of the vector
  
  ```idris example
  tail [1,2,3,4]
  ```

Totality: total
Visibility: public export

head : Vect (S len) elem -> elem

  Only the first element of the vector
  
  ```idris example
  head [1,2,3,4]
  ```

Totality: total
Visibility: public export

invertVectS : (xs : Vect (S n) a) -> xs = head xs :: tail xs

Totality: total
Visibility: export

last : Vect (S len) elem -> elem

  The last element of the vector
  
  ```idris example
  last [1,2,3,4]
  ```

Totality: total
Visibility: public export

init : Vect (S len) elem -> Vect len elem

  All but the last element of the vector
  
  ```idris example
  init [1,2,3,4]
  ```

Totality: total
Visibility: public export

take : (n : Nat) -> Vect (n + m) type -> Vect n type

  Extract the first `n` elements of a Vect.

Totality: total
Visibility: public export

take : (n : Nat) -> Stream a -> Vect n a

  Take precisely n elements from the stream.
  @ n how many elements to take
  @ xs the stream

Totality: total
Visibility: public export

drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem

  Drop the first `n` elements of a Vect.

Totality: total
Visibility: public export

drop' : (n : Nat) -> Vect l elem -> Vect (minus l n) elem

  Drop up to the first `n` elements of a Vect.

Totality: total
Visibility: public export

allFins : (n : Nat) -> Vect n (Fin n)

  Generate all of the Fin elements as a Vect whose length is the number of
  elements.
  
  Useful, for example, when one wants all the indices for specific Vect.

Totality: total
Visibility: public export

index : Fin len -> Vect len elem -> elem

  Extract a particular element from a vector
  
  ```idris example
  index 1 [1,2,3,4]
  ```

Totality: total
Visibility: public export

insertAt : Fin (S len) -> elem -> Vect len elem -> Vect (S len) elem

  Insert an element at a particular index
  
  ```idris example
  insertAt 1 8 [1,2,3,4]
  ```

Totality: total
Visibility: public export

deleteAt : Fin (S len) -> Vect (S len) elem -> Vect len elem

  Construct a new vector consisting of all but the indicated element
  
  ```idris example
  deleteAt 1 [1,2,3,4]
  ```

Totality: total
Visibility: public export

replaceAt : Fin len -> elem -> Vect len elem -> Vect len elem

  Replace an element at a particlar index with another
  
  ```idris example
  replaceAt 1 8 [1,2,3,4]
  ```

Totality: total
Visibility: public export

updateAt : Fin len -> (elem -> elem) -> Vect len elem -> Vect len elem

  Replace the element at a particular index with the result of applying a function to it
  @ i the index to replace at
  @ f the update function
  @ xs the vector to replace in
  
  ```idris example
  updateAt 1 (+10) [1,2,3,4]
  ```

Totality: total
Visibility: public export

(++) : Vect m elem -> Vect n elem -> Vect (m + n) elem

  Append two vectors
  
  ```idris example
  [1,2,3,4] ++ [5,6]
  ```

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

snoc : Vect n a -> a -> Vect (S n) a

  Add an element at the end of the vector.
  The main use case for it is to get the expected type signature
  `Vect n a -> a -> Vect (S n) a` instead of
  `Vect n a -> a -> Vect (n + 1) a` which you get by using `++ [x]`
  
  Snoc gets its name by reversing `cons`, indicating we are
  tacking on the element at the end rather than the begining.
  `append` would also be a suitable name.
  
  @ xs The vector to be appended
  @ v The value to append

Totality: total
Visibility: public export

unsnoc : Vect (S n) a -> (Vect n a, a)

  Pop the last element from a vector. This is the opposite of `snoc`, in that
  `(uncurry snoc) unsnoc xs` is `xs`. It is equivalent to `(init xs, last xs)`,
  but traverses the vector once.
  
  @ xs The vector to pop the element from.

Totality: total
Visibility: public export

replicate : (len : Nat) -> elem -> Vect len elem

  Repeat some value some number of times.
  
  @ len the number of times to repeat it
  @ x the value to repeat
  
  ```idris example
  replicate 4 1
  ```

Totality: total
Visibility: public export

mergeBy : (elem -> elem -> Ordering) -> Vect n elem -> Vect m elem -> Vect (n + m) elem

  Merge two ordered vectors
  
  ```idris example
  mergeBy compare (fromList [1,3,5]) (fromList [2,3,4,5,6])
  ```

Totality: total
Visibility: export

merge : Ord elem => Vect n elem -> Vect m elem -> Vect (n + m) elem

Totality: total
Visibility: export

replaceAtSameIndex : (xs : Vect n a) -> (i : Fin n) -> (0 y : a) -> index i (replaceAt i y xs) = y

Totality: total
Visibility: export

replaceAtDiffIndexPreserves : (xs : Vect n a) -> (i : Fin n) -> (j : Fin n) -> Not (i = j) -> (0 y : a) -> index i (replaceAt j y xs) = index i xs

Totality: total
Visibility: export

reverseOnto : Vect n elem -> Vect m elem -> Vect (n + m) elem

  Reverse the second vector, prepending the result to the first.
  
  ```idris example
  reverseOnto [0, 1] [10, 11, 12]
  ```

Totality: total
Visibility: public export

reverse : Vect len elem -> Vect len elem

  Reverse the order of the elements of a vector
  
  ```idris example
  reverse [1,2,3,4]
  ```

Totality: total
Visibility: public export

intersperse : elem -> Vect len elem -> Vect (len + pred len) elem

  Alternate an element between the other elements of a vector
  @ sep the element to intersperse
  @ xs the vector to separate with `sep`
  
  ```idris example
  intersperse 0 [1,2,3,4]
  ```

Totality: total
Visibility: export

toVect : (n : Nat) -> List a -> Maybe (Vect n a)

Totality: total
Visibility: public export

fromList' : Vect len elem -> (l : List elem) -> Vect (length l + len) elem

Totality: total
Visibility: public export

fromList : (xs : List elem) -> Vect (length xs) elem

  Convert a list to a vector.
  
  The length of the list should be statically known.
  
  ```idris example
  fromList [1,2,3,4]
  ```

Totality: total
Visibility: public export

mapMaybe : (a -> Maybe b) -> Vect len a -> (m : Nat ** Vect m b)

  Map a partial function across a vector, returning those elements for which
  the function had a value.
  
  The first projection of the resulting pair (ie the length) will always be
  at most the length of the input vector. This is not, however, guaranteed
  by the type.
  
  @ f the partial function (expressed by returning `Maybe`)
  @ xs the vector to check for results
  
  ```idris example
  mapMaybe ((find (=='a')) . unpack) (fromList ["abc","ade","bgh","xyz"])
  ```

Totality: total
Visibility: export

foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> Vect n t -> acc

Totality: total
Visibility: public export

foldrImplGoLemma : (x : a) -> (xs : Vect n a) -> (f : (a -> b -> b)) -> (e : b) -> (go : (b -> b)) -> go (foldrImpl f e (f x) xs) = foldrImpl f e (go . f x) xs

Totality: total
Visibility: export

concat : Vect m (Vect n elem) -> Vect (m * n) elem

  Flatten a vector of equal-length vectors
  
  ```idris example
  concat [[1,2,3], [4,5,6]]
  ```

Totality: total
Visibility: public export

foldr1 : (t -> t -> t) -> Vect (S n) t -> t

  Foldr without seeding the accumulator
  
  ```idris example
  foldr1 (-) (fromList [1,2,3])
  ```

Totality: total
Visibility: public export

foldl1 : (t -> t -> t) -> Vect (S n) t -> t

  Foldl without seeding the accumulator
  
  ```idris example
  foldl1 (-) (fromList [1,2,3])
  ```

Totality: total
Visibility: public export

scanr : (elem -> res -> res) -> res -> Vect len elem -> Vect (S len) res

  The scanr function is similar to foldr, but returns all the intermediate
  accumulator states in the form of a vector. Note the intermediate accumulator
  states appear in the result in reverse order - the first state appears last
  in the result.
  
  ```idris example
  scanr (-) 0 (fromList [1,2,3])
  ```

Totality: total
Visibility: public export

scanr1 : (elem -> elem -> elem) -> Vect len elem -> Vect len elem

  The scanr1 function is a variant of scanr that doesn't require an explicit
  starting value.
  It assumes the last element of the vector to be the starting value and then
  starts the fold with the element preceding it.
  
  ```idris example
  scanr1 (-) (fromList [1,2,3])
  ```

Totality: total
Visibility: public export

scanl : (res -> elem -> res) -> res -> Vect len elem -> Vect (S len) res

  The scanl function is similar to foldl, but returns all the intermediate
  accumulator states in the form of a vector.
  
  ```idris example
  scanl (-) 0 (fromList [1,2,3])
  ```

Totality: total
Visibility: public export

scanl1 : (elem -> elem -> elem) -> Vect len elem -> Vect len elem

  The scanl1 function is a variant of scanl that doesn't require an explicit
  starting value.
  It assumes the first element of the vector to be the starting value and then
  starts the fold with the element following it.
  
  ```idris example
  scanl1 (-) (fromList [1,2,3])
  ```

Totality: total
Visibility: public export

lookupBy : (key -> key -> Bool) -> key -> Vect n (key, val) -> Maybe val

  Find the association of some key with a user-provided comparison
  @ p the comparison operator for keys (True if they match)
  @ e the key to look for
  
  ```idris example
  lookupBy (==) 2 [(1, 'a'), (2, 'b'), (3, 'c')]
  ```

Totality: total
Visibility: public export

lookup : Eq key => key -> Vect n (key, val) -> Maybe val

  Find the assocation of some key using the default Boolean equality test
  
  ```idris example
  lookup 3 [(1, 'a'), (2, 'b'), (3, 'c')]
  ```

Totality: total
Visibility: public export

hasAnyBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool

  Check if any element of xs is found in elems by a user-provided comparison
  @ p the comparison operator
  @ elems the vector to search
  @ xs what to search for
  
  ```idris example
  hasAnyBy (==) [2,5] [1,2,3,4]
  ```

Totality: total
Visibility: public export

hasAny : Eq elem => Vect m elem -> Vect len elem -> Bool

  Check if any element of xs is found in elems using the default Boolean equality test
  
  ```idris example
  hasAny [2,5] [1,2,3,4]
  ```

Totality: total
Visibility: public export

find : (elem -> Bool) -> Vect len elem -> Maybe elem

  Find the first element of the vector that satisfies some test
  @ p the test to satisfy
  
  ```idris example
  find (== 3) [1,2,3,4]
  ```

Totality: total
Visibility: public export

findIndex : (elem -> Bool) -> Vect len elem -> Maybe (Fin len)

  Find the index of the first element of the vector that satisfies some test
  
  ```idris example
  findIndex (== 3) [1,2,3,4]
  ```

Totality: total
Visibility: public export

findIndices : (elem -> Bool) -> Vect m elem -> List (Fin m)

  Find the indices of all elements that satisfy some test
  
  ```idris example
  findIndices (< 3) [1,2,3,4]
  ```

Totality: total
Visibility: public export

elemIndexBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> Maybe (Fin m)

  Find the index of the first element of the vector that satisfies some test
  
  ```idris example
  elemIndexBy (==) 3 [1,2,3,4]
  ```

Totality: total
Visibility: public export

elemIndex : Eq elem => elem -> Vect m elem -> Maybe (Fin m)

  Find the index of the first element of the vector equal to the given one.
  
  ```idris example
  elemIndex 3 [1,2,3,4]
  ```

Totality: total
Visibility: public export

elemIndicesBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> List (Fin m)

  Find the indices of all elements that satisfy some test
  
  ```idris example
  elemIndicesBy (<=) 3 [1,2,3,4]
  ```

Totality: total
Visibility: public export

elemIndices : Eq elem => elem -> Vect m elem -> List (Fin m)

  Find the indices of all elements uquals to the given one
  
  ```idris example
  elemIndices 3 [1,2,3,4,3]
  ```

Totality: total
Visibility: public export

filter : (elem -> Bool) -> Vect len elem -> (p : Nat ** Vect p elem)

  Find all elements of a vector that satisfy some test
  
  ```idris example
  filter (< 3) (fromList [1,2,3,4])
  ```

Totality: total
Visibility: public export

nubBy : (elem -> elem -> Bool) -> Vect len elem -> (p : Nat ** Vect p elem)

  Make the elements of some vector unique by some test
  
  ```idris example
  nubBy (==) (fromList [1,2,2,3,4,4])
  ```

Totality: total
Visibility: public export

nub : Eq elem => Vect len elem -> (p : Nat ** Vect p elem)

  Make the elements of some vector unique by the default Boolean equality
  
  ```idris example
  nub (fromList [1,2,2,3,4,4])
  ```

Totality: total
Visibility: public export

deleteBy : (elem -> elem -> Bool) -> elem -> Vect len elem -> (p : Nat ** Vect p elem)

  Delete first element from list according to some test
  
  ```idris example
  deleteBy (<) 3 (fromList [1,2,2,3,4,4])
  ```

Totality: total
Visibility: public export

delete : Eq elem => elem -> Vect len elem -> (p : Nat ** Vect p elem)

  Delete first element from list equal to the given one
  
  ```idris example
  delete 2 (fromList [1,2,2,3,4,4])
  ```

Totality: total
Visibility: public export

splitAt : (n : Nat) -> Vect (n + m) elem -> (Vect n elem, Vect m elem)

  A tuple where the first element is a `Vect` of the `n` first elements and
  the second element is a `Vect` of the remaining elements of the original.
  It is equivalent to `(take n xs, drop n xs)` (`splitAtTakeDrop`),
  but is more efficient.
  
  @ n   the index to split at
  @ xs  the `Vect` to split in two
  
  ```idris example
  splitAt 2 (fromList [1,2,3,4])
  ```

Totality: total
Visibility: public export

partition : (elem -> Bool) -> Vect len elem -> ((p : Nat ** Vect p elem), (q : Nat ** Vect q elem))

  A tuple where the first element is a `Vect` of the `n` elements passing given test
  and the second element is a `Vect` of the remaining elements of the original.
  
  ```idris example
  partition (== 2) (fromList [1,2,3,2,4])
  ```

Totality: total
Visibility: public export

kSplits : (k : Nat) -> (n : Nat) -> Vect (k * n) a -> Vect k (Vect n a)

  Split a vector whose length is a multiple of two numbers, k times n, into k
  sections of length n.
  
  ```idris example
  > kSplits 2 4 [1, 2, 3, 4, 5, 6, 7, 8]
  [[1, 2, 3, 4], [5, 6, 7, 8]]
  ```

Totality: total
Visibility: public export

nSplits : (k : Nat) -> (n : Nat) -> Vect (k * n) a -> Vect n (Vect k a)

  Split a vector whose length is a multiple of two numbers, k times n, into n
  sections of length k.
  
  ```idris example
  > nSplits 2 4 [1, 2, 3, 4, 5, 6, 7, 8]
  [[1, 5], [2, 6], [3, 7], [4, 8]]
  ```

Totality: total
Visibility: public export

isPrefixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool

  Verify vector prefix
  
  ```idris example
  isPrefixOfBy (==) (fromList [1,2]) (fromList [1,2,3,4])
  ```

Totality: total
Visibility: public export

isPrefixOf : Eq elem => Vect m elem -> Vect len elem -> Bool

  Verify vector prefix
  
  ```idris example
  isPrefixOf (fromList [1,2]) (fromList [1,2,3,4])
  ```

Totality: total
Visibility: public export

isSuffixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool

  Verify vector suffix
  
  ```idris example
  isSuffixOfBy (==) (fromList [3,4]) (fromList [1,2,3,4])
  ```

Totality: total
Visibility: public export

isSuffixOf : Eq elem => Vect m elem -> Vect len elem -> Bool

  Verify vector suffix
  
  ```idris example
  isSuffixOf (fromList [3,4]) (fromList [1,2,3,4])
  ```

Totality: total
Visibility: public export

maybeToVect : Maybe elem -> (p : Nat ** Vect p elem)

  Convert Maybe type into Vect
  
  ```idris example
  maybeToVect (Just 2)
  ```

Totality: total
Visibility: public export

vectToMaybe : Vect len elem -> Maybe elem

  Convert first element of Vect (if exists) into Maybe.
  
  ```idris example
  vectToMaybe [2]
  ```

Totality: total
Visibility: public export

catMaybes : Vect n (Maybe elem) -> (p : Nat ** Vect p elem)

  Filter out Nothings from Vect and unwrap the Justs
  
  ```idris example
  catMaybes [Just 1, Just 2, Nothing, Nothing, Just 5]
  ```

Totality: total
Visibility: public export

diag : Vect len (Vect len elem) -> Vect len elem

  Get diagonal elements
  
  ```idris example
  diag [[1,2,3], [4,5,6], [7,8,9]]
  ```

Totality: total
Visibility: public export

tabulate : (Fin len -> a) -> Vect len a

Totality: total
Visibility: public export

range : Vect len (Fin len)

Totality: total
Visibility: public export

tabulate : (Subset Nat (\{arg:0} => LT {arg:0} len) -> a) -> Vect len a

Totality: total
Visibility: public export

range : Vect len (Subset Nat (\{arg:0} => LT {arg:0} len))

Totality: total
Visibility: public export

zipWithIndexLinear : (0 f : (a -> a -> {a:7178})) -> (xs : Vect n a) -> (ys : Vect n a) -> (i : Fin n) -> index i (zipWith f xs ys) = f (index i xs) (index i ys)

Totality: total
Visibility: export

zipWith3IndexLinear : (0 f : (a -> a -> a -> {a:7281})) -> (xs : Vect n a) -> (ys : Vect n a) -> (zs : Vect n a) -> (i : Fin n) -> index i (zipWith3 f xs ys zs) = f (index i xs) (index i ys) (index i zs)

Totality: total
Visibility: export

permute : Vect len a -> Vect len (Fin len) -> Vect len a

  Rearrange the elements of a vector according to some permutation of its
  indices.
  @ v the vector whose elements to rearrange
  @ p the permutation to apply
  
  ```idris example
  > permute ['a', 'b', 'c', 'd'] [0, 3, 2, 1]
  ['a', 'd' , 'c' ,'b']
  ```

Totality: total
Visibility: export

transpose : Vect m (Vect n elem) -> Vect n (Vect m elem)

  Transpose a `Vect` of `Vect`s, turning rows into columns and vice versa.
  
  This is like zipping all the inner `Vect`s together and is equivalent to `traverse id` (`transposeTraverse`).
  
  As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
  
  ```idris example
  transpose [[1,2], [3,4], [5,6], [7,8]]
  ```

Totality: total
Visibility: public export

exactLength : (len : Nat) -> Vect m a -> Maybe (Vect len a)

Totality: total
Visibility: export

overLength : (len : Nat) -> Vect m a -> Maybe (p : Nat ** Vect (plus p len) a)

  If the given Vect is at least the required length, return a Vect with
  at least that length in its type, otherwise return Nothing
  @len the required length
  @xs the vector with the desired length

Totality: total
Visibility: export