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

module SigVecsI where

open import NeilPrelude
open import RealTime
open import TimeDeltaList

open import InitDesc public

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

-- The change prefixes are inclusive of the time argument
-- (i.e. any changes at that point in time will appear in the list)

ChangeList = TimeDeltaList

ChangePrefix : Set  Set
ChangePrefix A = Time  ChangeList A

SigVec : SVDesc  Set
SigVec (C ini A)  =  Time  A
SigVec (C uni A)  =  Time⁺  A
SigVec (E A)      =  Maybe A × ChangePrefix A
SigVec (S A)      =  A × ChangePrefix A
SigVec (as , bs)  =  SigVec as × SigVec bs

SF : SVDesc  SVDesc  Set
SF as bs = SigVec as  SigVec bs

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

weakenC : {A : Set}  {i₁ i₂ : Init}  i₁ ⟨: i₂  SigVec (C i₁ A)  SigVec (C i₂ A)
weakenC {A} {ini} {ini} p s = s
weakenC {A} {ini} {uni} p s = λ t  s (t >0)
weakenC {A} {uni} {ini} () s
weakenC {A} {uni} {uni} p s = s

weakenSV : {as bs : SVDesc}  as <: bs  SigVec as  SigVec bs
weakenSV {C i₁ A} {C i₂ .A} (p , refl) = weakenC p
weakenSV {E A} {E .A} refl = id
weakenSV {S A} {S .A} refl = id
weakenSV {as₁ , bs₁} {as₂ , bs₂} (p , q) = weakenSV {as₁} {as₂} p  weakenSV {bs₁} {bs₂} q
weakenSV {C _ _} {E _} ()
weakenSV {C _ _} {S _} ()
weakenSV {C _ _} {_ , _} ()
weakenSV {E _ } {C _ _} ()
weakenSV {E _ } {S _} ()
weakenSV {E _} {_ , _} ()
weakenSV {S _} {C _ _} ()
weakenSV {S _} {E _} ()
weakenSV {S _} {_ , _} ()
weakenSV {_ , _} {C _ _} ()
weakenSV {_ , _} {E _} ()
weakenSV {_ , _} {S _} ()

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