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

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

module Data.DifferenceVec where

open import Data.DifferenceNat
open import Data.Vec.Base as Vec using (Vec)
open import Function.Base using (_⟨_⟩_)
import Data.Nat.Base as 

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  Vec._∷_ 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 Vec.[]

-- 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  Vec._++_  k

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

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

take :  {a} {A : Set a} m {n} 
       DiffVec A (fromℕ m + n)  DiffVec A (fromℕ m)
take ℕ.zero    xs = []
take (ℕ.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 ℕ.zero    xs = xs
drop (ℕ.suc m) xs = drop m (tail xs)