module Data.DifferenceList where
open import Data.List as L using (List)
open import Function
open import Data.Nat
infixr 5 _∷_ _++_
DiffList : ∀ {ℓ} → Set ℓ → Set ℓ
DiffList A = List A → List A
lift : ∀ {a} {A : Set a} →
(List A → List A) → (DiffList A → DiffList A)
lift f xs = λ k → f (xs k)
[] : ∀ {a} {A : Set a} → DiffList A
[] = λ k → k
_∷_ : ∀ {a} {A : Set a} → A → DiffList A → DiffList A
_∷_ x = lift (L._∷_ x)
[_] : ∀ {a} {A : Set a} → A → DiffList A
[ x ] = x ∷ []
_++_ : ∀ {a} {A : Set a} → DiffList A → DiffList A → DiffList A
xs ++ ys = λ k → xs (ys k)
toList : ∀ {a} {A : Set a} → DiffList A → List A
toList xs = xs L.[]
fromList : ∀ {a} {A : Set a} → List A → DiffList A
fromList xs = λ k → xs ⟨ L._++_ ⟩ k
map : ∀ {a b} {A : Set a} {B : Set b} →
(A → B) → DiffList A → DiffList B
map f xs = λ k → L.map f (toList xs) ⟨ L._++_ ⟩ k
concat : ∀ {a} {A : Set a} → DiffList (DiffList A) → DiffList A
concat xs = concat' (toList xs)
where
concat' : ∀ {a} {A : Set a} → List (DiffList A) → DiffList A
concat' = L.foldr _++_ []
take : ∀ {a} {A : Set a} → ℕ → DiffList A → DiffList A
take n = lift (L.take n)
drop : ∀ {a} {A : Set a} → ℕ → DiffList A → DiffList A
drop n = lift (L.drop n)