{-# LANGUAGE Arrows #-}
-- | Past-time Linear Temporal Logics based on SFs.
--
-- This module contains a definition of ptLTL with prev/last on top of Signal
-- Functions.
--
-- The difference between the future time and the past time LTL is that the
-- former needs a trace for evaluation, and the latter can be embedded into a
-- signal function network without additional support for evaluation.

module FRP.Yampa.LTLPast where

import FRP.Yampa

-- | True if both inputs are True.
andSF :: SF (Bool, Bool) Bool
andSF :: SF (Bool, Bool) Bool
andSF = ((Bool, Bool) -> Bool) -> SF (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
(&&))

-- | True if either or both inputs are True.
orSF :: SF (Bool, Bool) Bool
orSF :: SF (Bool, Bool) Bool
orSF = ((Bool, Bool) -> Bool) -> SF (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
(||))

-- | True if the input signal is False.
notSF :: SF Bool Bool
notSF :: SF Bool Bool
notSF = (Bool -> Bool) -> SF Bool Bool
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr Bool -> Bool
not

-- | True if the first signal is False or the second one is True.
impliesSF :: SF (Bool, Bool) Bool
impliesSF :: SF (Bool, Bool) Bool
impliesSF = ((Bool, Bool) -> Bool) -> SF (Bool, Bool) Bool
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (((Bool, Bool) -> Bool) -> SF (Bool, Bool) Bool)
-> ((Bool, Bool) -> Bool) -> SF (Bool, Bool) Bool
forall a b. (a -> b) -> a -> b
$ \(Bool
i,Bool
p) -> Bool -> Bool
not Bool
i Bool -> Bool -> Bool
|| Bool
p

-- | True a a time if the input signal has been always True so far.
sofarSF :: SF Bool Bool
sofarSF :: SF Bool Bool
sofarSF = Bool -> SF (Bool, Bool) (Bool, Bool) -> SF Bool Bool
forall c a b. c -> SF (a, c) (b, c) -> SF a b
loopPre Bool
True (SF (Bool, Bool) (Bool, Bool) -> SF Bool Bool)
-> SF (Bool, Bool) (Bool, Bool) -> SF Bool Bool
forall a b. (a -> b) -> a -> b
$ ((Bool, Bool) -> (Bool, Bool)) -> SF (Bool, Bool) (Bool, Bool)
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (((Bool, Bool) -> (Bool, Bool)) -> SF (Bool, Bool) (Bool, Bool))
-> ((Bool, Bool) -> (Bool, Bool)) -> SF (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')

-- | True at a time if the input signal has ever been True before.
everSF :: SF Bool Bool
everSF :: SF Bool Bool
everSF = Bool -> SF (Bool, Bool) (Bool, Bool) -> SF Bool Bool
forall c a b. c -> SF (a, c) (b, c) -> SF a b
loopPre Bool
False (SF (Bool, Bool) (Bool, Bool) -> SF Bool Bool)
-> SF (Bool, Bool) (Bool, Bool) -> SF Bool Bool
forall a b. (a -> b) -> a -> b
$ ((Bool, Bool) -> (Bool, Bool)) -> SF (Bool, Bool) (Bool, Bool)
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (((Bool, Bool) -> (Bool, Bool)) -> SF (Bool, Bool) (Bool, Bool))
-> ((Bool, Bool) -> (Bool, Bool)) -> SF (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')

-- | True if the signal was True in the last sample. False at time zero.
lastSF :: SF Bool Bool
lastSF :: SF Bool Bool
lastSF = Bool -> SF Bool Bool
forall a. a -> SF a a
iPre Bool
False

-- | Weak Until. True if the first signal is True until the second becomes
-- True, if ever.
untilSF :: SF (Bool, Bool) Bool
untilSF :: SF (Bool, Bool) Bool
untilSF = SF (Bool, Bool) (Bool, Event ())
-> (() -> SF (Bool, Bool) Bool) -> SF (Bool, Bool) Bool
forall a b c. SF a (b, Event c) -> (c -> SF a b) -> SF a b
switch
  (Bool
-> SF ((Bool, Bool), Bool) ((Bool, Event ()), Bool)
-> SF (Bool, Bool) (Bool, Event ())
forall c a b. c -> SF (a, c) (b, c) -> SF a b
loopPre Bool
True (SF ((Bool, Bool), Bool) ((Bool, Event ()), Bool)
 -> SF (Bool, Bool) (Bool, Event ()))
-> SF ((Bool, Bool), Bool) ((Bool, Event ()), Bool)
-> SF (Bool, Bool) (Bool, Event ())
forall a b. (a -> b) -> a -> b
$ (((Bool, Bool), Bool) -> ((Bool, Event ()), Bool))
-> SF ((Bool, Bool), Bool) ((Bool, Event ()), Bool)
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (\((Bool
i,Bool
u),Bool
o) -> let n :: Bool
n = Bool
o Bool -> Bool -> Bool
&& Bool
i
                                     in ((Bool
n, if (Bool
o Bool -> Bool -> Bool
&& Bool
u) then () -> Event ()
forall a. a -> Event a
Event () else Event ()
forall a. Event a
NoEvent), Bool
n)))
  (\()
_ -> ((Bool, Bool) -> Bool) -> SF (Bool, Bool) Bool
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (Bool, Bool) -> Bool
forall a b. (a, b) -> b
snd SF (Bool, Bool) Bool -> SF Bool Bool -> SF (Bool, Bool) Bool
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> SF Bool Bool
sofarSF)

-- -- * SF combinators that implement temporal combinators
--
-- type SPred a = SF a Bool
--
-- andSF' :: SPred a -> SPred a -> SPred a
-- andSF' sf1 sf2 = (sf1 &&& sf2) >>> arr (uncurry (&&))
--
-- orSF' :: SPred a -> SPred a -> SPred a
-- orSF' sf1 sf2 = (sf1 &&& sf2) >>> arr (uncurry (||))
--
-- notSF' :: SPred a -> SPred a
-- notSF' sf = sf >>> arr (not)
--
-- implySF' :: SPred a -> SPred a -> SPred a
-- implySF' sf1 sf2 = orSF' sf2 (notSF' sf1)
--
-- history' :: SPred a -> SPred a
-- history' sf = loopPre True $ proc (a, last) -> do
--   b <- sf -< a
--   let cur = last && b
--   returnA -< (cur, cur)
--
-- ever' :: SPred a -> SPred a
-- ever' sf = loopPre False $ proc (a, last) -> do
--   b <- sf -< a
--   let cur = last || b
--   returnA -< (cur, cur)