{-# OPTIONS --type-in-type  #-}

open import NeilPrelude
open import List
open import RealTime
open import StrictTotalOrder

module TimeDeltaList where

-----------------------------------------------------

TimeDeltaList : Set → Set
TimeDeltaList A = List (Δt × A)

TDList = TimeDeltaList

-----------------------------------------------------

mapTDL : {A B : Set} → (A → B) → TDList A → TDList B
mapTDL = map ∘ second

mapTDLtime : {A B : Set} → (Time → A → B) → Time → TDList A → TDList B
mapTDLtime f d [] = []
mapTDLtime f d ((δ , a) ∷ δas) = let d' = (d ₀+⁺ δ) >0 in (δ , f d' a) ∷ mapTDLtime f d' δas

-----------------------------------------------------

-- delayTDL increases the first time delta

delayTDL⁺ : {A : Set} → Time⁺ → TDList A → TDList A
delayTDL⁺ d [] = []
delayTDL⁺ d ((δ , a) ∷ δas) = (d ⁺+⁺ δ , a) ∷ δas

delayTDL : {A : Set} → Time → TDList A → TDList A
delayTDL d [] = []
delayTDL d ((δ , a) ∷ δas) = (d ₀+⁺ δ , a) ∷ δas

-- advanceTDL decreases the first time delta (the point of observation advances)
-- any time deltas we reach are discarded

advanceTDL⁺ : {A : Set} → Time⁺ → TDList A → TDList A
advanceTDL⁺ d [] = []
advanceTDL⁺ d ((δ , a) ∷ δas) with compareℜ⁺ δ d
advanceTDL⁺ d ((.d , a) ∷ δas) | refl   = δas
advanceTDL⁺ d ((δ , a)  ∷ δas) | less p = advanceTDL⁺ ((d ⁺-⁺ δ) p) δas
advanceTDL⁺ d ((δ , a)  ∷ δas) | more p = ((δ ⁺-⁺ d) p , a) ∷ δas

advanceTDL : {A : Set} → Time → TDList A → TDList A
advanceTDL d [] = []
advanceTDL d ((δ , a) ∷ δas) with compareLeqℜ₀ (δ >0) d
... | leq  p = advanceTDL (ℜ₀⁺₀-minus d δ p) δas
... | more p = (ℜ⁺₀⁺-minus δ d p , a) ∷ δas

sumTDL : {A : Set} → TDList A → Time
sumTDL = sumℜ⁺ ∘ map fst

lookupTDL⁺ : {A : Set} → TDList A → Time⁺ → Maybe A
lookupTDL⁺ [] t = nothing
lookupTDL⁺ ((δ , a) ∷ δas) t with compareℜ⁺ δ t
lookupTDL⁺ ((δ , a) ∷ δas) .δ | refl   = just a
lookupTDL⁺ ((δ , a) ∷ δas) t  | more p = nothing
lookupTDL⁺ ((δ , a) ∷ δas) t  | less p = lookupTDL⁺ δas ((t ⁺-⁺ δ) p)

lookupTDL : {A : Set} → TDList A → Time → Maybe A
lookupTDL δas O      = nothing
lookupTDL δas (t >0) = lookupTDL⁺ δas t

-- safelookupTDL⁺ : {A : Set} → A → TDList A → Time⁺ → A
-- safelookupTDL⁺ a₀ [] t = a₀
-- safelookupTDL⁺ a₀ ((δ , a₁) ∷ δas) t with compareℜ⁺ δ t
-- safelookupTDL⁺ a₀ ((δ , a₁) ∷ δas) .δ | refl   = a₁
-- safelookupTDL⁺ a₀ ((δ , a₁) ∷ δas) t  | more p = a₀
-- safelookupTDL⁺ a₀ ((δ , a₁) ∷ δas) t  | less p = safelookupTDL⁺ a₁ δas ((t ⁺-⁺ δ) p)

safelookupTDL : {A : Set} → A → TDList A → Time → A
safelookupTDL a₀ [] t = a₀
safelookupTDL a₀ ((δ , a₁) ∷ δas) t with compareLeqℜ₀ (δ >0) t
... | leq p  = safelookupTDL a₁ δas (ℜ₀⁺₀-minus t δ p)
... | more p = a₀

-----------------------------------------------------

-- "takeIncl" takes all changes upto and including the given time, and discards the rest
-- This is one of several places where using an Interval datatype rather than a Time would be neater
-- (as the only difference is whether the interval is closed or open)

takeIncl⁺ : {A : Set} → Time⁺ → TDList A → TDList A
takeIncl⁺ _ [] = []
takeIncl⁺ t  ((δ , a) ∷ δas) with compareℜ⁺ δ t
takeIncl⁺ t  ((δ , a) ∷ δas) | more p = []
takeIncl⁺ .δ ((δ , a) ∷ δas) | refl   = (δ , a) ∷ []
takeIncl⁺ t  ((δ , a) ∷ δas) | less p = (δ , a) ∷ takeIncl⁺ ((t ⁺-⁺ δ) p) δas

takeIncl : {A : Set} → Time → TDList A → TDList A
takeIncl O      δas = []
takeIncl (t >0) δas = takeIncl⁺ t δas 

-- takeIncl : {A : Set} → Time → TDList A → TDList A
-- takeIncl t [] = []
-- takeIncl t ((δ , a) ∷ δas) with compareLeqℜ₀ (δ >0) t
-- takeIncl t ((δ , a) ∷ δas) | leq p  = (δ , a) ∷ takeIncl (ℜ₀⁺₀-minus t δ p) δas
-- takeIncl t ((δ , a) ∷ δas) | more p = []


takeExcl⁺ : {A : Set} → Time⁺ → TDList A → TDList A
takeExcl⁺ _ [] = []
takeExcl⁺ t  ((δ , a) ∷ δas) with compareGeqℜ⁺ δ t
takeExcl⁺ t  ((δ , a) ∷ δas) | geq  p = []
takeExcl⁺ t  ((δ , a) ∷ δas) | less p = (δ , a) ∷ takeExcl⁺ ((t ⁺-⁺ δ) p) δas

takeExcl : {A : Set} → Time → TDList A → TDList A
takeExcl O      δas = []
takeExcl (t >0) δas = takeExcl⁺ t δas 

dropIncl⁺ : {A : Set} → Time⁺ → TDList A → TDList A
dropIncl⁺ _ [] = []
dropIncl⁺ t  ((δ , a) ∷ δas) with compareℜ⁺ δ t
dropIncl⁺ t  ((δ , a) ∷ δas) | more p = (δ , a) ∷ δas
dropIncl⁺ .δ ((δ , a) ∷ δas) | refl   = delayTDL⁺ δ δas
dropIncl⁺ t  ((δ , a) ∷ δas) | less p = delayTDL⁺ δ (dropIncl⁺ ((t ⁺-⁺ δ) p) δas)

dropIncl : {A : Set} → Time → TDList A → TDList A
dropIncl O      δas = δas
dropIncl (t >0) δas = dropIncl⁺ t δas

dropExcl⁺ : {A : Set} → Time⁺ → TDList A → TDList A
dropExcl⁺ _ [] = []
dropExcl⁺ t  ((δ , a) ∷ δas) with compareGeqℜ⁺ δ t
dropExcl⁺ t  ((δ , a) ∷ δas) | geq  p = (δ , a) ∷ δas
dropExcl⁺ t  ((δ , a) ∷ δas) | less p = delayTDL⁺ δ (dropExcl⁺ ((t ⁺-⁺ δ) p) δas)

dropExcl : {A : Set} → Time → TDList A → TDList A
dropExcl O      δas = δas
dropExcl (t >0) δas = dropExcl⁺ t δas