{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Small step state transition systems.
module Control.State.Transition.Extended
  ( RuleType (..),
    RuleTypeRep,
    RuleContext,
    IRC (..),
    TRC (..),
    Rule,
    TransitionRule,
    InitialRule,
    Assertion (..),
    AssertionViolation (..),
    AssertionException (..),
    STS (..),
    STUB,
    Embed (..),
    (?!),
    (?!:),
    validate,
    validateTrans,
    validateTransLabeled,
    Label,
    SingEP (..),
    EventPolicy (..),
    EventReturnType,
    labeled,
    labeledPred,
    labeledPredE,
    ifFailureFree,
    whenFailureFree,
    failBecause,
    judgmentContext,
    trans,
    liftSTS,
    tellEvent,
    tellEvents,
    EventReturnTypeRep,
    mapEventReturn,

    -- * Apply STS
    AssertionPolicy (..),
    ValidationPolicy (..),
    ApplySTSOpts (..),
    applySTSOpts,
    applySTSOptsEither,
    applySTS,
    applySTSIndifferently,
    reapplySTS,
    globalAssertionPolicy,

    -- * Exported to allow running rules independently
    applySTSInternal,
    applyRuleInternal,
    RuleInterpreter,
    STSInterpreter,

    -- * Random thing
    Threshold (..),
    sfor_,
  )
where

import Control.Exception (Exception (..), throw)
import Control.Monad (when)
import Control.Monad.Free.Church (F, MonadFree (wrap), foldF, liftF)
import Control.Monad.Identity (Identity (..))
import Control.Monad.State.Class (MonadState (..), modify)
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.Except (ExceptT, runExceptT, throwE)
import Control.Monad.Trans.State.Strict (StateT (..))
import Data.Bifunctor (Bifunctor (second), first)
import Data.Coerce (Coercible, coerce)
import Data.Data (Data, Typeable)
import Data.Default.Class (Default, def)
import Data.Foldable (find, traverse_)
import Data.Functor (($>), (<&>))
import Data.Kind (Type)
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty as NE
import Data.Typeable (typeRep)
import Data.Void (Void)
import NoThunks.Class (NoThunks (..))
import Validation (Validation (..), eitherToValidation)

-- | In order to avoid boolean blindness we create specialized type for the
-- concept of any rule having information about overall state of the nested
-- clause.
data IsFailing
  = Failing
  | NotFailing
  deriving (IsFailing -> IsFailing -> Bool
(IsFailing -> IsFailing -> Bool)
-> (IsFailing -> IsFailing -> Bool) -> Eq IsFailing
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IsFailing -> IsFailing -> Bool
$c/= :: IsFailing -> IsFailing -> Bool
== :: IsFailing -> IsFailing -> Bool
$c== :: IsFailing -> IsFailing -> Bool
Eq, Int -> IsFailing -> ShowS
[IsFailing] -> ShowS
IsFailing -> String
(Int -> IsFailing -> ShowS)
-> (IsFailing -> String)
-> ([IsFailing] -> ShowS)
-> Show IsFailing
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IsFailing] -> ShowS
$cshowList :: [IsFailing] -> ShowS
show :: IsFailing -> String
$cshow :: IsFailing -> String
showsPrec :: Int -> IsFailing -> ShowS
$cshowsPrec :: Int -> IsFailing -> ShowS
Show)

data RuleType
  = Initial
  | Transition

-- | Singleton instances.
--
--   Since our case is so small we don't bother with the singletons library.
data SRuleType a where
  SInitial :: SRuleType 'Initial
  STransition :: SRuleType 'Transition

class RuleTypeRep t where
  rTypeRep :: SRuleType t

instance RuleTypeRep 'Initial where
  rTypeRep :: SRuleType 'Initial
rTypeRep = SRuleType 'Initial
SInitial

instance RuleTypeRep 'Transition where
  rTypeRep :: SRuleType 'Transition
rTypeRep = SRuleType 'Transition
STransition

-- | Context available to initial rules.
newtype IRC sts = IRC (Environment sts)

-- | Context available to transition rules.
newtype TRC sts = TRC (Environment sts, State sts, Signal sts)

deriving instance
  ( Show (Environment sts),
    Show (State sts),
    Show (Signal sts)
  ) =>
  Show (TRC sts)

type family RuleContext (t :: RuleType) = (ctx :: Type -> Type) | ctx -> t where
  RuleContext 'Initial = IRC
  RuleContext 'Transition = TRC

type InitialRule sts = Rule sts 'Initial (State sts)

type TransitionRule sts = Rule sts 'Transition (State sts)

-- | An assertion is a validation condition for the STS system in question. It
--   should be used to define properties of the system as a whole that cannot be
--   violated under normal circumstances - e.g. a violation implies a failing in
--   the rule logic.
--
--   Assertions should not check for conditions that may differ between
--   different rules in a system, since the interpreter may stop the system upon
--   presence of a failed assertion.
--
--   Whether assertions are checked is a matter for the STS interpreter.
data Assertion sts
  = -- | Pre-condition. Checked before the rule fires.
    PreCondition String (TRC sts -> Bool)
  | -- | Post-condition. Checked after the rule fires, and given access
    --   to the resultant state as well as the initial context.
    PostCondition String (TRC sts -> State sts -> Bool)

data AssertionViolation sts = AssertionViolation
  { AssertionViolation sts -> String
avSTS :: String,
    AssertionViolation sts -> String
avMsg :: String,
    AssertionViolation sts -> TRC sts
avCtx :: TRC sts,
    AssertionViolation sts -> Maybe (State sts)
avState :: Maybe (State sts)
  }

instance STS sts => Show (AssertionViolation sts) where
  show :: AssertionViolation sts -> String
show = AssertionViolation sts -> String
forall sts. STS sts => AssertionViolation sts -> String
renderAssertionViolation

data AssertionException where
  AssertionException :: forall sts. STS sts => AssertionViolation sts -> AssertionException

instance Show AssertionException where
  show :: AssertionException -> String
show (AssertionException AssertionViolation sts
exc) = AssertionViolation sts -> String
forall a. Show a => a -> String
show AssertionViolation sts
exc

instance Exception AssertionException

-- | State transition system.
class
  ( Eq (PredicateFailure a),
    Show (PredicateFailure a),
    Monad (BaseM a),
    Typeable a
  ) =>
  STS a
  where
  -- | Type of the state which the system transitions between.
  type State a :: Type

  -- | Signal triggering a state change.
  type Signal a :: Type

  -- | Environment type.
  type Environment a :: Type

  -- | Monad into which to interpret the rules.
  type BaseM a :: Type -> Type

  type BaseM a = Identity

  -- | Event type.
  type Event a :: Type

  type Event a = Void

  -- | Descriptive type for the possible failures which might cause a transition
  -- to fail.
  --
  -- As a convention, `PredicateFailure`s which are "structural" (meaning that
  -- they are not "throwable" in practice, and are used to pass control from
  -- one transition rule to another) are prefixed with `S_`.
  --
  -- Structural `PredicateFailure`s represent conditions between rules where
  -- the disjunction of all rules' preconditions is equal to `True`. That is,
  -- either one rule will throw a structural `PredicateFailure` and the other
  -- will succeed, or vice-versa.
  type PredicateFailure a :: Type

  -- | Rules governing transition under this system.
  initialRules :: [InitialRule a]
  default initialRules :: Default (State a) => [InitialRule a]
  initialRules = [State a -> InitialRule a
forall (f :: * -> *) a. Applicative f => a -> f a
pure State a
forall a. Default a => a
def]

  transitionRules :: [TransitionRule a]

  -- | Assertions about the transition system.
  assertions :: [Assertion a]
  assertions = []

  -- | Render an assertion violation.
  --
  --   Defaults to using 'show', but note that this does not know how to render
  --   the context. So for more information you should define your own renderer
  --   here.
  renderAssertionViolation :: AssertionViolation a -> String
  renderAssertionViolation (AssertionViolation String
sts String
msg TRC a
_ Maybe (State a)
_) =
    String
"AssertionViolation (" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
sts String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"): " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
msg

-- | Embed one STS within another.
class (STS sub, BaseM sub ~ BaseM super) => Embed sub super where
  -- | Wrap a predicate failure of the subsystem in a failure of the super-system.
  wrapFailed :: PredicateFailure sub -> PredicateFailure super

  wrapEvent :: Event sub -> Event super
  default wrapEvent :: Coercible (Event sub) (Event super) => Event sub -> Event super
  wrapEvent = Event sub -> Event super
coerce

instance STS sts => Embed sts sts where
  wrapFailed :: PredicateFailure sts -> PredicateFailure sts
wrapFailed = PredicateFailure sts -> PredicateFailure sts
forall a. a -> a
id

data EventPolicy
  = EventPolicyReturn
  | EventPolicyDiscard

data SingEP ep where
  EPReturn :: SingEP 'EventPolicyReturn
  EPDiscard :: SingEP 'EventPolicyDiscard

type family EventReturnType ep sts a :: Type where
  EventReturnType 'EventPolicyReturn sts a = (a, [Event sts])
  EventReturnType _ _ a = a

class EventReturnTypeRep ert where
  eventReturnTypeRep :: SingEP ert

instance EventReturnTypeRep 'EventPolicyReturn where
  eventReturnTypeRep :: SingEP 'EventPolicyReturn
eventReturnTypeRep = SingEP 'EventPolicyReturn
EPReturn

instance EventReturnTypeRep 'EventPolicyDiscard where
  eventReturnTypeRep :: SingEP 'EventPolicyDiscard
eventReturnTypeRep = SingEP 'EventPolicyDiscard
EPDiscard

discardEvents :: forall ep a. SingEP ep -> forall s. EventReturnType ep s a -> a
discardEvents :: SingEP ep -> forall s. EventReturnType ep s a -> a
discardEvents SingEP ep
ep = case SingEP ep
ep of
  SingEP ep
EPReturn -> EventReturnType ep s a -> a
forall a b. (a, b) -> a
fst
  SingEP ep
EPDiscard -> EventReturnType ep s a -> a
forall a. a -> a
id

getEvents :: forall ep. SingEP ep -> forall s a. EventReturnType ep s a -> [Event s]
getEvents :: SingEP ep -> forall s a. EventReturnType ep s a -> [Event s]
getEvents SingEP ep
ep EventReturnType ep s a
ert = case SingEP ep
ep of
  SingEP ep
EPReturn -> (a, [Event s]) -> [Event s]
forall a b. (a, b) -> b
snd (a, [Event s])
EventReturnType ep s a
ert
  SingEP ep
EPDiscard -> []

-- | Map over an arbitrary 'EventReturnType'.
mapEventReturn ::
  forall ep sts a b.
  EventReturnTypeRep ep =>
  (a -> b) ->
  EventReturnType ep sts a ->
  EventReturnType ep sts b
mapEventReturn :: (a -> b) -> EventReturnType ep sts a -> EventReturnType ep sts b
mapEventReturn a -> b
f EventReturnType ep sts a
ert = case EventReturnTypeRep ep => SingEP ep
forall (ert :: EventPolicy). EventReturnTypeRep ert => SingEP ert
eventReturnTypeRep @ep of
  SingEP ep
EPReturn -> (a -> b) -> (a, [Event sts]) -> (b, [Event sts])
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first a -> b
f (a, [Event sts])
EventReturnType ep sts a
ert
  SingEP ep
EPDiscard -> a -> b
f a
EventReturnType ep sts a
ert

data Clause sts (rtype :: RuleType) a where
  Lift ::
    STS sts =>
    (BaseM sts) a ->
    (a -> b) ->
    Clause sts rtype b
  GetCtx ::
    (RuleContext rtype sts -> a) ->
    Clause sts rtype a
  SubTrans ::
    Embed sub sts =>
    RuleContext rtype sub ->
    -- Subsequent computation with state introduced
    (State sub -> a) ->
    Clause sts rtype a
  Writer ::
    [Event sts] ->
    a ->
    Clause sts rtype a
  Predicate ::
    Validation (NonEmpty e) a ->
    -- Type of failure to return if the predicate fails
    (e -> PredicateFailure sts) ->
    a ->
    Clause sts rtype a
  -- | Label part of a rule. The interpreter may be configured to only run parts
  -- of rules governed by (or by the lack of) certain labels.
  Label ::
    NonEmpty Label ->
    Rule sts rtype a ->
    a ->
    Clause sts rtype a
  IfFailureFree :: Rule sts rtype a -> Rule sts rtype a -> Clause sts rtype a

deriving instance Functor (Clause sts rtype)

type Rule sts rtype = F (Clause sts rtype)

-- | Label for a predicate. This can be used to control which predicates get
-- run.
type Label = String

-- | Fail with `PredicateFailure`'s in STS if `Validation` was unsuccessful.
validate :: Validation (NonEmpty (PredicateFailure sts)) () -> Rule sts ctx ()
validate :: Validation (NonEmpty (PredicateFailure sts)) () -> Rule sts ctx ()
validate = (PredicateFailure sts -> PredicateFailure sts)
-> Validation (NonEmpty (PredicateFailure sts)) ()
-> Rule sts ctx ()
forall e sts (ctx :: RuleType).
(e -> PredicateFailure sts)
-> Validation (NonEmpty e) () -> Rule sts ctx ()
validateTrans PredicateFailure sts -> PredicateFailure sts
forall a. a -> a
id

-- | Same as `validation`, except with ability to transform opaque failures
-- into `PredicateFailure`s with a help of supplied function.
validateTrans ::
  -- | Transformation function for all errors
  (e -> PredicateFailure sts) ->
  Validation (NonEmpty e) () ->
  Rule sts ctx ()
validateTrans :: (e -> PredicateFailure sts)
-> Validation (NonEmpty e) () -> Rule sts ctx ()
validateTrans e -> PredicateFailure sts
t Validation (NonEmpty e) ()
v = Clause sts ctx () -> Rule sts ctx ()
forall (f :: * -> *) (m :: * -> *) a.
(Functor f, MonadFree f m) =>
f a -> m a
liftF (Clause sts ctx () -> Rule sts ctx ())
-> Clause sts ctx () -> Rule sts ctx ()
forall a b. (a -> b) -> a -> b
$ Validation (NonEmpty e) ()
-> (e -> PredicateFailure sts) -> () -> Clause sts ctx ()
forall e a sts (rtype :: RuleType).
Validation (NonEmpty e) a
-> (e -> PredicateFailure sts) -> a -> Clause sts rtype a
Predicate Validation (NonEmpty e) ()
v e -> PredicateFailure sts
t ()

-- | Same as `validation`, except with ability to translate opaque failures
-- into `PredicateFailure`s with a help of supplied function.
validateTransLabeled ::
  -- | Transformation function for all errors
  (e -> PredicateFailure sts) ->
  -- | Supply a list of labels to be used as filters when STS is executed
  NonEmpty Label ->
  -- | Actual validations to be executed
  Validation (NonEmpty e) () ->
  Rule sts ctx ()
validateTransLabeled :: (e -> PredicateFailure sts)
-> NonEmpty String -> Validation (NonEmpty e) () -> Rule sts ctx ()
validateTransLabeled e -> PredicateFailure sts
t NonEmpty String
labels Validation (NonEmpty e) ()
v = Clause sts ctx () -> Rule sts ctx ()
forall (f :: * -> *) (m :: * -> *) a.
(Functor f, MonadFree f m) =>
f a -> m a
liftF (Clause sts ctx () -> Rule sts ctx ())
-> Clause sts ctx () -> Rule sts ctx ()
forall a b. (a -> b) -> a -> b
$ NonEmpty String -> Rule sts ctx () -> () -> Clause sts ctx ()
forall sts (rtype :: RuleType) a.
NonEmpty String -> Rule sts rtype a -> a -> Clause sts rtype a
Label NonEmpty String
labels (Clause sts ctx () -> Rule sts ctx ()
forall (f :: * -> *) (m :: * -> *) a.
(Functor f, MonadFree f m) =>
f a -> m a
liftF (Clause sts ctx () -> Rule sts ctx ())
-> Clause sts ctx () -> Rule sts ctx ()
forall a b. (a -> b) -> a -> b
$ Validation (NonEmpty e) ()
-> (e -> PredicateFailure sts) -> () -> Clause sts ctx ()
forall e a sts (rtype :: RuleType).
Validation (NonEmpty e) a
-> (e -> PredicateFailure sts) -> a -> Clause sts rtype a
Predicate Validation (NonEmpty e) ()
v e -> PredicateFailure sts
t ()) ()

-- | Oh noes!
--
--   This takes a condition (a boolean expression) and a failure and results in
--   a clause which will throw that failure if the condition fails.
(?!) :: Bool -> PredicateFailure sts -> Rule sts ctx ()
?! :: Bool -> PredicateFailure sts -> Rule sts ctx ()
(?!) Bool
cond PredicateFailure sts
onFail =
  Clause sts ctx () -> Rule sts ctx ()
forall (f :: * -> *) (m :: * -> *) a.
(Functor f, MonadFree f m) =>
f a -> m a
liftF (Clause sts ctx () -> Rule sts ctx ())
-> Clause sts ctx () -> Rule sts ctx ()
forall a b. (a -> b) -> a -> b
$
    Validation (NonEmpty (PredicateFailure sts)) ()
-> (PredicateFailure sts -> PredicateFailure sts)
-> ()
-> Clause sts ctx ()
forall e a sts (rtype :: RuleType).
Validation (NonEmpty e) a
-> (e -> PredicateFailure sts) -> a -> Clause sts rtype a
Predicate (if Bool
cond then () -> Validation (NonEmpty (PredicateFailure sts)) ()
forall e a. a -> Validation e a
Success () else NonEmpty (PredicateFailure sts)
-> Validation (NonEmpty (PredicateFailure sts)) ()
forall e a. e -> Validation e a
Failure (PredicateFailure sts
onFail PredicateFailure sts
-> [PredicateFailure sts] -> NonEmpty (PredicateFailure sts)
forall a. a -> [a] -> NonEmpty a
:| [])) PredicateFailure sts -> PredicateFailure sts
forall a. a -> a
id ()

infix 1 ?!

failBecause :: PredicateFailure sts -> Rule sts ctx ()
failBecause :: PredicateFailure sts -> Rule sts ctx ()
failBecause = (Bool
False Bool -> PredicateFailure sts -> Rule sts ctx ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?!)

-- | Oh noes with an explanation
--
--   We interpret this as "What?" "No!" "Because:"
(?!:) :: Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
?!: :: Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
(?!:) Either e ()
cond e -> PredicateFailure sts
onFail =
  Clause sts ctx () -> Rule sts ctx ()
forall (f :: * -> *) (m :: * -> *) a.
(Functor f, MonadFree f m) =>
f a -> m a
liftF (Clause sts ctx () -> Rule sts ctx ())
-> Clause sts ctx () -> Rule sts ctx ()
forall a b. (a -> b) -> a -> b
$
    Validation (NonEmpty e) ()
-> (e -> PredicateFailure sts) -> () -> Clause sts ctx ()
forall e a sts (rtype :: RuleType).
Validation (NonEmpty e) a
-> (e -> PredicateFailure sts) -> a -> Clause sts rtype a
Predicate (Either (NonEmpty e) () -> Validation (NonEmpty e) ()
forall e a. Either e a -> Validation e a
eitherToValidation (Either (NonEmpty e) () -> Validation (NonEmpty e) ())
-> Either (NonEmpty e) () -> Validation (NonEmpty e) ()
forall a b. (a -> b) -> a -> b
$ (e -> NonEmpty e) -> Either e () -> Either (NonEmpty e) ()
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first e -> NonEmpty e
forall (f :: * -> *) a. Applicative f => a -> f a
pure Either e ()
cond) e -> PredicateFailure sts
onFail ()

-- | Labeled predicate. This may be used to control which predicates are run
-- using 'ValidateSuchThat'.
labeledPred :: NonEmpty Label -> Bool -> PredicateFailure sts -> Rule sts ctx ()
labeledPred :: NonEmpty String -> Bool -> PredicateFailure sts -> Rule sts ctx ()
labeledPred NonEmpty String
lbls Bool
cond PredicateFailure sts
orElse = NonEmpty String -> Rule sts ctx () -> Rule sts ctx ()
forall sts (ctx :: RuleType).
NonEmpty String -> Rule sts ctx () -> Rule sts ctx ()
labeled NonEmpty String
lbls (Bool
cond Bool -> PredicateFailure sts -> Rule sts ctx ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure sts
orElse)

-- | Labeled predicate with an explanation
labeledPredE ::
  NonEmpty Label ->
  Either e () ->
  (e -> PredicateFailure sts) ->
  Rule sts ctx ()
labeledPredE :: NonEmpty String
-> Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
labeledPredE NonEmpty String
lbls Either e ()
cond e -> PredicateFailure sts
orElse = NonEmpty String -> Rule sts ctx () -> Rule sts ctx ()
forall sts (ctx :: RuleType).
NonEmpty String -> Rule sts ctx () -> Rule sts ctx ()
labeled NonEmpty String
lbls (Either e ()
cond Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
forall e sts (ctx :: RuleType).
Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
?!: e -> PredicateFailure sts
orElse)

-- | Labeled clause. This will only be executed if the interpreter is set to
-- execute clauses with this label.
labeled :: NonEmpty Label -> Rule sts ctx () -> Rule sts ctx ()
labeled :: NonEmpty String -> Rule sts ctx () -> Rule sts ctx ()
labeled NonEmpty String
lbls Rule sts ctx ()
subrule = Clause sts ctx () -> Rule sts ctx ()
forall (f :: * -> *) (m :: * -> *) a.
(Functor f, MonadFree f m) =>
f a -> m a
liftF (Clause sts ctx () -> Rule sts ctx ())
-> Clause sts ctx () -> Rule sts ctx ()
forall a b. (a -> b) -> a -> b
$ NonEmpty String -> Rule sts ctx () -> () -> Clause sts ctx ()
forall sts (rtype :: RuleType) a.
NonEmpty String -> Rule sts rtype a -> a -> Clause sts rtype a
Label NonEmpty String
lbls Rule sts ctx ()
subrule ()

trans ::
  Embed sub super => RuleContext rtype sub -> Rule super rtype (State sub)
trans :: RuleContext rtype sub -> Rule super rtype (State sub)
trans RuleContext rtype sub
ctx = Clause super rtype (Rule super rtype (State sub))
-> Rule super rtype (State sub)
forall (f :: * -> *) (m :: * -> *) a.
MonadFree f m =>
f (m a) -> m a
wrap (Clause super rtype (Rule super rtype (State sub))
 -> Rule super rtype (State sub))
-> Clause super rtype (Rule super rtype (State sub))
-> Rule super rtype (State sub)
forall a b. (a -> b) -> a -> b
$ RuleContext rtype sub
-> (State sub -> Rule super rtype (State sub))
-> Clause super rtype (Rule super rtype (State sub))
forall sub sts (rtype :: RuleType) a.
Embed sub sts =>
RuleContext rtype sub -> (State sub -> a) -> Clause sts rtype a
SubTrans RuleContext rtype sub
ctx State sub -> Rule super rtype (State sub)
forall (f :: * -> *) a. Applicative f => a -> f a
pure

ifFailureFree :: Rule sts rtype a -> Rule sts rtype a -> Rule sts rtype a
ifFailureFree :: Rule sts rtype a -> Rule sts rtype a -> Rule sts rtype a
ifFailureFree Rule sts rtype a
x Rule sts rtype a
y = Clause sts rtype a -> Rule sts rtype a
forall (f :: * -> *) (m :: * -> *) a.
(Functor f, MonadFree f m) =>
f a -> m a
liftF (Rule sts rtype a -> Rule sts rtype a -> Clause sts rtype a
forall sts (rtype :: RuleType) a.
Rule sts rtype a -> Rule sts rtype a -> Clause sts rtype a
IfFailureFree Rule sts rtype a
x Rule sts rtype a
y)

whenFailureFree :: Rule sts rtype () -> Rule sts rtype ()
whenFailureFree :: Rule sts rtype () -> Rule sts rtype ()
whenFailureFree Rule sts rtype ()
action = Rule sts rtype () -> Rule sts rtype () -> Rule sts rtype ()
forall sts (rtype :: RuleType) a.
Rule sts rtype a -> Rule sts rtype a -> Rule sts rtype a
ifFailureFree Rule sts rtype ()
action (() -> Rule sts rtype ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())

liftSTS ::
  STS sts =>
  (BaseM sts) a ->
  Rule sts ctx a
liftSTS :: BaseM sts a -> Rule sts ctx a
liftSTS BaseM sts a
f = Clause sts ctx (Rule sts ctx a) -> Rule sts ctx a
forall (f :: * -> *) (m :: * -> *) a.
MonadFree f m =>
f (m a) -> m a
wrap (Clause sts ctx (Rule sts ctx a) -> Rule sts ctx a)
-> Clause sts ctx (Rule sts ctx a) -> Rule sts ctx a
forall a b. (a -> b) -> a -> b
$ BaseM sts a
-> (a -> Rule sts ctx a) -> Clause sts ctx (Rule sts ctx a)
forall sts a b (rtype :: RuleType).
STS sts =>
BaseM sts a -> (a -> b) -> Clause sts rtype b
Lift BaseM sts a
f a -> Rule sts ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- | Get the judgment context
judgmentContext :: Rule sts rtype (RuleContext rtype sts)
judgmentContext :: Rule sts rtype (RuleContext rtype sts)
judgmentContext = Clause sts rtype (Rule sts rtype (RuleContext rtype sts))
-> Rule sts rtype (RuleContext rtype sts)
forall (f :: * -> *) (m :: * -> *) a.
MonadFree f m =>
f (m a) -> m a
wrap (Clause sts rtype (Rule sts rtype (RuleContext rtype sts))
 -> Rule sts rtype (RuleContext rtype sts))
-> Clause sts rtype (Rule sts rtype (RuleContext rtype sts))
-> Rule sts rtype (RuleContext rtype sts)
forall a b. (a -> b) -> a -> b
$ (RuleContext rtype sts -> Rule sts rtype (RuleContext rtype sts))
-> Clause sts rtype (Rule sts rtype (RuleContext rtype sts))
forall (rtype :: RuleType) sts a.
(RuleContext rtype sts -> a) -> Clause sts rtype a
GetCtx RuleContext rtype sts -> Rule sts rtype (RuleContext rtype sts)
forall (f :: * -> *) a. Applicative f => a -> f a
pure

{------------------------------------------------------------------------------
-- STS interpreters
------------------------------------------------------------------------------}

-- | Control which assertions are enabled.
data AssertionPolicy
  = AssertionsAll
  | -- | Only run preconditions
    AssertionsPre
  | -- | Only run postconditions
    AssertionsPost
  | AssertionsOff
  deriving (AssertionPolicy -> AssertionPolicy -> Bool
(AssertionPolicy -> AssertionPolicy -> Bool)
-> (AssertionPolicy -> AssertionPolicy -> Bool)
-> Eq AssertionPolicy
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AssertionPolicy -> AssertionPolicy -> Bool
$c/= :: AssertionPolicy -> AssertionPolicy -> Bool
== :: AssertionPolicy -> AssertionPolicy -> Bool
$c== :: AssertionPolicy -> AssertionPolicy -> Bool
Eq, Int -> AssertionPolicy -> ShowS
[AssertionPolicy] -> ShowS
AssertionPolicy -> String
(Int -> AssertionPolicy -> ShowS)
-> (AssertionPolicy -> String)
-> ([AssertionPolicy] -> ShowS)
-> Show AssertionPolicy
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AssertionPolicy] -> ShowS
$cshowList :: [AssertionPolicy] -> ShowS
show :: AssertionPolicy -> String
$cshow :: AssertionPolicy -> String
showsPrec :: Int -> AssertionPolicy -> ShowS
$cshowsPrec :: Int -> AssertionPolicy -> ShowS
Show)

-- | Control which predicates are evaluated during rule processing.
data ValidationPolicy
  = ValidateAll
  | ValidateNone
  | ValidateSuchThat ([Label] -> Bool)

data ApplySTSOpts ep = ApplySTSOpts
  { -- | Enable assertions during STS processing.
    --   If this option is enabled, STS processing will terminate on violation
    --   of an assertion.
    ApplySTSOpts ep -> AssertionPolicy
asoAssertions :: AssertionPolicy,
    -- | Validation policy
    ApplySTSOpts ep -> ValidationPolicy
asoValidation :: ValidationPolicy,
    -- | Event policy
    ApplySTSOpts ep -> SingEP ep
asoEvents :: SingEP ep
  }

type STSInterpreter ep =
  forall s m rtype.
  (STS s, RuleTypeRep rtype, m ~ BaseM s) =>
  RuleContext rtype s ->
  m (EventReturnType ep s (State s, [PredicateFailure s]))

type RuleInterpreter ep =
  forall s m rtype.
  (STS s, RuleTypeRep rtype, m ~ BaseM s) =>
  RuleContext rtype s ->
  Rule s rtype (State s) ->
  m (EventReturnType ep s (State s, [PredicateFailure s]))

-- | Apply an STS with options. Note that this returns both the final state and
-- the list of predicate failures.
applySTSOpts ::
  forall s m rtype ep.
  (STS s, RuleTypeRep rtype, m ~ BaseM s) =>
  ApplySTSOpts ep ->
  RuleContext rtype s ->
  m (EventReturnType ep s (State s, [PredicateFailure s]))
applySTSOpts :: ApplySTSOpts ep
-> RuleContext rtype s
-> m (EventReturnType ep s (State s, [PredicateFailure s]))
applySTSOpts ApplySTSOpts {AssertionPolicy
asoAssertions :: AssertionPolicy
asoAssertions :: forall (ep :: EventPolicy). ApplySTSOpts ep -> AssertionPolicy
asoAssertions, ValidationPolicy
asoValidation :: ValidationPolicy
asoValidation :: forall (ep :: EventPolicy). ApplySTSOpts ep -> ValidationPolicy
asoValidation, SingEP ep
asoEvents :: SingEP ep
asoEvents :: forall (ep :: EventPolicy). ApplySTSOpts ep -> SingEP ep
asoEvents} RuleContext rtype s
ctx =
  let goRule :: IsFailing -> RuleInterpreter ep
      goRule :: IsFailing -> RuleInterpreter ep
goRule IsFailing
isFailing = IsFailing
-> SingEP ep
-> ValidationPolicy
-> (IsFailing -> STSInterpreter ep)
-> RuleContext rtype s
-> Rule s rtype (State s)
-> m (EventReturnType ep s (State s, [PredicateFailure s]))
forall (ep :: EventPolicy) s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
IsFailing
-> SingEP ep
-> ValidationPolicy
-> (IsFailing -> STSInterpreter ep)
-> RuleContext rtype s
-> Rule s rtype (State s)
-> m (EventReturnType ep s (State s, [PredicateFailure s]))
applyRuleInternal IsFailing
isFailing SingEP ep
asoEvents ValidationPolicy
asoValidation IsFailing -> STSInterpreter ep
goSTS
      goSTS :: IsFailing -> STSInterpreter ep
      goSTS :: IsFailing -> STSInterpreter ep
goSTS IsFailing
isFailing RuleContext rtype s
c =
        ExceptT
  (AssertionViolation s)
  m
  (EventReturnType ep s (State s, [PredicateFailure s]))
-> m (Either
        (AssertionViolation s)
        (EventReturnType ep s (State s, [PredicateFailure s])))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (SingEP ep
-> AssertionPolicy
-> RuleInterpreter ep
-> RuleContext rtype s
-> ExceptT
     (AssertionViolation s)
     m
     (EventReturnType ep s (State s, [PredicateFailure s]))
forall s (m :: * -> *) (rtype :: RuleType) (ep :: EventPolicy).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
SingEP ep
-> AssertionPolicy
-> RuleInterpreter ep
-> RuleContext rtype s
-> ExceptT
     (AssertionViolation s)
     m
     (EventReturnType ep s (State s, [PredicateFailure s]))
applySTSInternal SingEP ep
asoEvents AssertionPolicy
asoAssertions (IsFailing -> RuleInterpreter ep
goRule IsFailing
isFailing) RuleContext rtype s
c) m (Either
     (AssertionViolation s)
     (EventReturnType ep s (State s, [PredicateFailure s])))
-> (Either
      (AssertionViolation s)
      (EventReturnType ep s (State s, [PredicateFailure s]))
    -> m (EventReturnType ep s (State s, [PredicateFailure s])))
-> m (EventReturnType ep s (State s, [PredicateFailure s]))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Left AssertionViolation s
err -> AssertionException
-> m (EventReturnType ep s (State s, [PredicateFailure s]))
forall a e. Exception e => e -> a
throw (AssertionException
 -> m (EventReturnType ep s (State s, [PredicateFailure s])))
-> AssertionException
-> m (EventReturnType ep s (State s, [PredicateFailure s]))
forall a b. (a -> b) -> a -> b
$! AssertionViolation s -> AssertionException
forall sts. STS sts => AssertionViolation sts -> AssertionException
AssertionException AssertionViolation s
err
          Right EventReturnType ep s (State s, [PredicateFailure s])
res -> EventReturnType ep s (State s, [PredicateFailure s])
-> m (EventReturnType ep s (State s, [PredicateFailure s]))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EventReturnType ep s (State s, [PredicateFailure s])
 -> m (EventReturnType ep s (State s, [PredicateFailure s])))
-> EventReturnType ep s (State s, [PredicateFailure s])
-> m (EventReturnType ep s (State s, [PredicateFailure s]))
forall a b. (a -> b) -> a -> b
$! EventReturnType ep s (State s, [PredicateFailure s])
res
   in IsFailing
-> RuleContext rtype s
-> m (EventReturnType ep s (State s, [PredicateFailure s]))
IsFailing -> STSInterpreter ep
goSTS IsFailing
NotFailing RuleContext rtype s
ctx

applySTSOptsEither ::
  forall s m rtype ep.
  (STS s, RuleTypeRep rtype, m ~ BaseM s) =>
  ApplySTSOpts ep ->
  RuleContext rtype s ->
  m (Either [PredicateFailure s] (EventReturnType ep s (State s)))
applySTSOptsEither :: ApplySTSOpts ep
-> RuleContext rtype s
-> m (Either [PredicateFailure s] (EventReturnType ep s (State s)))
applySTSOptsEither ApplySTSOpts ep
opts RuleContext rtype s
ctx =
  let r1 :: m (EventReturnType ep s (State s, [PredicateFailure s]))
r1 = ApplySTSOpts ep
-> RuleContext rtype s
-> m (EventReturnType ep s (State s, [PredicateFailure s]))
forall s (m :: * -> *) (rtype :: RuleType) (ep :: EventPolicy).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
ApplySTSOpts ep
-> RuleContext rtype s
-> m (EventReturnType ep s (State s, [PredicateFailure s]))
applySTSOpts ApplySTSOpts ep
opts RuleContext rtype s
ctx
   in case ApplySTSOpts ep -> SingEP ep
forall (ep :: EventPolicy). ApplySTSOpts ep -> SingEP ep
asoEvents ApplySTSOpts ep
opts of
        SingEP ep
EPDiscard ->
          m (State s, [PredicateFailure s])
m (EventReturnType ep s (State s, [PredicateFailure s]))
r1 m (State s, [PredicateFailure s])
-> ((State s, [PredicateFailure s])
    -> Either [PredicateFailure s] (State s))
-> m (Either [PredicateFailure s] (State s))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
            (State s
st, []) -> State s -> Either [PredicateFailure s] (State s)
forall a b. b -> Either a b
Right State s
st
            (State s
_, [PredicateFailure s]
pfs) -> [PredicateFailure s] -> Either [PredicateFailure s] (State s)
forall a b. a -> Either a b
Left [PredicateFailure s]
pfs
        SingEP ep
EPReturn ->
          m ((State s, [PredicateFailure s]), [Event s])
m (EventReturnType ep s (State s, [PredicateFailure s]))
r1 m ((State s, [PredicateFailure s]), [Event s])
-> (((State s, [PredicateFailure s]), [Event s])
    -> Either [PredicateFailure s] (State s, [Event s]))
-> m (Either [PredicateFailure s] (State s, [Event s]))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
            ((State s
st, []), [Event s]
evts) -> (State s, [Event s])
-> Either [PredicateFailure s] (State s, [Event s])
forall a b. b -> Either a b
Right (State s
st, [Event s]
evts)
            ((State s
_, [PredicateFailure s]
pfs), [Event s]
_) -> [PredicateFailure s]
-> Either [PredicateFailure s] (State s, [Event s])
forall a b. a -> Either a b
Left [PredicateFailure s]
pfs

applySTS ::
  forall s m rtype.
  (STS s, RuleTypeRep rtype, m ~ BaseM s) =>
  RuleContext rtype s ->
  m (Either [PredicateFailure s] (State s))
applySTS :: RuleContext rtype s -> m (Either [PredicateFailure s] (State s))
applySTS = ApplySTSOpts 'EventPolicyDiscard
-> RuleContext rtype s
-> m (Either
        [PredicateFailure s]
        (EventReturnType 'EventPolicyDiscard s (State s)))
forall s (m :: * -> *) (rtype :: RuleType) (ep :: EventPolicy).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
ApplySTSOpts ep
-> RuleContext rtype s
-> m (Either [PredicateFailure s] (EventReturnType ep s (State s)))
applySTSOptsEither ApplySTSOpts 'EventPolicyDiscard
defaultOpts
  where
    defaultOpts :: ApplySTSOpts 'EventPolicyDiscard
defaultOpts =
      ApplySTSOpts :: forall (ep :: EventPolicy).
AssertionPolicy -> ValidationPolicy -> SingEP ep -> ApplySTSOpts ep
ApplySTSOpts
        { asoAssertions :: AssertionPolicy
asoAssertions = AssertionPolicy
globalAssertionPolicy,
          asoValidation :: ValidationPolicy
asoValidation = ValidationPolicy
ValidateAll,
          asoEvents :: SingEP 'EventPolicyDiscard
asoEvents = SingEP 'EventPolicyDiscard
EPDiscard
        }

globalAssertionPolicy :: AssertionPolicy

#ifdef STS_ASSERT
globalAssertionPolicy = AssertionsAll
#else
globalAssertionPolicy :: AssertionPolicy
globalAssertionPolicy = AssertionPolicy
AssertionsOff
#endif

-- | Re-apply an STS.
--
--   It is assumed that the caller of this function has previously applied this
--   STS, and can guarantee that it completed successfully. No predicates or
--   assertions will be checked when calling this function.
reapplySTS ::
  forall s m rtype.
  (STS s, RuleTypeRep rtype, m ~ BaseM s) =>
  RuleContext rtype s ->
  m (State s)
reapplySTS :: RuleContext rtype s -> m (State s)
reapplySTS RuleContext rtype s
ctx = ApplySTSOpts 'EventPolicyDiscard
-> RuleContext rtype s
-> m (EventReturnType
        'EventPolicyDiscard s (State s, [PredicateFailure s]))
forall s (m :: * -> *) (rtype :: RuleType) (ep :: EventPolicy).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
ApplySTSOpts ep
-> RuleContext rtype s
-> m (EventReturnType ep s (State s, [PredicateFailure s]))
applySTSOpts ApplySTSOpts 'EventPolicyDiscard
defaultOpts RuleContext rtype s
ctx m (State s, [PredicateFailure s])
-> ((State s, [PredicateFailure s]) -> State s) -> m (State s)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (State s, [PredicateFailure s]) -> State s
forall a b. (a, b) -> a
fst
  where
    defaultOpts :: ApplySTSOpts 'EventPolicyDiscard
defaultOpts =
      ApplySTSOpts :: forall (ep :: EventPolicy).
AssertionPolicy -> ValidationPolicy -> SingEP ep -> ApplySTSOpts ep
ApplySTSOpts
        { asoAssertions :: AssertionPolicy
asoAssertions = AssertionPolicy
AssertionsOff,
          asoValidation :: ValidationPolicy
asoValidation = ValidationPolicy
ValidateNone,
          asoEvents :: SingEP 'EventPolicyDiscard
asoEvents = SingEP 'EventPolicyDiscard
EPDiscard
        }

applySTSIndifferently ::
  forall s m rtype.
  (STS s, RuleTypeRep rtype, m ~ BaseM s) =>
  RuleContext rtype s ->
  m (State s, [PredicateFailure s])
applySTSIndifferently :: RuleContext rtype s -> m (State s, [PredicateFailure s])
applySTSIndifferently =
  ApplySTSOpts 'EventPolicyDiscard
-> RuleContext rtype s
-> m (EventReturnType
        'EventPolicyDiscard s (State s, [PredicateFailure s]))
forall s (m :: * -> *) (rtype :: RuleType) (ep :: EventPolicy).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
ApplySTSOpts ep
-> RuleContext rtype s
-> m (EventReturnType ep s (State s, [PredicateFailure s]))
applySTSOpts
    ApplySTSOpts :: forall (ep :: EventPolicy).
AssertionPolicy -> ValidationPolicy -> SingEP ep -> ApplySTSOpts ep
ApplySTSOpts
      { asoAssertions :: AssertionPolicy
asoAssertions = AssertionPolicy
AssertionsAll,
        asoValidation :: ValidationPolicy
asoValidation = ValidationPolicy
ValidateAll,
        asoEvents :: SingEP 'EventPolicyDiscard
asoEvents = SingEP 'EventPolicyDiscard
EPDiscard
      }

-- | Apply a rule even if its predicates fail.
--
--   If the rule successfully applied, the list of predicate failures will be
--   empty.
applyRuleInternal ::
  forall (ep :: EventPolicy) s m rtype.
  (STS s, RuleTypeRep rtype, m ~ BaseM s) =>
  -- | We need to know if the current STS incurred at least one
  -- PredicateFailure.  This is necessary because `applyRuleInternal` is called
  -- recursively through the @goSTS@ argument, which will not have access to any
  -- of the predicate failures occured in other branches of STS rule execusion tree.
  IsFailing ->
  SingEP ep ->
  ValidationPolicy ->
  -- | Interpreter for subsystems
  (IsFailing -> STSInterpreter ep) ->
  RuleContext rtype s ->
  Rule s rtype (State s) ->
  m (EventReturnType ep s (State s, [PredicateFailure s]))
applyRuleInternal :: IsFailing
-> SingEP ep
-> ValidationPolicy
-> (IsFailing -> STSInterpreter ep)
-> RuleContext rtype s
-> Rule s rtype (State s)
-> m (EventReturnType ep s (State s, [PredicateFailure s]))
applyRuleInternal IsFailing
isAlreadyFailing SingEP ep
ep ValidationPolicy
vp IsFailing -> STSInterpreter ep
goSTS RuleContext rtype s
jc Rule s rtype (State s)
r = do
  (State s
s, ([PredicateFailure s], [Event s])
er) <- (StateT ([PredicateFailure s], [Event s]) m (State s)
 -> ([PredicateFailure s], [Event s])
 -> m (State s, ([PredicateFailure s], [Event s])))
-> ([PredicateFailure s], [Event s])
-> StateT ([PredicateFailure s], [Event s]) m (State s)
-> m (State s, ([PredicateFailure s], [Event s]))
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT ([PredicateFailure s], [Event s]) m (State s)
-> ([PredicateFailure s], [Event s])
-> m (State s, ([PredicateFailure s], [Event s]))
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT ([], []) (StateT ([PredicateFailure s], [Event s]) m (State s)
 -> m (State s, ([PredicateFailure s], [Event s])))
-> StateT ([PredicateFailure s], [Event s]) m (State s)
-> m (State s, ([PredicateFailure s], [Event s]))
forall a b. (a -> b) -> a -> b
$ (forall x.
 Clause s rtype x -> StateT ([PredicateFailure s], [Event s]) m x)
-> Rule s rtype (State s)
-> StateT ([PredicateFailure s], [Event s]) m (State s)
forall (m :: * -> *) (f :: * -> *) a.
Monad m =>
(forall x. f x -> m x) -> F f a -> m a
foldF forall x.
Clause s rtype x -> StateT ([PredicateFailure s], [Event s]) m x
runClause Rule s rtype (State s)
r
  case SingEP ep
ep of
    SingEP ep
EPDiscard -> (State s, [PredicateFailure s])
-> m (State s, [PredicateFailure s])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (State s
s, ([PredicateFailure s], [Event s]) -> [PredicateFailure s]
forall a b. (a, b) -> a
fst ([PredicateFailure s], [Event s])
er)
    SingEP ep
EPReturn -> ((State s, [PredicateFailure s]), [Event s])
-> m ((State s, [PredicateFailure s]), [Event s])
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((State s
s, ([PredicateFailure s], [Event s]) -> [PredicateFailure s]
forall a b. (a, b) -> a
fst ([PredicateFailure s], [Event s])
er), ([PredicateFailure s], [Event s]) -> [Event s]
forall a b. (a, b) -> b
snd ([PredicateFailure s], [Event s])
er)
  where
    isFailing :: StateT ([PredicateFailure s], [Event s]) m IsFailing
    isFailing :: StateT ([PredicateFailure s], [Event s]) m IsFailing
isFailing =
      case IsFailing
isAlreadyFailing of
        IsFailing
Failing -> IsFailing -> StateT ([PredicateFailure s], [Event s]) m IsFailing
forall (f :: * -> *) a. Applicative f => a -> f a
pure IsFailing
Failing
        IsFailing
NotFailing -> do
          Bool
isFailingNow <- [PredicateFailure s] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([PredicateFailure s] -> Bool)
-> (([PredicateFailure s], [Event s]) -> [PredicateFailure s])
-> ([PredicateFailure s], [Event s])
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([PredicateFailure s], [Event s]) -> [PredicateFailure s]
forall a b. (a, b) -> a
fst (([PredicateFailure s], [Event s]) -> Bool)
-> StateT
     ([PredicateFailure s], [Event s])
     m
     ([PredicateFailure s], [Event s])
-> StateT ([PredicateFailure s], [Event s]) m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT
  ([PredicateFailure s], [Event s])
  m
  ([PredicateFailure s], [Event s])
forall s (m :: * -> *). MonadState s m => m s
get
          IsFailing -> StateT ([PredicateFailure s], [Event s]) m IsFailing
forall (f :: * -> *) a. Applicative f => a -> f a
pure (IsFailing -> StateT ([PredicateFailure s], [Event s]) m IsFailing)
-> IsFailing
-> StateT ([PredicateFailure s], [Event s]) m IsFailing
forall a b. (a -> b) -> a -> b
$ if Bool
isFailingNow then IsFailing
NotFailing else IsFailing
Failing
    runClause :: Clause s rtype a -> StateT ([PredicateFailure s], [Event s]) m a
    runClause :: Clause s rtype a -> StateT ([PredicateFailure s], [Event s]) m a
runClause (Lift BaseM s a
f a -> a
next) = a -> a
next (a -> a)
-> StateT ([PredicateFailure s], [Event s]) m a
-> StateT ([PredicateFailure s], [Event s]) m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a -> StateT ([PredicateFailure s], [Event s]) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m a
BaseM s a
f
    runClause (GetCtx RuleContext rtype s -> a
next) = a -> StateT ([PredicateFailure s], [Event s]) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> StateT ([PredicateFailure s], [Event s]) m a)
-> a -> StateT ([PredicateFailure s], [Event s]) m a
forall a b. (a -> b) -> a -> b
$ RuleContext rtype s -> a
next RuleContext rtype s
jc
    runClause (IfFailureFree Rule s rtype a
notFailingRule Rule s rtype a
failingRule) = do
      StateT ([PredicateFailure s], [Event s]) m IsFailing
isFailing StateT ([PredicateFailure s], [Event s]) m IsFailing
-> (IsFailing -> StateT ([PredicateFailure s], [Event s]) m a)
-> StateT ([PredicateFailure s], [Event s]) m a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        IsFailing
Failing -> (forall x.
 Clause s rtype x -> StateT ([PredicateFailure s], [Event s]) m x)
-> Rule s rtype a -> StateT ([PredicateFailure s], [Event s]) m a
forall (m :: * -> *) (f :: * -> *) a.
Monad m =>
(forall x. f x -> m x) -> F f a -> m a
foldF forall x.
Clause s rtype x -> StateT ([PredicateFailure s], [Event s]) m x
runClause Rule s rtype a
failingRule
        IsFailing
NotFailing -> (forall x.
 Clause s rtype x -> StateT ([PredicateFailure s], [Event s]) m x)
-> Rule s rtype a -> StateT ([PredicateFailure s], [Event s]) m a
forall (m :: * -> *) (f :: * -> *) a.
Monad m =>
(forall x. f x -> m x) -> F f a -> m a
foldF forall x.
Clause s rtype x -> StateT ([PredicateFailure s], [Event s]) m x
runClause Rule s rtype a
notFailingRule
    runClause (Predicate Validation (NonEmpty e) a
cond e -> PredicateFailure s
orElse a
val) =
      case ValidationPolicy
vp of
        ValidationPolicy
ValidateNone -> a -> StateT ([PredicateFailure s], [Event s]) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
val
        ValidationPolicy
_ -> case Validation (NonEmpty e) a
cond of
          Success a
x -> a -> StateT ([PredicateFailure s], [Event s]) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
          Failure NonEmpty e
errs -> (([PredicateFailure s], [Event s])
 -> ([PredicateFailure s], [Event s]))
-> StateT ([PredicateFailure s], [Event s]) m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (([PredicateFailure s] -> [PredicateFailure s])
-> ([PredicateFailure s], [Event s])
-> ([PredicateFailure s], [Event s])
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((e -> PredicateFailure s) -> [e] -> [PredicateFailure s]
forall a b. (a -> b) -> [a] -> [b]
map e -> PredicateFailure s
orElse ([e] -> [e]
forall a. [a] -> [a]
reverse (NonEmpty e -> [e]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty e
errs)) [PredicateFailure s]
-> [PredicateFailure s] -> [PredicateFailure s]
forall a. Semigroup a => a -> a -> a
<>)) StateT ([PredicateFailure s], [Event s]) m ()
-> StateT ([PredicateFailure s], [Event s]) m a
-> StateT ([PredicateFailure s], [Event s]) m a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> StateT ([PredicateFailure s], [Event s]) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
val
    runClause (Label NonEmpty String
lbls Rule s rtype a
subrule a
val) =
      if [String] -> Bool
validateIf (NonEmpty String -> [String]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty String
lbls)
        then (forall x.
 Clause s rtype x -> StateT ([PredicateFailure s], [Event s]) m x)
-> Rule s rtype a -> StateT ([PredicateFailure s], [Event s]) m a
forall (m :: * -> *) (f :: * -> *) a.
Monad m =>
(forall x. f x -> m x) -> F f a -> m a
foldF forall x.
Clause s rtype x -> StateT ([PredicateFailure s], [Event s]) m x
runClause Rule s rtype a
subrule
        else a -> StateT ([PredicateFailure s], [Event s]) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
val
    runClause (SubTrans (subCtx :: RuleContext _rtype sub) State sub -> a
next) = do
      IsFailing
isFailingNow <- StateT ([PredicateFailure s], [Event s]) m IsFailing
isFailing
      EventReturnType ep sub (State sub, [PredicateFailure sub])
s <- m (EventReturnType ep sub (State sub, [PredicateFailure sub]))
-> StateT
     ([PredicateFailure s], [Event s])
     m
     (EventReturnType ep sub (State sub, [PredicateFailure sub]))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (EventReturnType ep sub (State sub, [PredicateFailure sub]))
 -> StateT
      ([PredicateFailure s], [Event s])
      m
      (EventReturnType ep sub (State sub, [PredicateFailure sub])))
-> m (EventReturnType ep sub (State sub, [PredicateFailure sub]))
-> StateT
     ([PredicateFailure s], [Event s])
     m
     (EventReturnType ep sub (State sub, [PredicateFailure sub]))
forall a b. (a -> b) -> a -> b
$ IsFailing
-> RuleContext rtype sub
-> m (EventReturnType ep sub (State sub, [PredicateFailure sub]))
IsFailing -> STSInterpreter ep
goSTS IsFailing
isFailingNow RuleContext rtype sub
subCtx
      let ss :: State sub
          sfails :: [PredicateFailure sub]
          sevs :: [Event sub]
          (State sub
ss, [PredicateFailure sub]
sfails) = SingEP ep
-> EventReturnType ep sub (State sub, [PredicateFailure sub])
-> (State sub, [PredicateFailure sub])
forall (ep :: EventPolicy) a.
SingEP ep -> forall s. EventReturnType ep s a -> a
discardEvents SingEP ep
ep @sub EventReturnType ep sub (State sub, [PredicateFailure sub])
s
          sevs :: [Event sub]
sevs = SingEP ep
-> EventReturnType ep sub (State sub, [PredicateFailure sub])
-> [Event sub]
forall (ep :: EventPolicy).
SingEP ep -> forall s a. EventReturnType ep s a -> [Event s]
getEvents SingEP ep
ep @sub @(State sub, [PredicateFailure sub]) EventReturnType ep sub (State sub, [PredicateFailure sub])
s
      (PredicateFailure s
 -> StateT ([PredicateFailure s], [Event s]) m ())
-> [PredicateFailure s]
-> StateT ([PredicateFailure s], [Event s]) m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (\PredicateFailure s
a -> (([PredicateFailure s], [Event s])
 -> ([PredicateFailure s], [Event s]))
-> StateT ([PredicateFailure s], [Event s]) m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (([PredicateFailure s] -> [PredicateFailure s])
-> ([PredicateFailure s], [Event s])
-> ([PredicateFailure s], [Event s])
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (PredicateFailure s
a PredicateFailure s -> [PredicateFailure s] -> [PredicateFailure s]
forall a. a -> [a] -> [a]
:))) ([PredicateFailure s]
 -> StateT ([PredicateFailure s], [Event s]) m ())
-> [PredicateFailure s]
-> StateT ([PredicateFailure s], [Event s]) m ()
forall a b. (a -> b) -> a -> b
$ Embed sub s => PredicateFailure sub -> PredicateFailure s
forall sub super.
Embed sub super =>
PredicateFailure sub -> PredicateFailure super
wrapFailed @sub @s (PredicateFailure sub -> PredicateFailure s)
-> [PredicateFailure sub] -> [PredicateFailure s]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PredicateFailure sub]
sfails
      Clause s rtype () -> StateT ([PredicateFailure s], [Event s]) m ()
forall x.
Clause s rtype x -> StateT ([PredicateFailure s], [Event s]) m x
runClause (Clause s rtype ()
 -> StateT ([PredicateFailure s], [Event s]) m ())
-> Clause s rtype ()
-> StateT ([PredicateFailure s], [Event s]) m ()
forall a b. (a -> b) -> a -> b
$ [Event s] -> () -> Clause s rtype ()
forall sts a (rtype :: RuleType).
[Event sts] -> a -> Clause sts rtype a
Writer (Embed sub s => Event sub -> Event s
forall sub super. Embed sub super => Event sub -> Event super
wrapEvent @sub @s (Event sub -> Event s) -> [Event sub] -> [Event s]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Event sub]
sevs) ()
      a -> StateT ([PredicateFailure s], [Event s]) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> StateT ([PredicateFailure s], [Event s]) m a)
-> a -> StateT ([PredicateFailure s], [Event s]) m a
forall a b. (a -> b) -> a -> b
$ State sub -> a
next State sub
ss
    runClause (Writer [Event s]
w a
a) = case SingEP ep
ep of
      SingEP ep
EPReturn -> (([PredicateFailure s], [Event s])
 -> ([PredicateFailure s], [Event s]))
-> StateT ([PredicateFailure s], [Event s]) m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (([Event s] -> [Event s])
-> ([PredicateFailure s], [Event s])
-> ([PredicateFailure s], [Event s])
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ([Event s] -> [Event s] -> [Event s]
forall a. Semigroup a => a -> a -> a
<> [Event s]
w)) StateT ([PredicateFailure s], [Event s]) m ()
-> a -> StateT ([PredicateFailure s], [Event s]) m a
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> a
a
      SingEP ep
EPDiscard -> a -> StateT ([PredicateFailure s], [Event s]) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a
    validateIf :: [String] -> Bool
validateIf [String]
lbls = case ValidationPolicy
vp of
      ValidationPolicy
ValidateAll -> Bool
True
      ValidationPolicy
ValidateNone -> Bool
False
      ValidateSuchThat [String] -> Bool
f -> [String] -> Bool
f [String]
lbls

applySTSInternal ::
  forall s m rtype ep.
  (STS s, RuleTypeRep rtype, m ~ BaseM s) =>
  SingEP ep ->
  AssertionPolicy ->
  -- | Interpreter for rules
  RuleInterpreter ep ->
  RuleContext rtype s ->
  ExceptT (AssertionViolation s) m (EventReturnType ep s (State s, [PredicateFailure s]))
applySTSInternal :: SingEP ep
-> AssertionPolicy
-> RuleInterpreter ep
-> RuleContext rtype s
-> ExceptT
     (AssertionViolation s)
     m
     (EventReturnType ep s (State s, [PredicateFailure s]))
applySTSInternal SingEP ep
ep AssertionPolicy
ap RuleInterpreter ep
goRule RuleContext rtype s
ctx =
  [EventReturnType ep s (State s, [PredicateFailure s])]
-> EventReturnType ep s (State s, [PredicateFailure s])
successOrFirstFailure ([EventReturnType ep s (State s, [PredicateFailure s])]
 -> EventReturnType ep s (State s, [PredicateFailure s]))
-> ExceptT
     (AssertionViolation s)
     m
     [EventReturnType ep s (State s, [PredicateFailure s])]
-> ExceptT
     (AssertionViolation s)
     m
     (EventReturnType ep s (State s, [PredicateFailure s]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SRuleType rtype
-> RuleContext rtype s
-> ExceptT
     (AssertionViolation s)
     m
     [EventReturnType ep s (State s, [PredicateFailure s])]
applySTSInternal' SRuleType rtype
forall (t :: RuleType). RuleTypeRep t => SRuleType t
rTypeRep RuleContext rtype s
ctx
  where
    successOrFirstFailure ::
      [EventReturnType ep s (State s, [PredicateFailure s])] ->
      EventReturnType ep s (State s, [PredicateFailure s])
    successOrFirstFailure :: [EventReturnType ep s (State s, [PredicateFailure s])]
-> EventReturnType ep s (State s, [PredicateFailure s])
successOrFirstFailure [EventReturnType ep s (State s, [PredicateFailure s])]
xs =
      case (EventReturnType ep s (State s, [PredicateFailure s]) -> Bool)
-> [EventReturnType ep s (State s, [PredicateFailure s])]
-> Maybe (EventReturnType ep s (State s, [PredicateFailure s]))
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\EventReturnType ep s (State s, [PredicateFailure s])
x -> [PredicateFailure s] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([PredicateFailure s] -> Bool) -> [PredicateFailure s] -> Bool
forall a b. (a -> b) -> a -> b
$ (State s, [PredicateFailure s]) -> [PredicateFailure s]
forall a b. (a, b) -> b
snd (SingEP ep
-> EventReturnType ep s (State s, [PredicateFailure s])
-> (State s, [PredicateFailure s])
forall (ep :: EventPolicy) a.
SingEP ep -> forall s. EventReturnType ep s a -> a
discardEvents SingEP ep
ep @s EventReturnType ep s (State s, [PredicateFailure s])
x :: (State s, [PredicateFailure s]))) [EventReturnType ep s (State s, [PredicateFailure s])]
xs of
        Maybe (EventReturnType ep s (State s, [PredicateFailure s]))
Nothing ->
          case [EventReturnType ep s (State s, [PredicateFailure s])]
xs of
            [] -> String -> EventReturnType ep s (State s, [PredicateFailure s])
forall a. HasCallStack => String -> a
error String
"applySTSInternal was called with an empty set of rules"
            EventReturnType ep s (State s, [PredicateFailure s])
s' : [EventReturnType ep s (State s, [PredicateFailure s])]
_ -> case SingEP ep
ep of
              SingEP ep
EPDiscard -> ((State s, [PredicateFailure s]) -> State s
forall a b. (a, b) -> a
fst (State s, [PredicateFailure s])
EventReturnType ep s (State s, [PredicateFailure s])
s', ((State s, [PredicateFailure s]) -> [PredicateFailure s])
-> [(State s, [PredicateFailure s])] -> [PredicateFailure s]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (State s, [PredicateFailure s]) -> [PredicateFailure s]
forall a b. (a, b) -> b
snd [(State s, [PredicateFailure s])]
[EventReturnType ep s (State s, [PredicateFailure s])]
xs)
              SingEP ep
EPReturn -> ((((State s, [PredicateFailure s]) -> State s
forall a b. (a, b) -> a
fst ((State s, [PredicateFailure s]) -> State s)
-> (((State s, [PredicateFailure s]), [Event s])
    -> (State s, [PredicateFailure s]))
-> ((State s, [PredicateFailure s]), [Event s])
-> State s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((State s, [PredicateFailure s]), [Event s])
-> (State s, [PredicateFailure s])
forall a b. (a, b) -> a
fst) ((State s, [PredicateFailure s]), [Event s])
EventReturnType ep s (State s, [PredicateFailure s])
s', (((State s, [PredicateFailure s]), [Event s])
 -> [PredicateFailure s])
-> [((State s, [PredicateFailure s]), [Event s])]
-> [PredicateFailure s]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((State s, [PredicateFailure s]) -> [PredicateFailure s]
forall a b. (a, b) -> b
snd ((State s, [PredicateFailure s]) -> [PredicateFailure s])
-> (((State s, [PredicateFailure s]), [Event s])
    -> (State s, [PredicateFailure s]))
-> ((State s, [PredicateFailure s]), [Event s])
-> [PredicateFailure s]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((State s, [PredicateFailure s]), [Event s])
-> (State s, [PredicateFailure s])
forall a b. (a, b) -> a
fst) [((State s, [PredicateFailure s]), [Event s])]
[EventReturnType ep s (State s, [PredicateFailure s])]
xs), ((State s, [PredicateFailure s]), [Event s]) -> [Event s]
forall a b. (a, b) -> b
snd ((State s, [PredicateFailure s]), [Event s])
EventReturnType ep s (State s, [PredicateFailure s])
s')
        Just EventReturnType ep s (State s, [PredicateFailure s])
s' -> case SingEP ep
ep of
          SingEP ep
EPDiscard -> ((State s, [PredicateFailure s]) -> State s
forall a b. (a, b) -> a
fst (State s, [PredicateFailure s])
EventReturnType ep s (State s, [PredicateFailure s])
s', [])
          SingEP ep
EPReturn -> (((State s, [PredicateFailure s]) -> State s
forall a b. (a, b) -> a
fst ((State s, [PredicateFailure s]) -> State s)
-> (State s, [PredicateFailure s]) -> State s
forall a b. (a -> b) -> a -> b
$ ((State s, [PredicateFailure s]), [Event s])
-> (State s, [PredicateFailure s])
forall a b. (a, b) -> a
fst ((State s, [PredicateFailure s]), [Event s])
EventReturnType ep s (State s, [PredicateFailure s])
s', []), ((State s, [PredicateFailure s]), [Event s]) -> [Event s]
forall a b. (a, b) -> b
snd ((State s, [PredicateFailure s]), [Event s])
EventReturnType ep s (State s, [PredicateFailure s])
s')
    applySTSInternal' ::
      SRuleType rtype ->
      RuleContext rtype s ->
      ExceptT (AssertionViolation s) m [EventReturnType ep s (State s, [PredicateFailure s])]
    applySTSInternal' :: SRuleType rtype
-> RuleContext rtype s
-> ExceptT
     (AssertionViolation s)
     m
     [EventReturnType ep s (State s, [PredicateFailure s])]
applySTSInternal' SRuleType rtype
SInitial RuleContext rtype s
env =
      m [EventReturnType ep s (State s, [PredicateFailure s])]
-> ExceptT
     (AssertionViolation s)
     m
     [EventReturnType ep s (State s, [PredicateFailure s])]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (RuleContext 'Initial s
-> F (Clause s 'Initial) (State s)
-> m (EventReturnType ep s (State s, [PredicateFailure s]))
RuleInterpreter ep
goRule RuleContext rtype s
RuleContext 'Initial s
env (F (Clause s 'Initial) (State s)
 -> m (EventReturnType ep s (State s, [PredicateFailure s])))
-> [F (Clause s 'Initial) (State s)]
-> m [EventReturnType ep s (State s, [PredicateFailure s])]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
`traverse` [F (Clause s 'Initial) (State s)]
forall a. STS a => [InitialRule a]
initialRules)
    applySTSInternal' SRuleType rtype
STransition RuleContext rtype s
jc = do
      Bool
-> ExceptT (AssertionViolation s) m ()
-> ExceptT (AssertionViolation s) m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (AssertionPolicy -> Bool
assertPre AssertionPolicy
ap) (ExceptT (AssertionViolation s) m ()
 -> ExceptT (AssertionViolation s) m ())
-> ExceptT (AssertionViolation s) m ()
-> ExceptT (AssertionViolation s) m ()
forall a b. (a -> b) -> a -> b
$
        [Assertion s]
-> (Assertion s -> ExceptT (AssertionViolation s) m ())
-> ExceptT (AssertionViolation s) m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
sfor_ (STS s => [Assertion s]
forall a. STS a => [Assertion a]
assertions @s) ((Assertion s -> ExceptT (AssertionViolation s) m ())
 -> ExceptT (AssertionViolation s) m ())
-> (Assertion s -> ExceptT (AssertionViolation s) m ())
-> ExceptT (AssertionViolation s) m ()
forall a b. (a -> b) -> a -> b
$! \case
          PreCondition String
msg TRC s -> Bool
cond
            | Bool -> Bool
not (TRC s -> Bool
cond RuleContext rtype s
TRC s
jc) ->
                let assertion :: AssertionViolation s
assertion =
                      AssertionViolation :: forall sts.
String
-> String -> TRC sts -> Maybe (State sts) -> AssertionViolation sts
AssertionViolation
                        { avSTS :: String
avSTS = TypeRep -> String
forall a. Show a => a -> String
show (TypeRep -> String) -> TypeRep -> String
forall a b. (a -> b) -> a -> b
$ AssertionViolation s -> TypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep AssertionViolation s
assertion,
                          avMsg :: String
avMsg = String
msg,
                          avCtx :: TRC s
avCtx = RuleContext rtype s
TRC s
jc,
                          avState :: Maybe (State s)
avState = Maybe (State s)
forall a. Maybe a
Nothing
                        }
                 in AssertionViolation s -> ExceptT (AssertionViolation s) m ()
forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE AssertionViolation s
assertion
          Assertion s
_ -> () -> ExceptT (AssertionViolation s) m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      [EventReturnType ep s (State s, [PredicateFailure s])]
res <- m [EventReturnType ep s (State s, [PredicateFailure s])]
-> ExceptT
     (AssertionViolation s)
     m
     [EventReturnType ep s (State s, [PredicateFailure s])]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (RuleContext 'Transition s
-> F (Clause s 'Transition) (State s)
-> m (EventReturnType ep s (State s, [PredicateFailure s]))
RuleInterpreter ep
goRule RuleContext rtype s
RuleContext 'Transition s
jc (F (Clause s 'Transition) (State s)
 -> m (EventReturnType ep s (State s, [PredicateFailure s])))
-> [F (Clause s 'Transition) (State s)]
-> m [EventReturnType ep s (State s, [PredicateFailure s])]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
`traverse` [F (Clause s 'Transition) (State s)]
forall a. STS a => [TransitionRule a]
transitionRules)
      -- We only care about running postconditions if the state transition was
      -- successful.
      Bool
-> ExceptT (AssertionViolation s) m ()
-> ExceptT (AssertionViolation s) m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (AssertionPolicy -> Bool
assertPost AssertionPolicy
ap) (ExceptT (AssertionViolation s) m ()
 -> ExceptT (AssertionViolation s) m ())
-> ExceptT (AssertionViolation s) m ()
-> ExceptT (AssertionViolation s) m ()
forall a b. (a -> b) -> a -> b
$
        let res' :: (EventReturnType ep s (State s, [PredicateFailure s]))
            res' :: EventReturnType ep s (State s, [PredicateFailure s])
res' = [EventReturnType ep s (State s, [PredicateFailure s])]
-> EventReturnType ep s (State s, [PredicateFailure s])
successOrFirstFailure [EventReturnType ep s (State s, [PredicateFailure s])]
res
         in case SingEP ep
-> EventReturnType ep s (State s, [PredicateFailure s])
-> (State s, [PredicateFailure s])
forall (ep :: EventPolicy) a.
SingEP ep -> forall s. EventReturnType ep s a -> a
discardEvents SingEP ep
ep @s EventReturnType ep s (State s, [PredicateFailure s])
res' :: (State s, [PredicateFailure s]) of
              (State s
st, []) ->
                [Assertion s]
-> (Assertion s -> ExceptT (AssertionViolation s) m ())
-> ExceptT (AssertionViolation s) m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
sfor_ (STS s => [Assertion s]
forall a. STS a => [Assertion a]
assertions @s) ((Assertion s -> ExceptT (AssertionViolation s) m ())
 -> ExceptT (AssertionViolation s) m ())
-> (Assertion s -> ExceptT (AssertionViolation s) m ())
-> ExceptT (AssertionViolation s) m ()
forall a b. (a -> b) -> a -> b
$! \case
                  PostCondition String
msg TRC s -> State s -> Bool
cond
                    | Bool -> Bool
not (TRC s -> State s -> Bool
cond RuleContext rtype s
TRC s
jc State s
st) ->
                        let assertion :: AssertionViolation s
assertion =
                              AssertionViolation :: forall sts.
String
-> String -> TRC sts -> Maybe (State sts) -> AssertionViolation sts
AssertionViolation
                                { avSTS :: String
avSTS = TypeRep -> String
forall a. Show a => a -> String
show (TypeRep -> String) -> TypeRep -> String
forall a b. (a -> b) -> a -> b
$ AssertionViolation s -> TypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep AssertionViolation s
assertion,
                                  avMsg :: String
avMsg = String
msg,
                                  avCtx :: TRC s
avCtx = RuleContext rtype s
TRC s
jc,
                                  avState :: Maybe (State s)
avState = State s -> Maybe (State s)
forall a. a -> Maybe a
Just State s
st
                                }
                         in AssertionViolation s -> ExceptT (AssertionViolation s) m ()
forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE AssertionViolation s
assertion
                  Assertion s
_ -> () -> ExceptT (AssertionViolation s) m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
              (State s, [PredicateFailure s])
_ -> () -> ExceptT (AssertionViolation s) m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      [EventReturnType ep s (State s, [PredicateFailure s])]
-> ExceptT
     (AssertionViolation s)
     m
     [EventReturnType ep s (State s, [PredicateFailure s])]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([EventReturnType ep s (State s, [PredicateFailure s])]
 -> ExceptT
      (AssertionViolation s)
      m
      [EventReturnType ep s (State s, [PredicateFailure s])])
-> [EventReturnType ep s (State s, [PredicateFailure s])]
-> ExceptT
     (AssertionViolation s)
     m
     [EventReturnType ep s (State s, [PredicateFailure s])]
forall a b. (a -> b) -> a -> b
$! [EventReturnType ep s (State s, [PredicateFailure s])]
res

    assertPre :: AssertionPolicy -> Bool
    assertPre :: AssertionPolicy -> Bool
assertPre AssertionPolicy
AssertionsAll = Bool
True
    assertPre AssertionPolicy
AssertionsPre = Bool
True
    assertPre AssertionPolicy
_ = Bool
False

    assertPost :: AssertionPolicy -> Bool
    assertPost :: AssertionPolicy -> Bool
assertPost AssertionPolicy
AssertionsAll = Bool
True
    assertPost AssertionPolicy
AssertionsPost = Bool
True
    assertPost AssertionPolicy
_ = Bool
False

-- | This can be used to specify predicate failures in STS rules where a value
-- is beyond a certain threshold.
--
-- TODO move this somewhere more sensible
newtype Threshold a = Threshold a
  deriving (Threshold a -> Threshold a -> Bool
(Threshold a -> Threshold a -> Bool)
-> (Threshold a -> Threshold a -> Bool) -> Eq (Threshold a)
forall a. Eq a => Threshold a -> Threshold a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Threshold a -> Threshold a -> Bool
$c/= :: forall a. Eq a => Threshold a -> Threshold a -> Bool
== :: Threshold a -> Threshold a -> Bool
$c== :: forall a. Eq a => Threshold a -> Threshold a -> Bool
Eq, Eq (Threshold a)
Eq (Threshold a)
-> (Threshold a -> Threshold a -> Ordering)
-> (Threshold a -> Threshold a -> Bool)
-> (Threshold a -> Threshold a -> Bool)
-> (Threshold a -> Threshold a -> Bool)
-> (Threshold a -> Threshold a -> Bool)
-> (Threshold a -> Threshold a -> Threshold a)
-> (Threshold a -> Threshold a -> Threshold a)
-> Ord (Threshold a)
Threshold a -> Threshold a -> Bool
Threshold a -> Threshold a -> Ordering
Threshold a -> Threshold a -> Threshold a
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
forall a. Ord a => Eq (Threshold a)
forall a. Ord a => Threshold a -> Threshold a -> Bool
forall a. Ord a => Threshold a -> Threshold a -> Ordering
forall a. Ord a => Threshold a -> Threshold a -> Threshold a
min :: Threshold a -> Threshold a -> Threshold a
$cmin :: forall a. Ord a => Threshold a -> Threshold a -> Threshold a
max :: Threshold a -> Threshold a -> Threshold a
$cmax :: forall a. Ord a => Threshold a -> Threshold a -> Threshold a
>= :: Threshold a -> Threshold a -> Bool
$c>= :: forall a. Ord a => Threshold a -> Threshold a -> Bool
> :: Threshold a -> Threshold a -> Bool
$c> :: forall a. Ord a => Threshold a -> Threshold a -> Bool
<= :: Threshold a -> Threshold a -> Bool
$c<= :: forall a. Ord a => Threshold a -> Threshold a -> Bool
< :: Threshold a -> Threshold a -> Bool
$c< :: forall a. Ord a => Threshold a -> Threshold a -> Bool
compare :: Threshold a -> Threshold a -> Ordering
$ccompare :: forall a. Ord a => Threshold a -> Threshold a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (Threshold a)
Ord, Int -> Threshold a -> ShowS
[Threshold a] -> ShowS
Threshold a -> String
(Int -> Threshold a -> ShowS)
-> (Threshold a -> String)
-> ([Threshold a] -> ShowS)
-> Show (Threshold a)
forall a. Show a => Int -> Threshold a -> ShowS
forall a. Show a => [Threshold a] -> ShowS
forall a. Show a => Threshold a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Threshold a] -> ShowS
$cshowList :: forall a. Show a => [Threshold a] -> ShowS
show :: Threshold a -> String
$cshow :: forall a. Show a => Threshold a -> String
showsPrec :: Int -> Threshold a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Threshold a -> ShowS
Show, Typeable (Threshold a)
DataType
Constr
Typeable (Threshold a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Threshold a -> c (Threshold a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Threshold a))
-> (Threshold a -> Constr)
-> (Threshold a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Threshold a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Threshold a)))
-> ((forall b. Data b => b -> b) -> Threshold a -> Threshold a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Threshold a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Threshold a -> r)
-> (forall u. (forall d. Data d => d -> u) -> Threshold a -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Threshold a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a))
-> Data (Threshold a)
Threshold a -> DataType
Threshold a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (Threshold a))
(forall b. Data b => b -> b) -> Threshold a -> Threshold a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Threshold a -> c (Threshold a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Threshold a)
forall a. Data a => Typeable (Threshold a)
forall a. Data a => Threshold a -> DataType
forall a. Data a => Threshold a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> Threshold a -> Threshold a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Threshold a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> Threshold a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Threshold a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Threshold a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Threshold a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Threshold a -> c (Threshold a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Threshold a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Threshold a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Threshold a -> u
forall u. (forall d. Data d => d -> u) -> Threshold a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Threshold a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Threshold a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Threshold a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Threshold a -> c (Threshold a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Threshold a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Threshold a))
$cThreshold :: Constr
$tThreshold :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a)
gmapMp :: (forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a)
gmapM :: (forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> Threshold a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Threshold a -> u
gmapQ :: (forall d. Data d => d -> u) -> Threshold a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> Threshold a -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Threshold a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Threshold a -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Threshold a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Threshold a -> r
gmapT :: (forall b. Data b => b -> b) -> Threshold a -> Threshold a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Threshold a -> Threshold a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Threshold a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Threshold a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Threshold a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Threshold a))
dataTypeOf :: Threshold a -> DataType
$cdataTypeOf :: forall a. Data a => Threshold a -> DataType
toConstr :: Threshold a -> Constr
$ctoConstr :: forall a. Data a => Threshold a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Threshold a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Threshold a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Threshold a -> c (Threshold a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Threshold a -> c (Threshold a)
$cp1Data :: forall a. Data a => Typeable (Threshold a)
Data, Typeable, [String] -> Threshold a -> IO (Maybe ThunkInfo)
Proxy (Threshold a) -> String
([String] -> Threshold a -> IO (Maybe ThunkInfo))
-> ([String] -> Threshold a -> IO (Maybe ThunkInfo))
-> (Proxy (Threshold a) -> String)
-> NoThunks (Threshold a)
forall a.
NoThunks a =>
[String] -> Threshold a -> IO (Maybe ThunkInfo)
forall a. NoThunks a => Proxy (Threshold a) -> String
forall a.
([String] -> a -> IO (Maybe ThunkInfo))
-> ([String] -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
showTypeOf :: Proxy (Threshold a) -> String
$cshowTypeOf :: forall a. NoThunks a => Proxy (Threshold a) -> String
wNoThunks :: [String] -> Threshold a -> IO (Maybe ThunkInfo)
$cwNoThunks :: forall a.
NoThunks a =>
[String] -> Threshold a -> IO (Maybe ThunkInfo)
noThunks :: [String] -> Threshold a -> IO (Maybe ThunkInfo)
$cnoThunks :: forall a.
NoThunks a =>
[String] -> Threshold a -> IO (Maybe ThunkInfo)
NoThunks)

{------------------------------------------------------------------------------
-- Utils
------------------------------------------------------------------------------}

-- | A stub rule with no transitions to use as a placeholder
data STUB (e :: Type) (st :: Type) (si :: Type) (f :: Type) (m :: Type -> Type)

instance
  ( Eq f,
    Monad m,
    Show f,
    Typeable e,
    Typeable f,
    Typeable si,
    Typeable st,
    Typeable m
  ) =>
  STS (STUB e st si f m)
  where
  type Environment (STUB e st si f m) = e
  type State (STUB e st si f m) = st
  type Signal (STUB e st si f m) = si
  type PredicateFailure (STUB e st si f m) = f
  type BaseM (STUB e st si f m) = m

  transitionRules :: [TransitionRule (STUB e st si f m)]
transitionRules = []
  initialRules :: [InitialRule (STUB e st si f m)]
initialRules = []

-- | Map each element of a structure to an action, evaluate these actions from
-- left to right, and ignore the results. For a version that doesn't ignore the
-- results see 'Data.Traversable.traverse'.
--
-- This is a strict variant on 'Data.Foldable.traverse_', which evaluates each
-- element of the structure even in a monad which would otherwise allow this to
-- be lazy.
straverse_ :: (Foldable t, Applicative f) => (a -> f b) -> t a -> f ()
straverse_ :: (a -> f b) -> t a -> f ()
straverse_ a -> f b
f = (a -> f () -> f ()) -> f () -> t a -> f ()
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> f () -> f ()
c (() -> f ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
  where
    -- See Note [List fusion and continuations in 'c']
    c :: a -> f () -> f ()
c !a
x !f ()
k = (f b -> f () -> f ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> f ()
k) (f b -> f ()) -> f b -> f ()
forall a b. (a -> b) -> a -> b
$! a -> f b
f a
x
    {-# INLINE c #-}

-- | 'sfor_' is 'straverse_' with its arguments flipped. For a version
-- that doesn't ignore the results see 'Data.Traversable.for'.
--
-- >>> sfor_ ([1..4] :: [Int]) print
-- 1
-- 2
-- 3
-- 4
sfor_ :: (Foldable t, Applicative f) => t a -> (a -> f b) -> f ()
{-# INLINE sfor_ #-}
sfor_ :: t a -> (a -> f b) -> f ()
sfor_ = ((a -> f b) -> t a -> f ()) -> t a -> (a -> f b) -> f ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> f b) -> t a -> f ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
straverse_

tellEvent ::
  Event sts ->
  Rule sts ctx ()
tellEvent :: Event sts -> Rule sts ctx ()
tellEvent Event sts
e = [Event sts] -> Rule sts ctx ()
forall sts (ctx :: RuleType). [Event sts] -> Rule sts ctx ()
tellEvents [Event sts
e]

tellEvents ::
  [Event sts] ->
  Rule sts ctx ()
tellEvents :: [Event sts] -> Rule sts ctx ()
tellEvents [Event sts]
es = Clause sts ctx () -> Rule sts ctx ()
forall (f :: * -> *) (m :: * -> *) a.
(Functor f, MonadFree f m) =>
f a -> m a
liftF (Clause sts ctx () -> Rule sts ctx ())
-> Clause sts ctx () -> Rule sts ctx ()
forall a b. (a -> b) -> a -> b
$ [Event sts] -> () -> Clause sts ctx ()
forall sts a (rtype :: RuleType).
[Event sts] -> a -> Clause sts rtype a
Writer [Event sts]
es ()