{-# LANGUAGE Arrows #-}
-- | Past LTL using MSFs.
--
-- Add assertions inside MSFs.
--
-- There are two ways of adding assertions to MSFs: piping the results of
-- Boolean-carrying MSFs into other MSFs, or wrapping MSFs into other MSFs
-- (using combinators).
module FRP.Dunai.LTLPast where

import Control.Monad.Trans.MSF.Maybe
import Data.Maybe
import Data.MonadicStreamFunction

-- * Past LTL as MSFs

-- ** Propositional MSFs

andSF :: Monad m => MSF m (Bool, Bool) Bool
andSF :: MSF m (Bool, Bool) Bool
andSF = ((Bool, Bool) -> Bool) -> MSF m (Bool, Bool) Bool
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr ((Bool -> Bool -> Bool) -> (Bool, Bool) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Bool -> Bool -> Bool
(&&))

orSF :: Monad m => MSF m (Bool, Bool) Bool
orSF :: MSF m (Bool, Bool) Bool
orSF = ((Bool, Bool) -> Bool) -> MSF m (Bool, Bool) Bool
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr ((Bool -> Bool -> Bool) -> (Bool, Bool) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Bool -> Bool -> Bool
(||))

notSF :: Monad m => MSF m Bool Bool
notSF :: MSF m Bool Bool
notSF = (Bool -> Bool) -> MSF m Bool Bool
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr Bool -> Bool
not

impliesSF :: Monad m => MSF m (Bool, Bool) Bool
impliesSF :: MSF m (Bool, Bool) Bool
impliesSF = ((Bool, Bool) -> Bool) -> MSF m (Bool, Bool) Bool
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (((Bool, Bool) -> Bool) -> MSF m (Bool, Bool) Bool)
-> ((Bool, Bool) -> Bool) -> MSF m (Bool, Bool) Bool
forall a b. (a -> b) -> a -> b
$ \(Bool
i,Bool
p) -> Bool -> Bool
not Bool
i Bool -> Bool -> Bool
|| Bool
p

-- ** Temporal MSFs

sofarSF :: Monad m => MSF m Bool Bool
sofarSF :: MSF m Bool Bool
sofarSF = Bool -> MSF m (Bool, Bool) (Bool, Bool) -> MSF m Bool Bool
forall (m :: * -> *) c a b.
Monad m =>
c -> MSF m (a, c) (b, c) -> MSF m a b
feedback Bool
True (MSF m (Bool, Bool) (Bool, Bool) -> MSF m Bool Bool)
-> MSF m (Bool, Bool) (Bool, Bool) -> MSF m Bool Bool
forall a b. (a -> b) -> a -> b
$ ((Bool, Bool) -> (Bool, Bool)) -> MSF m (Bool, Bool) (Bool, Bool)
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (((Bool, Bool) -> (Bool, Bool)) -> MSF m (Bool, Bool) (Bool, Bool))
-> ((Bool, Bool) -> (Bool, Bool))
-> MSF m (Bool, Bool) (Bool, Bool)
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')

everSF :: Monad m => MSF m Bool Bool
everSF :: MSF m Bool Bool
everSF = Bool -> MSF m (Bool, Bool) (Bool, Bool) -> MSF m Bool Bool
forall (m :: * -> *) c a b.
Monad m =>
c -> MSF m (a, c) (b, c) -> MSF m a b
feedback Bool
False (MSF m (Bool, Bool) (Bool, Bool) -> MSF m Bool Bool)
-> MSF m (Bool, Bool) (Bool, Bool) -> MSF m Bool Bool
forall a b. (a -> b) -> a -> b
$ ((Bool, Bool) -> (Bool, Bool)) -> MSF m (Bool, Bool) (Bool, Bool)
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (((Bool, Bool) -> (Bool, Bool)) -> MSF m (Bool, Bool) (Bool, Bool))
-> ((Bool, Bool) -> (Bool, Bool))
-> MSF m (Bool, Bool) (Bool, Bool)
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')

untilSF :: (Functor m, Monad m) => MSF m (Bool, Bool) Bool
untilSF :: MSF m (Bool, Bool) Bool
untilSF =
    MSF (MaybeT m) (Bool, Bool) Bool
-> MSF m (Bool, Bool) Bool -> MSF m (Bool, Bool) Bool
forall (m :: * -> *) a b.
(Functor m, Monad m) =>
MSF (MaybeT m) a b -> MSF m a b -> MSF m a b
catchMaybe (MSF m (Bool, Bool) (Bool, Bool) -> MSF (MaybeT m) (Bool, Bool) Bool
forall (m :: * -> *) a b.
Monad m =>
MSF m a (b, Bool) -> MSF (MaybeT m) a b
untilMaybeB (Bool
-> MSF m ((Bool, Bool), Bool) ((Bool, Bool), Bool)
-> MSF m (Bool, Bool) (Bool, Bool)
forall (m :: * -> *) c a b.
Monad m =>
c -> MSF m (a, c) (b, c) -> MSF m a b
feedback Bool
True (MSF m ((Bool, Bool), Bool) ((Bool, Bool), Bool)
 -> MSF m (Bool, Bool) (Bool, Bool))
-> MSF m ((Bool, Bool), Bool) ((Bool, Bool), Bool)
-> MSF m (Bool, Bool) (Bool, Bool)
forall a b. (a -> b) -> a -> b
$ (((Bool, Bool), Bool) -> ((Bool, Bool), Bool))
-> MSF m ((Bool, Bool), Bool) ((Bool, Bool), Bool)
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr ((Bool, Bool), Bool) -> ((Bool, Bool), Bool)
cond))
               ((Bool, Bool) -> Bool
forall a b. (a, b) -> b
snd ((Bool, Bool) -> Bool)
-> MSF m Bool Bool -> MSF m (Bool, Bool) Bool
forall (a :: * -> * -> *) b c d.
Arrow a =>
(b -> c) -> a c d -> a b d
^>> MSF m Bool Bool
forall (m :: * -> *). Monad m => MSF m Bool Bool
sofarSF)

  where

    untilMaybeB :: Monad m => MSF m a (b, Bool) -> MSF (MaybeT m) a b
    untilMaybeB :: 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) <- MSF m a (b, Bool) -> MSF (MaybeT m) a (b, Bool)
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
      MSF (MaybeT m) (Maybe b) b
forall (m :: * -> *) a. Monad m => MSF (MaybeT m) (Maybe a) a
inMaybeT -< if Bool
c then Maybe b
forall a. Maybe a
Nothing else b -> Maybe b
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

lastSF :: Monad m => MSF m Bool Bool
lastSF :: MSF m Bool Bool
lastSF = Bool -> MSF m Bool Bool
forall (m :: * -> *) a. Monad m => a -> MSF m a a
iPre Bool
False

-- data UnclearResult = Possibly Bool | Definitely Bool
--
-- causally :: SF a Bool -> SF a UnclearResult
-- causally = (>>> arr Definitely)
--
-- data TSF a = NonCausal (SF a UnclearResult)
--            | Causal    (SF a Bool)
--
-- evalTSF :: TSF a -> SignalSampleStream a -> Bool
-- evalTSF (Causal sf)    ss = firstSample $ fst $ evalSF sf ss
-- evalTSF (NonCausal sf) ss = clarifyResult $ lastSample $ fst $ evalSF sf ss
--
-- clarifyResult :: UnclearResult -> Bool
-- clarifyResult (Possibly x)   = x
-- clarifyResult (Definitely x) = x

-- * Past LTL combinators

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

-- ** Propositional MSFs
notSF' :: Monad m => SPred m a -> SPred m a
notSF' :: SPred m a -> SPred m a
notSF' SPred m a
sf = SPred m a
sf SPred m a -> MSF m Bool Bool -> SPred m a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> (Bool -> Bool) -> MSF m Bool Bool
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr Bool -> Bool
not

andSF' :: Monad m => SPred m a -> SPred m a -> SPred m a
andSF' :: SPred m a -> SPred m a -> SPred m a
andSF' SPred m a
sf1 SPred m a
sf2 = (SPred m a
sf1 SPred m a -> SPred m a -> MSF m a (Bool, Bool)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& SPred m a
sf2) MSF m a (Bool, Bool) -> MSF m (Bool, Bool) Bool -> SPred m a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> ((Bool, Bool) -> Bool) -> MSF m (Bool, Bool) Bool
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr ((Bool -> Bool -> Bool) -> (Bool, Bool) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Bool -> Bool -> Bool
(&&))

orSF' :: Monad m => SPred m a -> SPred m a -> SPred m a
orSF' :: SPred m a -> SPred m a -> SPred m a
orSF' SPred m a
sf1 SPred m a
sf2 = (SPred m a
sf1 SPred m a -> SPred m a -> MSF m a (Bool, Bool)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& SPred m a
sf2) MSF m a (Bool, Bool) -> MSF m (Bool, Bool) Bool -> SPred m a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> ((Bool, Bool) -> Bool) -> MSF m (Bool, Bool) Bool
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr ((Bool -> Bool -> Bool) -> (Bool, Bool) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Bool -> Bool -> Bool
(||))

implySF' :: Monad m => SPred m a -> SPred m a -> SPred m a
implySF' :: SPred m a -> SPred m a -> SPred m a
implySF' SPred m a
sf1 SPred m a
sf2 = SPred m a -> SPred m a -> SPred m a
forall (m :: * -> *) a.
Monad m =>
SPred m a -> SPred m a -> SPred m a
orSF' SPred m a
sf2 (SPred m a -> SPred m a
forall (m :: * -> *) a. Monad m => SPred m a -> SPred m a
notSF' SPred m a
sf1)

-- ** Temporal MSFs

history' :: Monad m => SPred m a -> SPred m a
history' :: SPred m a -> SPred m a
history' SPred m a
sf = Bool -> MSF m (a, Bool) (Bool, Bool) -> SPred m a
forall (m :: * -> *) c a b.
Monad m =>
c -> MSF m (a, c) (b, c) -> MSF m a b
feedback Bool
True (MSF m (a, Bool) (Bool, Bool) -> SPred m a)
-> MSF m (a, Bool) (Bool, Bool) -> SPred m a
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
  MSF m (Bool, Bool) (Bool, Bool)
forall (a :: * -> * -> *) b. Arrow a => a b b
returnA -< (Bool
cur, Bool
cur)

ever' :: Monad m => SPred m a -> SPred m a
ever' :: SPred m a -> SPred m a
ever' SPred m a
sf = Bool -> MSF m (a, Bool) (Bool, Bool) -> SPred m a
forall (m :: * -> *) c a b.
Monad m =>
c -> MSF m (a, c) (b, c) -> MSF m a b
feedback Bool
False (MSF m (a, Bool) (Bool, Bool) -> SPred m a)
-> MSF m (a, Bool) (Bool, Bool) -> SPred m a
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
  MSF m (Bool, Bool) (Bool, Bool)
forall (a :: * -> * -> *) b. Arrow a => a b b
returnA -< (Bool
cur, Bool
cur)

prev' :: Monad m => SPred m a -> SPred m a
prev' :: SPred m a -> SPred m a
prev' = Bool -> SPred m a -> SPred m a
forall (m :: * -> *) b a. Monad m => b -> MSF m a b -> MSF m a b
prev Bool
True

prev :: Monad m => b -> MSF m a b -> MSF m a b
prev :: b -> MSF m a b -> MSF m a b
prev b
b MSF m a b
sf = b -> MSF m (a, b) (b, b) -> MSF m a b
forall (m :: * -> *) c a b.
Monad m =>
c -> MSF m (a, c) (b, c) -> MSF m a b
feedback b
b (MSF m (a, b) (b, b) -> MSF m a b)
-> MSF m (a, b) (b, b) -> MSF m a b
forall a b. (a -> b) -> a -> b
$ proc (a
a, b
last) -> do
  b
b <- MSF m a b
sf -< a
a
  MSF m (b, b) (b, b)
forall (a :: * -> * -> *) b. Arrow a => a b b
returnA -< (b
last, b
b)