```------------------------------------------------------------------------
-- Vectors
------------------------------------------------------------------------

module Data.Vec where

open import Data.Nat
open import Data.Fin using (Fin; zero; suc)
open import Data.List as List using (List)
open import Data.Product using (_×_; _,_)

------------------------------------------------------------------------
-- Types

infixr 5 _∷_

data Vec (a : Set) : ℕ → Set where
[]  : Vec a zero
_∷_ : ∀ {n} (x : a) (xs : Vec a n) → Vec a (suc n)

infix 4 _∈_ _[_]=_

data _∈_ {a : Set} : a → {n : ℕ} → Vec a n → Set where
here  : ∀ {n} {x}   {xs : Vec a n} → x ∈ x ∷ xs
there : ∀ {n} {x y} {xs : Vec a n} (x∈xs : x ∈ xs) → x ∈ y ∷ xs

data _[_]=_ {a : Set} : {n : ℕ} → Vec a n → Fin n → a → Set where
here  : ∀ {n}     {x}   {xs : Vec a n} → x ∷ xs [ zero ]= x
there : ∀ {n} {i} {x y} {xs : Vec a n}
(xs[i]=x : xs [ i ]= x) → y ∷ xs [ suc i ]= x

------------------------------------------------------------------------
-- Some operations

head : ∀ {a n} → Vec a (1 + n) → a
head (x ∷ xs) = x

tail : ∀ {a n} → Vec a (1 + n) → Vec a n
tail (x ∷ xs) = xs

[_] : ∀ {a} → a → Vec a 1
[ x ] = x ∷ []

infixr 5 _++_

_++_ : ∀ {a m n} → Vec a m → Vec a n → Vec a (m + n)
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

map : ∀ {a b n} → (a → b) → Vec a n → Vec b n
map f []       = []
map f (x ∷ xs) = f x ∷ map f xs

zipWith :  ∀ {a b c n}
→ (a → b → c) → Vec a n → Vec b n → Vec c n
zipWith _⊕_ []       []       = []
zipWith _⊕_ (x ∷ xs) (y ∷ ys) = (x ⊕ y) ∷ zipWith _⊕_ xs ys

zip : ∀ {a b n} → Vec a n → Vec b n → Vec (a × b) n
zip = zipWith _,_

replicate : ∀ {a n} → a → Vec a n
replicate {n = zero}  x = []
replicate {n = suc n} x = x ∷ replicate x

foldr :  ∀ {a} (b : ℕ → Set) {m}
→ (∀ {n} → a → b n → b (suc n))
→ b zero
→ Vec a m → b m
foldr b _⊕_ n []       = n
foldr b _⊕_ n (x ∷ xs) = x ⊕ foldr b _⊕_ n xs

foldr₁ :  ∀ {a : Set} {m}
→ (a → a → a) → Vec a (suc m) → a
foldr₁ _⊕_ (x ∷ [])     = x
foldr₁ _⊕_ (x ∷ y ∷ ys) = x ⊕ foldr₁ _⊕_ (y ∷ ys)

foldl :  ∀ {a : Set} (b : ℕ → Set) {m}
→ (∀ {n} → b n → a → b (suc n))
→ b zero
→ Vec a m → b m
foldl b _⊕_ n []       = n
foldl b _⊕_ n (x ∷ xs) = foldl (λ n → b (suc n)) _⊕_ (n ⊕ x) xs

foldl₁ :  ∀ {a : Set} {m}
→ (a → a → a) → Vec a (suc m) → a
foldl₁ _⊕_ (x ∷ xs) = foldl _ _⊕_ x xs

concat : ∀ {a m n} → Vec (Vec a m) n → Vec a (n * m)
concat []         = []
concat (xs ∷ xss) = xs ++ concat xss

infixr 5 _++'_

data SplitAt {a : Set} (m : ℕ) {n : ℕ} : Vec a (m + n) → Set where
_++'_ : (xs : Vec a m) (ys : Vec a n) → SplitAt m (xs ++ ys)

splitAt : ∀ {a} m {n} (xs : Vec a (m + n)) → SplitAt m xs
splitAt zero    xs                = [] ++' xs
splitAt (suc m) (x ∷ xs)          with splitAt m xs
splitAt (suc m) (x ∷ .(ys ++ zs)) | ys ++' zs = (x ∷ ys) ++' zs

take : ∀ {a} m {n} → Vec a (m + n) → Vec a m
take m xs with splitAt m xs
take m .(xs ++ ys) | xs ++' ys = xs

drop : ∀ {a} m {n} → Vec a (m + n) → Vec a n
drop m xs with splitAt m xs
drop m .(xs ++ ys) | xs ++' ys = ys

data Group {a : Set} (n k : ℕ) : Vec a (n * k) → Set where
concat' : (xss : Vec (Vec a k) n) → Group n k (concat xss)

group : ∀ {a} n k (xs : Vec a (n * k)) → Group n k xs
group zero    k []                  = concat' []
group (suc n) k xs                  with splitAt k xs
group (suc n) k .(ys ++ zs)         | ys ++' zs with group n k zs
group (suc n) k .(ys ++ concat zss) | ys ++' ._ | concat' zss = concat' (ys ∷ zss)

reverse : ∀ {a n} → Vec a n → Vec a n
reverse {a} = foldl (Vec a) (λ rev x → x ∷ rev) []

sum : ∀ {n} → Vec ℕ n → ℕ
sum = foldr _ _+_ 0

toList : ∀ {a n} → Vec a n → List a
toList []       = List.[]
toList (x ∷ xs) = List._∷_ x (toList xs)

fromList : ∀ {a} → (xs : List a) → Vec a (List.length xs)
fromList List.[]         = []
fromList (List._∷_ x xs) = x ∷ fromList xs

-- Snoc.

infixl 5 _∷ʳ_

_∷ʳ_ : ∀ {a n} → Vec a n → a → Vec a (1 + n)
[]       ∷ʳ y = [ y ]
(x ∷ xs) ∷ʳ y = x ∷ (xs ∷ʳ y)

infixl 5 _∷ʳ'_

data InitLast {a : Set} (n : ℕ) : Vec a (1 + n) → Set where
_∷ʳ'_ : (xs : Vec a n) (x : a) → InitLast n (xs ∷ʳ x)

initLast : ∀ {a n} (xs : Vec a (1 + n)) → InitLast n xs
initLast {n = zero}  (x ∷ [])         = [] ∷ʳ' x
initLast {n = suc n} (x ∷ xs)         with initLast xs
initLast {n = suc n} (x ∷ .(ys ∷ʳ y)) | ys ∷ʳ' y = (x ∷ ys) ∷ʳ' y

init : ∀ {a n} → Vec a (1 + n) → Vec a n
init xs with initLast xs
init .(ys ∷ʳ y) | ys ∷ʳ' y = ys

last : ∀ {a n} → Vec a (1 + n) → a
last xs with initLast xs
last .(ys ∷ʳ y) | ys ∷ʳ' y = y

infixl 1 _>>=_

_>>=_ : ∀ {A B m n} → Vec A m → (A → Vec B n) → Vec B (m * n)
xs >>= f = concat (map f xs)

infixl 4 _⊛_

_⊛_ : ∀ {A B m n} → Vec (A → B) m → Vec A n → Vec B (m * n)
fs ⊛ xs = fs >>= λ f → map f xs

-- Interleaves the two vectors.

infixr 5 _⋎_

_⋎_ : ∀ {A m n} → Vec A m → Vec A n → Vec A (m +⋎ n)
[]       ⋎ ys = ys
(x ∷ xs) ⋎ ys = x ∷ (ys ⋎ xs)

lookup : ∀ {a n} → Fin n → Vec a n → a
lookup zero    (x ∷ xs) = x
lookup (suc i) (x ∷ xs) = lookup i xs

-- Update.

infixl 6 _[_]≔_

_[_]≔_ : ∀ {A n} → Vec A n → Fin n → A → Vec A n
[]       [ ()    ]≔ y
(x ∷ xs) [ zero  ]≔ y = y ∷ xs
(x ∷ xs) [ suc i ]≔ y = x ∷ xs [ i ]≔ y

-- Generates a vector containing all elements in Fin n. This function
-- is not placed in Data.Fin since Data.Vec depends on Data.Fin.

allFin : ∀ n → Vec (Fin n) n
allFin zero    = []
allFin (suc n) = zero ∷ map suc (allFin n)
```