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

open import Data.Product.NAry
open import Data.Maybe.Base
open import Data.List.Base as List using (List; []; _∷_; length)
open import Data.Dec.Base
open import Data.Fin.Base
open import Data.Nat.Base as Nat
open import Data.Id.Base

open import Meta.Idiom

import Data.Irr

module Data.Vec.Base where

open import Data.List.Length public
-- we need reexport make-irr for []v to work
open Data.Irr using (make-irr) public
open Data.Irr

private variable
  β„“ : Level
  A B C : Type β„“
  n k : Nat

VectorsπŸ”—

The type Vec is a representation of n-ary tuples with coordinates drawn from A.

record Vec {β„“} (A : Type β„“) (n : Nat) : Type β„“ where
  constructor vec
  field
    lower   : List A
    ⦃ len ⦄ : Irr (Length lower n)

pattern []v = vec []

infixr 20 _∷v_
_∷v_ : βˆ€ {n} β†’ A β†’ Vec A n β†’ Vec A (suc n)
_∷v_ v (vec vs ⦃ p ⦄) = vec (v ∷ vs) ⦃ suc <$> p ⦄

data Vec-view {ℓ} {A : Type ℓ} : {n : Nat} → Vec A n → Typeω where
  []     : Vec-view []v
  _∷_  : βˆ€ {n} a β†’ (vs : Vec A n) β†’ Vec-view {n = suc n} (a ∷v vs)

vec-view : βˆ€ {n} (v : Vec A n) β†’ Vec-view v
vec-view {n = zero} []v = []
vec-view {n = zero} (vec (x ∷ xs) ⦃ l ⦄) with () ← recover l
vec-view {n = suc n} (vec (x ∷ xs)) = x ∷ vec xs
  ⦃ len-uncons <$> auto ⦄
vec-view {n = suc n} (vec [] ⦃ l ⦄) with () ← recover l

list→vec : (xs : List A) → Vec A (length xs)
list→vec xs = vec xs

head : Vec A (suc n) β†’ A
head (vec (x ∷ xs)) = x
head (vec [] ⦃ l ⦄) with () ← recover l

tail : Vec A (suc n) β†’ Vec A n
tail v with (x ∷ xs) ← vec-view v = xs

The type Vec A n 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.

lookup : Vec A n β†’ Fin n β†’ A
lookup (vec xs) (fin n) = from-just! _ $ List.!?-just xs n p where abstract
  p : n Nat.< length xs
  p = ≀-trans auto $ subst (Nat._≀ length xs) (has-length auto) auto

List syntaxπŸ”—

A similar type to Vec can be defined by recursion as an iteraded non-dependent product. The resulting type Vecβ‚“ has the advantage of supporting usual tuple syntax, but is fiddlier to eliminate. This is solved by implementing the From-product typeclass for Vec, which enables list syntax for the latter.

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                = []v
    go (suc zero) xs          = xs ∷v []v
    go (suc (suc n)) (x , xs) = x ∷v go (suc n) xs

_++_ : βˆ€ {n k} β†’ Vec A n β†’ Vec A k β†’ Vec A (n + k)
vec xs ++ vec ys = vec (xs List.++ ys) ⦃ liftA2 len-++ auto auto ⦄

Vec-elim
  : βˆ€ {β„“ β„“'} {A : Type β„“} (P : βˆ€ {n} β†’ Vec A n β†’ Type β„“')
  β†’ P []v
  β†’ (βˆ€ {n} x (xs : Vec A n) β†’ P xs β†’ P (x ∷v xs))
  β†’ βˆ€ {n} (xs : Vec A n) β†’ P xs
Vec-elim P p[] p∷ v with vec-view v
... | [] = p[]
... | (x ∷ xs) = p∷ x xs $ Vec-elim P p[] p∷ xs

Vec-cast : {x y : Nat} β†’ x ≑ y β†’ Vec A x β†’ Vec A y
Vec-cast {A = A} {x = x} {y = y} p (vec l ⦃ len ⦄) =
  vec l ⦃ subst (Ξ» n β†’ Length l n) p <$> len ⦄

tabulate : (Fin n β†’ A) β†’ Vec A n
tabulate v  = vec (List.tabulate v) ⦃ forget (len-tabulate v) ⦄

instance
  Map-Vec : βˆ€ {n} β†’ Map (eff (Ξ» A β†’ Vec A n ) )
  Map-Vec .Map.map f (vec l) = vec (f <$> l) ⦃ len-map <$> auto ⦄

zip :  Vec A n β†’ Vec B n β†’ Vec (A Γ— B) n
zip (vec u) (vec v) = vec (List.zip u v) ⦃ liftA2 len-zip auto auto ⦄

zip-with : (A β†’ B β†’ C) β†’ Vec A n β†’ Vec B n β†’ Vec C n
zip-with f (vec u) (vec v) = vec (List.zip-with f u v)
  ⦃ liftA2 len-zip-with auto auto ⦄

replicate : (n : Nat) β†’ A β†’ Vec A n
replicate zero a = []v
replicate (suc n) a = a ∷v replicate n a

_ : Path (Vec Nat 3) [ 1 , 2 , 3 ] (1 ∷v 2 ∷v 3 ∷v []v)
_ = refl