{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
module FRP.Dunai.LTLFuture where
import Control.Monad.Trans.MSF.Reader
import Data.MonadicStreamFunction
import Data.MonadicStreamFunction.InternalCore (unMSF)
import FRP.Dunai.Stream
data TPred m a where
Prop :: MSF m a Bool -> TPred m a
And :: TPred m a -> TPred m a -> TPred m a
Or :: TPred m a -> TPred m a -> TPred m a
Not :: TPred m a -> TPred m a
Implies :: TPred m a -> TPred m a -> TPred m a
Always :: TPred m a -> TPred m a
Eventually :: TPred m a -> TPred m a
Next :: TPred m a -> TPred m a
Until :: TPred m a -> TPred m a -> TPred m a
tPredMap :: Monad m => (MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a)
tPredMap f (Prop sf) = Prop <$> f sf
tPredMap f (And t1 t2) = And <$> (tPredMap f t1) <*> (tPredMap f t2)
tPredMap f (Or t1 t2) = Or <$> (tPredMap f t1) <*> (tPredMap f t2)
tPredMap f (Not t1) = Not <$> (tPredMap f t1)
tPredMap f (Implies t1 t2) = Implies <$> (tPredMap f t1) <*> (tPredMap f t2)
tPredMap f (Always t1) = Always <$> (tPredMap f t1)
tPredMap f (Eventually t1) = Eventually <$> (tPredMap f t1)
tPredMap f (Next t1) = Next <$> (tPredMap f t1)
tPredMap f (Until t1 t2) = Until <$> (tPredMap f t1) <*> (tPredMap f t2)
evalT :: Monad m => TPred (ReaderT DTime m) a -> SignalSampleStream a -> m Bool
evalT (Prop sf) = \stream -> (myHead . fst) <$> evalSF sf stream
evalT (And t1 t2) = \stream -> (&&) <$> (evalT t1 stream) <*> (evalT t2 stream)
evalT (Or t1 t2) = \stream -> (||) <$> (evalT t1 stream) <*> (evalT t2 stream)
evalT (Not t1) = \stream -> not <$> (evalT t1 stream)
evalT (Implies t1 t2) = \stream -> (||) <$> (not <$> (evalT t1 stream)) <*> (evalT t2 stream)
evalT (Always t1) = \stream -> (&&) <$> (evalT t1 stream) <*> (evalT (Next (Always t1)) stream)
evalT (Eventually t1) = \stream -> (||) <$> (evalT t1 stream) <*> (evalT (Next (Eventually t1)) stream)
evalT (Until t1 t2) = \stream -> (||) <$> ((&&) <$> (evalT t1 stream) <*> (evalT (Next (Until t1 t2)) stream)) <*> (evalT t2 stream)
evalT (Next t1) = \stream -> case stream of
([]) -> return False
(a:[]) -> return True
(a1:as) -> tauApp t1 a1 >>= (`evalT` as)
tauApp :: forall m a . Monad m => TPred (ReaderT DTime m) a -> (DTime, a) -> m (TPred (ReaderT DTime m) a)
tauApp pred (dtime, sample) = runReaderT f dtime
where
f :: ReaderT DTime m (TPred (ReaderT DTime m) a)
f = (tPredMap (\s -> snd <$> unMSF s sample) pred)
myHead :: [a] -> a
myHead [] = error "My head: empty list"
myHead (x:_) = x