{-# OPTIONS --type-in-type --no-termination-check
   #-}

module Utilities where

open import NeilPrelude
open import Maybe
open import List
open import RealTime
open import SigVecs
open import TimeDeltaList
open import TimeDeltaListProps
open import StrictTotalOrder

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

lastChangeTime : {A : Set}  ChangeList A  Time
lastChangeTime = sumTDL

lookupCP : {A : Set}  ChangePrefix A  Time  Maybe A
lookupCP cp t = lookupTDL (cp t) t

valS : {A : Set}  SigVec (S A)  Time  A
valS (a₀ , cp) t with reverse (cp t)
... | []             = a₀
... | (_ , a₁)  _   = a₁

occ : {A : Set}  SigVec (E A)  Time  Maybe A 
occ (ma , _)  O  = ma
occ (ma , cp) t  = lookupCP cp t

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

mapCL : {A B : Set}  (A  B)  ChangeList A  ChangeList B
mapCL = mapTDL

mapCP : {A B : Set}  (A  B)  ChangePrefix A  ChangePrefix B
mapCP = result  mapCL

mapCLtime : {A B : Set}  (Time  A  B)  ChangeList A  ChangeList B
mapCLtime f = mapTDLtime f O

mapCPtime : {A B : Set}  (Time  A  B)  ChangePrefix A  ChangePrefix B
mapCPtime f = result (mapTDLtime f O) -- result ∘ mapCLtime

mapC : {A B : Set}  (A  B)  SigVec (C A)  SigVec (C B)
mapC =  result

mapE : {A B : Set}  (A  B)  SigVec (E A)  SigVec (E B)
mapE f (ma , cp) = maybeMap f ma , mapCP f cp

mapS : {A B : Set}  (A  B)  SigVec (S A)  SigVec (S B)
mapS f (a , cp) = f a , mapCP f cp

mapC2 : {A B Z : Set}  (A  B  Z)  SigVec (C A)  SigVec (C B)  SigVec (C Z)
mapC2 f s1 s2 t = f (s1 t) (s2 t)

mapS2 : {A B Z : Set}  (A  B  Z)  SigVec (S A)  SigVec (S B)  SigVec (S Z)
mapS2 {A} {B} {Z} f (a , cpa) (b , cpb) = f a b , λ t  mergeS a b (cpa t) (cpb t) 
  where
        mergeS : A  B  ChangeList A  ChangeList B  ChangeList Z
        mergeS a₀ b₀ [] δbs = mapCL (f a₀) δbs
        mergeS a₀ b₀ δas [] = mapCL (flip f b₀) δas
        mergeS a₀ b₀ ((δ₁  , a₁)  δas) ((δ₂ , b₁)  δbs) with compareℜ⁺ δ₁ δ₂
        mergeS a₀ b₀ ((.δ₂ , a₁)  δas) ((δ₂ , b₁)  δbs) | refl   = (δ₂ , f a₁ b₁)  mergeS a₁ b₁ δas δbs
        mergeS a₀ b₀ ((δ₁  , a₁)  δas) ((δ₂ , b₁)  δbs) | less p = (δ₁ , f a₁ b₀)  mergeS a₁ b₀ δas (((δ₂ ⁺-⁺ δ₁) p , b₁)  δbs)
        mergeS a₀ b₀ ((δ₁  , a₁)  δas) ((δ₂ , b₁)  δbs) | more p = (δ₂ , f a₀ b₁)  mergeS a₀ b₁ (((δ₁ ⁺-⁺ δ₂) p , a₁)  δas) δbs

mergeE2 : {A B Z : Set}  (A  Z)  (B  Z)  (A  B  Z)  SigVec (E A)  SigVec (E B)  SigVec (E Z)
mergeE2 {A} {B} {Z} fa fb fab (ma , cpa) (mb , cpb) = (maybeMerge fa fb fab ma mb , λ t  mergeCL (cpa t) (cpb t))
  where
        mergeCL : ChangeList A  ChangeList B  ChangeList Z
        mergeCL [] δbs = mapCL fb δbs
        mergeCL δas [] = mapCL fa δas
        mergeCL ((δ₁  , a)  δas) ((δ₂ , b)  δbs) with compareℜ⁺ δ₁ δ₂
        mergeCL ((.δ₂ , a)  δas) ((δ₂ , b)  δbs) | refl   = (δ₂ , fab a b)  mergeCL δas δbs
        mergeCL ((δ₁  , a)  δas) ((δ₂ , b)  δbs) | less p = (δ₁ , fa a)  mergeCL δas (((δ₂ ⁺-⁺ δ₁) p , b)  δbs)
        mergeCL ((δ₁  , a)  δas) ((δ₂ , b)  δbs) | more p = (δ₂ , fb b)  mergeCL (((δ₁ ⁺-⁺ δ₂) p , a)  δas) δbs

joinE2 : {A B Z : Set}  (A  B  Z)  SigVec (E A)  SigVec (E B)  SigVec (E Z)
joinE2 {A} {B} {Z} f (ma , cpa) (mb , cpb) = (maybeMap2 f ma mb , λ t  joinCL O (cpa t) (cpb t))
  where
        joinCL : Time  ChangeList A  ChangeList B  ChangeList Z
        joinCL _ [] _  = []
        joinCL _ _  [] = []
        joinCL d ((δ₁ , a)  δas) ((δ₂ , b)  δbs) with compareℜ⁺ δ₁ δ₂
        joinCL d ((.δ₂ , a)  δas) ((δ₂ , b)  δbs) | refl   = (d ₀+⁺ δ₂ , f a b)  joinCL O δas δbs
        joinCL d ((δ₁ , a)  δas)  ((δ₂ , b)  δbs) | less p = joinCL ((d ₀+⁺ δ₁) >0) δas (((δ₂ ⁺-⁺ δ₁) p , b)  δbs)
        joinCL d ((δ₁ , a)  δas)  ((δ₂ , b)  δbs) | more p = joinCL ((d ₀+⁺ δ₂) >0) (((δ₁ ⁺-⁺ δ₂) p , a)  δas) δbs

mapCE : {A B Z : Set}  (A  B  Z)  SigVec (C A)  SigVec (E B)  SigVec (E Z)
mapCE f s (mb , cp) = (maybeMap (f (s O)) mb , mapCPtime (f  s) cp)

mapSE : {A B Z : Set}  (A  B  Z)  SigVec (S A)  SigVec (E B)  SigVec (E Z)
mapSE f s (mb , cp) = (maybeMap (f (valS s O)) mb , mapCPtime (f  valS s) cp)


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

-- When we delay a change prefix we may have an initial value to include

delayCP : {A : Set}  Time⁺  Maybe A  ChangePrefix A  ChangePrefix A
delayCP d ma cp t with compareGeqℜ₀ t (d >0)
delayCP d ma cp t       | less p = []
delayCP d nothing  cp t | geq  p = delayTDL⁺ d (cp (ℜ₀⁺₀-minus t d p))
delayCP d (just a) cp t | geq  p = (d , a)     cp (ℜ₀⁺₀-minus t d p)

advanceCP : {A : Set}  Time  ChangePrefix A  ChangePrefix A
advanceCP d cp t = advanceTDL d (cp (t ₀+₀ d))

advance : {as : SVDesc}  Time  SigVec as  SigVec as
advance {C _}     d s = λ t  s (t ₀+₀ d)
advance {S _}     d s = valS s d , advanceCP d (snd s)
advance {E _}     d s = occ  s d , advanceCP d (snd s)
advance {as , bs} d (s₁ , s₂) = advance {as} d s₁ , advance {bs} d s₂


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

-- takeExclEnd ignores a change at the sample time, and also returns the remaining time after the last change (which thus has to be positive) 

lem-sumCLexcl : {A : Set}  (t : Time⁺)  (cp : ChangePrefix A)  sumTDL (takeExcl⁺ t (cp (t >0))) <ℜ₀ (t >0)
lem-sumCLexcl t cp = lemTDL-sumExclLess t (cp (t >0))

takeExclEnd : {A : Set}  ChangePrefix A  Time⁺  ChangeList A × Δt
takeExclEnd cp t =  let δas = takeExcl⁺ t (cp (t >0))
                    in δas , ℜ⁺₀⁺-minus t (lastChangeTime δas) (lem-sumCLexcl t cp)


-- firstOcc returns the first occurrence upto the specified time.  If the first occurrence is after this time it will return nothing

fstOcc : {A : Set}  SigVec (E A)  Time  Maybe (Time × A)
fstOcc (just a  , _) _ = just (O , a)
fstOcc (nothing , cp) t with cp t
... | []          = nothing
... | (δ , a)  _ = just (δ >0 , a)


private
         -- We rely on the sample time being at least the event time 
         postulate ≤-trustme : {te : EventTime⁺}  {t : SampleTime}  (te >0) ≤ℜ₀ t

         _-_ : (t : SampleTime)  (te : EventTime⁺)  Time
         t - te = ℜ₀⁺₀-minus t te ≤-trustme


spliceC : {A : Set}  SigVec (C A)  SigVec (C A)  EventTime⁺  SigVec (C A)
spliceC _ s₂ te t = s₂ (t - te)

spliceS : {A : Set}  SigVec (S A)  SigVec (S A)  EventTime⁺  SigVec (S A)
spliceS (a₁ , cp₁) (a₂ , cp₂) te with takeExclEnd cp₁ te
... | δas₁ , δ = (a₁ , λ t  δas₁ ++ (δ , a₂)  cp₂ (t - te))

spliceE : {A : Set}  SigVec (E A)  SigVec (E A)  EventTime⁺  SigVec (E A)
spliceE (ma₁ , cp₁) (ma₂ , cp₂) te with takeExclEnd cp₁ te
... | δas₁ , δ = (ma₁ , λ t   let δas₂ = cp₂ (t - te)
                                in δas₁ ++ maybe (delayTDL⁺ δ δas₂)  a₂  (δ , a₂)  δas₂) ma₂)

splice⁺ : {as : SVDesc}  SigVec as  SigVec as  EventTime⁺  SigVec as
splice⁺ {C _}      s₁           s₂           te  = spliceC s₁ s₂ te
splice⁺ {S _}      s₁           s₂           te  = spliceS s₁ s₂ te
splice⁺ {E _}      s₁           s₂           te  = spliceE s₁ s₂ te
splice⁺ {as , bs}  (sa₁ , sb₁)  (sa₂ , sb₂)  te  = splice⁺ {as} sa₁ sa₂ te , splice⁺ {bs} sb₁ sb₂ te

splice : {as : SVDesc}  SigVec as  SigVec as  EventTime  SigVec as
splice {as} s₁ s₂ O       = s₂
splice {as} s₁ s₂ (te >0) = splice⁺ {as} s₁ s₂ te

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

svAtTime : {as : SVDesc}  (SampleTime  SigVec as)  SigVec as
svAtTime {C _}     f = λ t  f t t
svAtTime {E _}     f = fst (f O) , λ t  snd (f t) t
svAtTime {S _}     f = fst (f O) , λ t  snd (f t) t
svAtTime {as , bs} f = (svAtTime {as} (fst  f) , svAtTime {bs} (snd  f))

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

at : {as : SVDesc}  SigVec as  Time  Sample as
at {C _}     s          t  =  s t
at {S _}     s          t  =  valS s t
at {E _}     s          t  =  occ s t
at {as , bs} (sa , sb)  t  =  (at {as} sa t , at {bs} sb t)

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