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

module Properties where

open import NeilPrelude
open import RealTime
open import Logic
open import Utilities
open import TimeDeltaList
open import SigVecs

import TemporalFunction
open TemporalFunction Time _<ℜ₀_ <ℜ₀-irreflexive <ℜ₀-trans public

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

-- Side Conditions of Change Prefixes

-- We expect all signals to be Stable and Contained

Stable : {A : Set} → ChangePrefix A → Set
Stable cp = {t₁ t₂ : Time} → t₁ ≤ t₂ → (cp t₁ ≡ takeIncl t₁ (cp t₂))

Contained : {A : Set} → ChangePrefix A → Set
Contained cp = {t : Time} → (lastChangeTime (cp t) ≤ t)

Stability : Set
Stability = {A : Set} → (cp : ChangePrefix A) → Stable cp

Containment : Set
Containment = {A : Set} → (cp : ChangePrefix A) → Contained cp

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

-- Change Properties

UnchangingCP : {A : Set} → ChangePrefix A → TimePred
UnchangingCP cp t = IsNothing (lookupCP cp t)

UnchangingC : {A : Set} → SigVec (C A) → TimePred
UnchangingC s t = ((EqualAt s t) Since (EqualAt s t)) t

UnchangingE : {A : Set} → SigVec (E A) → TimePred
UnchangingE (ma , _)   O  =  IsNothing ma
UnchangingE (_  , cp)  t  =  UnchangingCP cp t

UnchangingS : {A : Set} → SigVec (S A) → TimePred
UnchangingS _         O   =  False
UnchangingS (_ , cp)  t   =  UnchangingCP cp t

Unchanging : {as : SVDesc} → SigVec as → TimePred
Unchanging {C _} s = UnchangingC s
Unchanging {S _} s = UnchangingS s
Unchanging {E _} s = UnchangingE s
Unchanging {as , bs} (s₁ , s₂) = Unchanging {as} s₁ ∧ Unchanging {bs} s₂

Changing : {as : SVDesc} → SigVec as → TimePred
Changing {as} s =  ¬ (Unchanging {as} s)

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

Changeless : {as : SVDesc} → SigVec as → TimePred
Changeless {as} s = G (Unchanging {as} s)

Changelessʳ : {as : SVDesc} → SigVec as → TimePred
Changelessʳ {as} s = Gʳ (Unchanging {as} s)

EqSample : {as : SVDesc} → SigVec as → SigVec as → TimePred
EqSample {as} s₁ s₂ t = at {as} s₁ t ≡ at {as} s₂ t

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

-- We expect all signal functions to be causal

Causal : {as bs : SVDesc} → SF as bs → Set
Causal {as} {bs} sf = (s1 s2 : SigVec as) → Always (Hʳ (EqSample {as} s1 s2) ⇒ EqSample {bs} (sf s1) (sf s2))

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

Stateless : {as bs : SVDesc} → SF as bs → Set
Stateless {as} {bs} sf = (s1 s2 : SigVec as) → Always (EqSample {as} s1 s2 ⇒ EqSample {bs} (sf s1) (sf s2))

Decoupled : {as bs : SVDesc} → SF as bs → Set
Decoupled {as} {bs} sf = (s1 s2 : SigVec as) → Always (H (EqSample {as} s1 s2) ⇒ EqSample {bs} (sf s1) (sf s2))

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

Source : {as bs : SVDesc} → SF as bs → TimePred
Source {as} {bs} sf t = (s1 s2 : SigVec as) → (H (EqSample {as} s1 s2) ⇒ Gʳ (EqSample {bs} (sf s1) (sf s2))) t

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

ChangelessSF : {as bs : SVDesc} → SF as bs → TimePred
ChangelessSF {as} {bs} sf t = (s : SigVec as) → Changeless {bs} (sf s) t

ChangelessSFʳ : {as bs : SVDesc} → SF as bs → TimePred
ChangelessSFʳ {as} {bs} sf t = (s : SigVec as) → Changelessʳ {bs} (sf s) t

ChangePrp : {as bs : SVDesc} → SF as bs → TimePred
ChangePrp {as} {bs} sf t = (s : SigVec as) → Gʳ (Unchanging {as} s ⇒ Unchanging {bs} (sf s)) t

ChangeDep : {as bs : SVDesc} → SF as bs → TimePred
ChangeDep {as} {bs} sf t = (s : SigVec as) → (Unchanging {bs} (sf s) Wʳ Changing {as} s) t

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