------------------------------------------------------------------------
-- The Agda standard library
--
-- Vectors with fast append
------------------------------------------------------------------------

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} {A : Set a}  DiffVec A 0#
[] = λ k  k

_∷_ :  {a} {A : Set a} {n}  A  DiffVec A n  DiffVec A (suc n)
x  xs = λ k  V._∷_ x (xs k)

[_] :  {a} {A : Set a}  A  DiffVec A 1#
[ x ] = x  []

_++_ :  {a} {A : Set a} {m n} 
       DiffVec A m  DiffVec A n  DiffVec A (m + n)
xs ++ ys = λ k  xs (ys k)

toVec :  {a} {A : Set a} {n}  DiffVec A n  Vec A (toℕ n)
toVec xs = xs V.[]

-- fromVec xs is linear in the length of xs.

fromVec :  {a} {A : Set a} {n}  Vec A n  DiffVec A (fromℕ n)
fromVec xs = λ k  xs  V._++_  k

head :  {a} {A : Set a} {n}  DiffVec A (suc n)  A
head xs = V.head (toVec xs)

tail :  {a} {A : Set a} {n}  DiffVec A (suc n)  DiffVec A n
tail xs = λ k  V.tail (xs k)

take :  {a} {A : Set 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} {A : Set 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)