{-# LANGUAGE CPP #-}
{-# OPTIONS_GHC -Wno-unused-matches #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Redundant irrefutable pattern" #-}
module Hermod.ReCon.LTL.Satisfy(
    SatisfactionResult(..)
  , satisfies
  , satisfiesS
  , SatisfyMetrics(..)
  ) where

import           Hermod.ReCon.LTL.Formula
import           Hermod.ReCon.LTL.Internal.IR.HomogeneousFormula (eval)
import           Hermod.ReCon.LTL.Internal.Progress
import           Hermod.ReCon.LTL.Internal.Rewrite

import           Control.Monad.Reader (runReader)

import           Prelude hiding (Foldable (..), lookup)

import           Data.Foldable (Foldable(..))
import           Data.IORef (IORef, modifyIORef')
import           Data.Word (Word64)

import           Streaming

#ifdef TRACE
import qualified Hermod.ReCon.LTL.Formula.Prec       as Prec
import           Hermod.ReCon.LTL.Formula.Pretty     (prettyFormula)
import qualified Data.Text                                 as Text
import           Debug.Trace                               (trace)
#endif


-- This file concerns checking formula satisfiability against some input.
-- The input can be either pure and finite foldable (e.g. a list, cf. `satisfies`)
--   or effectful and potentially infinite (i.e. a Stream, cf. `satisfiesS`).

-- | The result of checking satisfaction of a formula against a timeline.
--   If unsatisfied, stores points in the timeline "relevant" to the formula.
data SatisfactionResult event ty = Satisfied | Unsatisfied (Relevance event ty) deriving (Int -> SatisfactionResult event ty -> ShowS
[SatisfactionResult event ty] -> ShowS
SatisfactionResult event ty -> String
(Int -> SatisfactionResult event ty -> ShowS)
-> (SatisfactionResult event ty -> String)
-> ([SatisfactionResult event ty] -> ShowS)
-> Show (SatisfactionResult event ty)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall event ty.
(Show event, Show ty) =>
Int -> SatisfactionResult event ty -> ShowS
forall event ty.
(Show event, Show ty) =>
[SatisfactionResult event ty] -> ShowS
forall event ty.
(Show event, Show ty) =>
SatisfactionResult event ty -> String
$cshowsPrec :: forall event ty.
(Show event, Show ty) =>
Int -> SatisfactionResult event ty -> ShowS
showsPrec :: Int -> SatisfactionResult event ty -> ShowS
$cshow :: forall event ty.
(Show event, Show ty) =>
SatisfactionResult event ty -> String
show :: SatisfactionResult event ty -> String
$cshowList :: forall event ty.
(Show event, Show ty) =>
[SatisfactionResult event ty] -> ShowS
showList :: [SatisfactionResult event ty] -> ShowS
Show, SatisfactionResult event ty -> SatisfactionResult event ty -> Bool
(SatisfactionResult event ty
 -> SatisfactionResult event ty -> Bool)
-> (SatisfactionResult event ty
    -> SatisfactionResult event ty -> Bool)
-> Eq (SatisfactionResult event ty)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall event ty.
(Eq event, Eq ty) =>
SatisfactionResult event ty -> SatisfactionResult event ty -> Bool
$c== :: forall event ty.
(Eq event, Eq ty) =>
SatisfactionResult event ty -> SatisfactionResult event ty -> Bool
== :: SatisfactionResult event ty -> SatisfactionResult event ty -> Bool
$c/= :: forall event ty.
(Eq event, Eq ty) =>
SatisfactionResult event ty -> SatisfactionResult event ty -> Bool
/= :: SatisfactionResult event ty -> SatisfactionResult event ty -> Bool
Eq)

traceFormula :: Show ty => String -> Formula event ty -> Formula event ty
traceFormula :: forall ty event.
Show ty =>
String -> Formula event ty -> Formula event ty
traceFormula ~String
str Formula event ty
x =
#ifdef TRACE

  trace (str <> " " <> Text.unpack (prettyFormula x Prec.Universe)) x
#else
  Formula event ty
x
#endif

handleNext :: (Event event ty, Ord event, Ord ty, Show ty)
           => OnMissingKey
           -> (Int, Formula event ty)
           -> event
           -> Either (SatisfactionResult event ty) (Int, Formula event ty)
handleNext :: forall event ty.
(Event event ty, Ord event, Ord ty, Show ty) =>
OnMissingKey
-> (Int, Formula event ty)
-> event
-> Either (SatisfactionResult event ty) (Int, Formula event ty)
handleNext OnMissingKey
omk (!Int
n, !Formula event ty
formula0) event
m =
  let formula1 :: Formula event ty
formula1 = String -> Formula event ty -> Formula event ty
forall ty event.
Show ty =>
String -> Formula event ty -> Formula event ty
traceFormula (String
"(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")\ninitial:") Formula event ty
formula0
      formula2 :: Formula event ty
formula2 = String -> Formula event ty -> Formula event ty
forall ty event.
Show ty =>
String -> Formula event ty -> Formula event ty
traceFormula String
"next:" (Formula event ty -> Formula event ty)
-> Formula event ty -> Formula event ty
forall a b. (a -> b) -> a -> b
$ Reader OnMissingKey (Formula event ty)
-> OnMissingKey -> Formula event ty
forall r a. Reader r a -> r -> a
runReader (Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
forall event ty.
(Event event ty, Eq ty) =>
Formula event ty -> event -> Reader OnMissingKey (Formula event ty)
next Formula event ty
formula1 event
m) OnMissingKey
omk
      formula3 :: Formula event ty
formula3 = String -> Formula event ty -> Formula event ty
forall ty event.
Show ty =>
String -> Formula event ty -> Formula event ty
traceFormula String
"rewrite-hom:" (Formula event ty -> Formula event ty
forall event ty. Formula event ty -> Formula event ty
rewriteHomogeneous Formula event ty
formula2)
      formula5 :: Formula event ty
formula5 = String -> Formula event ty -> Formula event ty
forall ty event.
Show ty =>
String -> Formula event ty -> Formula event ty
traceFormula String
"rewrite-id:" (Formula event ty -> Formula event ty
forall ty event. Eq ty => Formula event ty -> Formula event ty
rewriteIdentity Formula event ty
formula3) in
  case Formula event ty
formula5 of
    Formula event ty
Top     -> SatisfactionResult event ty
-> Either (SatisfactionResult event ty) (Int, Formula event ty)
forall a b. a -> Either a b
Left SatisfactionResult event ty
forall event ty. SatisfactionResult event ty
Satisfied
    Formula event ty
Bottom  -> SatisfactionResult event ty
-> Either (SatisfactionResult event ty) (Int, Formula event ty)
forall a b. a -> Either a b
Left (Relevance event ty -> SatisfactionResult event ty
forall event ty. Relevance event ty -> SatisfactionResult event ty
Unsatisfied (Formula event ty -> Relevance event ty
forall event ty.
(Ord event, Ord ty) =>
Formula event ty -> Relevance event ty
relevance Formula event ty
formula0))
    Formula event ty
formula -> (Int, Formula event ty)
-> Either (SatisfactionResult event ty) (Int, Formula event ty)
forall a b. b -> Either a b
Right (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Formula event ty
formula5)

handleEnd :: (Ord event, Ord ty, Show ty) => (Int, Formula event ty) -> SatisfactionResult event ty
handleEnd :: forall event ty.
(Ord event, Ord ty, Show ty) =>
(Int, Formula event ty) -> SatisfactionResult event ty
handleEnd (!Int
n, !Formula event ty
formula) =
    if (HomogeneousFormula -> Bool
eval (HomogeneousFormula -> Bool)
-> (Formula event ty -> HomogeneousFormula)
-> Formula event ty
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula event ty -> HomogeneousFormula
forall event a. Formula event a -> HomogeneousFormula
terminate) Formula event ty
formula
    then SatisfactionResult event ty
forall event ty. SatisfactionResult event ty
Satisfied
    else Relevance event ty -> SatisfactionResult event ty
forall event ty. Relevance event ty -> SatisfactionResult event ty
Unsatisfied (Formula event ty -> Relevance event ty
forall event ty.
(Ord event, Ord ty) =>
Formula event ty -> Relevance event ty
relevance Formula event ty
formula)

-- | Check if the formula is satisfied in the given event timeline.
satisfies :: (Event event ty, Ord event, Ord ty, Show ty, Foldable f)
          => OnMissingKey
          -> Formula event ty
          -> f event
          -> SatisfactionResult event ty
satisfies :: forall event ty (f :: * -> *).
(Event event ty, Ord event, Ord ty, Show ty, Foldable f) =>
OnMissingKey
-> Formula event ty -> f event -> SatisfactionResult event ty
satisfies OnMissingKey
omk Formula event ty
formula f event
xs = Either (SatisfactionResult event ty) (SatisfactionResult event ty)
-> SatisfactionResult event ty
forall a. Either a a -> a
fromEither (Either (SatisfactionResult event ty) (SatisfactionResult event ty)
 -> SatisfactionResult event ty)
-> Either
     (SatisfactionResult event ty) (SatisfactionResult event ty)
-> SatisfactionResult event ty
forall a b. (a -> b) -> a -> b
$ (Int, Formula event ty) -> SatisfactionResult event ty
forall event ty.
(Ord event, Ord ty, Show ty) =>
(Int, Formula event ty) -> SatisfactionResult event ty
handleEnd ((Int, Formula event ty) -> SatisfactionResult event ty)
-> Either (SatisfactionResult event ty) (Int, Formula event ty)
-> Either
     (SatisfactionResult event ty) (SatisfactionResult event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Either (SatisfactionResult event ty) (Int, Formula event ty)
 -> event
 -> Either (SatisfactionResult event ty) (Int, Formula event ty))
-> Either (SatisfactionResult event ty) (Int, Formula event ty)
-> f event
-> Either (SatisfactionResult event ty) (Int, Formula event ty)
forall b a. (b -> a -> b) -> b -> f a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Either (SatisfactionResult event ty) (Int, Formula event ty)
acc event
e -> Either (SatisfactionResult event ty) (Int, Formula event ty)
acc Either (SatisfactionResult event ty) (Int, Formula event ty)
-> ((Int, Formula event ty)
    -> Either (SatisfactionResult event ty) (Int, Formula event ty))
-> Either (SatisfactionResult event ty) (Int, Formula event ty)
forall a b.
Either (SatisfactionResult event ty) a
-> (a -> Either (SatisfactionResult event ty) b)
-> Either (SatisfactionResult event ty) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ((Int, Formula event ty)
 -> event
 -> Either (SatisfactionResult event ty) (Int, Formula event ty))
-> event
-> (Int, Formula event ty)
-> Either (SatisfactionResult event ty) (Int, Formula event ty)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (OnMissingKey
-> (Int, Formula event ty)
-> event
-> Either (SatisfactionResult event ty) (Int, Formula event ty)
forall event ty.
(Event event ty, Ord event, Ord ty, Show ty) =>
OnMissingKey
-> (Int, Formula event ty)
-> event
-> Either (SatisfactionResult event ty) (Int, Formula event ty)
handleNext OnMissingKey
omk) event
e) ((Int, Formula event ty)
-> Either (SatisfactionResult event ty) (Int, Formula event ty)
forall a b. b -> Either a b
Right (Int
0, Formula event ty
formula)) f event
xs
  where
    fromEither :: Either a a -> a
    fromEither :: forall a. Either a a -> a
fromEither = (a -> a) -> (a -> a) -> Either a a -> a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> a
forall a. a -> a
id a -> a
forall a. a -> a
id

data SatisfyMetrics event ty = SatisfyMetrics {
  forall event ty. SatisfyMetrics event ty -> Word64
eventsConsumed   :: Word64,
  forall event ty. SatisfyMetrics event ty -> Formula event ty
currentFormula   :: Formula event ty,
  -- | μs
  forall event ty. SatisfyMetrics event ty -> Word64
currentTimestamp :: Word64
}

-- | Given a formula and a stream of events, forms an `IO` computation that returns a `SatisfactionResult` once
--    the formula is equivalent to ⊤ or ⊥. This may happen either once the stream terminates or if
--    the formula is falsified early by some prefix of the stream.
satisfiesS :: (Event event ty, Ord event, Ord ty, Show ty)
           => OnMissingKey
           -> Formula event ty
           -> Stream (Of event) IO ()
           -> IORef (SatisfyMetrics event ty)
           -> IO (SatisfactionResult event ty)
satisfiesS :: forall event ty.
(Event event ty, Ord event, Ord ty, Show ty) =>
OnMissingKey
-> Formula event ty
-> Stream (Of event) IO ()
-> IORef (SatisfyMetrics event ty)
-> IO (SatisfactionResult event ty)
satisfiesS OnMissingKey
omk Formula event ty
formula_ Stream (Of event) IO ()
input_ IORef (SatisfyMetrics event ty)
metrics_ = Stream IO IO (SatisfactionResult event ty)
-> IO (SatisfactionResult event ty)
forall (m :: * -> *) r. Monad m => Stream m m r -> m r
run (Stream IO IO (SatisfactionResult event ty)
 -> IO (SatisfactionResult event ty))
-> Stream IO IO (SatisfactionResult event ty)
-> IO (SatisfactionResult event ty)
forall a b. (a -> b) -> a -> b
$ (forall x. Identity x -> IO (IO x))
-> Stream Identity IO (SatisfactionResult event ty)
-> Stream IO IO (SatisfactionResult event ty)
forall (m :: * -> *) (f :: * -> *) (g :: * -> *) r.
(Monad m, Functor f) =>
(forall x. f x -> m (g x)) -> Stream f m r -> Stream g m r
mapped (IO x -> IO (IO x)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure(IO x -> IO (IO x))
-> (Identity x -> IO x) -> Identity x -> IO (IO x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> IO x
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (x -> IO x) -> (Identity x -> x) -> Identity x -> IO x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity x -> x
forall a. Identity a -> a
runIdentity) (Stream Identity IO (SatisfactionResult event ty)
 -> Stream IO IO (SatisfactionResult event ty))
-> Stream Identity IO (SatisfactionResult event ty)
-> Stream IO IO (SatisfactionResult event ty)
forall a b. (a -> b) -> a -> b
$ ((Int, Formula event ty, Stream (Of event) IO ())
 -> IO
      (Either
         (SatisfactionResult event ty)
         (Identity (Int, Formula event ty, Stream (Of event) IO ()))))
-> (Int, Formula event ty, Stream (Of event) IO ())
-> Stream Identity IO (SatisfactionResult event ty)
forall (m :: * -> *) (f :: * -> *) s r.
(Monad m, Functor f) =>
(s -> m (Either r (f s))) -> s -> Stream f m r
unfold (IORef (SatisfyMetrics event ty)
-> (Int, Formula event ty, Stream (Of event) IO ())
-> IO
     (Either
        (SatisfactionResult event ty)
        (Identity (Int, Formula event ty, Stream (Of event) IO ())))
forall event ty.
(Event event ty, Ord event, Ord ty, Show ty) =>
IORef (SatisfyMetrics event ty)
-> (Int, Formula event ty, Stream (Of event) IO ())
-> IO
     (Either
        (SatisfactionResult event ty)
        (Identity (Int, Formula event ty, Stream (Of event) IO ())))
go IORef (SatisfyMetrics event ty)
metrics_) (Int
0, Formula event ty
formula_,  Stream (Of event) IO ()
input_) where
  go :: (Event event ty, Ord event, Ord ty, Show ty)
     => IORef (SatisfyMetrics event ty)
     -> (Int, Formula event ty, Stream (Of event) IO ())
     -> IO (Either (SatisfactionResult event ty) (Identity (Int, Formula event ty, Stream (Of event) IO ())))
  go :: forall event ty.
(Event event ty, Ord event, Ord ty, Show ty) =>
IORef (SatisfyMetrics event ty)
-> (Int, Formula event ty, Stream (Of event) IO ())
-> IO
     (Either
        (SatisfactionResult event ty)
        (Identity (Int, Formula event ty, Stream (Of event) IO ())))
go IORef (SatisfyMetrics event ty)
metrics (!Int
n, !Formula event ty
formula, !Stream (Of event) IO ()
input) = Stream (Of event) IO ()
-> IO (Either () (Of event (Stream (Of event) IO ())))
forall (m :: * -> *) (f :: * -> *) r.
Monad m =>
Stream f m r -> m (Either r (f (Stream f m r)))
inspect Stream (Of event) IO ()
input IO (Either () (Of event (Stream (Of event) IO ())))
-> (Either () (Of event (Stream (Of event) IO ()))
    -> IO
         (Either
            (SatisfactionResult event ty)
            (Identity (Int, Formula event ty, Stream (Of event) IO ()))))
-> IO
     (Either
        (SatisfactionResult event ty)
        (Identity (Int, Formula event ty, Stream (Of event) IO ())))
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Left () -> Either
  (SatisfactionResult event ty)
  (Identity (Int, Formula event ty, Stream (Of event) IO ()))
-> IO
     (Either
        (SatisfactionResult event ty)
        (Identity (Int, Formula event ty, Stream (Of event) IO ())))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either
   (SatisfactionResult event ty)
   (Identity (Int, Formula event ty, Stream (Of event) IO ()))
 -> IO
      (Either
         (SatisfactionResult event ty)
         (Identity (Int, Formula event ty, Stream (Of event) IO ()))))
-> Either
     (SatisfactionResult event ty)
     (Identity (Int, Formula event ty, Stream (Of event) IO ()))
-> IO
     (Either
        (SatisfactionResult event ty)
        (Identity (Int, Formula event ty, Stream (Of event) IO ())))
forall a b. (a -> b) -> a -> b
$ SatisfactionResult event ty
-> Either
     (SatisfactionResult event ty)
     (Identity (Int, Formula event ty, Stream (Of event) IO ()))
forall a b. a -> Either a b
Left (SatisfactionResult event ty
 -> Either
      (SatisfactionResult event ty)
      (Identity (Int, Formula event ty, Stream (Of event) IO ())))
-> SatisfactionResult event ty
-> Either
     (SatisfactionResult event ty)
     (Identity (Int, Formula event ty, Stream (Of event) IO ()))
forall a b. (a -> b) -> a -> b
$
      (Int, Formula event ty) -> SatisfactionResult event ty
forall event ty.
(Ord event, Ord ty, Show ty) =>
(Int, Formula event ty) -> SatisfactionResult event ty
handleEnd (Int
n, Formula event ty
formula)
    Right (event
event :> Stream (Of event) IO ()
more) -> do
      IORef (SatisfyMetrics event ty)
-> (SatisfyMetrics event ty -> SatisfyMetrics event ty) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef (SatisfyMetrics event ty)
metrics (\SatisfyMetrics event ty
x -> Word64 -> Formula event ty -> Word64 -> SatisfyMetrics event ty
forall event ty.
Word64 -> Formula event ty -> Word64 -> SatisfyMetrics event ty
SatisfyMetrics (Word64
1 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ SatisfyMetrics event ty
x.eventsConsumed) Formula event ty
formula (event -> Word64
forall a ty. Event a ty => a -> Word64
beg event
event))
      Either
  (SatisfactionResult event ty)
  (Identity (Int, Formula event ty, Stream (Of event) IO ()))
-> IO
     (Either
        (SatisfactionResult event ty)
        (Identity (Int, Formula event ty, Stream (Of event) IO ())))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either
   (SatisfactionResult event ty)
   (Identity (Int, Formula event ty, Stream (Of event) IO ()))
 -> IO
      (Either
         (SatisfactionResult event ty)
         (Identity (Int, Formula event ty, Stream (Of event) IO ()))))
-> Either
     (SatisfactionResult event ty)
     (Identity (Int, Formula event ty, Stream (Of event) IO ()))
-> IO
     (Either
        (SatisfactionResult event ty)
        (Identity (Int, Formula event ty, Stream (Of event) IO ())))
forall a b. (a -> b) -> a -> b
$
        ((Int, Formula event ty)
 -> Identity (Int, Formula event ty, Stream (Of event) IO ()))
-> Either (SatisfactionResult event ty) (Int, Formula event ty)
-> Either
     (SatisfactionResult event ty)
     (Identity (Int, Formula event ty, Stream (Of event) IO ()))
forall a b.
(a -> b)
-> Either (SatisfactionResult event ty) a
-> Either (SatisfactionResult event ty) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
          (\(!Int
n', !Formula event ty
formula') -> (Int, Formula event ty, Stream (Of event) IO ())
-> Identity (Int, Formula event ty, Stream (Of event) IO ())
forall a. a -> Identity a
Identity (Int
n', Formula event ty
formula', Stream (Of event) IO ()
more))
          (OnMissingKey
-> (Int, Formula event ty)
-> event
-> Either (SatisfactionResult event ty) (Int, Formula event ty)
forall event ty.
(Event event ty, Ord event, Ord ty, Show ty) =>
OnMissingKey
-> (Int, Formula event ty)
-> event
-> Either (SatisfactionResult event ty) (Int, Formula event ty)
handleNext OnMissingKey
omk (Int
n, Formula event ty
formula) event
event)