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

module SigVecs where

open import NeilPrelude
open import RealTime
open import TimeDeltaList

import SVDesc
open SVDesc 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 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

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