open import 1Lab.Path
open import 1Lab.Type

open import Data.Product.NAry
open import Data.List.Base hiding (lookup ; tabulate)
open import Data.Fin.Base
open import Data.Nat.Base

module Data.Vec.Base where


# Vectorsπ

The type Vec is a representation of n-ary tuples with coordinates drawn from A. Therefore, it is equivalent to the type i.e., the functions from the standard finite set with elements to the type The halves of this equivalence are called lookup and tabulate.

data Vec {β} (A : Type β) : Nat β Type β where
[]  : Vec A zero
_β·_ : β {n} β A β Vec A n β Vec A (suc n)

Vec-elim
: β {β β'} {A : Type β} (P : β {n} β Vec A n β Type β')
β P []
β (β {n} x (xs : Vec A n) β P xs β P (x β· xs))
β β {n} (xs : Vec A n) β P xs
Vec-elim P p[] pβ· [] = p[]
Vec-elim P p[] pβ· (x β· xs) = pβ· x xs (Vec-elim P p[] pβ· xs)

infixr 20 _β·_

private variable
β : Level
A B C : Type β
n k : Nat

lookup : Vec A n β Fin n β A
lookup (x β· xs) fzero = x
lookup (x β· xs) (fsuc i) = lookup xs i

Vec-cast : {x y : Nat} β x β‘ y β Vec A x β Vec A y
Vec-cast {A = A} {x = x} {y = y} p xs =
Vec-elim (Ξ» {n} _ β (y : Nat) β n β‘ y β Vec A y)
(Ξ» { zero _ β []
; (suc x) p β absurd (zeroβ suc p)
})
(Ξ» { {n} head tail cast-tail zero 1+n=len β absurd (sucβ zero 1+n=len)
; {n} head tail cast-tail (suc len) 1+n=len β
head β· cast-tail len (suc-inj 1+n=len)
})
xs y p

-- Will always compute:
lookup-safe : Vec A n β Fin n β A
lookup-safe {A = A} xs n =
Fin-elim (Ξ» {n} _ β Vec A n β A)
(Ξ» {k} xs β Vec-elim (Ξ» {k'} _ β suc k β‘ k' β A)
(Ξ» p β absurd (sucβ zero p))
(Ξ» x _ _ _ β x) xs refl)
(Ξ» {i} j cont vec β
Vec-elim (Ξ» {k'} xs β suc i β‘ k' β A)
(Ξ» p β absurd (sucβ zero p))
(Ξ» {n} head tail _ si=sn β cont (Vec-cast (suc-inj (sym si=sn)) tail)) vec refl)
n xs

tabulate : (Fin n β A) β Vec A n
tabulate {zero} f  = []
tabulate {suc n} f = f fzero β· tabulate (Ξ» x β f (fsuc x))

map : (A β B) β Vec A n β Vec B n
map f [] = []
map f (x β· xs) = f x β· map f xs

zip-with : (A β B β C) β Vec A n β Vec B n β Vec C n
zip-with f [] [] = []
zip-with f (x β· xs) (y β· ys) = f x y β· zip-with f xs ys

replicate : (n : Nat) β A β Vec A n
replicate zero a = []
replicate (suc n) a = a β· replicate n a

instance
From-prod-Vec : From-product A (Vec A)
From-prod-Vec .From-product.from-prod = go where
go : β n β Vecβ A n β Vec A n
go zero xs                = []
go (suc zero) xs          = xs β· []
go (suc (suc n)) (x , xs) = x β· go (suc n) xs

_ : Path (Vec Nat 3) [ 1 , 2 , 3 ] (1 β· 2 β· 3 β· [])
_ = refl