{-# 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 #-}
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,
AssertionPolicy (..),
ValidationPolicy (..),
ApplySTSOpts (..),
applySTSOpts,
applySTSOptsEither,
applySTS,
applySTSIndifferently,
reapplySTS,
globalAssertionPolicy,
applySTSInternal,
applyRuleInternal,
RuleInterpreter,
STSInterpreter,
runRule,
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 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)
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
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
newtype IRC sts = IRC (Environment sts)
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)
data Assertion sts
=
PreCondition String (TRC sts -> Bool)
|
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
class
( Eq (PredicateFailure a)
, Show (PredicateFailure a)
, Monad (BaseM a)
, Typeable a
) =>
STS a
where
type State a :: Type
type Signal a :: Type
type Environment a :: Type
type BaseM a :: Type -> Type
type BaseM a = Identity
type Event a :: Type
type Event a = Void
type PredicateFailure a :: Type
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 :: [Assertion a]
assertions = []
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
class (STS sub, BaseM sub ~ BaseM super) => Embed sub super where
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 -> []
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 ->
(State sub -> a) ->
Clause sts rtype a
Writer ::
[Event sts] ->
a ->
Clause sts rtype a
Predicate ::
Validation (NonEmpty e) a ->
(e -> PredicateFailure sts) ->
a ->
Clause sts rtype a
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)
type Label = String
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
validateTrans ::
(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 ()
validateTransLabeled ::
(e -> PredicateFailure sts) ->
NonEmpty Label ->
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 ()) ()
(?!) :: 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 ()
?!)
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 ()
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
:| [])
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 ()
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))
(?!:) :: 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 ()
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)
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 :: 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
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
data AssertionPolicy
= AssertionsAll
|
AssertionsPre
|
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)
data ValidationPolicy
= ValidateAll
| ValidateNone
| ValidateSuchThat ([Label] -> Bool)
data ApplySTSOpts ep = ApplySTSOpts
{ forall (ep :: EventPolicy). ApplySTSOpts ep -> AssertionPolicy
asoAssertions :: AssertionPolicy
, forall (ep :: EventPolicy). ApplySTSOpts ep -> ValidationPolicy
asoValidation :: ValidationPolicy
, forall (ep :: EventPolicy). 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]))
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
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
}
applyRuleInternal ::
forall (ep :: EventPolicy) s m rtype 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 :: 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 ->
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)
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
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)
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 = []
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
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_ :: (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 ::
(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