{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedLists #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

-- | Simple example of a transition system whose states contain the sum of the
-- integers seen in the signals, where 'sum' is an abstract monoidal sum given
-- in the enviroment.
module Test.Control.State.Transition.Examples.GlobalSum where

import Control.Arrow (right)
import Control.Monad.Reader
import Control.State.Transition.Extended
import Data.Foldable as F (foldl')
import Data.Void (Void)
import Test.Hspec
import Prelude hiding (sum)

newtype Ops = Ops
  { Ops -> [Int] -> Int
opSum :: [Int] -> Int
  }

data GSUM

newtype GSUMEvent = ErrorEvent Void deriving (GSUMEvent -> GSUMEvent -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GSUMEvent -> GSUMEvent -> Bool
$c/= :: GSUMEvent -> GSUMEvent -> Bool
== :: GSUMEvent -> GSUMEvent -> Bool
$c== :: GSUMEvent -> GSUMEvent -> Bool
Eq, Int -> GSUMEvent -> ShowS
[GSUMEvent] -> ShowS
GSUMEvent -> Label
forall a.
(Int -> a -> ShowS) -> (a -> Label) -> ([a] -> ShowS) -> Show a
showList :: [GSUMEvent] -> ShowS
$cshowList :: [GSUMEvent] -> ShowS
show :: GSUMEvent -> Label
$cshow :: GSUMEvent -> Label
showsPrec :: Int -> GSUMEvent -> ShowS
$cshowsPrec :: Int -> GSUMEvent -> ShowS
Show)

data NoFailure = NoFailure deriving (NoFailure -> NoFailure -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NoFailure -> NoFailure -> Bool
$c/= :: NoFailure -> NoFailure -> Bool
== :: NoFailure -> NoFailure -> Bool
$c== :: NoFailure -> NoFailure -> Bool
Eq, Int -> NoFailure -> ShowS
[NoFailure] -> ShowS
NoFailure -> Label
forall a.
(Int -> a -> ShowS) -> (a -> Label) -> ([a] -> ShowS) -> Show a
showList :: [NoFailure] -> ShowS
$cshowList :: [NoFailure] -> ShowS
show :: NoFailure -> Label
$cshow :: NoFailure -> Label
showsPrec :: Int -> NoFailure -> ShowS
$cshowsPrec :: Int -> NoFailure -> ShowS
Show)

instance STS GSUM where
  type Environment GSUM = ()

  type State GSUM = Int

  type Signal GSUM = [Int]

  type BaseM GSUM = Reader Ops

  type PredicateFailure GSUM = NoFailure

  type Event _ = GSUMEvent

  initialRules :: [InitialRule GSUM]
initialRules = [forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
0]

  transitionRules :: [TransitionRule GSUM]
transitionRules =
    [ do
        TRC ((), State GSUM
st, Signal GSUM
xs) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        [Int] -> Int
sum <- forall sts a (ctx :: RuleType).
STS sts =>
BaseM sts a -> Rule sts ctx a
liftSTS forall a b. (a -> b) -> a -> b
$ forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader Ops -> [Int] -> Int
opSum
        forall sts (ctx :: RuleType). Event sts -> Rule sts ctx ()
tellEvent forall a b. (a -> b) -> a -> b
$ Void -> GSUMEvent
ErrorEvent (forall a. HasCallStack => Label -> a
error Label
"Event has been evaluated!")
        forall sts (ctx :: RuleType).
NonEmpty Label -> Rule sts ctx () -> Rule sts ctx ()
labeled [Label
"testLabel"] forall a b. (a -> b) -> a -> b
$ ([Int] -> Int
sum Signal GSUM
xs forall a. Eq a => a -> a -> Bool
/= Int
56) forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! NoFailure
NoFailure
        [Int] -> Int
sum Signal GSUM
xs forall a. Eq a => a -> a -> Bool
/= Int
56 forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! NoFailure
NoFailure
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! State GSUM
st forall a. Num a => a -> a -> a
+ [Int] -> Int
sum Signal GSUM
xs
    ]

spec :: Spec
spec :: Spec
spec =
  forall a. HasCallStack => Label -> SpecWith a -> SpecWith a
describe Label
"STS.Extended" forall a b. (a -> b) -> a -> b
$ do
    forall a.
(HasCallStack, Example a) =>
Label -> a -> SpecWith (Arg a)
it Label
"Sum" forall a b. (a -> b) -> a -> b
$ Either (NonEmpty NoFailure) Int
withSum forall a. (HasCallStack, Show a, Eq a) => a -> a -> Expectation
`shouldBe` forall a b. b -> Either a b
Right Int
55
    forall a.
(HasCallStack, Example a) =>
Label -> a -> SpecWith (Arg a)
it Label
"Product" forall a b. (a -> b) -> a -> b
$ Either (NonEmpty NoFailure) Int
withProduct forall a. (HasCallStack, Show a, Eq a) => a -> a -> Expectation
`shouldBe` forall a b. b -> Either a b
Right Int
3628800
    forall a.
(HasCallStack, Example a) =>
Label -> a -> SpecWith (Arg a)
it Label
"Sum/Lazy Events" forall a b. (a -> b) -> a -> b
$ Either (NonEmpty NoFailure) Int
withLazyEventsSum forall a. (HasCallStack, Show a, Eq a) => a -> a -> Expectation
`shouldBe` forall a b. b -> Either a b
Right Int
55
    forall a. HasCallStack => Label -> SpecWith a -> SpecWith a
describe Label
"Sum/Validate" forall a b. (a -> b) -> a -> b
$ do
      forall a.
(HasCallStack, Example a) =>
Label -> a -> SpecWith (Arg a)
it Label
"Filtered" forall a b. (a -> b) -> a -> b
$
        ValidationPolicy -> Either (NonEmpty NoFailure) Int
withLblSum (([Label] -> Bool) -> ValidationPolicy
ValidateSuchThat (Label
"testLabel" forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem`)) forall a. (HasCallStack, Show a, Eq a) => a -> a -> Expectation
`shouldBe` forall a b. a -> Either a b
Left [NoFailure
NoFailure]
      forall a.
(HasCallStack, Example a) =>
Label -> a -> SpecWith (Arg a)
it Label
"Unfiltered" forall a b. (a -> b) -> a -> b
$
        ValidationPolicy -> Either (NonEmpty NoFailure) Int
withLblSum (([Label] -> Bool) -> ValidationPolicy
ValidateSuchThat (forall a b. a -> b -> a
const Bool
True)) forall a. (HasCallStack, Show a, Eq a) => a -> a -> Expectation
`shouldBe` forall a b. a -> Either a b
Left [NoFailure
NoFailure, NoFailure
NoFailure]
      forall a.
(HasCallStack, Example a) =>
Label -> a -> SpecWith (Arg a)
it Label
"None" forall a b. (a -> b) -> a -> b
$
        ValidationPolicy -> Either (NonEmpty NoFailure) Int
withLblSum ValidationPolicy
ValidateNone forall a. (HasCallStack, Show a, Eq a) => a -> a -> Expectation
`shouldBe` forall a b. b -> Either a b
Right Int
56
  where
    inputs :: Signal GSUM
inputs = [Item (Signal GSUM)
1 .. Item (Signal GSUM)
10]
    ctx :: TRC GSUM
ctx = forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC ((), State GSUM
0, Signal GSUM
inputs)
    withSum :: Either (NonEmpty NoFailure) Int
withSum = forall r a. Reader r a -> r -> a
runReader (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTS @GSUM TRC GSUM
ctx) (([Int] -> Int) -> Ops
Ops (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
F.foldl' forall a. Num a => a -> a -> a
(+) Int
0))
    withLblSum :: ValidationPolicy -> Either (NonEmpty NoFailure) Int
withLblSum ValidationPolicy
vp =
      forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either d b) (Either d c)
right forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$
        forall r a. Reader r a -> r -> a
runReader (forall s (m :: * -> *) (rtype :: RuleType) (ep :: EventPolicy).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
ApplySTSOpts ep
-> RuleContext rtype s
-> m (Either
        (NonEmpty (PredicateFailure s)) (EventReturnType ep s (State s)))
applySTSOptsEither @GSUM ApplySTSOpts 'EventPolicyReturn
lblOpts TRC GSUM
ctx) (([Int] -> Int) -> Ops
Ops (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
F.foldl' forall a. Num a => a -> a -> a
(+) Int
1))
      where
        lblOpts :: ApplySTSOpts 'EventPolicyReturn
lblOpts =
          ApplySTSOpts
            { asoAssertions :: AssertionPolicy
asoAssertions = AssertionPolicy
AssertionsOff
            , asoValidation :: ValidationPolicy
asoValidation = ValidationPolicy
vp
            , asoEvents :: SingEP 'EventPolicyReturn
asoEvents = SingEP 'EventPolicyReturn
EPReturn
            }

    withProduct :: Either (NonEmpty NoFailure) Int
withProduct = forall r a. Reader r a -> r -> a
runReader (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTS @GSUM TRC GSUM
ctx) (([Int] -> Int) -> Ops
Ops (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
F.foldl' forall a. Num a => a -> a -> a
(*) Int
1))
    withLazyEventsSum :: Either (NonEmpty NoFailure) Int
withLazyEventsSum =
      forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either d b) (Either d c)
right forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$
        forall r a. Reader r a -> r -> a
runReader (forall s (m :: * -> *) (rtype :: RuleType) (ep :: EventPolicy).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
ApplySTSOpts ep
-> RuleContext rtype s
-> m (Either
        (NonEmpty (PredicateFailure s)) (EventReturnType ep s (State s)))
applySTSOptsEither @GSUM ApplySTSOpts 'EventPolicyReturn
evtOpts TRC GSUM
ctx) (([Int] -> Int) -> Ops
Ops (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
F.foldl' forall a. Num a => a -> a -> a
(+) Int
0))
      where
        evtOpts :: ApplySTSOpts 'EventPolicyReturn
evtOpts =
          ApplySTSOpts
            { asoAssertions :: AssertionPolicy
asoAssertions = AssertionPolicy
AssertionsOff
            , asoValidation :: ValidationPolicy
asoValidation = ValidationPolicy
ValidateAll
            , asoEvents :: SingEP 'EventPolicyReturn
asoEvents = SingEP 'EventPolicyReturn
EPReturn
            }