Module Vec

## Meta-data

• Description: Base library for operations on type-indexed vectors
• Authors: Dominic Orchard, Vilem-Benjamin Liepelt
• Issue-tracking: https://github.com/dorchard/granule/issues
• Repository: https://github.com/dorchard/granule

## Contents

```data Vec (n : Nat) (t : Type) where
Nil  : Vec 0 t
; Cons : t -> (Vec n t) -> Vec (n + 1) t```
Sized vectors
```length : forall {a : Type, n : Nat}
. (Vec n (a [0])) -> N n```
Length of an indexed vector into an indexed nat discarding the elements
```length' : forall {a : Type, n : Nat}
. (Vec n a) -> (N n, Vec n a)```

```map : forall {a : Type, b : Type, n : Nat}
. ((a -> b) [n]) -> (Vec n a) -> Vec n b```

```index : forall {a : Type, n : Nat, m : Nat}
. {m > n} =>
(N n) -> ((Vec m a) [0..1]) -> a```
Safe random-access indexing from a vector
```foldr : forall {a : Type, b : Type, n : Nat}
. ((a -> b -> b) [n]) -> b -> (Vec n a) -> b```
Right fold
```foldr1 : forall {a : Type, n : Nat}
. ((a -> a -> a) [n]) -> (Vec (n + 1) a) -> a```
Foldr1 (no need for an initial value as vector has at least one element)
```foldl : forall {a : Type, b : Type, n : Nat}
. ((b -> a -> b) [n]) -> b -> (Vec n a) -> b```
Left fold
```append : forall {a : Type, m : Nat, n : Nat}
. (Vec n a) -> (Vec m a) -> Vec (n + m) a```
Append two vectors
```concat : forall {a : Type, m : Nat, n : Nat}
. (Vec n (Vec m a)) -> Vec (n * m) a```
Concatenate a vector of vectors
```dropElems : forall {a : Type, m : Nat, n : Nat}
. (N m) -> ((Vec n a) [0..1]) -> Vec (n - m) a```
Drop the first m elements
```take : forall {a : Type, m : Nat, n : Nat}
. (N m) -> ((Vec n a) [0..1]) -> Vec (n + (m - n)) a```
Take the first m elements
```head : forall {a : Type, n : Nat}
. ((Vec (n + 1) a) [0..1]) -> a```
Return the first item (head) of the vector NB: non-linear in the vector
```tail : forall {a : Type, n : Nat}
. ((Vec (n + 1) a) [0..1]) -> Vec n a```
Return the vector with the first item removed NB: non-linear in the vector
```uncons : forall {a : Type, n : Nat}
. (Vec (n + 1) a) -> (a, Vec n a)```
Take a vector and return the head element paired with the tail
```split : forall {a : Type, m : Nat, n : Nat}
. (N n) -> (Vec (n + m) a) -> (Vec n a, Vec m a)```
Split a vector at position 'n'
```sum : forall {n : Nat}
. (Vec n Int) -> Int```
Sum a vector of integers (using foldr)
```product : forall {n : Nat}
. (Vec n Int) -> Int```
Product of a vector of integers (using foldr)
```replicate : forall {a : Type, n : Nat}
. (N n) -> (a [n]) -> Vec n a```
Replicate n x is a vector of length n with x the value of every element
```range : forall {n : Nat}
. (N n) -> Vec n Int```
Make a vector of length n with all integers from 0 to n-1 e.g. range (S (S (S (S Z)))) should yield Cons 0 (Cons 1 (Cons 2 (Cons 3 Nil)))
```range' : forall {n : Nat}
. (N n) -> (Int [n]) -> Vec n Int```
Make a vector of length n with all integers from start up until n + i - 1 e.g. range' (S (S (S (S Z)))) [-6] should yield Cons -6 (Cons -5 (Cons -4 (Cons -3 Nil)))
```pullVec : forall {a : Type, s : Coeffect, k : s, n : Nat}
. (Vec n (a [k])) -> (Vec n a) [k]```
pullVec pulls non linearity in elements into a non linearity on the whole vector
```pushVec : forall {a : Type, s : Coeffect, k : s, n : Nat}
. {((1 : s)) ≤ k, Pushable k} =>
((Vec n a) [k]) -> Vec n (a [k])```
pushVec pushes in non linearity of vector into the elements
```copySpine : forall {a : Type, n : Nat}
. (Vec n a) -> (Vec n (), Vec n a)```
Copy the spine of a vector
```stringToVec : String -> exists {n : Nat}
. Vec n Char```
Convert a string into a vector