module Data.DifferenceVec where
open import Data.DifferenceNat
open import Data.Vec as V using (Vec)
open import Function
import Data.Nat as N
infixr 5 _∷_ _++_
DiffVec : Set → Diffℕ → Set
DiffVec A m = ∀ {n} → Vec A n → Vec A (m n)
[] : ∀ {A} → DiffVec A 0#
[] = λ k → k
_∷_ : ∀ {A n} → A → DiffVec A n → DiffVec A (suc n)
x ∷ xs = λ k → V._∷_ x (xs k)
[_] : ∀ {A} → A → DiffVec A 1#
[ x ] = x ∷ []
_++_ : ∀ {A m n} → DiffVec A m → DiffVec A n → DiffVec A (m + n)
xs ++ ys = λ k → xs (ys k)
toVec : ∀ {A n} → DiffVec A n → Vec A (toℕ n)
toVec xs = xs V.[]
fromVec : ∀ {A n} → Vec A n → DiffVec A (fromℕ n)
fromVec xs = λ k → xs ⟨ V._++_ ⟩ k
head : ∀ {A n} → DiffVec A (suc n) → A
head xs = V.head (toVec xs)
tail : ∀ {A n} → DiffVec A (suc n) → DiffVec A n
tail xs = λ k → V.tail (xs k)
take : ∀ {a} m {n} → DiffVec a (fromℕ m + n) → DiffVec a (fromℕ m)
take N.zero xs = []
take (N.suc m) xs = head xs ∷ take m (tail xs)
drop : ∀ {a} m {n} → DiffVec a (fromℕ m + n) → DiffVec a n
drop N.zero xs = xs
drop (N.suc m) xs = drop m (tail xs)