{-# LANGUAGE CPP                 #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE ScopedTypeVariables #-}
-- |
-- Copyright  : (c) Ivan Perez, 2017
-- License    : BSD3
-- Maintainer : ivan.perez@keera.co.uk
--
-- Future-time linear temporal logic implemented on top of monadic stream
-- functions.
--
-- This module can be used to define LTL-like predicates on Monadic Stream
-- Functions, and to evaluate them. The main entry point is the function
-- 'evalT', which takes a temporal predicate, and a stream of inputs, and
-- evaluates the predicate against the stream. Evaluation takes place at time
-- 0, although it is possible to express conditions on future samples.
--
-- /Disclaimer/: This is not necessarily the same as LTL.
module FRP.Dunai.LTLFuture
    ( TPred(..)
    , tPredMap
    , evalT
    )
  where

-- External imports
#if !MIN_VERSION_base(4,8,0)
import Control.Applicative (Applicative, pure, (<$>), (<*>))
#endif

import Control.Monad.Trans.MSF.Reader          (ReaderT, readerS, runReaderS)
import Data.MonadicStreamFunction              (MSF)
import Data.MonadicStreamFunction.InternalCore (unMSF)

-- Internal imports
import FRP.Dunai.Stream (DTime, SignalSampleStream)

-- * Temporal Logics based on SFs

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

-- | Apply a transformation to the leaves of a temporal predicate (to the SFs).
tPredMap :: (Functor m, Applicative m, Monad m)
         => (MSF m a Bool -> m (MSF m a Bool))  -- ^ Transformation to apply
         -> TPred m a                           -- ^ Temporal predicate
         -> m (TPred m a)
tPredMap :: forall (m :: * -> *) a.
(Functor m, Applicative m, Monad m) =>
(MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a)
tPredMap MSF m a Bool -> m (MSF m a Bool)
f (Prop MSF m a Bool
sf)       = MSF m a Bool -> TPred m a
forall (m :: * -> *) a. MSF m a Bool -> TPred m a
Prop       (MSF m a Bool -> TPred m a) -> m (MSF m a Bool) -> m (TPred m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MSF m a Bool -> m (MSF m a Bool)
f MSF m a Bool
sf
tPredMap MSF m a Bool -> m (MSF m a Bool)
f (And TPred m a
t1 TPred m a
t2)     = TPred m a -> TPred m a -> TPred m a
forall (m :: * -> *) a. TPred m a -> TPred m a -> TPred m a
And        (TPred m a -> TPred m a -> TPred m a)
-> m (TPred m a) -> m (TPred m a -> TPred m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a)
forall (m :: * -> *) a.
(Functor m, Applicative m, Monad m) =>
(MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a)
tPredMap MSF m a Bool -> m (MSF m a Bool)
f TPred m a
t1 m (TPred m a -> TPred m a) -> m (TPred m a) -> m (TPred m a)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a)
forall (m :: * -> *) a.
(Functor m, Applicative m, Monad m) =>
(MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a)
tPredMap MSF m a Bool -> m (MSF m a Bool)
f TPred m a
t2
tPredMap MSF m a Bool -> m (MSF m a Bool)
f (Or TPred m a
t1 TPred m a
t2)      = TPred m a -> TPred m a -> TPred m a
forall (m :: * -> *) a. TPred m a -> TPred m a -> TPred m a
Or         (TPred m a -> TPred m a -> TPred m a)
-> m (TPred m a) -> m (TPred m a -> TPred m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a)
forall (m :: * -> *) a.
(Functor m, Applicative m, Monad m) =>
(MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a)
tPredMap MSF m a Bool -> m (MSF m a Bool)
f TPred m a
t1 m (TPred m a -> TPred m a) -> m (TPred m a) -> m (TPred m a)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a)
forall (m :: * -> *) a.
(Functor m, Applicative m, Monad m) =>
(MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a)
tPredMap MSF m a Bool -> m (MSF m a Bool)
f TPred m a
t2
tPredMap MSF m a Bool -> m (MSF m a Bool)
f (Not TPred m a
t1)        = TPred m a -> TPred m a
forall (m :: * -> *) a. TPred m a -> TPred m a
Not        (TPred m a -> TPred m a) -> m (TPred m a) -> m (TPred m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a)
forall (m :: * -> *) a.
(Functor m, Applicative m, Monad m) =>
(MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a)
tPredMap MSF m a Bool -> m (MSF m a Bool)
f TPred m a
t1
tPredMap MSF m a Bool -> m (MSF m a Bool)
f (Implies TPred m a
t1 TPred m a
t2) = TPred m a -> TPred m a -> TPred m a
forall (m :: * -> *) a. TPred m a -> TPred m a -> TPred m a
Implies    (TPred m a -> TPred m a -> TPred m a)
-> m (TPred m a) -> m (TPred m a -> TPred m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a)
forall (m :: * -> *) a.
(Functor m, Applicative m, Monad m) =>
(MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a)
tPredMap MSF m a Bool -> m (MSF m a Bool)
f TPred m a
t1 m (TPred m a -> TPred m a) -> m (TPred m a) -> m (TPred m a)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a)
forall (m :: * -> *) a.
(Functor m, Applicative m, Monad m) =>
(MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a)
tPredMap MSF m a Bool -> m (MSF m a Bool)
f TPred m a
t2
tPredMap MSF m a Bool -> m (MSF m a Bool)
f (Always TPred m a
t1)     = TPred m a -> TPred m a
forall (m :: * -> *) a. TPred m a -> TPred m a
Always     (TPred m a -> TPred m a) -> m (TPred m a) -> m (TPred m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a)
forall (m :: * -> *) a.
(Functor m, Applicative m, Monad m) =>
(MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a)
tPredMap MSF m a Bool -> m (MSF m a Bool)
f TPred m a
t1
tPredMap MSF m a Bool -> m (MSF m a Bool)
f (Eventually TPred m a
t1) = TPred m a -> TPred m a
forall (m :: * -> *) a. TPred m a -> TPred m a
Eventually (TPred m a -> TPred m a) -> m (TPred m a) -> m (TPred m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a)
forall (m :: * -> *) a.
(Functor m, Applicative m, Monad m) =>
(MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a)
tPredMap MSF m a Bool -> m (MSF m a Bool)
f TPred m a
t1
tPredMap MSF m a Bool -> m (MSF m a Bool)
f (Next TPred m a
t1)       = TPred m a -> TPred m a
forall (m :: * -> *) a. TPred m a -> TPred m a
Next       (TPred m a -> TPred m a) -> m (TPred m a) -> m (TPred m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a)
forall (m :: * -> *) a.
(Functor m, Applicative m, Monad m) =>
(MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a)
tPredMap MSF m a Bool -> m (MSF m a Bool)
f TPred m a
t1
tPredMap MSF m a Bool -> m (MSF m a Bool)
f (Until TPred m a
t1 TPred m a
t2)   = TPred m a -> TPred m a -> TPred m a
forall (m :: * -> *) a. TPred m a -> TPred m a -> TPred m a
Until      (TPred m a -> TPred m a -> TPred m a)
-> m (TPred m a) -> m (TPred m a -> TPred m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a)
forall (m :: * -> *) a.
(Functor m, Applicative m, Monad m) =>
(MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a)
tPredMap MSF m a Bool -> m (MSF m a Bool)
f TPred m a
t1 m (TPred m a -> TPred m a) -> m (TPred m a) -> m (TPred m a)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a)
forall (m :: * -> *) a.
(Functor m, Applicative m, Monad m) =>
(MSF m a Bool -> m (MSF m a Bool)) -> TPred m a -> m (TPred m a)
tPredMap MSF m a Bool -> m (MSF m a Bool)
f TPred m a
t2

-- * Temporal Evaluation

-- | Evaluates a temporal predicate at time T=0 against a sample stream.
--
-- Returns 'True' if the temporal proposition is currently true.
evalT :: (Functor m, Applicative m, Monad m)
      => TPred (ReaderT DTime m) a
      -> SignalSampleStream a
      -> m Bool
evalT :: forall (m :: * -> *) a.
(Functor m, Applicative m, Monad m) =>
TPred (ReaderT DTime m) a -> SignalSampleStream a -> m Bool
evalT (Prop MSF (ReaderT DTime m) a Bool
_sf)      []     = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
evalT (And TPred (ReaderT DTime m) a
t1 TPred (ReaderT DTime m) a
t2)     []     = Bool -> Bool -> Bool
(&&) (Bool -> Bool -> Bool) -> m Bool -> m (Bool -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TPred (ReaderT DTime m) a -> [(DTime, a)] -> m Bool
forall (m :: * -> *) a.
(Functor m, Applicative m, Monad m) =>
TPred (ReaderT DTime m) a -> SignalSampleStream a -> m Bool
evalT TPred (ReaderT DTime m) a
t1 [] m (Bool -> Bool) -> m Bool -> m Bool
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TPred (ReaderT DTime m) a -> [(DTime, a)] -> m Bool
forall (m :: * -> *) a.
(Functor m, Applicative m, Monad m) =>
TPred (ReaderT DTime m) a -> SignalSampleStream a -> m Bool
evalT TPred (ReaderT DTime m) a
t2 []
evalT (Or  TPred (ReaderT DTime m) a
t1 TPred (ReaderT DTime m) a
t2)     []     = Bool -> Bool -> Bool
(||) (Bool -> Bool -> Bool) -> m Bool -> m (Bool -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TPred (ReaderT DTime m) a -> [(DTime, a)] -> m Bool
forall (m :: * -> *) a.
(Functor m, Applicative m, Monad m) =>
TPred (ReaderT DTime m) a -> SignalSampleStream a -> m Bool
evalT TPred (ReaderT DTime m) a
t1 [] m (Bool -> Bool) -> m Bool -> m Bool
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TPred (ReaderT DTime m) a -> [(DTime, a)] -> m Bool
forall (m :: * -> *) a.
(Functor m, Applicative m, Monad m) =>
TPred (ReaderT DTime m) a -> SignalSampleStream a -> m Bool
evalT TPred (ReaderT DTime m) a
t2 []
evalT (Not TPred (ReaderT DTime m) a
t1)        []     = Bool -> Bool
not  (Bool -> Bool) -> m Bool -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TPred (ReaderT DTime m) a -> [(DTime, a)] -> m Bool
forall (m :: * -> *) a.
(Functor m, Applicative m, Monad m) =>
TPred (ReaderT DTime m) a -> SignalSampleStream a -> m Bool
evalT TPred (ReaderT DTime m) a
t1 []
evalT (Implies TPred (ReaderT DTime m) a
t1 TPred (ReaderT DTime m) a
t2) []     = Bool -> Bool -> Bool
(||) (Bool -> Bool -> Bool) -> m Bool -> m (Bool -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Bool -> Bool
not (Bool -> Bool) -> m Bool -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TPred (ReaderT DTime m) a -> [(DTime, a)] -> m Bool
forall (m :: * -> *) a.
(Functor m, Applicative m, Monad m) =>
TPred (ReaderT DTime m) a -> SignalSampleStream a -> m Bool
evalT TPred (ReaderT DTime m) a
t1 []) m (Bool -> Bool) -> m Bool -> m Bool
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TPred (ReaderT DTime m) a -> [(DTime, a)] -> m Bool
forall (m :: * -> *) a.
(Functor m, Applicative m, Monad m) =>
TPred (ReaderT DTime m) a -> SignalSampleStream a -> m Bool
evalT TPred (ReaderT DTime m) a
t2 []
evalT (Always TPred (ReaderT DTime m) a
_t)     []     = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
evalT (Eventually TPred (ReaderT DTime m) a
_t) []     = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
evalT (Next TPred (ReaderT DTime m) a
_t)       []     = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
evalT (Until TPred (ReaderT DTime m) a
t1 TPred (ReaderT DTime m) a
t2)   []     = Bool -> Bool -> Bool
(||) (Bool -> Bool -> Bool) -> m Bool -> m (Bool -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TPred (ReaderT DTime m) a -> [(DTime, a)] -> m Bool
forall (m :: * -> *) a.
(Functor m, Applicative m, Monad m) =>
TPred (ReaderT DTime m) a -> SignalSampleStream a -> m Bool
evalT TPred (ReaderT DTime m) a
t1 [] m (Bool -> Bool) -> m Bool -> m Bool
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TPred (ReaderT DTime m) a -> [(DTime, a)] -> m Bool
forall (m :: * -> *) a.
(Functor m, Applicative m, Monad m) =>
TPred (ReaderT DTime m) a -> SignalSampleStream a -> m Bool
evalT TPred (ReaderT DTime m) a
t2 []
evalT TPred (ReaderT DTime m) a
op              ((DTime, a)
x:[(DTime, a)]
xs) = do
  (MultiRes
r, TPred (ReaderT DTime m) a
op') <- TPred (ReaderT DTime m) a
-> (DTime, a) -> m (MultiRes, TPred (ReaderT DTime m) a)
forall (m :: * -> *) a.
(Applicative m, Monad m) =>
TPred (ReaderT DTime m) a
-> (DTime, a) -> m (MultiRes, TPred (ReaderT DTime m) a)
stepF TPred (ReaderT DTime m) a
op (DTime, a)
x
  case (MultiRes
r, [(DTime, a)]
xs) of
    (Def Bool
x,    [(DTime, a)]
_) -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
x
    (SoFar Bool
x, []) -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
x
    (SoFar Bool
_, [(DTime, a)]
xs) -> TPred (ReaderT DTime m) a -> [(DTime, a)] -> m Bool
forall (m :: * -> *) a.
(Functor m, Applicative m, Monad m) =>
TPred (ReaderT DTime m) a -> SignalSampleStream a -> m Bool
evalT TPred (ReaderT DTime m) a
op' [(DTime, a)]
xs

-- ** Multi-valued temporal evaluation

-- | Multi-valued logic result
data MultiRes
  = Def Bool   -- ^ Definite value known
  | SoFar Bool -- ^ Value so far, but could change

-- | Multi-valued implementation of @and@.
andM :: MultiRes -> MultiRes -> MultiRes
andM :: MultiRes -> MultiRes -> MultiRes
andM (Def Bool
False)   MultiRes
_             = Bool -> MultiRes
Def Bool
False
andM MultiRes
_             (Def Bool
False)   = Bool -> MultiRes
Def Bool
False
andM (Def Bool
True)    MultiRes
x             = MultiRes
x
andM MultiRes
x             (Def Bool
True)    = MultiRes
x
andM (SoFar Bool
False) (SoFar Bool
_)     = Bool -> MultiRes
SoFar Bool
False
andM (SoFar Bool
_)     (SoFar Bool
False) = Bool -> MultiRes
SoFar Bool
False
andM (SoFar Bool
True)  (SoFar Bool
x)     = Bool -> MultiRes
SoFar Bool
x

-- | Multi-valued implementation of @or@.
orM :: MultiRes -> MultiRes -> MultiRes
orM :: MultiRes -> MultiRes -> MultiRes
orM (Def Bool
False)   MultiRes
x             = MultiRes
x
orM MultiRes
_             (Def Bool
False)   = Bool -> MultiRes
Def Bool
False
orM (Def Bool
True)    MultiRes
x             = MultiRes
x
orM MultiRes
x             (Def Bool
True)    = MultiRes
x
orM (SoFar Bool
False) (SoFar Bool
_)     = Bool -> MultiRes
SoFar Bool
False
orM (SoFar Bool
_)     (SoFar Bool
False) = Bool -> MultiRes
SoFar Bool
False
orM (SoFar Bool
True)  (SoFar Bool
x)     = Bool -> MultiRes
SoFar Bool
x

-- | Perform one step of evaluation of a temporal predicate.
stepF :: (Applicative m, Monad m)
      => TPred (ReaderT DTime m) a
      -> (DTime, a)
      -> m (MultiRes, TPred (ReaderT DTime m) a)

stepF :: forall (m :: * -> *) a.
(Applicative m, Monad m) =>
TPred (ReaderT DTime m) a
-> (DTime, a) -> m (MultiRes, TPred (ReaderT DTime m) a)
stepF (Prop MSF (ReaderT DTime m) a Bool
sf) (DTime, a)
x = do
  (Bool
b, MSF m (DTime, a) Bool
sf') <- MSF m (DTime, a) Bool
-> (DTime, a) -> m (Bool, MSF m (DTime, a) Bool)
forall (m :: * -> *) a b. MSF m a b -> a -> m (b, MSF m a b)
unMSF (MSF (ReaderT DTime m) a Bool -> MSF m (DTime, a) Bool
forall (m :: * -> *) r a b.
Monad m =>
MSF (ReaderT r m) a b -> MSF m (r, a) b
runReaderS MSF (ReaderT DTime m) a Bool
sf) (DTime, a)
x
  (MultiRes, TPred (ReaderT DTime m) a)
-> m (MultiRes, TPred (ReaderT DTime m) a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> MultiRes
Def Bool
b, MSF (ReaderT DTime m) a Bool -> TPred (ReaderT DTime m) a
forall (m :: * -> *) a. MSF m a Bool -> TPred m a
Prop (MSF m (DTime, a) Bool -> MSF (ReaderT DTime m) a Bool
forall (m :: * -> *) r a b.
Monad m =>
MSF m (r, a) b -> MSF (ReaderT r m) a b
readerS MSF m (DTime, a) Bool
sf'))

stepF (Always TPred (ReaderT DTime m) a
sf) (DTime, a)
x = do
  (MultiRes
b, TPred (ReaderT DTime m) a
sf') <- TPred (ReaderT DTime m) a
-> (DTime, a) -> m (MultiRes, TPred (ReaderT DTime m) a)
forall (m :: * -> *) a.
(Applicative m, Monad m) =>
TPred (ReaderT DTime m) a
-> (DTime, a) -> m (MultiRes, TPred (ReaderT DTime m) a)
stepF TPred (ReaderT DTime m) a
sf (DTime, a)
x
  case MultiRes
b of
    Def Bool
True    -> (MultiRes, TPred (ReaderT DTime m) a)
-> m (MultiRes, TPred (ReaderT DTime m) a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> MultiRes
SoFar Bool
True,  TPred (ReaderT DTime m) a -> TPred (ReaderT DTime m) a
forall (m :: * -> *) a. TPred m a -> TPred m a
Always TPred (ReaderT DTime m) a
sf')
    Def Bool
False   -> (MultiRes, TPred (ReaderT DTime m) a)
-> m (MultiRes, TPred (ReaderT DTime m) a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> MultiRes
Def Bool
False,   TPred (ReaderT DTime m) a -> TPred (ReaderT DTime m) a
forall (m :: * -> *) a. TPred m a -> TPred m a
Always TPred (ReaderT DTime m) a
sf')
    SoFar Bool
True  -> (MultiRes, TPred (ReaderT DTime m) a)
-> m (MultiRes, TPred (ReaderT DTime m) a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> MultiRes
SoFar Bool
True,  TPred (ReaderT DTime m) a -> TPred (ReaderT DTime m) a
forall (m :: * -> *) a. TPred m a -> TPred m a
Always TPred (ReaderT DTime m) a
sf')
    SoFar Bool
False -> (MultiRes, TPred (ReaderT DTime m) a)
-> m (MultiRes, TPred (ReaderT DTime m) a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> MultiRes
SoFar Bool
False, TPred (ReaderT DTime m) a -> TPred (ReaderT DTime m) a
forall (m :: * -> *) a. TPred m a -> TPred m a
Always TPred (ReaderT DTime m) a
sf')

stepF (Eventually TPred (ReaderT DTime m) a
sf) (DTime, a)
x = do
  (MultiRes
b, TPred (ReaderT DTime m) a
sf') <- TPred (ReaderT DTime m) a
-> (DTime, a) -> m (MultiRes, TPred (ReaderT DTime m) a)
forall (m :: * -> *) a.
(Applicative m, Monad m) =>
TPred (ReaderT DTime m) a
-> (DTime, a) -> m (MultiRes, TPred (ReaderT DTime m) a)
stepF TPred (ReaderT DTime m) a
sf (DTime, a)
x
  case MultiRes
b of
    Def   Bool
True  -> (MultiRes, TPred (ReaderT DTime m) a)
-> m (MultiRes, TPred (ReaderT DTime m) a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> MultiRes
SoFar Bool
True,  TPred (ReaderT DTime m) a -> TPred (ReaderT DTime m) a
forall (m :: * -> *) a. TPred m a -> TPred m a
Always TPred (ReaderT DTime m) a
sf')
    Def   Bool
False -> (MultiRes, TPred (ReaderT DTime m) a)
-> m (MultiRes, TPred (ReaderT DTime m) a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> MultiRes
SoFar Bool
False, TPred (ReaderT DTime m) a -> TPred (ReaderT DTime m) a
forall (m :: * -> *) a. TPred m a -> TPred m a
Always TPred (ReaderT DTime m) a
sf')
    SoFar Bool
True  -> (MultiRes, TPred (ReaderT DTime m) a)
-> m (MultiRes, TPred (ReaderT DTime m) a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> MultiRes
SoFar Bool
True,  TPred (ReaderT DTime m) a -> TPred (ReaderT DTime m) a
forall (m :: * -> *) a. TPred m a -> TPred m a
Always TPred (ReaderT DTime m) a
sf')
    SoFar Bool
False -> (MultiRes, TPred (ReaderT DTime m) a)
-> m (MultiRes, TPred (ReaderT DTime m) a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> MultiRes
SoFar Bool
False, TPred (ReaderT DTime m) a -> TPred (ReaderT DTime m) a
forall (m :: * -> *) a. TPred m a -> TPred m a
Always TPred (ReaderT DTime m) a
sf')

stepF (Not TPred (ReaderT DTime m) a
sf) (DTime, a)
x = do
  (MultiRes
b, TPred (ReaderT DTime m) a
sf') <- TPred (ReaderT DTime m) a
-> (DTime, a) -> m (MultiRes, TPred (ReaderT DTime m) a)
forall (m :: * -> *) a.
(Applicative m, Monad m) =>
TPred (ReaderT DTime m) a
-> (DTime, a) -> m (MultiRes, TPred (ReaderT DTime m) a)
stepF TPred (ReaderT DTime m) a
sf (DTime, a)
x
  case MultiRes
b of
    Def Bool
x   -> (MultiRes, TPred (ReaderT DTime m) a)
-> m (MultiRes, TPred (ReaderT DTime m) a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> MultiRes
Def (Bool -> Bool
not Bool
x),   TPred (ReaderT DTime m) a -> TPred (ReaderT DTime m) a
forall (m :: * -> *) a. TPred m a -> TPred m a
Not TPred (ReaderT DTime m) a
sf')
    SoFar Bool
x -> (MultiRes, TPred (ReaderT DTime m) a)
-> m (MultiRes, TPred (ReaderT DTime m) a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> MultiRes
SoFar (Bool -> Bool
not Bool
x), TPred (ReaderT DTime m) a -> TPred (ReaderT DTime m) a
forall (m :: * -> *) a. TPred m a -> TPred m a
Not TPred (ReaderT DTime m) a
sf')

stepF (And TPred (ReaderT DTime m) a
sf1 TPred (ReaderT DTime m) a
sf2) (DTime, a)
x = do
  (MultiRes
b1, TPred (ReaderT DTime m) a
sf1') <- TPred (ReaderT DTime m) a
-> (DTime, a) -> m (MultiRes, TPred (ReaderT DTime m) a)
forall (m :: * -> *) a.
(Applicative m, Monad m) =>
TPred (ReaderT DTime m) a
-> (DTime, a) -> m (MultiRes, TPred (ReaderT DTime m) a)
stepF TPred (ReaderT DTime m) a
sf1 (DTime, a)
x
  (MultiRes
b2, TPred (ReaderT DTime m) a
sf2') <- TPred (ReaderT DTime m) a
-> (DTime, a) -> m (MultiRes, TPred (ReaderT DTime m) a)
forall (m :: * -> *) a.
(Applicative m, Monad m) =>
TPred (ReaderT DTime m) a
-> (DTime, a) -> m (MultiRes, TPred (ReaderT DTime m) a)
stepF TPred (ReaderT DTime m) a
sf2 (DTime, a)
x
  let r :: MultiRes
r = MultiRes -> MultiRes -> MultiRes
andM MultiRes
b1 MultiRes
b2
  (MultiRes, TPred (ReaderT DTime m) a)
-> m (MultiRes, TPred (ReaderT DTime m) a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MultiRes
r, TPred (ReaderT DTime m) a
-> TPred (ReaderT DTime m) a -> TPred (ReaderT DTime m) a
forall (m :: * -> *) a. TPred m a -> TPred m a -> TPred m a
And TPred (ReaderT DTime m) a
sf1' TPred (ReaderT DTime m) a
sf2')

stepF (Or TPred (ReaderT DTime m) a
sf1 TPred (ReaderT DTime m) a
sf2) (DTime, a)
x = do
  (MultiRes
b1, TPred (ReaderT DTime m) a
sf1') <- TPred (ReaderT DTime m) a
-> (DTime, a) -> m (MultiRes, TPred (ReaderT DTime m) a)
forall (m :: * -> *) a.
(Applicative m, Monad m) =>
TPred (ReaderT DTime m) a
-> (DTime, a) -> m (MultiRes, TPred (ReaderT DTime m) a)
stepF TPred (ReaderT DTime m) a
sf1 (DTime, a)
x
  (MultiRes
b2, TPred (ReaderT DTime m) a
sf2') <- TPred (ReaderT DTime m) a
-> (DTime, a) -> m (MultiRes, TPred (ReaderT DTime m) a)
forall (m :: * -> *) a.
(Applicative m, Monad m) =>
TPred (ReaderT DTime m) a
-> (DTime, a) -> m (MultiRes, TPred (ReaderT DTime m) a)
stepF TPred (ReaderT DTime m) a
sf2 (DTime, a)
x
  let r :: MultiRes
r = MultiRes -> MultiRes -> MultiRes
orM MultiRes
b1 MultiRes
b2
  (MultiRes, TPred (ReaderT DTime m) a)
-> m (MultiRes, TPred (ReaderT DTime m) a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MultiRes
r, TPred (ReaderT DTime m) a
-> TPred (ReaderT DTime m) a -> TPred (ReaderT DTime m) a
forall (m :: * -> *) a. TPred m a -> TPred m a -> TPred m a
Or TPred (ReaderT DTime m) a
sf1' TPred (ReaderT DTime m) a
sf2')

stepF (Implies TPred (ReaderT DTime m) a
sf1 TPred (ReaderT DTime m) a
sf2) (DTime, a)
x =
  TPred (ReaderT DTime m) a
-> (DTime, a) -> m (MultiRes, TPred (ReaderT DTime m) a)
forall (m :: * -> *) a.
(Applicative m, Monad m) =>
TPred (ReaderT DTime m) a
-> (DTime, a) -> m (MultiRes, TPred (ReaderT DTime m) a)
stepF (TPred (ReaderT DTime m) a -> TPred (ReaderT DTime m) a
forall (m :: * -> *) a. TPred m a -> TPred m a
Not TPred (ReaderT DTime m) a
sf1 TPred (ReaderT DTime m) a
-> TPred (ReaderT DTime m) a -> TPred (ReaderT DTime m) a
forall (m :: * -> *) a. TPred m a -> TPred m a -> TPred m a
`Or` TPred (ReaderT DTime m) a
sf2) (DTime, a)
x