{-# 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
(GSUMEvent -> GSUMEvent -> Bool)
-> (GSUMEvent -> GSUMEvent -> Bool) -> Eq GSUMEvent
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: GSUMEvent -> GSUMEvent -> Bool
== :: GSUMEvent -> GSUMEvent -> Bool
$c/= :: GSUMEvent -> GSUMEvent -> Bool
/= :: GSUMEvent -> GSUMEvent -> Bool
Eq, Int -> GSUMEvent -> ShowS
[GSUMEvent] -> ShowS
GSUMEvent -> Label
(Int -> GSUMEvent -> ShowS)
-> (GSUMEvent -> Label) -> ([GSUMEvent] -> ShowS) -> Show GSUMEvent
forall a.
(Int -> a -> ShowS) -> (a -> Label) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GSUMEvent -> ShowS
showsPrec :: Int -> GSUMEvent -> ShowS
$cshow :: GSUMEvent -> Label
show :: GSUMEvent -> Label
$cshowList :: [GSUMEvent] -> ShowS
showList :: [GSUMEvent] -> ShowS
Show)

data NoFailure = NoFailure deriving (NoFailure -> NoFailure -> Bool
(NoFailure -> NoFailure -> Bool)
-> (NoFailure -> NoFailure -> Bool) -> Eq NoFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: NoFailure -> NoFailure -> Bool
== :: NoFailure -> NoFailure -> Bool
$c/= :: NoFailure -> NoFailure -> Bool
/= :: NoFailure -> NoFailure -> Bool
Eq, Int -> NoFailure -> ShowS
[NoFailure] -> ShowS
NoFailure -> Label
(Int -> NoFailure -> ShowS)
-> (NoFailure -> Label) -> ([NoFailure] -> ShowS) -> Show NoFailure
forall a.
(Int -> a -> ShowS) -> (a -> Label) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NoFailure -> ShowS
showsPrec :: Int -> NoFailure -> ShowS
$cshow :: NoFailure -> Label
show :: NoFailure -> Label
$cshowList :: [NoFailure] -> ShowS
showList :: [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 = [Int -> Rule GSUM 'Initial Int
forall a. a -> F (Clause GSUM 'Initial) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
0]

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

spec :: Spec
spec :: Spec
spec =
  Label -> Spec -> Spec
forall a. HasCallStack => Label -> SpecWith a -> SpecWith a
describe Label
"STS.Extended" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    Label -> Expectation -> SpecM (Arg Expectation) ()
forall a.
(HasCallStack, Example a) =>
Label -> a -> SpecWith (Arg a)
it Label
"Sum" (Expectation -> SpecM (Arg Expectation) ())
-> Expectation -> SpecM (Arg Expectation) ()
forall a b. (a -> b) -> a -> b
$ Either (NonEmpty NoFailure) Int
withSum Either (NonEmpty NoFailure) Int
-> Either (NonEmpty NoFailure) Int -> Expectation
forall a. (HasCallStack, Show a, Eq a) => a -> a -> Expectation
`shouldBe` Int -> Either (NonEmpty NoFailure) Int
forall a b. b -> Either a b
Right Int
55
    Label -> Expectation -> SpecM (Arg Expectation) ()
forall a.
(HasCallStack, Example a) =>
Label -> a -> SpecWith (Arg a)
it Label
"Product" (Expectation -> SpecM (Arg Expectation) ())
-> Expectation -> SpecM (Arg Expectation) ()
forall a b. (a -> b) -> a -> b
$ Either (NonEmpty NoFailure) Int
withProduct Either (NonEmpty NoFailure) Int
-> Either (NonEmpty NoFailure) Int -> Expectation
forall a. (HasCallStack, Show a, Eq a) => a -> a -> Expectation
`shouldBe` Int -> Either (NonEmpty NoFailure) Int
forall a b. b -> Either a b
Right Int
3628800
    Label -> Expectation -> SpecM (Arg Expectation) ()
forall a.
(HasCallStack, Example a) =>
Label -> a -> SpecWith (Arg a)
it Label
"Sum/Lazy Events" (Expectation -> SpecM (Arg Expectation) ())
-> Expectation -> SpecM (Arg Expectation) ()
forall a b. (a -> b) -> a -> b
$ Either (NonEmpty NoFailure) Int
withLazyEventsSum Either (NonEmpty NoFailure) Int
-> Either (NonEmpty NoFailure) Int -> Expectation
forall a. (HasCallStack, Show a, Eq a) => a -> a -> Expectation
`shouldBe` Int -> Either (NonEmpty NoFailure) Int
forall a b. b -> Either a b
Right Int
55
    Label -> Spec -> Spec
forall a. HasCallStack => Label -> SpecWith a -> SpecWith a
describe Label
"Sum/Validate" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
      Label -> Expectation -> SpecM (Arg Expectation) ()
forall a.
(HasCallStack, Example a) =>
Label -> a -> SpecWith (Arg a)
it Label
"Filtered" (Expectation -> SpecM (Arg Expectation) ())
-> Expectation -> SpecM (Arg Expectation) ()
forall a b. (a -> b) -> a -> b
$
        ValidationPolicy -> Either (NonEmpty NoFailure) Int
withLblSum (([Label] -> Bool) -> ValidationPolicy
ValidateSuchThat (Label
"testLabel" Label -> [Label] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem`)) Either (NonEmpty NoFailure) Int
-> Either (NonEmpty NoFailure) Int -> Expectation
forall a. (HasCallStack, Show a, Eq a) => a -> a -> Expectation
`shouldBe` NonEmpty NoFailure -> Either (NonEmpty NoFailure) Int
forall a b. a -> Either a b
Left [Item (NonEmpty NoFailure)
NoFailure
NoFailure]
      Label -> Expectation -> SpecM (Arg Expectation) ()
forall a.
(HasCallStack, Example a) =>
Label -> a -> SpecWith (Arg a)
it Label
"Unfiltered" (Expectation -> SpecM (Arg Expectation) ())
-> Expectation -> SpecM (Arg Expectation) ()
forall a b. (a -> b) -> a -> b
$
        ValidationPolicy -> Either (NonEmpty NoFailure) Int
withLblSum (([Label] -> Bool) -> ValidationPolicy
ValidateSuchThat (Bool -> [Label] -> Bool
forall a b. a -> b -> a
const Bool
True)) Either (NonEmpty NoFailure) Int
-> Either (NonEmpty NoFailure) Int -> Expectation
forall a. (HasCallStack, Show a, Eq a) => a -> a -> Expectation
`shouldBe` NonEmpty NoFailure -> Either (NonEmpty NoFailure) Int
forall a b. a -> Either a b
Left [Item (NonEmpty NoFailure)
NoFailure
NoFailure, Item (NonEmpty NoFailure)
NoFailure
NoFailure]
      Label -> Expectation -> SpecM (Arg Expectation) ()
forall a.
(HasCallStack, Example a) =>
Label -> a -> SpecWith (Arg a)
it Label
"None" (Expectation -> SpecM (Arg Expectation) ())
-> Expectation -> SpecM (Arg Expectation) ()
forall a b. (a -> b) -> a -> b
$
        ValidationPolicy -> Either (NonEmpty NoFailure) Int
withLblSum ValidationPolicy
ValidateNone Either (NonEmpty NoFailure) Int
-> Either (NonEmpty NoFailure) Int -> Expectation
forall a. (HasCallStack, Show a, Eq a) => a -> a -> Expectation
`shouldBe` Int -> Either (NonEmpty NoFailure) Int
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 = (Environment GSUM, State GSUM, Signal GSUM) -> TRC GSUM
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC ((), State GSUM
0, Signal GSUM
inputs)
    withSum :: Either (NonEmpty NoFailure) Int
withSum = Reader Ops (Either (NonEmpty NoFailure) Int)
-> Ops -> Either (NonEmpty NoFailure) Int
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 RuleContext 'Transition GSUM
TRC GSUM
ctx) (([Int] -> Int) -> Ops
Ops ((Int -> Int -> Int) -> Int -> [Int] -> Int
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
F.foldl' Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) Int
0))
    withLblSum :: ValidationPolicy -> Either (NonEmpty NoFailure) Int
withLblSum ValidationPolicy
vp =
      ((Int, [GSUMEvent]) -> Int)
-> Either (NonEmpty NoFailure) (Int, [GSUMEvent])
-> Either (NonEmpty NoFailure) Int
forall b c d. (b -> c) -> Either d b -> Either d c
forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either d b) (Either d c)
right (Int, [GSUMEvent]) -> Int
forall a b. (a, b) -> a
fst (Either (NonEmpty NoFailure) (Int, [GSUMEvent])
 -> Either (NonEmpty NoFailure) Int)
-> Either (NonEmpty NoFailure) (Int, [GSUMEvent])
-> Either (NonEmpty NoFailure) Int
forall a b. (a -> b) -> a -> b
$
        Reader Ops (Either (NonEmpty NoFailure) (Int, [GSUMEvent]))
-> Ops -> Either (NonEmpty NoFailure) (Int, [GSUMEvent])
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 RuleContext 'Transition GSUM
TRC GSUM
ctx) (([Int] -> Int) -> Ops
Ops ((Int -> Int -> Int) -> Int -> [Int] -> Int
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
F.foldl' Int -> Int -> Int
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 = Reader Ops (Either (NonEmpty NoFailure) Int)
-> Ops -> Either (NonEmpty NoFailure) Int
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 RuleContext 'Transition GSUM
TRC GSUM
ctx) (([Int] -> Int) -> Ops
Ops ((Int -> Int -> Int) -> Int -> [Int] -> Int
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
F.foldl' Int -> Int -> Int
forall a. Num a => a -> a -> a
(*) Int
1))
    withLazyEventsSum :: Either (NonEmpty NoFailure) Int
withLazyEventsSum =
      ((Int, [GSUMEvent]) -> Int)
-> Either (NonEmpty NoFailure) (Int, [GSUMEvent])
-> Either (NonEmpty NoFailure) Int
forall b c d. (b -> c) -> Either d b -> Either d c
forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either d b) (Either d c)
right (Int, [GSUMEvent]) -> Int
forall a b. (a, b) -> a
fst (Either (NonEmpty NoFailure) (Int, [GSUMEvent])
 -> Either (NonEmpty NoFailure) Int)
-> Either (NonEmpty NoFailure) (Int, [GSUMEvent])
-> Either (NonEmpty NoFailure) Int
forall a b. (a -> b) -> a -> b
$
        Reader Ops (Either (NonEmpty NoFailure) (Int, [GSUMEvent]))
-> Ops -> Either (NonEmpty NoFailure) (Int, [GSUMEvent])
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 RuleContext 'Transition GSUM
TRC GSUM
ctx) (([Int] -> Int) -> Ops
Ops ((Int -> Int -> Int) -> Int -> [Int] -> Int
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
F.foldl' Int -> Int -> Int
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
            }