open import Arith::Fin
open import Data::List hiding (++, ++-assoc, !!)
open import Paths

open data Vec (A : Type) (n : Nat) : Type
| A, 0 ⇒ vnil
| A, suc m ⇒ infixr :> A (Vec A m)
  tighter =

variable A B : Type
variable n m o : Nat

def vmap (f : A → B) (xs : Vec A n) : Vec B n
| f, vnil ⇒ vnil
| f, x :> xs ⇒ f x :> vmap f xs

overlap def infix ++ (xs : Vec A n) (ys : Vec A m) : Vec A (n + m)
| vnil, ys ⇒ ys
| xs, vnil ⇒ xs
| x :> xs, ys ⇒ x :> (xs ++ ys)
tighter =

overlap def ++-assoc (xs : Vec A n) (ys : Vec A m) (zs : Vec A o)
  : Path (\i ⇒ Vec A (+-assoc i)) ((xs ++ ys) ++ zs) (xs ++ (ys ++ zs))
| vnil, ys, zs ⇒ idp
| xs, vnil, zs ⇒ idp
| xs, ys, vnil ⇒ idp
// TODO: Debug the following
// | x :> xs, ys, zs => pmapd (\i => x :>) (++-assoc xs ys zs)
| x :> xs, ys, zs ⇒ \i ⇒ x :> (++-assoc xs ys zs i)

def infix !! (l : Vec A n) (i : Fin n) : A
| a :> l, fzero ⇒ a
| a :> l, fsuc i ⇒ l !! i

def fold (f : Fn B A → B) (init : B) (xs : Vec A n) : B
| f, init, vnil ⇒ init
| f, acc, x :> xs ⇒ fold f (f acc x) xs

def last (Vec A (suc n)) : A
| x :> vnil ⇒ x
// | _ :> xs => last xs
// ^ The purpose of #243 is to make this work
| _ :> (x :> xs) ⇒ last (x :> xs)

def head (Vec A (suc n)) : A
| x :> _ ⇒ x

def tail (Vec A (suc n)) : Vec A n
| _ :> xs ⇒ xs

def toList (Vec A n) : List A
| a :> xs ⇒ a :< toList xs
| vnil ⇒ nil

def fromList (l : List A) : Vec A (length l)
| a :< l ⇒ a :> fromList l
| nil ⇒ vnil