{-# LANGUAGE BangPatterns        #-}
{-# LANGUAGE DeriveFunctor       #-}
{-# LANGUAGE DeriveFoldable      #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Ouroboros.Network.Testing.Data.Signal
  ( -- * Events
    Events
  , eventsFromList
  , eventsFromListUpToTime
  , eventsToList
  , eventsToListWithId
  , selectEvents
    -- * Low level access
  , primitiveTransformEvents
  , TS (..)
  , E (..)
    -- * Signals
  , Signal (..)
  , mergeSignals
    -- ** Invariants
  , eventsInvariant
  , signalInvariant
    -- ** Construction and conversion
  , fromChangeEvents
  , toChangeEvents
  , fromEvents
  , fromEventsWith
    -- ** QuickCheck
  , signalProperty
    -- * Simple signal transformations
  , truncateAt
  , stable
  , nub
  , nubBy
    -- * Temporal operations
  , linger
  , timeout
  , until
  , difference
  , scanl
  , always
  , eventually
    -- * Set-based temporal operations
  , keyedTimeout
  , keyedLinger
  , keyedUntil
  ) where

import           Prelude hiding (scanl, until)

import           Data.Bool (bool)
import qualified Data.Foldable as Deque (toList)
import           Data.List (groupBy)
import           Data.Maybe (maybeToList)
import           Data.OrdPSQ (OrdPSQ)
import qualified Data.OrdPSQ as PSQ
import           Data.Set (Set)
import qualified Data.Set as Set
import           Deque.Lazy (Deque)
import qualified Deque.Lazy as Deque

import           Control.Monad.Class.MonadTime.SI (DiffTime, Time (..), addTime)


import           Test.QuickCheck

--
-- Time stamps and events
--

-- The instance Applicative Signal relies on merging event streams.
-- The IO simulator's treatment of time means that we can have many
-- events that occur at the same virtual time, though they are stil
-- causually ordered.
--
-- We need these compound time stamps to be able to resolve the order
-- of the events that have the same Time when merging event streams.
-- The compound time stamp records the event number from the original
-- trace, for events derivied from the original trace. For artificially
-- constructed events, they can use small or big counters to be ordered
-- before or after other events at the same time. Negative counters are
-- permitted for this purpose.

data TS = TS !Time !Int
  deriving (TS -> TS -> Bool
(TS -> TS -> Bool) -> (TS -> TS -> Bool) -> Eq TS
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TS -> TS -> Bool
== :: TS -> TS -> Bool
$c/= :: TS -> TS -> Bool
/= :: TS -> TS -> Bool
Eq, Eq TS
Eq TS =>
(TS -> TS -> Ordering)
-> (TS -> TS -> Bool)
-> (TS -> TS -> Bool)
-> (TS -> TS -> Bool)
-> (TS -> TS -> Bool)
-> (TS -> TS -> TS)
-> (TS -> TS -> TS)
-> Ord TS
TS -> TS -> Bool
TS -> TS -> Ordering
TS -> TS -> TS
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: TS -> TS -> Ordering
compare :: TS -> TS -> Ordering
$c< :: TS -> TS -> Bool
< :: TS -> TS -> Bool
$c<= :: TS -> TS -> Bool
<= :: TS -> TS -> Bool
$c> :: TS -> TS -> Bool
> :: TS -> TS -> Bool
$c>= :: TS -> TS -> Bool
>= :: TS -> TS -> Bool
$cmax :: TS -> TS -> TS
max :: TS -> TS -> TS
$cmin :: TS -> TS -> TS
min :: TS -> TS -> TS
Ord, Int -> TS -> ShowS
[TS] -> ShowS
TS -> String
(Int -> TS -> ShowS)
-> (TS -> String) -> ([TS] -> ShowS) -> Show TS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TS -> ShowS
showsPrec :: Int -> TS -> ShowS
$cshow :: TS -> String
show :: TS -> String
$cshowList :: [TS] -> ShowS
showList :: [TS] -> ShowS
Show)

-- A single event or entry in a time series, annotated with its timestamp.
--
data E a = E {-# UNPACK #-} !TS a
  deriving (Int -> E a -> ShowS
[E a] -> ShowS
E a -> String
(Int -> E a -> ShowS)
-> (E a -> String) -> ([E a] -> ShowS) -> Show (E a)
forall a. Show a => Int -> E a -> ShowS
forall a. Show a => [E a] -> ShowS
forall a. Show a => E a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> E a -> ShowS
showsPrec :: Int -> E a -> ShowS
$cshow :: forall a. Show a => E a -> String
show :: E a -> String
$cshowList :: forall a. Show a => [E a] -> ShowS
showList :: [E a] -> ShowS
Show, (forall a b. (a -> b) -> E a -> E b)
-> (forall a b. a -> E b -> E a) -> Functor E
forall a b. a -> E b -> E a
forall a b. (a -> b) -> E a -> E b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> E a -> E b
fmap :: forall a b. (a -> b) -> E a -> E b
$c<$ :: forall a b. a -> E b -> E a
<$ :: forall a b. a -> E b -> E a
Functor, (forall m. Monoid m => E m -> m)
-> (forall m a. Monoid m => (a -> m) -> E a -> m)
-> (forall m a. Monoid m => (a -> m) -> E a -> m)
-> (forall a b. (a -> b -> b) -> b -> E a -> b)
-> (forall a b. (a -> b -> b) -> b -> E a -> b)
-> (forall b a. (b -> a -> b) -> b -> E a -> b)
-> (forall b a. (b -> a -> b) -> b -> E a -> b)
-> (forall a. (a -> a -> a) -> E a -> a)
-> (forall a. (a -> a -> a) -> E a -> a)
-> (forall a. E a -> [a])
-> (forall a. E a -> Bool)
-> (forall a. E a -> Int)
-> (forall a. Eq a => a -> E a -> Bool)
-> (forall a. Ord a => E a -> a)
-> (forall a. Ord a => E a -> a)
-> (forall a. Num a => E a -> a)
-> (forall a. Num a => E a -> a)
-> Foldable E
forall a. Eq a => a -> E a -> Bool
forall a. Num a => E a -> a
forall a. Ord a => E a -> a
forall m. Monoid m => E m -> m
forall a. E a -> Bool
forall a. E a -> Int
forall a. E a -> [a]
forall a. (a -> a -> a) -> E a -> a
forall m a. Monoid m => (a -> m) -> E a -> m
forall b a. (b -> a -> b) -> b -> E a -> b
forall a b. (a -> b -> b) -> b -> E a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => E m -> m
fold :: forall m. Monoid m => E m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> E a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> E a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> E a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> E a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> E a -> b
foldr :: forall a b. (a -> b -> b) -> b -> E a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> E a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> E a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> E a -> b
foldl :: forall b a. (b -> a -> b) -> b -> E a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> E a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> E a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> E a -> a
foldr1 :: forall a. (a -> a -> a) -> E a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> E a -> a
foldl1 :: forall a. (a -> a -> a) -> E a -> a
$ctoList :: forall a. E a -> [a]
toList :: forall a. E a -> [a]
$cnull :: forall a. E a -> Bool
null :: forall a. E a -> Bool
$clength :: forall a. E a -> Int
length :: forall a. E a -> Int
$celem :: forall a. Eq a => a -> E a -> Bool
elem :: forall a. Eq a => a -> E a -> Bool
$cmaximum :: forall a. Ord a => E a -> a
maximum :: forall a. Ord a => E a -> a
$cminimum :: forall a. Ord a => E a -> a
minimum :: forall a. Ord a => E a -> a
$csum :: forall a. Num a => E a -> a
sum :: forall a. Num a => E a -> a
$cproduct :: forall a. Num a => E a -> a
product :: forall a. Num a => E a -> a
Foldable)


--
-- Events
--

-- | A time-ordered trace of discrete events that occur at specific times.
--
-- This corresponds for example to a trace of events or observations from a
-- simulation.
--
newtype Events a = Events [E a]
  deriving (Int -> Events a -> ShowS
[Events a] -> ShowS
Events a -> String
(Int -> Events a -> ShowS)
-> (Events a -> String) -> ([Events a] -> ShowS) -> Show (Events a)
forall a. Show a => Int -> Events a -> ShowS
forall a. Show a => [Events a] -> ShowS
forall a. Show a => Events a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Events a -> ShowS
showsPrec :: Int -> Events a -> ShowS
$cshow :: forall a. Show a => Events a -> String
show :: Events a -> String
$cshowList :: forall a. Show a => [Events a] -> ShowS
showList :: [Events a] -> ShowS
Show, (forall a b. (a -> b) -> Events a -> Events b)
-> (forall a b. a -> Events b -> Events a) -> Functor Events
forall a b. a -> Events b -> Events a
forall a b. (a -> b) -> Events a -> Events b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Events a -> Events b
fmap :: forall a b. (a -> b) -> Events a -> Events b
$c<$ :: forall a b. a -> Events b -> Events a
<$ :: forall a b. a -> Events b -> Events a
Functor, (forall m. Monoid m => Events m -> m)
-> (forall m a. Monoid m => (a -> m) -> Events a -> m)
-> (forall m a. Monoid m => (a -> m) -> Events a -> m)
-> (forall a b. (a -> b -> b) -> b -> Events a -> b)
-> (forall a b. (a -> b -> b) -> b -> Events a -> b)
-> (forall b a. (b -> a -> b) -> b -> Events a -> b)
-> (forall b a. (b -> a -> b) -> b -> Events a -> b)
-> (forall a. (a -> a -> a) -> Events a -> a)
-> (forall a. (a -> a -> a) -> Events a -> a)
-> (forall a. Events a -> [a])
-> (forall a. Events a -> Bool)
-> (forall a. Events a -> Int)
-> (forall a. Eq a => a -> Events a -> Bool)
-> (forall a. Ord a => Events a -> a)
-> (forall a. Ord a => Events a -> a)
-> (forall a. Num a => Events a -> a)
-> (forall a. Num a => Events a -> a)
-> Foldable Events
forall a. Eq a => a -> Events a -> Bool
forall a. Num a => Events a -> a
forall a. Ord a => Events a -> a
forall m. Monoid m => Events m -> m
forall a. Events a -> Bool
forall a. Events a -> Int
forall a. Events a -> [a]
forall a. (a -> a -> a) -> Events a -> a
forall m a. Monoid m => (a -> m) -> Events a -> m
forall b a. (b -> a -> b) -> b -> Events a -> b
forall a b. (a -> b -> b) -> b -> Events a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Events m -> m
fold :: forall m. Monoid m => Events m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Events a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Events a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Events a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Events a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Events a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Events a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Events a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Events a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Events a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Events a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Events a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Events a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Events a -> a
foldr1 :: forall a. (a -> a -> a) -> Events a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Events a -> a
foldl1 :: forall a. (a -> a -> a) -> Events a -> a
$ctoList :: forall a. Events a -> [a]
toList :: forall a. Events a -> [a]
$cnull :: forall a. Events a -> Bool
null :: forall a. Events a -> Bool
$clength :: forall a. Events a -> Int
length :: forall a. Events a -> Int
$celem :: forall a. Eq a => a -> Events a -> Bool
elem :: forall a. Eq a => a -> Events a -> Bool
$cmaximum :: forall a. Ord a => Events a -> a
maximum :: forall a. Ord a => Events a -> a
$cminimum :: forall a. Ord a => Events a -> a
minimum :: forall a. Ord a => Events a -> a
$csum :: forall a. Num a => Events a -> a
sum :: forall a. Num a => Events a -> a
$cproduct :: forall a. Num a => Events a -> a
product :: forall a. Num a => Events a -> a
Foldable)

-- | Construct 'Events' from a time series.
--
eventsFromList :: [(Time, a)] -> Events a
eventsFromList :: forall a. [(Time, a)] -> Events a
eventsFromList [(Time, a)]
txs =
    [E a] -> Events a
forall a. [E a] -> Events a
Events [ TS -> a -> E a
forall a. TS -> a -> E a
E (Time -> Int -> TS
TS Time
t Int
i) a
x
           | ((Time
t, a
x), Int
i) <- [(Time, a)] -> [Int] -> [((Time, a), Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Time, a)]
txs [Int
100, Int
102..] ]

-- | Construct 'Events' from a time series.
--
-- The time series is truncated at (but not including) the given time. This is
-- necessary to check properties over finite prefixes of infinite time series.
--
eventsFromListUpToTime :: Time -> [(Time, a)] -> Events a
eventsFromListUpToTime :: forall a. Time -> [(Time, a)] -> Events a
eventsFromListUpToTime Time
horizon =
  [(Time, a)] -> Events a
forall a. [(Time, a)] -> Events a
eventsFromList ([(Time, a)] -> Events a)
-> ([(Time, a)] -> [(Time, a)]) -> [(Time, a)] -> Events a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Time, a) -> Bool) -> [(Time, a)] -> [(Time, a)]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (\(Time
t,a
_) -> Time
t Time -> Time -> Bool
forall a. Ord a => a -> a -> Bool
< Time
horizon)

eventsToList :: Events a -> [(Time, a)]
eventsToList :: forall a. Events a -> [(Time, a)]
eventsToList (Events [E a]
txs) = [ (Time
t, a
x) | E (TS Time
t Int
_i) a
x <- [E a]
txs ]

eventsToListWithId :: Events a -> [E a]
eventsToListWithId :: forall a. Events a -> [E a]
eventsToListWithId (Events [E a]
txs) = [E a]
txs

selectEvents :: (a -> Maybe b) -> Events a -> Events b
selectEvents :: forall a b. (a -> Maybe b) -> Events a -> Events b
selectEvents a -> Maybe b
select (Events [E a]
txs) =
    [E b] -> Events b
forall a. [E a] -> Events a
Events [ TS -> b -> E b
forall a. TS -> a -> E a
E TS
t b
y | E TS
t a
x <- [E a]
txs, b
y <- Maybe b -> [b]
forall a. Maybe a -> [a]
maybeToList (a -> Maybe b
select a
x) ]

primitiveTransformEvents :: ([E a] -> [E b]) -> Events a -> Events b
primitiveTransformEvents :: forall a b. ([E a] -> [E b]) -> Events a -> Events b
primitiveTransformEvents [E a] -> [E b]
f (Events [E a]
txs) = [E b] -> Events b
forall a. [E a] -> Events a
Events ([E a] -> [E b]
f [E a]
txs)

-- | Events are all ordered by time and causal order
--
eventsInvariant :: Events a -> Bool
eventsInvariant :: forall a. Events a -> Bool
eventsInvariant (Events [])  = Bool
True
eventsInvariant (Events [E a
_]) = Bool
True
eventsInvariant (Events ((E (TS Time
t Int
i) a
_) : (E (TS Time
t' Int
i') a
_) : [E a]
es)) =
  Time
t Time -> Time -> Bool
forall a. Ord a => a -> a -> Bool
<= Time
t' Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
i' Bool -> Bool -> Bool
&& Events a -> Bool
forall a. Events a -> Bool
eventsInvariant ([E a] -> Events a
forall a. [E a] -> Events a
Events [E a]
es)

--
-- Signals
--

-- | A signal is a time-varying value. It has a value at all times. It changes
-- value at discrete times, i.e. it is not continuous.
--
data Signal a = Signal a     -- ^ Initital signal value
                       [E a] -- ^ List of discrete times at which the signal
                             --   changes to a given value.
  deriving (Int -> Signal a -> ShowS
[Signal a] -> ShowS
Signal a -> String
(Int -> Signal a -> ShowS)
-> (Signal a -> String) -> ([Signal a] -> ShowS) -> Show (Signal a)
forall a. Show a => Int -> Signal a -> ShowS
forall a. Show a => [Signal a] -> ShowS
forall a. Show a => Signal a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Signal a -> ShowS
showsPrec :: Int -> Signal a -> ShowS
$cshow :: forall a. Show a => Signal a -> String
show :: Signal a -> String
$cshowList :: forall a. Show a => [Signal a] -> ShowS
showList :: [Signal a] -> ShowS
Show, (forall a b. (a -> b) -> Signal a -> Signal b)
-> (forall a b. a -> Signal b -> Signal a) -> Functor Signal
forall a b. a -> Signal b -> Signal a
forall a b. (a -> b) -> Signal a -> Signal b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Signal a -> Signal b
fmap :: forall a b. (a -> b) -> Signal a -> Signal b
$c<$ :: forall a b. a -> Signal b -> Signal a
<$ :: forall a b. a -> Signal b -> Signal a
Functor)

instance Applicative Signal where
    pure :: forall a. a -> Signal a
pure  a
x = a -> [E a] -> Signal a
forall a. a -> [E a] -> Signal a
Signal a
x []
    Signal (a -> b)
f <*> :: forall a b. Signal (a -> b) -> Signal a -> Signal b
<*> Signal a
x = Signal (a -> b) -> Signal a -> Signal b
forall a b. Signal (a -> b) -> Signal a -> Signal b
mergeSignals Signal (a -> b)
f Signal a
x

-- | Signal time changing events are all ordered by timestamp and causal order
--
signalInvariant :: Signal a -> Bool
signalInvariant :: forall a. Signal a -> Bool
signalInvariant (Signal a
_ [E a]
es) =
  Events a -> Bool
forall a. Events a -> Bool
eventsInvariant ([E a] -> Events a
forall a. [E a] -> Events a
Events [E a]
es)

mergeSignals :: Signal (a -> b) -> Signal a -> Signal b
mergeSignals :: forall a b. Signal (a -> b) -> Signal a -> Signal b
mergeSignals (Signal a -> b
f0 [E (a -> b)]
fs0) (Signal a
x0 [E a]
xs0) =
    b -> [E b] -> Signal b
forall a. a -> [E a] -> Signal a
Signal (a -> b
f0 a
x0) ((a -> b) -> a -> [MergeResult (E (a -> b)) (E a)] -> [E b]
forall a b.
(a -> b) -> a -> [MergeResult (E (a -> b)) (E a)] -> [E b]
go a -> b
f0 a
x0 ((E (a -> b) -> E a -> Ordering)
-> [E (a -> b)] -> [E a] -> [MergeResult (E (a -> b)) (E a)]
forall a b. (a -> b -> Ordering) -> [a] -> [b] -> [MergeResult a b]
mergeBy E (a -> b) -> E a -> Ordering
forall a b. E a -> E b -> Ordering
compareTimestamp [E (a -> b)]
fs0 [E a]
xs0))
  where
    go :: (a -> b) -> a -> [MergeResult (E (a -> b)) (E a)] -> [E b]
    go :: forall a b.
(a -> b) -> a -> [MergeResult (E (a -> b)) (E a)] -> [E b]
go a -> b
_ a
_ []                                  = []
    go a -> b
_ a
x (OnlyInLeft   (E TS
t a -> b
f)         : [MergeResult (E (a -> b)) (E a)]
rs) = TS -> b -> E b
forall a. TS -> a -> E a
E TS
t (a -> b
f a
x) E b -> [E b] -> [E b]
forall a. a -> [a] -> [a]
: (a -> b) -> a -> [MergeResult (E (a -> b)) (E a)] -> [E b]
forall a b.
(a -> b) -> a -> [MergeResult (E (a -> b)) (E a)] -> [E b]
go a -> b
f a
x [MergeResult (E (a -> b)) (E a)]
rs
    go a -> b
f a
_ (OnlyInRight          (E TS
t a
x) : [MergeResult (E (a -> b)) (E a)]
rs) = TS -> b -> E b
forall a. TS -> a -> E a
E TS
t (a -> b
f a
x) E b -> [E b] -> [E b]
forall a. a -> [a] -> [a]
: (a -> b) -> a -> [MergeResult (E (a -> b)) (E a)] -> [E b]
forall a b.
(a -> b) -> a -> [MergeResult (E (a -> b)) (E a)] -> [E b]
go a -> b
f a
x [MergeResult (E (a -> b)) (E a)]
rs
    go a -> b
_ a
_ (InBoth       (E TS
t a -> b
f) (E TS
_ a
x) : [MergeResult (E (a -> b)) (E a)]
rs) = TS -> b -> E b
forall a. TS -> a -> E a
E TS
t (a -> b
f a
x) E b -> [E b] -> [E b]
forall a. a -> [a] -> [a]
: (a -> b) -> a -> [MergeResult (E (a -> b)) (E a)] -> [E b]
forall a b.
(a -> b) -> a -> [MergeResult (E (a -> b)) (E a)] -> [E b]
go a -> b
f a
x [MergeResult (E (a -> b)) (E a)]
rs

compareTimestamp :: E a -> E b -> Ordering
compareTimestamp :: forall a b. E a -> E b -> Ordering
compareTimestamp (E TS
ts a
_) (E TS
ts' b
_) = TS -> TS -> Ordering
forall a. Ord a => a -> a -> Ordering
compare TS
ts TS
ts'

-- | Construct a 'Signal' from an initial value and a time series of events
-- that represent new values of the signal.
--
-- This only makes sense for events that sample a single time-varying value.
--
fromChangeEvents :: a -> Events a -> Signal a
fromChangeEvents :: forall a. a -> Events a -> Signal a
fromChangeEvents a
x (Events [E a]
xs) = a -> [E a] -> Signal a
forall a. a -> [E a] -> Signal a
Signal a
x [E a]
xs

-- | Convert a 'Signal' into a time series of events when the signal value
-- changes.
--
toChangeEvents :: Signal a -> Events a
toChangeEvents :: forall a. Signal a -> Events a
toChangeEvents = [E a] -> Events a
forall a. [E a] -> Events a
Events ([E a] -> Events a) -> (Signal a -> [E a]) -> Signal a -> Events a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signal a -> [E a]
forall a. Signal a -> [E a]
toTimeSeries

toTimeSeries :: Signal a -> [E a]
toTimeSeries :: forall a. Signal a -> [E a]
toTimeSeries (Signal a
x [E a]
xs) = TS -> a -> E a
forall a. TS -> a -> E a
E (Time -> Int -> TS
TS (DiffTime -> Time
Time DiffTime
0) Int
0) a
x E a -> [E a] -> [E a]
forall a. a -> [a] -> [a]
: [E a]
xs

-- | Construct a 'Signal' that represents a time series of discrete events. The
-- signal is @Just@ the event value at the time of the event, and is @Nothing@
-- at all other times.
--
-- Note that this signal \"instantaneously\" takes the event value and reverts
-- to @Nothing@ before time moves on. Therefore this kind of signal is not
-- \"stable\" in the sense of 'stableSignal'.
--
fromEvents :: Events a -> Signal (Maybe a)
fromEvents :: forall a. Events a -> Signal (Maybe a)
fromEvents (Events [E a]
txs) =
    Maybe a -> [E (Maybe a)] -> Signal (Maybe a)
forall a. a -> [E a] -> Signal a
Signal Maybe a
forall a. Maybe a
Nothing
           [ TS -> Maybe a -> E (Maybe a)
forall a. TS -> a -> E a
E (Time -> Int -> TS
TS Time
t Int
i') Maybe a
s
           | E (TS Time
t Int
i) a
x <- [E a]
txs
           , (Int
i', Maybe a
s) <- [(Int
i, a -> Maybe a
forall a. a -> Maybe a
Just a
x), (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, Maybe a
forall a. Maybe a
Nothing)]
           ]


-- | Like 'fromEvents' but it is using the given value 'a' instead of 'Nothing.
-- It is equivalent to `\a -> fmap (fromMaybe a) . fromEvents`
--
fromEventsWith :: a -> Events a -> Signal a
fromEventsWith :: forall a. a -> Events a -> Signal a
fromEventsWith a
a (Events [E a]
txs) =
    a -> [E a] -> Signal a
forall a. a -> [E a] -> Signal a
Signal a
a
           [ TS -> a -> E a
forall a. TS -> a -> E a
E (Time -> Int -> TS
TS Time
t Int
i') a
s
           | E (TS Time
t Int
i) a
x <- [E a]
txs
           , (Int
i', a
s) <- [(Int
i, a
x), (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, a
a)]
           ]

-- | A signal can change value more than once at a single point of time.
--
-- Sometimes we are interested only in the final \"stable\" value of the signal
-- before time moves on. This function discards the other values, keeping only
-- the final value at each time.
--
stable :: Signal a -> Signal a
stable :: forall a. Signal a -> Signal a
stable (Signal a
x [E a]
xs) =
    a -> [E a] -> Signal a
forall a. a -> [E a] -> Signal a
Signal a
x ((([E a] -> E a) -> [[E a]] -> [E a]
forall a b. (a -> b) -> [a] -> [b]
map [E a] -> E a
forall a. HasCallStack => [a] -> a
last ([[E a]] -> [E a]) -> ([E a] -> [[E a]]) -> [E a] -> [E a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (E a -> E a -> Bool) -> [E a] -> [[E a]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy E a -> E a -> Bool
forall {a} {a}. E a -> E a -> Bool
sameTime) [E a]
xs)
  where
    sameTime :: E a -> E a -> Bool
sameTime (E (TS Time
t Int
_) a
_) (E (TS Time
t' Int
_) a
_) = Time
t Time -> Time -> Bool
forall a. Eq a => a -> a -> Bool
== Time
t'

-- Truncate a 'Signal' after a given time. This is typically necessary to
-- check properties over finite prefixes of infinite signals.
--
truncateAt :: Time -> Signal a -> Signal a
truncateAt :: forall a. Time -> Signal a -> Signal a
truncateAt Time
horizon (Signal a
x [E a]
txs) =
    a -> [E a] -> Signal a
forall a. a -> [E a] -> Signal a
Signal a
x ((E a -> Bool) -> [E a] -> [E a]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (\(E (TS Time
t Int
_) a
_) -> Time
t Time -> Time -> Bool
forall a. Ord a => a -> a -> Bool
< Time
horizon) [E a]
txs)

-- | Sometimes the way a signal is constructed leads to duplicate signal values
-- which can slow down signal processing. This tidies up the signal by
-- eliminating the duplicates. This does not change the meaning (provided the
-- 'Eq' instance is true equality).
--
nub :: Eq a => Signal a -> Signal a
nub :: forall a. Eq a => Signal a -> Signal a
nub = (a -> a -> Bool) -> Signal a -> Signal a
forall a. (a -> a -> Bool) -> Signal a -> Signal a
nubBy a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==)

nubBy :: (a -> a -> Bool) -> Signal a -> Signal a
nubBy :: forall a. (a -> a -> Bool) -> Signal a -> Signal a
nubBy a -> a -> Bool
eq (Signal a
x0 [E a]
xs0) =
    a -> [E a] -> Signal a
forall a. a -> [E a] -> Signal a
Signal a
x0 (a -> [E a] -> [E a]
go a
x0 [E a]
xs0)
  where
    go :: a -> [E a] -> [E a]
go a
_ [] = []
    go a
x (E TS
t a
x' : [E a]
xs)
      | a
x a -> a -> Bool
`eq` a
x' = a -> [E a] -> [E a]
go a
x [E a]
xs
      | Bool
otherwise = TS -> a -> E a
forall a. TS -> a -> E a
E TS
t a
x' E a -> [E a] -> [E a]
forall a. a -> [a] -> [a]
: a -> [E a] -> [E a]
go a
x' [E a]
xs


-- | A linger signal remains @True@ for the given time after the underlying
-- signal is @True@.
--
linger :: DiffTime
       -> (a -> Bool)
       -> Signal a
       -> Signal Bool
linger :: forall a. DiffTime -> (a -> Bool) -> Signal a -> Signal Bool
linger DiffTime
d a -> Bool
arm =
    (Set () -> Bool) -> Signal (Set ()) -> Signal Bool
forall a b. (a -> b) -> Signal a -> Signal b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Bool -> Bool
not (Bool -> Bool) -> (Set () -> Bool) -> Set () -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set () -> Bool
forall a. Set a -> Bool
Set.null)
  (Signal (Set ()) -> Signal Bool)
-> (Signal a -> Signal (Set ())) -> Signal a -> Signal Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DiffTime -> (a -> Set ()) -> Signal a -> Signal (Set ())
forall a b.
Ord b =>
DiffTime -> (a -> Set b) -> Signal a -> Signal (Set b)
keyedLinger DiffTime
d (Set () -> Set () -> Bool -> Set ()
forall a. a -> a -> Bool -> a
bool Set ()
forall a. Set a
Set.empty (() -> Set ()
forall a. a -> Set a
Set.singleton ()) (Bool -> Set ()) -> (a -> Bool) -> a -> Set ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Bool
arm)


-- | Make a timeout signal, based on observing an underlying signal.
--
-- The timeout signal takes the value @True@ when the timeout has occurred, and
-- @False@ otherwise.
--
-- The timeout is controlled by an \"arming\" function on the underlying signal.
-- The arming function should return @True@ when the timeout should be started,
-- and it returns the time to wait before the timeout fires. The arming function
-- should return @False@ when the timeout should be cancelled or not started.
--
-- The output signal becomes @True@ when the arming function has been
-- continuously active (i.e. returning @True@) for the given duration.
--
timeout :: forall a.
           DiffTime    -- ^ timeout duration
        -> (a -> Bool) -- ^ the arming function
        -> Signal a
        -> Signal Bool
timeout :: forall a. DiffTime -> (a -> Bool) -> Signal a -> Signal Bool
timeout DiffTime
d a -> Bool
arm =
    (Set () -> Bool) -> Signal (Set ()) -> Signal Bool
forall a b. (a -> b) -> Signal a -> Signal b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Bool -> Bool
not (Bool -> Bool) -> (Set () -> Bool) -> Set () -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set () -> Bool
forall a. Set a -> Bool
Set.null)
  (Signal (Set ()) -> Signal Bool)
-> (Signal a -> Signal (Set ())) -> Signal a -> Signal Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DiffTime -> (a -> Set ()) -> Signal a -> Signal (Set ())
forall a b.
Ord b =>
DiffTime -> (a -> Set b) -> Signal a -> Signal (Set b)
keyedTimeout DiffTime
d (Set () -> Set () -> Bool -> Set ()
forall a. a -> a -> Bool -> a
bool Set ()
forall a. Set a
Set.empty (() -> Set ()
forall a. a -> Set a
Set.singleton ()) (Bool -> Set ()) -> (a -> Bool) -> a -> Set ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Bool
arm)


until :: (a -> Bool) -- ^ Start
      -> (a -> Bool) -- ^ Stop
      -> Signal a
      -> Signal Bool
until :: forall a. (a -> Bool) -> (a -> Bool) -> Signal a -> Signal Bool
until a -> Bool
start a -> Bool
stop =
    (Set () -> Bool) -> Signal (Set ()) -> Signal Bool
forall a b. (a -> b) -> Signal a -> Signal b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Bool -> Bool
not (Bool -> Bool) -> (Set () -> Bool) -> Set () -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set () -> Bool
forall a. Set a -> Bool
Set.null)
  (Signal (Set ()) -> Signal Bool)
-> (Signal a -> Signal (Set ())) -> Signal a -> Signal Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Set ())
-> (a -> Set ()) -> (a -> Bool) -> Signal a -> Signal (Set ())
forall a b.
Ord b =>
(a -> Set b)
-> (a -> Set b) -> (a -> Bool) -> Signal a -> Signal (Set b)
keyedUntil (Set () -> Set () -> Bool -> Set ()
forall a. a -> a -> Bool -> a
bool Set ()
forall a. Set a
Set.empty (() -> Set ()
forall a. a -> Set a
Set.singleton ()) (Bool -> Set ()) -> (a -> Bool) -> a -> Set ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Bool
start)
               (Set () -> Set () -> Bool -> Set ()
forall a. a -> a -> Bool -> a
bool Set ()
forall a. Set a
Set.empty (() -> Set ()
forall a. a -> Set a
Set.singleton ()) (Bool -> Set ()) -> (a -> Bool) -> a -> Set ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Bool
stop)
               (Bool -> a -> Bool
forall a b. a -> b -> a
const Bool
False)


-- | Make a signal that keeps track of recent activity, based on observing an
-- underlying signal.
--
-- The underlying signal is scrutinised with the provided \"activity interest\"
-- function that tells us if the signal value is activity of interest to track.
-- If it is, the given key is entered into the result signal set for the given
-- time duration. If the same activity occurs again before the duration expires
-- then the expiry will be extended to the new deadline (it is not cumulative).
-- The key will be removed from the result signal set when it expires.
--
-- Example: We cannot directly verify successful promotions due to certain
-- constraints (network attenuations), but we can ensure that the system takes
-- all promotion opportunities. To achieve this, we need to discard peers that
-- we have attempted to connect during the backoff period. For every failure
-- event in the input signal, we want to produce a signal that includes those
-- events for a specified duration. This allows us to then combine the trace
-- with all promotion opportunities and all the failed attempts and discard
-- those. This allow us to correctly identify valid promotion opportunities.
--
keyedLinger :: forall a b. Ord b
            => DiffTime
            -> (a -> Set b)  -- ^ The activity set signal
            -> Signal a
            -> Signal (Set b)
keyedLinger :: forall a b.
Ord b =>
DiffTime -> (a -> Set b) -> Signal a -> Signal (Set b)
keyedLinger DiffTime
d a -> Set b
arm =
    Set b -> [E (Set b)] -> Signal (Set b)
forall a. a -> [E a] -> Signal a
Signal Set b
forall a. Set a
Set.empty
  ([E (Set b)] -> Signal (Set b))
-> (Signal a -> [E (Set b)]) -> Signal a -> Signal (Set b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set b -> OrdPSQ b Time () -> [E (Set b)] -> [E (Set b)]
go Set b
forall a. Set a
Set.empty OrdPSQ b Time ()
forall k p v. OrdPSQ k p v
PSQ.empty
  ([E (Set b)] -> [E (Set b)])
-> (Signal a -> [E (Set b)]) -> Signal a -> [E (Set b)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signal (Set b) -> [E (Set b)]
forall a. Signal a -> [E a]
toTimeSeries
  (Signal (Set b) -> [E (Set b)])
-> (Signal a -> Signal (Set b)) -> Signal a -> [E (Set b)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Set b) -> Signal a -> Signal (Set b)
forall a b. (a -> b) -> Signal a -> Signal b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Set b
arm
  where
    go :: Set b
       -> OrdPSQ b Time ()
       -> [E (Set b)]
       -> [E (Set b)]
    go :: Set b -> OrdPSQ b Time () -> [E (Set b)] -> [E (Set b)]
go !Set b
_ !OrdPSQ b Time ()
_ [] = []

    go !Set b
lingerSet !OrdPSQ b Time ()
lingerPSQ (E ts :: TS
ts@(TS Time
t Int
_) Set b
xs : [E (Set b)]
txs)
      | Just (b
y, Time
t', ()
_, OrdPSQ b Time ()
lingerPSQ') <- OrdPSQ b Time () -> Maybe (b, Time, (), OrdPSQ b Time ())
forall k p v.
(Ord k, Ord p) =>
OrdPSQ k p v -> Maybe (k, p, v, OrdPSQ k p v)
PSQ.minView OrdPSQ b Time ()
lingerPSQ
      , Time
t' Time -> Time -> Bool
forall a. Ord a => a -> a -> Bool
< Time
t
      , ([(b, Time, ())]
ys, OrdPSQ b Time ()
lingerPSQ'') <- Time -> OrdPSQ b Time () -> ([(b, Time, ())], OrdPSQ b Time ())
forall k p v.
(Ord k, Ord p) =>
p -> OrdPSQ k p v -> ([(k, p, v)], OrdPSQ k p v)
PSQ.atMostView Time
t' OrdPSQ b Time ()
lingerPSQ'
      , let armed :: Set b
armed = [b] -> Set b
forall a. Ord a => [a] -> Set a
Set.fromList ([b] -> Set b) -> [b] -> Set b
forall a b. (a -> b) -> a -> b
$ b
y b -> [b] -> [b]
forall a. a -> [a] -> [a]
: ((b, Time, ()) -> b) -> [(b, Time, ())] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (\(b
a, Time
_, ()
_) -> b
a) [(b, Time, ())]
ys
            lingerSet' :: Set b
lingerSet' = Set b -> Set b -> Set b
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set b
lingerSet Set b
armed
      = TS -> Set b -> E (Set b)
forall a. TS -> a -> E a
E (Time -> Int -> TS
TS Time
t' Int
0) Set b
lingerSet' E (Set b) -> [E (Set b)] -> [E (Set b)]
forall a. a -> [a] -> [a]
: Set b -> OrdPSQ b Time () -> [E (Set b)] -> [E (Set b)]
go Set b
lingerSet' OrdPSQ b Time ()
lingerPSQ'' (TS -> Set b -> E (Set b)
forall a. TS -> a -> E a
E TS
ts Set b
xs E (Set b) -> [E (Set b)] -> [E (Set b)]
forall a. a -> [a] -> [a]
: [E (Set b)]
txs)

    go !Set b
lingerSet !OrdPSQ b Time ()
lingerPSQ (E ts :: TS
ts@(TS Time
t Int
_) Set b
x : [E (Set b)]
txs) =
      let lingerSet' :: Set b
lingerSet' = Set b
lingerSet Set b -> Set b -> Set b
forall a. Semigroup a => a -> a -> a
<> Set b
x
          t' :: Time
t'         = DiffTime -> Time -> Time
addTime DiffTime
d Time
t
          lingerPSQ' :: OrdPSQ b Time ()
lingerPSQ' = (OrdPSQ b Time () -> b -> OrdPSQ b Time ())
-> OrdPSQ b Time () -> Set b -> OrdPSQ b Time ()
forall a b. (a -> b -> a) -> a -> Set b -> a
Set.foldl' (\OrdPSQ b Time ()
s b
y -> b -> Time -> () -> OrdPSQ b Time () -> OrdPSQ b Time ()
forall k p v.
(Ord k, Ord p) =>
k -> p -> v -> OrdPSQ k p v -> OrdPSQ k p v
PSQ.insert b
y Time
t' () OrdPSQ b Time ()
s) OrdPSQ b Time ()
lingerPSQ Set b
x
       in if Set b
lingerSet' Set b -> Set b -> Bool
forall a. Eq a => a -> a -> Bool
/= Set b
lingerSet
            then TS -> Set b -> E (Set b)
forall a. TS -> a -> E a
E TS
ts Set b
lingerSet' E (Set b) -> [E (Set b)] -> [E (Set b)]
forall a. a -> [a] -> [a]
: Set b -> OrdPSQ b Time () -> [E (Set b)] -> [E (Set b)]
go Set b
lingerSet' OrdPSQ b Time ()
lingerPSQ' [E (Set b)]
txs
            else                   Set b -> OrdPSQ b Time () -> [E (Set b)] -> [E (Set b)]
go Set b
lingerSet' OrdPSQ b Time ()
lingerPSQ' [E (Set b)]
txs

-- | Make a signal that says if a given event longed at least a certain time
-- (timeout), based on observing an underlying signal.
--
-- The underlying signal is scrutinised with the provided \"timeout arming\"
-- function that tells us if the signal value is interesting to track.
-- If it is, we arm it with a timeout and see, if until the timeout goes off
-- there's no other event to arm. If any activity occurs again before the
-- previous timeout, then the timeout is reset with the new event and the other
-- one is discarded.
--
-- Example: We have a signal that tracks if a button is pressed or not, i.e.
-- it's true if it is pressed and false otherwise. Then `timeout 5 id s` will
-- return a signal that checks whether the button is left pressed for at least
-- 5 seconds. So the output signal becomes true if the button remains pressed
-- for 5 continuous seconds and is false if the buttom is released before 5
-- seconds. However, if we wanted to analyse 3 buttons, we could combine the
-- 3 button signals, but we still wouldn't be able to get a signal that
-- would give us at what times each button was left pressed more than a given
-- number of time units. We could only check if either any, all or a
-- particular configuration of them as pressed for a duration. If we wanted to
-- be able to know exactly which buttons were left pressed we would need to
-- have a timeout for each button individually. That's the extra expressive
-- power that `keyedTimeout` offers.
-- offers
--
-- This function is often used in property tests with a negative predicate.
-- E.g. The system doesn't stay in a wrong state more than 5 seconds =
-- `all Set.null $ keyedTimeout 5s wrongState`
--
keyedTimeout :: forall a b. Ord b
             => DiffTime
             -> (a -> Set b)  -- ^ The timeout arming set signal
             -> Signal a
             -> Signal (Set b)
keyedTimeout :: forall a b.
Ord b =>
DiffTime -> (a -> Set b) -> Signal a -> Signal (Set b)
keyedTimeout DiffTime
d a -> Set b
arm =
    Set b -> [E (Set b)] -> Signal (Set b)
forall a. a -> [E a] -> Signal a
Signal Set b
forall a. Set a
Set.empty
  ([E (Set b)] -> Signal (Set b))
-> (Signal a -> [E (Set b)]) -> Signal a -> Signal (Set b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set b -> OrdPSQ b Time () -> Set b -> [E (Set b)] -> [E (Set b)]
go Set b
forall a. Set a
Set.empty OrdPSQ b Time ()
forall k p v. OrdPSQ k p v
PSQ.empty Set b
forall a. Set a
Set.empty
  ([E (Set b)] -> [E (Set b)])
-> (Signal a -> [E (Set b)]) -> Signal a -> [E (Set b)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signal (Set b) -> [E (Set b)]
forall a. Signal a -> [E a]
toTimeSeries
  (Signal (Set b) -> [E (Set b)])
-> (Signal a -> Signal (Set b)) -> Signal a -> [E (Set b)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Set b) -> Signal a -> Signal (Set b)
forall a b. (a -> b) -> Signal a -> Signal b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Set b
arm
  where
    go :: Set b
       -> OrdPSQ b Time ()
       -> Set b
       -> [E (Set b)]
       -> [E (Set b)]
    go :: Set b -> OrdPSQ b Time () -> Set b -> [E (Set b)] -> [E (Set b)]
go !Set b
_ !OrdPSQ b Time ()
_ !Set b
_ [] = []

    go !Set b
armedSet !OrdPSQ b Time ()
armedPSQ !Set b
timedout (E ts :: TS
ts@(TS Time
t Int
_) Set b
x : [E (Set b)]
txs)
      | Just (b
y, Time
t', ()
_, OrdPSQ b Time ()
armedPSQ') <- OrdPSQ b Time () -> Maybe (b, Time, (), OrdPSQ b Time ())
forall k p v.
(Ord k, Ord p) =>
OrdPSQ k p v -> Maybe (k, p, v, OrdPSQ k p v)
PSQ.minView OrdPSQ b Time ()
armedPSQ
      , Time
t' Time -> Time -> Bool
forall a. Ord a => a -> a -> Bool
< Time
t
      , ([(b, Time, ())]
xs, OrdPSQ b Time ()
armedPSQ'') <- Time -> OrdPSQ b Time () -> ([(b, Time, ())], OrdPSQ b Time ())
forall k p v.
(Ord k, Ord p) =>
p -> OrdPSQ k p v -> ([(k, p, v)], OrdPSQ k p v)
PSQ.atMostView Time
t' OrdPSQ b Time ()
armedPSQ'
      , let armed :: Set b
armed = [b] -> Set b
forall a. Ord a => [a] -> Set a
Set.fromList ([b] -> Set b) -> [b] -> Set b
forall a b. (a -> b) -> a -> b
$ b
y b -> [b] -> [b]
forall a. a -> [a] -> [a]
: ((b, Time, ()) -> b) -> [(b, Time, ())] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (\(b
a, Time
_, ()
_) -> b
a) [(b, Time, ())]
xs
            armedSet' :: Set b
armedSet' = Set b -> Set b -> Set b
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set b
armedSet Set b
armed
            timedout' :: Set b
timedout' = Set b
timedout Set b -> Set b -> Set b
forall a. Semigroup a => a -> a -> a
<> Set b
armed
      = TS -> Set b -> E (Set b)
forall a. TS -> a -> E a
E (Time -> Int -> TS
TS Time
t' Int
0) Set b
timedout' E (Set b) -> [E (Set b)] -> [E (Set b)]
forall a. a -> [a] -> [a]
: Set b -> OrdPSQ b Time () -> Set b -> [E (Set b)] -> [E (Set b)]
go Set b
armedSet' OrdPSQ b Time ()
armedPSQ'' Set b
timedout' (TS -> Set b -> E (Set b)
forall a. TS -> a -> E a
E TS
ts Set b
x E (Set b) -> [E (Set b)] -> [E (Set b)]
forall a. a -> [a] -> [a]
: [E (Set b)]
txs)

    go !Set b
armedSet !OrdPSQ b Time ()
armedPSQ !Set b
timedout (E ts :: TS
ts@(TS Time
t Int
_) Set b
x : [E (Set b)]
txs) =
      let armedAdd :: Set b
armedAdd  = Set b
x        Set b -> Set b -> Set b
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set b
armedSet
          armedDel :: Set b
armedDel  = Set b
armedSet Set b -> Set b -> Set b
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set b
x
          t' :: Time
t'        = DiffTime -> Time -> Time
addTime DiffTime
d Time
t
          armedPSQ' :: OrdPSQ b Time ()
armedPSQ' = (OrdPSQ b Time () -> Set b -> OrdPSQ b Time ())
-> Set b -> OrdPSQ b Time () -> OrdPSQ b Time ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((OrdPSQ b Time () -> b -> OrdPSQ b Time ())
-> OrdPSQ b Time () -> Set b -> OrdPSQ b Time ()
forall a b. (a -> b -> a) -> a -> Set b -> a
Set.foldl' (\OrdPSQ b Time ()
s b
y -> b -> Time -> () -> OrdPSQ b Time () -> OrdPSQ b Time ()
forall k p v.
(Ord k, Ord p) =>
k -> p -> v -> OrdPSQ k p v -> OrdPSQ k p v
PSQ.insert b
y Time
t' () OrdPSQ b Time ()
s)) Set b
armedAdd
                    (OrdPSQ b Time () -> OrdPSQ b Time ())
-> (OrdPSQ b Time () -> OrdPSQ b Time ())
-> OrdPSQ b Time ()
-> OrdPSQ b Time ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OrdPSQ b Time () -> Set b -> OrdPSQ b Time ())
-> Set b -> OrdPSQ b Time () -> OrdPSQ b Time ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((OrdPSQ b Time () -> b -> OrdPSQ b Time ())
-> OrdPSQ b Time () -> Set b -> OrdPSQ b Time ()
forall a b. (a -> b -> a) -> a -> Set b -> a
Set.foldl' (\OrdPSQ b Time ()
s b
y -> b -> OrdPSQ b Time () -> OrdPSQ b Time ()
forall k p v. (Ord k, Ord p) => k -> OrdPSQ k p v -> OrdPSQ k p v
PSQ.delete b
y       OrdPSQ b Time ()
s)) Set b
armedDel
                    (OrdPSQ b Time () -> OrdPSQ b Time ())
-> OrdPSQ b Time () -> OrdPSQ b Time ()
forall a b. (a -> b) -> a -> b
$ OrdPSQ b Time ()
armedPSQ
          timedout' :: Set b
timedout' = Set b
timedout Set b -> Set b -> Set b
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Set b
x
       in if Set b
timedout' Set b -> Set b -> Bool
forall a. Eq a => a -> a -> Bool
/= Set b
timedout
            then TS -> Set b -> E (Set b)
forall a. TS -> a -> E a
E TS
ts Set b
timedout' E (Set b) -> [E (Set b)] -> [E (Set b)]
forall a. a -> [a] -> [a]
: Set b -> OrdPSQ b Time () -> Set b -> [E (Set b)] -> [E (Set b)]
go Set b
x OrdPSQ b Time ()
armedPSQ' Set b
timedout' [E (Set b)]
txs
            else                  Set b -> OrdPSQ b Time () -> Set b -> [E (Set b)] -> [E (Set b)]
go Set b
x OrdPSQ b Time ()
armedPSQ' Set b
timedout' [E (Set b)]
txs

keyedUntil :: forall a b. Ord b
           => (a -> Set b)   -- ^ Start set signal
           -> (a -> Set b)   -- ^ Stop set signal
           -> (a -> Bool)    -- ^ Stop all signal
           -> Signal a
           -> Signal (Set b)
keyedUntil :: forall a b.
Ord b =>
(a -> Set b)
-> (a -> Set b) -> (a -> Bool) -> Signal a -> Signal (Set b)
keyedUntil a -> Set b
start a -> Set b
stop a -> Bool
stopAll =
    Set b -> [E (Set b)] -> Signal (Set b)
forall a. a -> [E a] -> Signal a
Signal Set b
forall a. Set a
Set.empty
  ([E (Set b)] -> Signal (Set b))
-> (Signal a -> [E (Set b)]) -> Signal a -> Signal (Set b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set b -> [E a] -> [E (Set b)]
go Set b
forall a. Set a
Set.empty
  ([E a] -> [E (Set b)])
-> (Signal a -> [E a]) -> Signal a -> [E (Set b)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signal a -> [E a]
forall a. Signal a -> [E a]
toTimeSeries
  where

    go :: Set b
       -> [E a]
       -> [E (Set b)]
    go :: Set b -> [E a] -> [E (Set b)]
go Set b
_ [] = []
    go Set b
active (E TS
t a
x : [E a]
txs)
       | Set b
active' Set b -> Set b -> Bool
forall a. Eq a => a -> a -> Bool
/= Set b
active = TS -> Set b -> E (Set b)
forall a. TS -> a -> E a
E TS
t Set b
active' E (Set b) -> [E (Set b)] -> [E (Set b)]
forall a. a -> [a] -> [a]
: Set b -> [E a] -> [E (Set b)]
go Set b
active' [E a]
txs
       | Bool
otherwise         =               Set b -> [E a] -> [E (Set b)]
go Set b
active' [E a]
txs
      where
        active' :: Set b
active'
          | a -> Bool
stopAll a
x = Set b
forall a. Set a
Set.empty
          | Bool
otherwise = (Set b
active Set b -> Set b -> Set b
forall a. Semigroup a => a -> a -> a
<> a -> Set b
start a
x) Set b -> Set b -> Set b
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ a -> Set b
stop a
x

difference :: (a -> a -> b)
           -> Signal a
           -> Signal (Maybe b)
difference :: forall a b. (a -> a -> b) -> Signal a -> Signal (Maybe b)
difference a -> a -> b
diff (Signal a
x0 [E a]
txs0) =
    Maybe b -> [E (Maybe b)] -> Signal (Maybe b)
forall a. a -> [E a] -> Signal a
Signal Maybe b
forall a. Maybe a
Nothing (a -> [E a] -> [E (Maybe b)]
go a
x0 [E a]
txs0)
  where
    go :: a -> [E a] -> [E (Maybe b)]
go a
_ []                    = []
    go a
x (E (TS Time
t Int
i) a
x' : [E a]
txs) = TS -> Maybe b -> E (Maybe b)
forall a. TS -> a -> E a
E (Time -> Int -> TS
TS Time
t Int
i)    (b -> Maybe b
forall a. a -> Maybe a
Just (b -> Maybe b) -> b -> Maybe b
forall a b. (a -> b) -> a -> b
$! a -> a -> b
diff a
x a
x')
                               E (Maybe b) -> [E (Maybe b)] -> [E (Maybe b)]
forall a. a -> [a] -> [a]
: TS -> Maybe b -> E (Maybe b)
forall a. TS -> a -> E a
E (Time -> Int -> TS
TS Time
t (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)) Maybe b
forall a. Maybe a
Nothing
                               E (Maybe b) -> [E (Maybe b)] -> [E (Maybe b)]
forall a. a -> [a] -> [a]
: a -> [E a] -> [E (Maybe b)]
go a
x' [E a]
txs


scanl :: (b -> a -> b) -> b -> Signal a -> Signal b
scanl :: forall b a. (b -> a -> b) -> b -> Signal a -> Signal b
scanl b -> a -> b
f b
z (Signal a
x0 [E a]
txs0) =
    let a0 :: b
a0 = b -> a -> b
f b
z a
x0 in
    b -> [E b] -> Signal b
forall a. a -> [E a] -> Signal a
Signal b
a0 (b -> [E a] -> [E b]
go b
a0 [E a]
txs0)
  where
    go :: b -> [E a] -> [E b]
go !b
_ []             = []
    go !b
a (E TS
ts a
x : [E a]
txs) = TS -> b -> E b
forall a. TS -> a -> E a
E TS
ts b
a' E b -> [E b] -> [E b]
forall a. a -> [a] -> [a]
: b -> [E a] -> [E b]
go b
a' [E a]
txs
                          where
                            a' :: b
a' = b -> a -> b
f b
a a
x

-- | Starting on a given event does the predicate holds for all the trace.
--
-- If there's no events after the given time, return True
always :: TS -> (b -> Bool) -> Signal b -> Bool
always :: forall b. TS -> (b -> Bool) -> Signal b -> Bool
always (TS Time
time Int
i) b -> Bool
p (Signal b
x0 [E b]
txs0)
  | Time
time Time -> Time -> Bool
forall a. Ord a => a -> a -> Bool
<= DiffTime -> Time
Time DiffTime
0 = b -> Bool
p b
x0 Bool -> Bool -> Bool
&& (E b -> Bool) -> [E b] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(E TS
_ b
b) -> b -> Bool
p b
b) [E b]
txs0
  | Bool
otherwise = case (E b -> Bool) -> [E b] -> [E b]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (\(E (TS Time
time' Int
i') b
_) -> Time
time' Time -> Time -> Bool
forall a. Ord a => a -> a -> Bool
<= Time
time Bool -> Bool -> Bool
&& Int
i' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
i) [E b]
txs0 of
    [] -> Bool
True
    [E b]
r  -> (E b -> Bool) -> [E b] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(E TS
_ b
b) -> b -> Bool
p b
b) [E b]
r

-- | Starting on a given event does the predicate eventually holds.
--
-- If there's no events after the given time, return True
eventually :: TS -> (b -> Bool) -> Signal b -> Bool
eventually :: forall b. TS -> (b -> Bool) -> Signal b -> Bool
eventually (TS Time
time Int
i) b -> Bool
p (Signal b
x0 [E b]
txs0)
  | Time
time Time -> Time -> Bool
forall a. Ord a => a -> a -> Bool
<= DiffTime -> Time
Time DiffTime
0 = b -> Bool
p b
x0 Bool -> Bool -> Bool
|| (E b -> Bool) -> [E b] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\(E TS
_ b
b) -> b -> Bool
p b
b) [E b]
txs0
  | Bool
otherwise = case (E b -> Bool) -> [E b] -> [E b]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (\(E (TS Time
time' Int
i') b
_) -> Time
time' Time -> Time -> Bool
forall a. Ord a => a -> a -> Bool
<= Time
time Bool -> Bool -> Bool
&& Int
i' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
i) [E b]
txs0 of
    [] -> Bool
True
    [E b]
r  -> (E b -> Bool) -> [E b] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\(E TS
_ b
b) -> b -> Bool
p b
b) [E b]
r

--
-- QuickCheck
--

-- | Check a property over a 'Signal'. The property should be true at all times.
--
-- On failure it shows the @n@ most recent signal values.
--
signalProperty :: forall a. Int -> (a -> String)
               -> (a -> Bool) -> Signal a -> Property
signalProperty :: forall a.
Int -> (a -> String) -> (a -> Bool) -> Signal a -> Property
signalProperty Int
atMost a -> String
showSignalValue a -> Bool
p =
    Int -> Deque (Time, a) -> [(Time, a)] -> Property
go Int
0 Deque (Time, a)
forall a. Monoid a => a
mempty ([(Time, a)] -> Property)
-> (Signal a -> [(Time, a)]) -> Signal a -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Events a -> [(Time, a)]
forall a. Events a -> [(Time, a)]
eventsToList (Events a -> [(Time, a)])
-> (Signal a -> Events a) -> Signal a -> [(Time, a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signal a -> Events a
forall a. Signal a -> Events a
toChangeEvents
  where
    go :: Int -> Deque (Time, a) -> [(Time, a)] -> Property
    go :: Int -> Deque (Time, a) -> [(Time, a)] -> Property
go !Int
_ !Deque (Time, a)
_ []                   = Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
    go !Int
n !Deque (Time, a)
recent ((Time
t, a
x) : [(Time, a)]
txs) | a -> Bool
p a
x = Property
next
      where
        next :: Property
next
          | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
atMost = Int -> Deque (Time, a) -> [(Time, a)] -> Property
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (              (Time, a) -> Deque (Time, a) -> Deque (Time, a)
forall a. a -> Deque a -> Deque a
Deque.snoc (Time
t,a
x)  Deque (Time, a)
recent) [(Time, a)]
txs
          | Bool
otherwise  = Int -> Deque (Time, a) -> [(Time, a)] -> Property
go Int
n     ((Deque (Time, a) -> Deque (Time, a)
forall a. Deque a -> Deque a
Deque.tail (Deque (Time, a) -> Deque (Time, a))
-> (Deque (Time, a) -> Deque (Time, a))
-> Deque (Time, a)
-> Deque (Time, a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Time, a) -> Deque (Time, a) -> Deque (Time, a)
forall a. a -> Deque a -> Deque a
Deque.snoc (Time
t,a
x)) Deque (Time, a)
recent) [(Time, a)]
txs

    go !Int
_ !Deque (Time, a)
recent ((Time
t, a
x) : [(Time, a)]
_) = String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
details Bool
False
      where
        details :: String
details =
          [String] -> String
unlines [ String
"Last " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
atMost String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" signal values:"
                  , [String] -> String
unlines [ Time -> String
forall a. Show a => a -> String
show Time
t' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\t: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
showSignalValue a
x'
                            | (Time
t',a
x') <- Deque (Time, a) -> [(Time, a)]
forall a. Deque a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Deque.toList Deque (Time, a)
recent ]
                  , String
"Property violated at: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Time -> String
forall a. Show a => a -> String
show Time
t
                  , String
"Invalid signal value:"
                  , a -> String
showSignalValue a
x
                  ]

--
-- Utils
--

-- | Generic merging utility. For sorted input lists this is a full outer join.
--
mergeBy :: (a -> b -> Ordering) -> [a] -> [b] -> [MergeResult a b]
mergeBy :: forall a b. (a -> b -> Ordering) -> [a] -> [b] -> [MergeResult a b]
mergeBy a -> b -> Ordering
cmp = [a] -> [b] -> [MergeResult a b]
merge
  where
    merge :: [a] -> [b] -> [MergeResult a b]
merge []     [b]
ys     = [ b -> MergeResult a b
forall a b. b -> MergeResult a b
OnlyInRight b
y | b
y <- [b]
ys]
    merge [a]
xs     []     = [ a -> MergeResult a b
forall a b. a -> MergeResult a b
OnlyInLeft  a
x | a
x <- [a]
xs]
    merge (a
x:[a]
xs) (b
y:[b]
ys) =
      case a
x a -> b -> Ordering
`cmp` b
y of
        Ordering
GT -> b -> MergeResult a b
forall a b. b -> MergeResult a b
OnlyInRight   b
y MergeResult a b -> [MergeResult a b] -> [MergeResult a b]
forall a. a -> [a] -> [a]
: [a] -> [b] -> [MergeResult a b]
merge (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
xs) [b]
ys
        Ordering
EQ -> a -> b -> MergeResult a b
forall a b. a -> b -> MergeResult a b
InBoth      a
x b
y MergeResult a b -> [MergeResult a b] -> [MergeResult a b]
forall a. a -> [a] -> [a]
: [a] -> [b] -> [MergeResult a b]
merge [a]
xs     [b]
ys
        Ordering
LT -> a -> MergeResult a b
forall a b. a -> MergeResult a b
OnlyInLeft  a
x   MergeResult a b -> [MergeResult a b] -> [MergeResult a b]
forall a. a -> [a] -> [a]
: [a] -> [b] -> [MergeResult a b]
merge [a]
xs  (b
yb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
ys)

data MergeResult a b = OnlyInLeft a | InBoth a b | OnlyInRight b
  deriving (MergeResult a b -> MergeResult a b -> Bool
(MergeResult a b -> MergeResult a b -> Bool)
-> (MergeResult a b -> MergeResult a b -> Bool)
-> Eq (MergeResult a b)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a b.
(Eq a, Eq b) =>
MergeResult a b -> MergeResult a b -> Bool
$c== :: forall a b.
(Eq a, Eq b) =>
MergeResult a b -> MergeResult a b -> Bool
== :: MergeResult a b -> MergeResult a b -> Bool
$c/= :: forall a b.
(Eq a, Eq b) =>
MergeResult a b -> MergeResult a b -> Bool
/= :: MergeResult a b -> MergeResult a b -> Bool
Eq, Int -> MergeResult a b -> ShowS
[MergeResult a b] -> ShowS
MergeResult a b -> String
(Int -> MergeResult a b -> ShowS)
-> (MergeResult a b -> String)
-> ([MergeResult a b] -> ShowS)
-> Show (MergeResult a b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b. (Show a, Show b) => Int -> MergeResult a b -> ShowS
forall a b. (Show a, Show b) => [MergeResult a b] -> ShowS
forall a b. (Show a, Show b) => MergeResult a b -> String
$cshowsPrec :: forall a b. (Show a, Show b) => Int -> MergeResult a b -> ShowS
showsPrec :: Int -> MergeResult a b -> ShowS
$cshow :: forall a b. (Show a, Show b) => MergeResult a b -> String
show :: MergeResult a b -> String
$cshowList :: forall a b. (Show a, Show b) => [MergeResult a b] -> ShowS
showList :: [MergeResult a b] -> ShowS
Show)