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 ) -> 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
```drop : 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