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) n with fin-view n
... | zero  = x
... | suc 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

_++_ : βˆ€ {n k} β†’ Vec A n β†’ Vec A k β†’ Vec A (n + k)
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

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