{-# 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 TypeOperators #-}
{-# 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,
  failOnJust,
  failOnNonEmpty,
  failureOnJust,
  failureOnNonEmpty,
  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,
  runRule,

  -- * 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 (Default, def)
import Data.Foldable as F (find, toList, 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
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
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
  { forall sts. AssertionViolation sts -> String
avSTS :: String
  , forall sts. AssertionViolation sts -> String
avMsg :: String
  , forall sts. AssertionViolation sts -> TRC sts
avCtx :: TRC sts
  , forall sts. AssertionViolation sts -> Maybe (State sts)
avState :: Maybe (State sts)
  }

instance STS sts => Show (AssertionViolation sts) where
  show :: AssertionViolation sts -> String
show = 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) = 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 = [forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 (" forall a. Semigroup a => a -> a -> a
<> String
sts forall a. Semigroup a => a -> a -> a
<> String
"): " 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 = coerce :: forall a b. Coercible a b => a -> b
coerce

instance STS sts => Embed sts sts where
  wrapFailed :: PredicateFailure sts -> PredicateFailure sts
wrapFailed = 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 :: forall (ep :: EventPolicy) a.
SingEP ep -> forall s. EventReturnType ep s a -> a
discardEvents SingEP ep
ep = case SingEP ep
ep of
  SingEP ep
EPReturn -> forall a b. (a, b) -> a
fst
  SingEP ep
EPDiscard -> forall a. a -> a
id

getEvents :: forall ep. SingEP ep -> forall s a. EventReturnType ep s a -> [Event s]
getEvents :: forall (ep :: EventPolicy).
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 -> forall a b. (a, b) -> b
snd 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 :: forall (ep :: EventPolicy) sts a b.
EventReturnTypeRep ep =>
(a -> b) -> EventReturnType ep sts a -> EventReturnType ep sts b
mapEventReturn a -> b
f EventReturnType ep sts a
ert = case forall (ert :: EventPolicy). EventReturnTypeRep ert => SingEP ert
eventReturnTypeRep @ep of
  SingEP ep
EPReturn -> forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first a -> b
f EventReturnType ep sts a
ert
  SingEP ep
EPDiscard -> a -> b
f 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 :: forall sts (ctx :: RuleType).
Validation (NonEmpty (PredicateFailure sts)) () -> Rule sts ctx ()
validate = forall e sts (ctx :: RuleType).
(e -> PredicateFailure sts)
-> Validation (NonEmpty e) () -> Rule sts ctx ()
validateTrans 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 :: forall e sts (ctx :: RuleType).
(e -> PredicateFailure sts)
-> Validation (NonEmpty e) () -> Rule sts ctx ()
validateTrans e -> PredicateFailure sts
t Validation (NonEmpty e) ()
v = forall (f :: * -> *) (m :: * -> *) a.
(Functor f, MonadFree f m) =>
f a -> m a
liftF forall a b. (a -> b) -> a -> b
$ forall sts a sts (rtype :: RuleType).
Validation (NonEmpty sts) a
-> (sts -> 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 :: forall e sts (ctx :: RuleType).
(e -> PredicateFailure sts)
-> NonEmpty String -> Validation (NonEmpty e) () -> Rule sts ctx ()
validateTransLabeled e -> PredicateFailure sts
t NonEmpty String
labels Validation (NonEmpty e) ()
v = forall (f :: * -> *) (m :: * -> *) a.
(Functor f, MonadFree f m) =>
f a -> m a
liftF forall a b. (a -> b) -> a -> b
$ forall sts (rtype :: RuleType) a.
NonEmpty String -> Rule sts rtype a -> a -> Clause sts rtype a
Label NonEmpty String
labels (forall (f :: * -> *) (m :: * -> *) a.
(Functor f, MonadFree f m) =>
f a -> m a
liftF forall a b. (a -> b) -> a -> b
$ forall sts a sts (rtype :: RuleType).
Validation (NonEmpty sts) a
-> (sts -> 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 ()
?! :: forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
(?!) Bool
cond PredicateFailure sts
onFail =
  forall (f :: * -> *) (m :: * -> *) a.
(Functor f, MonadFree f m) =>
f a -> m a
liftF forall a b. (a -> b) -> a -> b
$
    forall sts a sts (rtype :: RuleType).
Validation (NonEmpty sts) a
-> (sts -> PredicateFailure sts) -> a -> Clause sts rtype a
Predicate (if Bool
cond then forall e a. a -> Validation e a
Success () else forall e a. e -> Validation e a
Failure (PredicateFailure sts
onFail forall a. a -> [a] -> NonEmpty a
:| [])) forall a. a -> a
id ()

infix 1 ?!

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

-- | Produce a predicate failure when condition contains a Just value, contents of which
-- can be used inside the predicate failure
failOnJust :: Maybe a -> (a -> PredicateFailure sts) -> Rule sts ctx ()
failOnJust :: forall a sts (ctx :: RuleType).
Maybe a -> (a -> PredicateFailure sts) -> Rule sts ctx ()
failOnJust Maybe a
cond a -> PredicateFailure sts
onJust = forall (f :: * -> *) (m :: * -> *) a.
(Functor f, MonadFree f m) =>
f a -> m a
liftF forall a b. (a -> b) -> a -> b
$ forall sts a sts (rtype :: RuleType).
Validation (NonEmpty sts) a
-> (sts -> PredicateFailure sts) -> a -> Clause sts rtype a
Predicate (forall a e. Maybe a -> (a -> e) -> Validation (NonEmpty e) ()
failureOnJust Maybe a
cond a -> PredicateFailure sts
onJust) forall a. a -> a
id ()

-- | Produce a failure when condition contains a Just value, contents of which can be used
-- inside the failure
failureOnJust :: Maybe a -> (a -> e) -> Validation (NonEmpty e) ()
failureOnJust :: forall a e. Maybe a -> (a -> e) -> Validation (NonEmpty e) ()
failureOnJust Maybe a
cond a -> e
onJust =
  case Maybe a
cond of
    Maybe a
Nothing -> forall e a. a -> Validation e a
Success ()
    Just a
a -> forall e a. e -> Validation e a
Failure (a -> e
onJust a
a forall a. a -> [a] -> NonEmpty a
:| [])

-- | Produce a predicate failure when supplied foldable is not empty, contents of which
-- will be converted to a NonEmpty list and can be used inside the predicate failure.
failOnNonEmpty :: Foldable f => f a -> (NonEmpty a -> PredicateFailure sts) -> Rule sts ctx ()
failOnNonEmpty :: forall (f :: * -> *) a sts (ctx :: RuleType).
Foldable f =>
f a -> (NonEmpty a -> PredicateFailure sts) -> Rule sts ctx ()
failOnNonEmpty f a
cond NonEmpty a -> PredicateFailure sts
onNonEmpty = forall (f :: * -> *) (m :: * -> *) a.
(Functor f, MonadFree f m) =>
f a -> m a
liftF forall a b. (a -> b) -> a -> b
$ forall sts a sts (rtype :: RuleType).
Validation (NonEmpty sts) a
-> (sts -> PredicateFailure sts) -> a -> Clause sts rtype a
Predicate (forall (f :: * -> *) a e.
Foldable f =>
f a -> (NonEmpty a -> e) -> Validation (NonEmpty e) ()
failureOnNonEmpty f a
cond NonEmpty a -> PredicateFailure sts
onNonEmpty) forall a. a -> a
id ()

-- | Produce a failure when supplied foldable is not empty, contents of which will be
-- converted to a NonEmpty list and theh can be used inside the  failure.
failureOnNonEmpty :: Foldable f => f a -> (NonEmpty a -> e) -> Validation (NonEmpty e) ()
failureOnNonEmpty :: forall (f :: * -> *) a e.
Foldable f =>
f a -> (NonEmpty a -> e) -> Validation (NonEmpty e) ()
failureOnNonEmpty f a
cond = forall a e. Maybe a -> (a -> e) -> Validation (NonEmpty e) ()
failureOnJust (forall a. [a] -> Maybe (NonEmpty a)
NE.nonEmpty (forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList f a
cond))

-- | Oh noes with an explanation
--
--   We interpret this as "What?" "No!" "Because:"
(?!:) :: Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
?!: :: forall e sts (ctx :: RuleType).
Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
(?!:) Either e ()
cond e -> PredicateFailure sts
onFail =
  forall (f :: * -> *) (m :: * -> *) a.
(Functor f, MonadFree f m) =>
f a -> m a
liftF forall a b. (a -> b) -> a -> b
$
    forall sts a sts (rtype :: RuleType).
Validation (NonEmpty sts) a
-> (sts -> PredicateFailure sts) -> a -> Clause sts rtype a
Predicate (forall e a. Either e a -> Validation e a
eitherToValidation forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first 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 :: forall sts (ctx :: RuleType).
NonEmpty String -> Bool -> PredicateFailure sts -> Rule sts ctx ()
labeledPred NonEmpty String
lbls Bool
cond PredicateFailure sts
orElse = forall sts (ctx :: RuleType).
NonEmpty String -> Rule sts ctx () -> Rule sts ctx ()
labeled NonEmpty String
lbls (Bool
cond 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 :: forall e sts (ctx :: RuleType).
NonEmpty String
-> Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
labeledPredE NonEmpty String
lbls Either e ()
cond e -> PredicateFailure sts
orElse = forall sts (ctx :: RuleType).
NonEmpty String -> Rule sts ctx () -> Rule sts ctx ()
labeled NonEmpty String
lbls (Either e ()
cond 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 :: forall sts (ctx :: RuleType).
NonEmpty String -> Rule sts ctx () -> Rule sts ctx ()
labeled NonEmpty String
lbls Rule sts ctx ()
subrule = forall (f :: * -> *) (m :: * -> *) a.
(Functor f, MonadFree f m) =>
f a -> m a
liftF forall a b. (a -> b) -> a -> b
$ 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 :: forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans RuleContext rtype sub
ctx = forall (f :: * -> *) (m :: * -> *) a.
MonadFree f m =>
f (m a) -> m a
wrap forall a b. (a -> b) -> a -> b
$ forall sts sts (rtype :: RuleType) a.
Embed sts sts =>
RuleContext rtype sts -> (State sts -> a) -> Clause sts rtype a
SubTrans RuleContext rtype sub
ctx forall (f :: * -> *) a. Applicative f => a -> f a
pure

ifFailureFree :: Rule sts rtype a -> Rule sts rtype a -> Rule sts rtype a
ifFailureFree :: forall sts (rtype :: RuleType) a.
Rule sts rtype a -> Rule sts rtype a -> Rule sts rtype a
ifFailureFree Rule sts rtype a
x Rule sts rtype a
y = forall (f :: * -> *) (m :: * -> *) a.
(Functor f, MonadFree f m) =>
f a -> m a
liftF (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 :: forall sts (rtype :: RuleType).
Rule sts rtype () -> Rule sts rtype ()
whenFailureFree Rule sts rtype ()
action = forall sts (rtype :: RuleType) a.
Rule sts rtype a -> Rule sts rtype a -> Rule sts rtype a
ifFailureFree Rule sts rtype ()
action (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())

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

-- | Get the judgment context
judgmentContext :: Rule sts rtype (RuleContext rtype sts)
judgmentContext :: forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext = forall (f :: * -> *) (m :: * -> *) a.
MonadFree f m =>
f (m a) -> m a
wrap forall a b. (a -> b) -> a -> b
$ forall (rtype :: RuleType) sts a.
(RuleContext rtype sts -> a) -> Clause sts rtype a
GetCtx 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
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
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
  { forall (ep :: EventPolicy). ApplySTSOpts ep -> AssertionPolicy
asoAssertions :: AssertionPolicy
  -- ^ Enable assertions during STS processing.
  --   If this option is enabled, STS processing will terminate on violation
  --   of an assertion.
  , forall (ep :: EventPolicy). ApplySTSOpts ep -> ValidationPolicy
asoValidation :: ValidationPolicy
  -- ^ Validation policy
  , forall (ep :: EventPolicy). ApplySTSOpts ep -> SingEP ep
asoEvents :: SingEP ep
  -- ^ Event policy
  }

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 :: 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 {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 = forall (ep :: EventPolicy) s (m :: * -> *) (rtype :: RuleType)
       result.
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
IsFailing
-> SingEP ep
-> ValidationPolicy
-> (IsFailing -> STSInterpreter ep)
-> RuleContext rtype s
-> Rule s rtype result
-> m (EventReturnType ep s (result, [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 =
        forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (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) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Left AssertionViolation s
err -> forall a e. Exception e => e -> a
throw forall a b. (a -> b) -> a -> b
$! forall sts. STS sts => AssertionViolation sts -> AssertionException
AssertionException AssertionViolation s
err
          Right EventReturnType ep s (State s, [PredicateFailure s])
res -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! EventReturnType ep s (State s, [PredicateFailure s])
res
   in 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 (NonEmpty (PredicateFailure s)) (EventReturnType ep s (State s)))
applySTSOptsEither :: 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 ApplySTSOpts ep
opts RuleContext rtype s
ctx =
  let r1 :: BaseM s (EventReturnType ep s (State s, [PredicateFailure s]))
r1 = 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 forall (ep :: EventPolicy). ApplySTSOpts ep -> SingEP ep
asoEvents ApplySTSOpts ep
opts of
        SingEP ep
EPDiscard ->
          BaseM s (EventReturnType ep s (State s, [PredicateFailure s]))
r1 forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
            (State s
st, []) -> forall a b. b -> Either a b
Right State s
st
            (State s
_, PredicateFailure s
pf : [PredicateFailure s]
pfs) -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ PredicateFailure s
pf forall a. a -> [a] -> NonEmpty a
:| [PredicateFailure s]
pfs
        SingEP ep
EPReturn ->
          BaseM s (EventReturnType ep s (State s, [PredicateFailure s]))
r1 forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
            ((State s
st, []), [Event s]
evts) -> forall a b. b -> Either a b
Right (State s
st, [Event s]
evts)
            ((State s
_, PredicateFailure s
pf : [PredicateFailure s]
pfs), [Event s]
_) -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ PredicateFailure s
pf forall a. a -> [a] -> NonEmpty a
:| [PredicateFailure s]
pfs

applySTS ::
  forall s m rtype.
  (STS s, RuleTypeRep rtype, m ~ BaseM s) =>
  RuleContext rtype s ->
  m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTS :: forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTS = 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 ApplySTSOpts 'EventPolicyDiscard
defaultOpts
  where
    defaultOpts :: ApplySTSOpts 'EventPolicyDiscard
defaultOpts =
      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 :: forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s -> m (State s)
reapplySTS RuleContext rtype s
ctx = 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 forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> forall a b. (a, b) -> a
fst
  where
    defaultOpts :: ApplySTSOpts 'EventPolicyDiscard
defaultOpts =
      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 :: forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s -> m (State s, [PredicateFailure s])
applySTSIndifferently =
  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
      { 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 result.
  (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 result ->
  m (EventReturnType ep s (result, [PredicateFailure s]))
applyRuleInternal :: forall (ep :: EventPolicy) s (m :: * -> *) (rtype :: RuleType)
       result.
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
IsFailing
-> SingEP ep
-> ValidationPolicy
-> (IsFailing -> STSInterpreter ep)
-> RuleContext rtype s
-> Rule s rtype result
-> m (EventReturnType ep s (result, [PredicateFailure s]))
applyRuleInternal IsFailing
isAlreadyFailing SingEP ep
ep ValidationPolicy
vp IsFailing -> STSInterpreter ep
goSTS RuleContext rtype s
jc Rule s rtype result
r = do
  (result
s, ([PredicateFailure s], [Event s])
er) <- forall a b c. (a -> b -> c) -> b -> a -> c
flip forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT ([], []) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (f :: * -> *) a.
Monad m =>
(forall x. f x -> m x) -> F f a -> m a
foldF forall a.
Clause s rtype a -> StateT ([PredicateFailure s], [Event s]) m a
runClause Rule s rtype result
r
  case SingEP ep
ep of
    SingEP ep
EPDiscard -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (result
s, forall a b. (a, b) -> a
fst ([PredicateFailure s], [Event s])
er)
    SingEP ep
EPReturn -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ((result
s, forall a b. (a, b) -> a
fst ([PredicateFailure s], [Event s])
er), 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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure IsFailing
Failing
        IsFailing
NotFailing -> do
          Bool
isFailingNow <- forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
          forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 :: forall a.
Clause s rtype a -> StateT ([PredicateFailure s], [Event s]) m a
runClause (Lift BaseM s a
f a -> a
next) = a -> a
next forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift BaseM s a
f
    runClause (GetCtx RuleContext rtype s -> a
next) = forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        IsFailing
Failing -> forall (m :: * -> *) (f :: * -> *) a.
Monad m =>
(forall x. f x -> m x) -> F f a -> m a
foldF forall a.
Clause s rtype a -> StateT ([PredicateFailure s], [Event s]) m a
runClause Rule s rtype a
failingRule
        IsFailing
NotFailing -> forall (m :: * -> *) (f :: * -> *) a.
Monad m =>
(forall x. f x -> m x) -> F f a -> m a
foldF forall a.
Clause s rtype a -> StateT ([PredicateFailure s], [Event s]) m a
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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure a
val
        ValidationPolicy
_ -> case Validation (NonEmpty e) a
cond of
          Success a
x -> forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
          Failure NonEmpty e
errs -> forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (forall a b. (a -> b) -> [a] -> [b]
map e -> PredicateFailure s
orElse (forall a. [a] -> [a]
reverse (forall a. NonEmpty a -> [a]
NE.toList NonEmpty e
errs)) forall a. Semigroup a => a -> a -> a
<>)) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> 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 (forall a. NonEmpty a -> [a]
NE.toList NonEmpty String
lbls)
        then forall (m :: * -> *) (f :: * -> *) a.
Monad m =>
(forall x. f x -> m x) -> F f a -> m a
foldF forall a.
Clause s rtype a -> StateT ([PredicateFailure s], [Event s]) m a
runClause Rule s rtype a
subrule
        else forall (f :: * -> *) a. Applicative f => a -> f a
pure a
val
    runClause (SubTrans (RuleContext rtype sub
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 <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ 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) = 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 = 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
      forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (\PredicateFailure s
a -> forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (PredicateFailure s
a forall a. a -> [a] -> [a]
:))) forall a b. (a -> b) -> a -> b
$ forall sub super.
Embed sub super =>
PredicateFailure sub -> PredicateFailure super
wrapFailed @sub @s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PredicateFailure sub]
sfails
      forall a.
Clause s rtype a -> StateT ([PredicateFailure s], [Event s]) m a
runClause forall a b. (a -> b) -> a -> b
$ forall sts a (rtype :: RuleType).
[Event sts] -> a -> Clause sts rtype a
Writer (forall sub super. Embed sub super => Event sub -> Event super
wrapEvent @sub @s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Event sub]
sevs) ()
      forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 -> forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (forall a. Semigroup a => a -> a -> a
<> [Event s]
w)) forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> a
a
      SingEP ep
EPDiscard -> 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 :: 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
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 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' 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 forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\EventReturnType ep s (State s, [PredicateFailure s])
x -> forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> b
snd (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
            [] -> 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 -> (forall a b. (a, b) -> a
fst EventReturnType ep s (State s, [PredicateFailure s])
s', forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a b. (a, b) -> b
snd [EventReturnType ep s (State s, [PredicateFailure s])]
xs)
              SingEP ep
EPReturn -> (((forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) EventReturnType ep s (State s, [PredicateFailure s])
s', forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [EventReturnType ep s (State s, [PredicateFailure s])]
xs), forall a b. (a, b) -> b
snd 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 -> (forall a b. (a, b) -> a
fst EventReturnType ep s (State s, [PredicateFailure s])
s', [])
          SingEP ep
EPReturn -> ((forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst EventReturnType ep s (State s, [PredicateFailure s])
s', []), forall a b. (a, b) -> b
snd 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 =
      forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (RuleInterpreter ep
goRule RuleContext rtype s
env forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
`traverse` forall a. STS a => [InitialRule a]
initialRules)
    applySTSInternal' SRuleType rtype
STransition RuleContext rtype s
jc = do
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (AssertionPolicy -> Bool
assertPre AssertionPolicy
ap) forall a b. (a -> b) -> a -> b
$
        forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
sfor_ (forall a. STS a => [Assertion a]
assertions @s) 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
jc) ->
                let assertion :: AssertionViolation s
assertion =
                      AssertionViolation
                        { avSTS :: String
avSTS = forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ 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
jc
                        , avState :: Maybe (State s)
avState = forall a. Maybe a
Nothing
                        }
                 in forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE AssertionViolation s
assertion
          Assertion s
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      [EventReturnType ep s (State s, [PredicateFailure s])]
res <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (RuleInterpreter ep
goRule RuleContext rtype s
jc forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
`traverse` forall a. STS a => [TransitionRule a]
transitionRules)
      -- We only care about running postconditions if the state transition was
      -- successful.
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (AssertionPolicy -> Bool
assertPost AssertionPolicy
ap) 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 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, []) ->
                forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
sfor_ (forall a. STS a => [Assertion a]
assertions @s) 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
jc State s
st) ->
                        let assertion :: AssertionViolation s
assertion =
                              AssertionViolation
                                { avSTS :: String
avSTS = forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ 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
jc
                                , avState :: Maybe (State s)
avState = forall a. a -> Maybe a
Just State s
st
                                }
                         in forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE AssertionViolation s
assertion
                  Assertion s
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
              (State s, [PredicateFailure s])
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      forall (f :: * -> *) a. Applicative f => a -> f a
pure 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
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, 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
Ord, Int -> Threshold a -> ShowS
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, Threshold a -> DataType
Threshold a -> Constr
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 (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))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. 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 u. (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 :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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)
Data, Typeable, [String] -> Threshold a -> IO (Maybe ThunkInfo)
Proxy (Threshold a) -> String
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_ :: forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
straverse_ a -> f b
f = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> f () -> f ()
c (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 = (forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> f ()
k) 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_ :: forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
sfor_ = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
straverse_

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

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

-- =================================

-- | runRule :: RuleInterpreter 'EventPolicyDiscard
--   run a rule given its context, to get a BaseM computation
runRule ::
  (STS s, RuleTypeRep rtype) =>
  RuleContext rtype s ->
  Rule s rtype result ->
  BaseM s (result, [PredicateFailure s])
runRule :: forall s (rtype :: RuleType) result.
(STS s, RuleTypeRep rtype) =>
RuleContext rtype s
-> Rule s rtype result -> BaseM s (result, [PredicateFailure s])
runRule RuleContext rtype s
cntxt Rule s rtype result
rule = forall (ep :: EventPolicy) s (m :: * -> *) (rtype :: RuleType)
       result.
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
IsFailing
-> SingEP ep
-> ValidationPolicy
-> (IsFailing -> STSInterpreter ep)
-> RuleContext rtype s
-> Rule s rtype result
-> m (EventReturnType ep s (result, [PredicateFailure s]))
applyRuleInternal IsFailing
NotFailing SingEP 'EventPolicyDiscard
EPDiscard ValidationPolicy
ValidateAll IsFailing -> STSInterpreter 'EventPolicyDiscard
goSTS RuleContext rtype s
cntxt Rule s rtype result
rule
  where
    goRule :: IsFailing
-> RuleContext rtype s
-> Rule s rtype result
-> BaseM
     s
     (EventReturnType
        'EventPolicyDiscard s (result, [PredicateFailure s]))
goRule IsFailing
isFailing RuleContext rtype s
c Rule s rtype result
r = forall (ep :: EventPolicy) s (m :: * -> *) (rtype :: RuleType)
       result.
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
IsFailing
-> SingEP ep
-> ValidationPolicy
-> (IsFailing -> STSInterpreter ep)
-> RuleContext rtype s
-> Rule s rtype result
-> m (EventReturnType ep s (result, [PredicateFailure s]))
applyRuleInternal IsFailing
isFailing SingEP 'EventPolicyDiscard
EPDiscard ValidationPolicy
ValidateAll IsFailing -> STSInterpreter 'EventPolicyDiscard
goSTS RuleContext rtype s
c Rule s rtype result
r
    goSTS :: IsFailing -> STSInterpreter 'EventPolicyDiscard
    goSTS :: IsFailing -> STSInterpreter 'EventPolicyDiscard
goSTS IsFailing
isFailing RuleContext rtype s
c =
      forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (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 'EventPolicyDiscard
EPDiscard AssertionPolicy
AssertionsOff (forall {s} {rtype :: RuleType} {result}.
(STS s, RuleTypeRep rtype) =>
IsFailing
-> RuleContext rtype s
-> Rule s rtype result
-> BaseM s (result, [PredicateFailure s])
goRule IsFailing
isFailing) RuleContext rtype s
c) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Left AssertionViolation s
err -> forall a e. Exception e => e -> a
throw forall a b. (a -> b) -> a -> b
$! forall sts. STS sts => AssertionViolation sts -> AssertionException
AssertionException AssertionViolation s
err
        Right (State s, [PredicateFailure s])
res -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! (State s, [PredicateFailure s])
res