{-# LANGUAGE Arrows #-}
-- |
-- Copyright  : (c) Ivan Perez, 2017
-- License    : BSD3
-- Maintainer : ivan.perez@keera.co.uk
--
-- Past-time LTL using MSFs.
--
-- This module provides ways of defining past-, discrete-time temporal
-- predicates with MSFs.
--
-- There are two ways of doing so: piping the results of Boolean-carrying MSFs
-- into other MSFs (Past-time LTL using MSFs), or wrapping MSFs into other MSFs
-- (Past-time LTL as MSF combinators).
module FRP.Dunai.LTLPast where

-- External imports
import Control.Monad.Trans.MSF.Maybe (MaybeT, catchMaybe, inMaybeT)
import Data.MonadicStreamFunction    (MSF, arr, feedback, iPre, liftTransS,
                                      returnA, (&&&), (>>>), (^>>))

-- * Past-time linear temporal logic using MSFs.

-- ** Propositional MSFs

-- | Output True when both inputs are True.
andSF :: Monad m => MSF m (Bool, Bool) Bool
andSF :: forall (m :: * -> *). Monad m => MSF m (Bool, Bool) Bool
andSF = forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Bool -> Bool -> Bool
(&&))

-- | Output True when at least one input is True.
orSF :: Monad m => MSF m (Bool, Bool) Bool
orSF :: forall (m :: * -> *). Monad m => MSF m (Bool, Bool) Bool
orSF = forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Bool -> Bool -> Bool
(||))

-- | Output True when the input is False.
notSF :: Monad m => MSF m Bool Bool
notSF :: forall (m :: * -> *). Monad m => MSF m Bool Bool
notSF = forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr Bool -> Bool
not

-- | Output True when the second input is True or the first one is False.
impliesSF :: Monad m => MSF m (Bool, Bool) Bool
impliesSF :: forall (m :: * -> *). Monad m => MSF m (Bool, Bool) Bool
impliesSF = forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr forall a b. (a -> b) -> a -> b
$ \(Bool
i, Bool
p) -> Bool -> Bool
not Bool
i Bool -> Bool -> Bool
|| Bool
p

-- ** Temporal MSFs

-- | Output True when every input up until the current time has been True.
--
-- This corresponds to Historically, or the past-time version of Globally or
-- Always.
sofarSF :: Monad m => MSF m Bool Bool
sofarSF :: forall (m :: * -> *). Monad m => MSF m Bool Bool
sofarSF = forall (m :: * -> *) c a b.
Monad m =>
c -> MSF m (a, c) (b, c) -> MSF m a b
feedback Bool
True forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr forall a b. (a -> b) -> a -> b
$ \(Bool
n, Bool
o) -> let n' :: Bool
n' = Bool
o Bool -> Bool -> Bool
&& Bool
n in (Bool
n', Bool
n')

-- | Output True when at least one input up until the current time has been
-- True.
--
-- This corresponds to Ever, or the past-time version of Eventually.
everSF :: Monad m => MSF m Bool Bool
everSF :: forall (m :: * -> *). Monad m => MSF m Bool Bool
everSF = forall (m :: * -> *) c a b.
Monad m =>
c -> MSF m (a, c) (b, c) -> MSF m a b
feedback Bool
False forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr forall a b. (a -> b) -> a -> b
$ \(Bool
n, Bool
o) -> let n' :: Bool
n' = Bool
o Bool -> Bool -> Bool
|| Bool
n in (Bool
n', Bool
n')

-- | Output True if the first element has always been True, or the second has
-- been True ever since the first one became False.
untilSF :: (Functor m, Monad m) => MSF m (Bool, Bool) Bool
untilSF :: forall (m :: * -> *).
(Functor m, Monad m) =>
MSF m (Bool, Bool) Bool
untilSF =
    forall (m :: * -> *) a b.
(Functor m, Monad m) =>
MSF (MaybeT m) a b -> MSF m a b -> MSF m a b
catchMaybe (forall (m :: * -> *) a b.
Monad m =>
MSF m a (b, Bool) -> MSF (MaybeT m) a b
untilMaybeB (forall (m :: * -> *) c a b.
Monad m =>
c -> MSF m (a, c) (b, c) -> MSF m a b
feedback Bool
True forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr ((Bool, Bool), Bool) -> ((Bool, Bool), Bool)
cond))
               (forall a b. (a, b) -> b
snd forall (a :: * -> * -> *) b c d.
Arrow a =>
(b -> c) -> a c d -> a b d
^>> forall (m :: * -> *). Monad m => MSF m Bool Bool
sofarSF)

  where

    untilMaybeB :: Monad m => MSF m a (b, Bool) -> MSF (MaybeT m) a b
    untilMaybeB :: forall (m :: * -> *) a b.
Monad m =>
MSF m a (b, Bool) -> MSF (MaybeT m) a b
untilMaybeB MSF m a (b, Bool)
msf = proc a
a -> do
      (b
b, Bool
c) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a b.
(MonadTrans t, Monad m, Monad (t m)) =>
MSF m a b -> MSF (t m) a b
liftTransS MSF m a (b, Bool)
msf -< a
a
      forall (m :: * -> *) a. Monad m => MSF (MaybeT m) (Maybe a) a
inMaybeT -< if Bool
c then forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just b
b

    cond :: ((Bool, Bool), Bool) -> ((Bool, Bool), Bool)
cond ((Bool
i, Bool
u), Bool
o) = ((Bool
n, Bool
o Bool -> Bool -> Bool
&& Bool
u), Bool
n)
      where
        n :: Bool
n = Bool
o Bool -> Bool -> Bool
&& Bool
i

-- | Output True if the input was True at the last time.
--
-- False at time zero.
lastSF :: Monad m => MSF m Bool Bool
lastSF :: forall (m :: * -> *). Monad m => MSF m Bool Bool
lastSF = forall (m :: * -> *) a. Monad m => a -> MSF m a a
iPre Bool
False

-- * Past-time linear temporal logic as MSF combinators.

-- | A signal predicate is an MSF whose output is a Boolean value.
type SPred m a = MSF m a Bool

-- ** Propositional MSFs

-- | Output True at times when the input is False.
{-# DEPRECATED notSF' "Use notSF instead" #-}
notSF' :: Monad m => SPred m a -> SPred m a
notSF' :: forall (m :: * -> *) a. Monad m => SPred m a -> SPred m a
notSF' SPred m a
sf = SPred m a
sf forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr Bool -> Bool
not

-- | Output True at times when both inputs are True.
{-# DEPRECATED andSF' "Use andSF instead" #-}
andSF' :: Monad m => SPred m a -> SPred m a -> SPred m a
andSF' :: forall (m :: * -> *) a.
Monad m =>
SPred m a -> SPred m a -> SPred m a
andSF' SPred m a
sf1 SPred m a
sf2 = (SPred m a
sf1 forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& SPred m a
sf2) forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Bool -> Bool -> Bool
(&&))

-- | Output True at times when at least one of the inputs is True.
{-# DEPRECATED orSF' "Use orSF instead" #-}
orSF' :: Monad m => SPred m a -> SPred m a -> SPred m a
orSF' :: forall (m :: * -> *) a.
Monad m =>
SPred m a -> SPred m a -> SPred m a
orSF' SPred m a
sf1 SPred m a
sf2 = (SPred m a
sf1 forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& SPred m a
sf2) forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Bool -> Bool -> Bool
(||))

-- | Output True at times when the first input stream is False or the second
-- one is True.
{-# DEPRECATED implySF' "Use impliesSF instead" #-}
implySF' :: Monad m => SPred m a -> SPred m a -> SPred m a
implySF' :: forall (m :: * -> *) a.
Monad m =>
SPred m a -> SPred m a -> SPred m a
implySF' SPred m a
sf1 SPred m a
sf2 = forall (m :: * -> *) a.
Monad m =>
SPred m a -> SPred m a -> SPred m a
orSF' SPred m a
sf2 (forall (m :: * -> *) a. Monad m => SPred m a -> SPred m a
notSF' SPred m a
sf1)

-- ** Temporal MSFs

-- | Output True at a time if the input has always been True up until that
-- time.
--
-- This corresponds to Historically, or the past-time version of Globally or
-- Always.
{-# DEPRECATED history' "Use sofarSF instead" #-}
history' :: Monad m => SPred m a -> SPred m a
history' :: forall (m :: * -> *) a. Monad m => SPred m a -> SPred m a
history' SPred m a
sf = forall (m :: * -> *) c a b.
Monad m =>
c -> MSF m (a, c) (b, c) -> MSF m a b
feedback Bool
True forall a b. (a -> b) -> a -> b
$ proc (a
a, Bool
last) -> do
  Bool
b <- SPred m a
sf -< a
a
  let cur :: Bool
cur = Bool
last Bool -> Bool -> Bool
&& Bool
b
  forall (a :: * -> * -> *) b. Arrow a => a b b
returnA -< (Bool
cur, Bool
cur)

-- | Output True at a time if the input has ever been True up until that time.
--
-- This corresponds to Ever, or the past-time version of Eventually.
{-# DEPRECATED ever' "Use everSF instead" #-}
ever' :: Monad m => SPred m a -> SPred m a
ever' :: forall (m :: * -> *) a. Monad m => SPred m a -> SPred m a
ever' SPred m a
sf = forall (m :: * -> *) c a b.
Monad m =>
c -> MSF m (a, c) (b, c) -> MSF m a b
feedback Bool
False forall a b. (a -> b) -> a -> b
$ proc (a
a, Bool
last) -> do
  Bool
b <- SPred m a
sf -< a
a
  let cur :: Bool
cur = Bool
last Bool -> Bool -> Bool
|| Bool
b
  forall (a :: * -> * -> *) b. Arrow a => a b b
returnA -< (Bool
cur, Bool
cur)

-- | Output True at a time if the input at the last time was True.
{-# DEPRECATED prev' "Use lastSF instead" #-}
prev' :: Monad m => SPred m a -> SPred m a
prev' :: forall (m :: * -> *) a. Monad m => SPred m a -> SPred m a
prev' SPred m a
sf = forall (m :: * -> *) c a b.
Monad m =>
c -> MSF m (a, c) (b, c) -> MSF m a b
feedback Bool
True forall a b. (a -> b) -> a -> b
$ proc (a
a, Bool
last) -> do
  Bool
b <- SPred m a
sf -< a
a
  forall (a :: * -> * -> *) b. Arrow a => a b b
returnA -< (Bool
last, Bool
b)