------------------------------------------------------------------------
-- The Agda standard library
--
-- Vectors defined as functions from a finite set to a type.
------------------------------------------------------------------------

-- This implementation is designed for reasoning about fixed-size
-- vectors where ease of retrieval of elements is prioritised.

-- See `Data.Vec` for an alternative implementation using inductive
-- data-types, which is more suitable for reasoning about vectors that
-- will grow or shrink in size.

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Vec.Functional where

open import Data.Fin.Base
open import Data.List.Base as L using (List)
open import Data.Nat.Base as  using (; zero; suc; NonZero; pred)
open import Data.Product.Base using (Σ; ; _×_; _,_; proj₁; proj₂; uncurry)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
open import Data.Vec.Base as V using (Vec)
open import Function.Base using (_∘_; const; flip; _ˢ_; id)
open import Level using (Level)

infixr 5 _∷_ _++_
infixl 4 _⊛_
infixl 1 _>>=_

private
  variable
    a b c : Level
    A B C : Set a
    m n : 

------------------------------------------------------------------------
-- Definition

Vector : Set a    Set a
Vector A n = Fin n  A

------------------------------------------------------------------------
-- Conversion

toVec : Vector A n  Vec A n
toVec = V.tabulate

fromVec : Vec A n  Vector A n
fromVec = V.lookup

toList : Vector A n  List A
toList = L.tabulate

fromList :  (xs : List A)  Vector A (L.length xs)
fromList = L.lookup

------------------------------------------------------------------------
-- Basic operations

[] : Vector A zero
[] ()

_∷_ : A  Vector A n  Vector A (suc n)
(x  xs) zero    = x
(x  xs) (suc i) = xs i

length : Vector A n  
length {n = n} _ = n

head : Vector A (suc n)  A
head xs = xs zero

tail : Vector A (suc n)  Vector A n
tail xs = xs  suc

uncons : Vector A (suc n)  A × Vector A n
uncons xs = head xs , tail xs

replicate : (n : )  A  Vector A n
replicate n = const

insertAt : Vector A n  Fin (suc n)  A  Vector A (suc n)
insertAt {n = n}     xs zero    v zero    = v
insertAt {n = n}     xs zero    v (suc j) = xs j
insertAt {n = suc n} xs (suc i) v zero    = head xs
insertAt {n = suc n} xs (suc i) v (suc j) = insertAt (tail xs) i v j

removeAt : Vector A (suc n)  Fin (suc n)  Vector A n
removeAt t i = t  punchIn i

updateAt : Vector A n  Fin n  (A  A)  Vector A n
updateAt {n = suc n} xs zero    f zero    = f (head xs)
updateAt {n = suc n} xs zero    f (suc j) = xs (suc j)
updateAt {n = suc n} xs (suc i) f zero    = head xs
updateAt {n = suc n} xs (suc i) f (suc j) = updateAt (tail xs) i f j

------------------------------------------------------------------------
-- Transformations

map : (A  B)   {n}  Vector A n  Vector B n
map f xs = f  xs

_++_ : Vector A m  Vector A n  Vector A (m ℕ.+ n)
_++_ {m = m} xs ys i = [ xs , ys ] (splitAt m i)

concat : Vector (Vector A m) n  Vector A (n ℕ.* m)
concat {m = m} xss i = uncurry (flip xss) (quotRem m i)

foldr : (A  B  B)  B   {n}  Vector A n  B
foldr f z {n = zero}  xs = z
foldr f z {n = suc n} xs = f (head xs) (foldr f z (tail xs))

foldl : (B  A  B)  B   {n}  Vector A n  B
foldl f z {n = zero}  xs = z
foldl f z {n = suc n} xs = foldl f (f z (head xs)) (tail xs)

rearrange : (Fin m  Fin n)  Vector A n  Vector A m
rearrange r xs = xs  r

_⊛_ : Vector (A  B) n  Vector A n  Vector B n
_⊛_ = _ˢ_

_>>=_ : Vector A m  (A  Vector B n)  Vector B (m ℕ.* n)
xs >>= f = concat (map f xs)

zipWith : (A  B  C)   {n}  Vector A n  Vector B n  Vector C n
zipWith f xs ys i = f (xs i) (ys i)

unzipWith : (A  B × C)  Vector A n  Vector B n × Vector C n
unzipWith f xs = proj₁  f  xs , proj₂  f  xs

zip : Vector A n  Vector B n  Vector (A × B) n
zip = zipWith _,_

unzip : Vector (A × B) n  Vector A n × Vector B n
unzip = unzipWith id

take :  m {n}  Vector A (m ℕ.+ n)  Vector A m
take _ {n = n} xs = xs  (_↑ˡ n)

drop :  m {n}  Vector A (m ℕ.+ n)  Vector A n
drop m xs = xs  (m ↑ʳ_)

reverse : Vector A n  Vector A n
reverse xs = xs  opposite

init : Vector A (suc n)  Vector A n
init xs = xs  inject₁

last : Vector A (suc n)  A
last {n = n} xs = xs (fromℕ n)

transpose : Vector (Vector A n) m  Vector (Vector A m) n
transpose = flip

------------------------------------------------------------------------
-- DEPRECATED
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 2.0

remove : Fin (suc n)  Vector A (suc n)  Vector A n
remove = flip removeAt
{-# WARNING_ON_USAGE remove
"Warning: remove was deprecated in v2.0.
Please use removeAt instead.
NOTE: argument order has been flipped."
#-}
insert = insertAt
{-# WARNING_ON_USAGE insert
"Warning: insert was deprecated in v2.0.
Please use insertAt instead."
#-}