{-# LANGUAGE GADTs #-}
module FRP.Yampa.LTLFuture
( TPred(..)
, evalT
)
where
import FRP.Yampa (DTime, SF, evalFuture)
import FRP.Yampa.Stream (SignalSampleStream, evalSF, firstSample)
data TPred a where
SP :: SF a Bool -> TPred a
And :: TPred a -> TPred a -> TPred a
Or :: TPred a -> TPred a -> TPred a
Not :: TPred a -> TPred a
Implies :: TPred a -> TPred a -> TPred a
Always :: TPred a -> TPred a
Eventually :: TPred a -> TPred a
Next :: TPred a -> TPred a
Until :: TPred a -> TPred a -> TPred a
evalT :: TPred a -> SignalSampleStream a -> Bool
evalT :: forall a. TPred a -> SignalSampleStream a -> Bool
evalT (SP SF a Bool
sf) = \SignalSampleStream a
stream -> forall a. SignalSampleStream a -> a
firstSample forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall a b.
SF a b
-> SignalSampleStream a -> (SignalSampleStream b, FutureSF a b)
evalSF SF a Bool
sf SignalSampleStream a
stream
evalT (And TPred a
t1 TPred a
t2) = \SignalSampleStream a
stream -> forall a. TPred a -> SignalSampleStream a -> Bool
evalT TPred a
t1 SignalSampleStream a
stream Bool -> Bool -> Bool
&& forall a. TPred a -> SignalSampleStream a -> Bool
evalT TPred a
t2 SignalSampleStream a
stream
evalT (Or TPred a
t1 TPred a
t2) = \SignalSampleStream a
stream -> forall a. TPred a -> SignalSampleStream a -> Bool
evalT TPred a
t1 SignalSampleStream a
stream Bool -> Bool -> Bool
|| forall a. TPred a -> SignalSampleStream a -> Bool
evalT TPred a
t2 SignalSampleStream a
stream
evalT (Not TPred a
t1) = \SignalSampleStream a
stream -> Bool -> Bool
not (forall a. TPred a -> SignalSampleStream a -> Bool
evalT TPred a
t1 SignalSampleStream a
stream)
evalT (Implies TPred a
t1 TPred a
t2) = \SignalSampleStream a
stream -> Bool -> Bool
not (forall a. TPred a -> SignalSampleStream a -> Bool
evalT TPred a
t1 SignalSampleStream a
stream) Bool -> Bool -> Bool
|| forall a. TPred a -> SignalSampleStream a -> Bool
evalT TPred a
t2 SignalSampleStream a
stream
evalT (Always TPred a
t1) = \SignalSampleStream a
stream ->
forall a. TPred a -> SignalSampleStream a -> Bool
evalT TPred a
t1 SignalSampleStream a
stream Bool -> Bool -> Bool
&& forall a. TPred a -> SignalSampleStream a -> Bool
evalT (forall a. TPred a -> TPred a
Next (forall a. TPred a -> TPred a
Always TPred a
t1)) SignalSampleStream a
stream
evalT (Eventually TPred a
t1) = \SignalSampleStream a
stream ->
case SignalSampleStream a
stream of
(a
a, []) -> forall a. TPred a -> SignalSampleStream a -> Bool
evalT TPred a
t1 SignalSampleStream a
stream
(a
a1, (DTime
dt, a
a2) : [(DTime, a)]
as) -> forall a. TPred a -> SignalSampleStream a -> Bool
evalT TPred a
t1 SignalSampleStream a
stream
Bool -> Bool -> Bool
|| forall a. TPred a -> SignalSampleStream a -> Bool
evalT (forall a. TPred a -> a -> DTime -> TPred a
tauApp (forall a. TPred a -> TPred a
Eventually TPred a
t1) a
a1 DTime
dt) (a
a2, [(DTime, a)]
as)
evalT (Until TPred a
t1 TPred a
t2) = \SignalSampleStream a
stream ->
(forall a. TPred a -> SignalSampleStream a -> Bool
evalT TPred a
t1 SignalSampleStream a
stream Bool -> Bool -> Bool
&& forall a. TPred a -> SignalSampleStream a -> Bool
evalT (forall a. TPred a -> TPred a
Next (forall a. TPred a -> TPred a -> TPred a
Until TPred a
t1 TPred a
t2)) SignalSampleStream a
stream)
Bool -> Bool -> Bool
|| forall a. TPred a -> SignalSampleStream a -> Bool
evalT TPred a
t2 SignalSampleStream a
stream
evalT (Next TPred a
t1) = \SignalSampleStream a
stream ->
case SignalSampleStream a
stream of
(a
a, []) -> Bool
True
(a
a1, (DTime
dt, a
a2) : [(DTime, a)]
as) -> forall a. TPred a -> SignalSampleStream a -> Bool
evalT (forall a. TPred a -> a -> DTime -> TPred a
tauApp TPred a
t1 a
a1 DTime
dt) (a
a2, [(DTime, a)]
as)
tauApp :: TPred a -> a -> DTime -> TPred a
tauApp :: forall a. TPred a -> a -> DTime -> TPred a
tauApp TPred a
pred a
sample DTime
dtime =
forall a. (SF a Bool -> SF a Bool) -> TPred a -> TPred a
tPredMap (\SF a Bool
sf -> forall a b. (a, b) -> b
snd (forall a b. SF a b -> a -> DTime -> (b, SF a b)
evalFuture SF a Bool
sf a
sample DTime
dtime)) TPred a
pred
tPredMap :: (SF a Bool -> SF a Bool) -> TPred a -> TPred a
tPredMap :: forall a. (SF a Bool -> SF a Bool) -> TPred a -> TPred a
tPredMap SF a Bool -> SF a Bool
f (SP SF a Bool
sf) = forall a. SF a Bool -> TPred a
SP (SF a Bool -> SF a Bool
f SF a Bool
sf)
tPredMap SF a Bool -> SF a Bool
f (And TPred a
t1 TPred a
t2) = forall a. TPred a -> TPred a -> TPred a
And (forall a. (SF a Bool -> SF a Bool) -> TPred a -> TPred a
tPredMap SF a Bool -> SF a Bool
f TPred a
t1) (forall a. (SF a Bool -> SF a Bool) -> TPred a -> TPred a
tPredMap SF a Bool -> SF a Bool
f TPred a
t2)
tPredMap SF a Bool -> SF a Bool
f (Or TPred a
t1 TPred a
t2) = forall a. TPred a -> TPred a -> TPred a
Or (forall a. (SF a Bool -> SF a Bool) -> TPred a -> TPred a
tPredMap SF a Bool -> SF a Bool
f TPred a
t1) (forall a. (SF a Bool -> SF a Bool) -> TPred a -> TPred a
tPredMap SF a Bool -> SF a Bool
f TPred a
t2)
tPredMap SF a Bool -> SF a Bool
f (Not TPred a
t1) = forall a. TPred a -> TPred a
Not (forall a. (SF a Bool -> SF a Bool) -> TPred a -> TPred a
tPredMap SF a Bool -> SF a Bool
f TPred a
t1)
tPredMap SF a Bool -> SF a Bool
f (Implies TPred a
t1 TPred a
t2) = forall a. TPred a -> TPred a -> TPred a
Implies (forall a. (SF a Bool -> SF a Bool) -> TPred a -> TPred a
tPredMap SF a Bool -> SF a Bool
f TPred a
t1) (forall a. (SF a Bool -> SF a Bool) -> TPred a -> TPred a
tPredMap SF a Bool -> SF a Bool
f TPred a
t2)
tPredMap SF a Bool -> SF a Bool
f (Always TPred a
t1) = forall a. TPred a -> TPred a
Always (forall a. (SF a Bool -> SF a Bool) -> TPred a -> TPred a
tPredMap SF a Bool -> SF a Bool
f TPred a
t1)
tPredMap SF a Bool -> SF a Bool
f (Eventually TPred a
t1) = forall a. TPred a -> TPred a
Eventually (forall a. (SF a Bool -> SF a Bool) -> TPred a -> TPred a
tPredMap SF a Bool -> SF a Bool
f TPred a
t1)
tPredMap SF a Bool -> SF a Bool
f (Next TPred a
t1) = forall a. TPred a -> TPred a
Next (forall a. (SF a Bool -> SF a Bool) -> TPred a -> TPred a
tPredMap SF a Bool -> SF a Bool
f TPred a
t1)
tPredMap SF a Bool -> SF a Bool
f (Until TPred a
t1 TPred a
t2) = forall a. TPred a -> TPred a -> TPred a
Until (forall a. (SF a Bool -> SF a Bool) -> TPred a -> TPred a
tPredMap SF a Bool -> SF a Bool
f TPred a
t1) (forall a. (SF a Bool -> SF a Bool) -> TPred a -> TPred a
tPredMap SF a Bool -> SF a Bool
f TPred a
t2)