{-# LANGUAGE GADTs #-}
-- |
-- Copyright  : (c) Ivan Perez, 2017-2022
-- License    : BSD-style (see the LICENSE file in the distribution)
-- Maintainer : ivan.perez@keera.co.uk
--
-- Linear Temporal Logics based on SFs.
--
-- This module contains a definition of LTL with Next on top of Signal
-- Functions.
--
-- LTL predicates are parameterized over an input. A basic proposition is a
-- Signal Function that produces a boolean function.
module FRP.Yampa.LTLFuture
    ( TPred(..)
    , evalT
    )
  where

-- External imports
import FRP.Yampa (DTime, SF, evalFuture)

-- Internal imports
import FRP.Yampa.Stream (SignalSampleStream, evalSF, firstSample)

-- | Type representing future-time linear temporal logic predicates with until
-- and next.
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

-- | Evaluates a temporal predicate at time t=0 with a concrete sample stream.
--
-- Returns 'True' if the temporal proposition is currently true.
evalT :: TPred a -> SignalSampleStream a -> Bool
evalT :: forall a. TPred a -> SignalSampleStream a -> Bool
evalT (SP SF a Bool
sf)         = \SignalSampleStream a
stream -> SignalSampleStream Bool -> Bool
forall a. SignalSampleStream a -> a
firstSample (SignalSampleStream Bool -> Bool)
-> SignalSampleStream Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (SignalSampleStream Bool, FutureSF a Bool)
-> SignalSampleStream Bool
forall a b. (a, b) -> a
fst ((SignalSampleStream Bool, FutureSF a Bool)
 -> SignalSampleStream Bool)
-> (SignalSampleStream Bool, FutureSF a Bool)
-> SignalSampleStream Bool
forall a b. (a -> b) -> a -> b
$ SF a Bool
-> SignalSampleStream a
-> (SignalSampleStream Bool, FutureSF a Bool)
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 -> TPred a -> SignalSampleStream a -> Bool
forall a. TPred a -> SignalSampleStream a -> Bool
evalT TPred a
t1 SignalSampleStream a
stream Bool -> Bool -> Bool
&& TPred a -> SignalSampleStream a -> 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 -> TPred a -> SignalSampleStream a -> Bool
forall a. TPred a -> SignalSampleStream a -> Bool
evalT TPred a
t1 SignalSampleStream a
stream Bool -> Bool -> Bool
|| TPred a -> SignalSampleStream a -> 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 (TPred a -> SignalSampleStream a -> Bool
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 (TPred a -> SignalSampleStream a -> Bool
forall a. TPred a -> SignalSampleStream a -> Bool
evalT TPred a
t1 SignalSampleStream a
stream) Bool -> Bool -> Bool
|| TPred a -> SignalSampleStream a -> Bool
forall a. TPred a -> SignalSampleStream a -> Bool
evalT TPred a
t2 SignalSampleStream a
stream
evalT (Always  TPred a
t1)    = \SignalSampleStream a
stream ->
  TPred a -> SignalSampleStream a -> Bool
forall a. TPred a -> SignalSampleStream a -> Bool
evalT TPred a
t1 SignalSampleStream a
stream Bool -> Bool -> Bool
&& TPred a -> SignalSampleStream a -> Bool
forall a. TPred a -> SignalSampleStream a -> Bool
evalT (TPred a -> TPred a
forall a. TPred a -> TPred a
Next (TPred a -> TPred a
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, [])             -> TPred a -> SignalSampleStream a -> Bool
forall a. TPred a -> SignalSampleStream a -> Bool
evalT TPred a
t1 SignalSampleStream a
stream
    (a
a1, (DTime
dt, a
a2) : [(DTime, a)]
as) -> TPred a -> SignalSampleStream a -> Bool
forall a. TPred a -> SignalSampleStream a -> Bool
evalT TPred a
t1 SignalSampleStream a
stream
                             Bool -> Bool -> Bool
|| TPred a -> SignalSampleStream a -> Bool
forall a. TPred a -> SignalSampleStream a -> Bool
evalT (TPred a -> a -> DTime -> TPred a
forall a. TPred a -> a -> DTime -> TPred a
tauApp (TPred a -> TPred a
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 ->
  (TPred a -> SignalSampleStream a -> Bool
forall a. TPred a -> SignalSampleStream a -> Bool
evalT TPred a
t1 SignalSampleStream a
stream Bool -> Bool -> Bool
&& TPred a -> SignalSampleStream a -> Bool
forall a. TPred a -> SignalSampleStream a -> Bool
evalT (TPred a -> TPred a
forall a. TPred a -> TPred a
Next (TPred a -> TPred a -> TPred a
forall a. TPred a -> TPred a -> TPred a
Until TPred a
t1 TPred a
t2)) SignalSampleStream a
stream)
    Bool -> Bool -> Bool
|| TPred a -> SignalSampleStream a -> 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 -- This is important. It determines how
                                -- always and next behave at the end of the
                                -- stream, which affects that is and isn't a
                                -- tautology. It should be reviewed very
                                -- carefully.
    (a
a1, (DTime
dt, a
a2) : [(DTime, a)]
as) -> TPred a -> SignalSampleStream a -> Bool
forall a. TPred a -> SignalSampleStream a -> Bool
evalT (TPred a -> a -> DTime -> TPred a
forall a. TPred a -> a -> DTime -> TPred a
tauApp TPred a
t1 a
a1 DTime
dt) (a
a2, [(DTime, a)]
as)

-- | Tau-application (transportation to the future)
tauApp :: TPred a -> a -> DTime -> TPred a
tauApp :: forall a. TPred a -> a -> DTime -> TPred a
tauApp TPred a
pred a
sample DTime
dtime =
  (SF a Bool -> SF a Bool) -> TPred a -> TPred a
forall a. (SF a Bool -> SF a Bool) -> TPred a -> TPred a
tPredMap (\SF a Bool
sf -> (Bool, SF a Bool) -> SF a Bool
forall a b. (a, b) -> b
snd (SF a Bool -> a -> DTime -> (Bool, SF a Bool)
forall a b. SF a b -> a -> DTime -> (b, SF a b)
evalFuture SF a Bool
sf a
sample DTime
dtime)) TPred a
pred

-- | Apply a transformation to the leaves (to the SFs)
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)         = SF a Bool -> TPred a
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)     = TPred a -> TPred a -> TPred a
forall a. TPred a -> TPred a -> TPred a
And ((SF a Bool -> SF a Bool) -> TPred a -> TPred a
forall a. (SF a Bool -> SF a Bool) -> TPred a -> TPred a
tPredMap SF a Bool -> SF a Bool
f TPred a
t1) ((SF a Bool -> SF a Bool) -> TPred a -> TPred a
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)      = TPred a -> TPred a -> TPred a
forall a. TPred a -> TPred a -> TPred a
Or ((SF a Bool -> SF a Bool) -> TPred a -> TPred a
forall a. (SF a Bool -> SF a Bool) -> TPred a -> TPred a
tPredMap SF a Bool -> SF a Bool
f TPred a
t1) ((SF a Bool -> SF a Bool) -> TPred a -> TPred a
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)        = TPred a -> TPred a
forall a. TPred a -> TPred a
Not ((SF a Bool -> SF a Bool) -> TPred a -> TPred a
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) = TPred a -> TPred a -> TPred a
forall a. TPred a -> TPred a -> TPred a
Implies ((SF a Bool -> SF a Bool) -> TPred a -> TPred a
forall a. (SF a Bool -> SF a Bool) -> TPred a -> TPred a
tPredMap SF a Bool -> SF a Bool
f TPred a
t1) ((SF a Bool -> SF a Bool) -> TPred a -> TPred a
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)     = TPred a -> TPred a
forall a. TPred a -> TPred a
Always ((SF a Bool -> SF a Bool) -> TPred a -> TPred a
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) = TPred a -> TPred a
forall a. TPred a -> TPred a
Eventually ((SF a Bool -> SF a Bool) -> TPred a -> TPred a
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)       = TPred a -> TPred a
forall a. TPred a -> TPred a
Next ((SF a Bool -> SF a Bool) -> TPred a -> TPred a
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)   = TPred a -> TPred a -> TPred a
forall a. TPred a -> TPred a -> TPred a
Until ((SF a Bool -> SF a Bool) -> TPred a -> TPred a
forall a. (SF a Bool -> SF a Bool) -> TPred a -> TPred a
tPredMap SF a Bool -> SF a Bool
f TPred a
t1) ((SF a Bool -> SF a Bool) -> TPred a -> TPred a
forall a. (SF a Bool -> SF a Bool) -> TPred a -> TPred a
tPredMap SF a Bool -> SF a Bool
f TPred a
t2)