{-# 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 : ℕ
Vector : Set a → ℕ → Set a
Vector A n = Fin n → A
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
[] : 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
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
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."
#-}