{-# 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)

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