{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
module Control.State.Transition.Extended
( RuleType (..),
RuleTypeRep,
RuleContext,
IRC (..),
TRC (..),
Rule,
TransitionRule,
InitialRule,
Assertion (..),
AssertionViolation (..),
STS (..),
Embed (..),
(?!),
(?!:),
failBecause,
judgmentContext,
trans,
liftSTS,
AssertionPolicy (..),
ValidationPolicy (..),
ApplySTSOpts (..),
applySTSOpts,
applySTS,
applySTSIndifferently,
reapplySTS,
Threshold (..),
)
where
import Control.Exception (Exception (..), throw)
import Control.Monad (when)
import Control.Monad.Except (MonadError (..))
import Control.Monad.Free.Church
import Control.Monad.Identity (Identity (..))
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.State.Strict (modify, runStateT)
import qualified Control.Monad.Trans.State.Strict as MonadState
import Data.Data (Data, Typeable)
import Data.Foldable (find, traverse_)
import Data.Functor ((<&>))
import Data.Kind (Type)
import Data.Proxy (Proxy (..))
import Data.Typeable (typeRep)
import NoThunks.Class (NoThunks (..))
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
{ AssertionViolation sts -> String
avSTS :: String,
AssertionViolation sts -> String
avMsg :: String,
AssertionViolation sts -> TRC sts
avCtx :: TRC sts,
AssertionViolation sts -> Maybe (State sts)
avState :: Maybe (State sts)
}
instance STS sts => Show (AssertionViolation sts) where
show :: AssertionViolation sts -> String
show = AssertionViolation sts -> String
forall sts. STS sts => AssertionViolation sts -> String
renderAssertionViolation
instance
(STS sts) =>
Exception (AssertionViolation sts)
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 PredicateFailure a = (b :: Type) | b -> a
initialRules :: [InitialRule a]
transitionRules :: [TransitionRule a]
assertions :: [Assertion a]
assertions = []
renderAssertionViolation :: AssertionViolation a -> String
renderAssertionViolation (AssertionViolation String
sts String
msg TRC a
_ Maybe (State a)
_) =
String
"AssertionViolation (" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
sts String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"): " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
msg
class (STS sub, BaseM sub ~ BaseM super) => Embed sub super where
wrapFailed :: PredicateFailure sub -> PredicateFailure super
instance STS sts => Embed sts sts where
wrapFailed :: PredicateFailure sts -> PredicateFailure sts
wrapFailed = PredicateFailure sts -> PredicateFailure sts
forall a. a -> a
id
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
Predicate ::
Either e a ->
(e -> PredicateFailure sts) ->
a ->
Clause sts rtype a
deriving instance Functor (Clause sts rtype)
type Rule sts rtype = F (Clause sts rtype)
(?!) :: Bool -> PredicateFailure sts -> Rule sts ctx ()
Bool
cond ?! :: Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure sts
orElse = Clause sts ctx () -> Rule sts ctx ()
forall (f :: * -> *) (m :: * -> *) a.
(Functor f, MonadFree f m) =>
f a -> m a
liftF (Clause sts ctx () -> Rule sts ctx ())
-> Clause sts ctx () -> Rule sts ctx ()
forall a b. (a -> b) -> a -> b
$ Either () ()
-> (() -> PredicateFailure sts) -> () -> Clause sts ctx ()
forall e a sts (rtype :: RuleType).
Either e a
-> (e -> PredicateFailure sts) -> a -> Clause sts rtype a
Predicate (if Bool
cond then () -> Either () ()
forall a b. b -> Either a b
Right () else () -> Either () ()
forall a b. a -> Either a b
Left ()) (PredicateFailure sts -> () -> PredicateFailure sts
forall a b. a -> b -> a
const PredicateFailure sts
orElse) ()
infix 1 ?!
failBecause :: PredicateFailure sts -> Rule sts ctx ()
failBecause :: PredicateFailure sts -> Rule sts ctx ()
failBecause = (Bool
False Bool -> PredicateFailure sts -> Rule sts ctx ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?!)
(?!:) :: Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
Either e ()
cond ?!: :: Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
?!: e -> PredicateFailure sts
orElse = Clause sts ctx () -> Rule sts ctx ()
forall (f :: * -> *) (m :: * -> *) a.
(Functor f, MonadFree f m) =>
f a -> m a
liftF (Clause sts ctx () -> Rule sts ctx ())
-> Clause sts ctx () -> Rule sts ctx ()
forall a b. (a -> b) -> a -> b
$ Either e ()
-> (e -> PredicateFailure sts) -> () -> Clause sts ctx ()
forall e a sts (rtype :: RuleType).
Either e a
-> (e -> PredicateFailure sts) -> a -> Clause sts rtype a
Predicate Either e ()
cond e -> PredicateFailure sts
orElse ()
trans ::
Embed sub super => RuleContext rtype sub -> Rule super rtype (State sub)
trans :: RuleContext rtype sub -> Rule super rtype (State sub)
trans RuleContext rtype sub
ctx = Clause super rtype (Rule super rtype (State sub))
-> Rule super rtype (State sub)
forall (f :: * -> *) (m :: * -> *) a.
MonadFree f m =>
f (m a) -> m a
wrap (Clause super rtype (Rule super rtype (State sub))
-> Rule super rtype (State sub))
-> Clause super rtype (Rule super rtype (State sub))
-> Rule super rtype (State sub)
forall a b. (a -> b) -> a -> b
$ RuleContext rtype sub
-> (State sub -> Rule super rtype (State sub))
-> Clause super rtype (Rule super rtype (State sub))
forall sub sts (rtype :: RuleType) a.
Embed sub sts =>
RuleContext rtype sub -> (State sub -> a) -> Clause sts rtype a
SubTrans RuleContext rtype sub
ctx State sub -> Rule super rtype (State sub)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
liftSTS ::
STS sts =>
(BaseM sts) a ->
Rule sts ctx a
liftSTS :: BaseM sts a -> Rule sts ctx a
liftSTS BaseM sts a
f = Clause sts ctx (Rule sts ctx a) -> Rule sts ctx a
forall (f :: * -> *) (m :: * -> *) a.
MonadFree f m =>
f (m a) -> m a
wrap (Clause sts ctx (Rule sts ctx a) -> Rule sts ctx a)
-> Clause sts ctx (Rule sts ctx a) -> Rule sts ctx a
forall a b. (a -> b) -> a -> b
$ BaseM sts a
-> (a -> Rule sts ctx a) -> Clause sts ctx (Rule sts ctx a)
forall sts a b (rtype :: RuleType).
STS sts =>
BaseM sts a -> (a -> b) -> Clause sts rtype b
Lift BaseM sts a
f a -> Rule sts ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
judgmentContext :: Rule sts rtype (RuleContext rtype sts)
judgmentContext :: Rule sts rtype (RuleContext rtype sts)
judgmentContext = Clause sts rtype (Rule sts rtype (RuleContext rtype sts))
-> Rule sts rtype (RuleContext rtype sts)
forall (f :: * -> *) (m :: * -> *) a.
MonadFree f m =>
f (m a) -> m a
wrap (Clause sts rtype (Rule sts rtype (RuleContext rtype sts))
-> Rule sts rtype (RuleContext rtype sts))
-> Clause sts rtype (Rule sts rtype (RuleContext rtype sts))
-> Rule sts rtype (RuleContext rtype sts)
forall a b. (a -> b) -> a -> b
$ (RuleContext rtype sts -> Rule sts rtype (RuleContext rtype sts))
-> Clause sts rtype (Rule sts rtype (RuleContext rtype sts))
forall (rtype :: RuleType) sts a.
(RuleContext rtype sts -> a) -> Clause sts rtype a
GetCtx RuleContext rtype sts -> Rule sts rtype (RuleContext rtype sts)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
data AssertionPolicy
= AssertionsAll
|
AssertionsPre
|
AssertionsPost
| AssertionsOff
deriving (AssertionPolicy -> AssertionPolicy -> Bool
(AssertionPolicy -> AssertionPolicy -> Bool)
-> (AssertionPolicy -> AssertionPolicy -> Bool)
-> Eq AssertionPolicy
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AssertionPolicy -> AssertionPolicy -> Bool
$c/= :: AssertionPolicy -> AssertionPolicy -> Bool
== :: AssertionPolicy -> AssertionPolicy -> Bool
$c== :: AssertionPolicy -> AssertionPolicy -> Bool
Eq, Int -> AssertionPolicy -> ShowS
[AssertionPolicy] -> ShowS
AssertionPolicy -> String
(Int -> AssertionPolicy -> ShowS)
-> (AssertionPolicy -> String)
-> ([AssertionPolicy] -> ShowS)
-> Show AssertionPolicy
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AssertionPolicy] -> ShowS
$cshowList :: [AssertionPolicy] -> ShowS
show :: AssertionPolicy -> String
$cshow :: AssertionPolicy -> String
showsPrec :: Int -> AssertionPolicy -> ShowS
$cshowsPrec :: Int -> AssertionPolicy -> ShowS
Show)
data ValidationPolicy
= ValidateAll
| ValidateNone
deriving (ValidationPolicy -> ValidationPolicy -> Bool
(ValidationPolicy -> ValidationPolicy -> Bool)
-> (ValidationPolicy -> ValidationPolicy -> Bool)
-> Eq ValidationPolicy
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ValidationPolicy -> ValidationPolicy -> Bool
$c/= :: ValidationPolicy -> ValidationPolicy -> Bool
== :: ValidationPolicy -> ValidationPolicy -> Bool
$c== :: ValidationPolicy -> ValidationPolicy -> Bool
Eq, Int -> ValidationPolicy -> ShowS
[ValidationPolicy] -> ShowS
ValidationPolicy -> String
(Int -> ValidationPolicy -> ShowS)
-> (ValidationPolicy -> String)
-> ([ValidationPolicy] -> ShowS)
-> Show ValidationPolicy
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ValidationPolicy] -> ShowS
$cshowList :: [ValidationPolicy] -> ShowS
show :: ValidationPolicy -> String
$cshow :: ValidationPolicy -> String
showsPrec :: Int -> ValidationPolicy -> ShowS
$cshowsPrec :: Int -> ValidationPolicy -> ShowS
Show)
data ApplySTSOpts = ApplySTSOpts
{
ApplySTSOpts -> AssertionPolicy
asoAssertions :: AssertionPolicy,
ApplySTSOpts -> ValidationPolicy
asoValidation :: ValidationPolicy
}
deriving (ApplySTSOpts -> ApplySTSOpts -> Bool
(ApplySTSOpts -> ApplySTSOpts -> Bool)
-> (ApplySTSOpts -> ApplySTSOpts -> Bool) -> Eq ApplySTSOpts
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ApplySTSOpts -> ApplySTSOpts -> Bool
$c/= :: ApplySTSOpts -> ApplySTSOpts -> Bool
== :: ApplySTSOpts -> ApplySTSOpts -> Bool
$c== :: ApplySTSOpts -> ApplySTSOpts -> Bool
Eq, Int -> ApplySTSOpts -> ShowS
[ApplySTSOpts] -> ShowS
ApplySTSOpts -> String
(Int -> ApplySTSOpts -> ShowS)
-> (ApplySTSOpts -> String)
-> ([ApplySTSOpts] -> ShowS)
-> Show ApplySTSOpts
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ApplySTSOpts] -> ShowS
$cshowList :: [ApplySTSOpts] -> ShowS
show :: ApplySTSOpts -> String
$cshow :: ApplySTSOpts -> String
showsPrec :: Int -> ApplySTSOpts -> ShowS
$cshowsPrec :: Int -> ApplySTSOpts -> ShowS
Show)
type STSInterpreter =
forall s m rtype.
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s ->
m (State s, [[PredicateFailure s]])
type RuleInterpreter =
forall s m rtype.
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s ->
Rule s rtype (State s) ->
m (State s, [PredicateFailure s])
applySTSOpts ::
forall s m rtype.
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
ApplySTSOpts ->
RuleContext rtype s ->
m (State s, [[PredicateFailure s]])
applySTSOpts :: ApplySTSOpts
-> RuleContext rtype s -> m (State s, [[PredicateFailure s]])
applySTSOpts ApplySTSOpts {AssertionPolicy
asoAssertions :: AssertionPolicy
asoAssertions :: ApplySTSOpts -> AssertionPolicy
asoAssertions, ValidationPolicy
asoValidation :: ValidationPolicy
asoValidation :: ApplySTSOpts -> ValidationPolicy
asoValidation} RuleContext rtype s
ctx =
let goRule :: RuleInterpreter
goRule :: RuleContext rtype s
-> Rule s rtype (State s) -> m (State s, [PredicateFailure s])
goRule = ValidationPolicy
-> STSInterpreter
-> RuleContext rtype s
-> Rule s rtype (State s)
-> m (State s, [PredicateFailure s])
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
ValidationPolicy
-> STSInterpreter
-> RuleContext rtype s
-> Rule s rtype (State s)
-> m (State s, [PredicateFailure s])
applyRuleInternal ValidationPolicy
asoValidation STSInterpreter
goSTS
goSTS :: STSInterpreter
goSTS :: RuleContext rtype s -> m (State s, [[PredicateFailure s]])
goSTS = AssertionPolicy
-> RuleInterpreter
-> RuleContext rtype s
-> m (State s, [[PredicateFailure s]])
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
AssertionPolicy
-> RuleInterpreter
-> RuleContext rtype s
-> m (State s, [[PredicateFailure s]])
applySTSInternal AssertionPolicy
asoAssertions RuleInterpreter
goRule
in RuleContext rtype s -> m (State s, [[PredicateFailure s]])
STSInterpreter
goSTS RuleContext rtype s
ctx
applySTS ::
forall s m rtype.
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s ->
m (Either [[PredicateFailure s]] (State s))
applySTS :: RuleContext rtype s -> m (Either [[PredicateFailure s]] (State s))
applySTS RuleContext rtype s
ctx =
ApplySTSOpts
-> RuleContext rtype s -> m (State s, [[PredicateFailure s]])
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
ApplySTSOpts
-> RuleContext rtype s -> m (State s, [[PredicateFailure s]])
applySTSOpts ApplySTSOpts
defaultOpts RuleContext rtype s
ctx m (State s, [[PredicateFailure s]])
-> ((State s, [[PredicateFailure s]])
-> Either [[PredicateFailure s]] (State s))
-> m (Either [[PredicateFailure s]] (State s))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
(State s
st, []) -> State s -> Either [[PredicateFailure s]] (State s)
forall a b. b -> Either a b
Right State s
st
(State s
_, [[PredicateFailure s]]
pfs) -> [[PredicateFailure s]] -> Either [[PredicateFailure s]] (State s)
forall a b. a -> Either a b
Left [[PredicateFailure s]]
pfs
where
#ifdef STS_ASSERT
defaultOpts =
ApplySTSOpts
{ asoAssertions = AssertionsAll,
asoValidation = ValidateAll
}
#else
defaultOpts :: ApplySTSOpts
defaultOpts =
ApplySTSOpts :: AssertionPolicy -> ValidationPolicy -> ApplySTSOpts
ApplySTSOpts
{ asoAssertions :: AssertionPolicy
asoAssertions = AssertionPolicy
AssertionsOff,
asoValidation :: ValidationPolicy
asoValidation = ValidationPolicy
ValidateAll
}
#endif
reapplySTS ::
forall s m rtype.
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s ->
m (State s)
reapplySTS :: RuleContext rtype s -> m (State s)
reapplySTS RuleContext rtype s
ctx =
ApplySTSOpts
-> RuleContext rtype s -> m (State s, [[PredicateFailure s]])
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
ApplySTSOpts
-> RuleContext rtype s -> m (State s, [[PredicateFailure s]])
applySTSOpts ApplySTSOpts
defaultOpts RuleContext rtype s
ctx m (State s, [[PredicateFailure s]])
-> ((State s, [[PredicateFailure s]]) -> State s) -> m (State s)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (State s, [[PredicateFailure s]]) -> State s
forall a b. (a, b) -> a
fst
where
defaultOpts :: ApplySTSOpts
defaultOpts =
ApplySTSOpts :: AssertionPolicy -> ValidationPolicy -> ApplySTSOpts
ApplySTSOpts
{ asoAssertions :: AssertionPolicy
asoAssertions = AssertionPolicy
AssertionsOff,
asoValidation :: ValidationPolicy
asoValidation = ValidationPolicy
ValidateNone
}
applySTSIndifferently ::
forall s m rtype.
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s ->
m (State s, [[PredicateFailure s]])
applySTSIndifferently :: RuleContext rtype s -> m (State s, [[PredicateFailure s]])
applySTSIndifferently RuleContext rtype s
ctx =
ApplySTSOpts
-> RuleContext rtype s -> m (State s, [[PredicateFailure s]])
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
ApplySTSOpts
-> RuleContext rtype s -> m (State s, [[PredicateFailure s]])
applySTSOpts ApplySTSOpts
opts RuleContext rtype s
ctx
where
opts :: ApplySTSOpts
opts =
ApplySTSOpts :: AssertionPolicy -> ValidationPolicy -> ApplySTSOpts
ApplySTSOpts
{ asoAssertions :: AssertionPolicy
asoAssertions = AssertionPolicy
AssertionsAll,
asoValidation :: ValidationPolicy
asoValidation = ValidationPolicy
ValidateAll
}
applyRuleInternal ::
forall s m rtype.
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
ValidationPolicy ->
STSInterpreter ->
RuleContext rtype s ->
Rule s rtype (State s) ->
m (State s, [PredicateFailure s])
applyRuleInternal :: ValidationPolicy
-> STSInterpreter
-> RuleContext rtype s
-> Rule s rtype (State s)
-> m (State s, [PredicateFailure s])
applyRuleInternal ValidationPolicy
vp STSInterpreter
goSTS RuleContext rtype s
jc Rule s rtype (State s)
r = (StateT [PredicateFailure s] m (State s)
-> [PredicateFailure s] -> m (State s, [PredicateFailure s]))
-> [PredicateFailure s]
-> StateT [PredicateFailure s] m (State s)
-> m (State s, [PredicateFailure s])
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT [PredicateFailure s] m (State s)
-> [PredicateFailure s] -> m (State s, [PredicateFailure s])
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT [] (StateT [PredicateFailure s] m (State s)
-> m (State s, [PredicateFailure s]))
-> StateT [PredicateFailure s] m (State s)
-> m (State s, [PredicateFailure s])
forall a b. (a -> b) -> a -> b
$ (forall x. Clause s rtype x -> StateT [PredicateFailure s] m x)
-> Rule s rtype (State s)
-> StateT [PredicateFailure s] m (State s)
forall (m :: * -> *) (f :: * -> *) a.
Monad m =>
(forall x. f x -> m x) -> F f a -> m a
foldF forall x. Clause s rtype x -> StateT [PredicateFailure s] m x
runClause Rule s rtype (State s)
r
where
runClause :: Clause s rtype a -> MonadState.StateT [PredicateFailure s] m a
runClause :: Clause s rtype a -> StateT [PredicateFailure s] m a
runClause (Lift BaseM s a
f a -> a
next) = a -> a
next (a -> a)
-> StateT [PredicateFailure s] m a
-> StateT [PredicateFailure s] m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a -> StateT [PredicateFailure s] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m a
BaseM s a
f
runClause (GetCtx RuleContext rtype s -> a
next) = RuleContext rtype s -> a
next (RuleContext rtype s -> a)
-> StateT [PredicateFailure s] m (RuleContext rtype s)
-> StateT [PredicateFailure s] m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RuleContext rtype s
-> StateT [PredicateFailure s] m (RuleContext rtype s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure RuleContext rtype s
jc
runClause (Predicate Either e a
cond e -> PredicateFailure s
orElse a
val) = case ValidationPolicy
vp of
ValidationPolicy
ValidateAll -> do
case Either e a -> (e -> Either e a) -> Either e a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError Either e a
cond e -> Either e a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError of
Left e
err -> ([PredicateFailure s] -> [PredicateFailure s])
-> StateT [PredicateFailure s] m ()
forall (m :: * -> *) s. Monad m => (s -> s) -> StateT s m ()
modify (e -> PredicateFailure s
orElse e
err PredicateFailure s -> [PredicateFailure s] -> [PredicateFailure s]
forall a. a -> [a] -> [a]
:) StateT [PredicateFailure s] m ()
-> StateT [PredicateFailure s] m a
-> StateT [PredicateFailure s] m a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> StateT [PredicateFailure s] m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
val
Right a
x -> a -> StateT [PredicateFailure s] m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
ValidationPolicy
ValidateNone -> a -> StateT [PredicateFailure s] m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
val
runClause (SubTrans RuleContext rtype sub
subCtx State sub -> a
next) = do
(State sub
ss, [[PredicateFailure sub]]
sfails) <- m (State sub, [[PredicateFailure sub]])
-> StateT
[PredicateFailure s] m (State sub, [[PredicateFailure sub]])
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (State sub, [[PredicateFailure sub]])
-> StateT
[PredicateFailure s] m (State sub, [[PredicateFailure sub]]))
-> m (State sub, [[PredicateFailure sub]])
-> StateT
[PredicateFailure s] m (State sub, [[PredicateFailure sub]])
forall a b. (a -> b) -> a -> b
$ RuleContext rtype sub -> m (State sub, [[PredicateFailure sub]])
STSInterpreter
goSTS RuleContext rtype sub
subCtx
(PredicateFailure s -> StateT [PredicateFailure s] m ())
-> [PredicateFailure s] -> StateT [PredicateFailure s] m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (\PredicateFailure s
a -> ([PredicateFailure s] -> [PredicateFailure s])
-> StateT [PredicateFailure s] m ()
forall (m :: * -> *) s. Monad m => (s -> s) -> StateT s m ()
modify (PredicateFailure s
a PredicateFailure s -> [PredicateFailure s] -> [PredicateFailure s]
forall a. a -> [a] -> [a]
:)) ([PredicateFailure s] -> StateT [PredicateFailure s] m ())
-> [PredicateFailure s] -> StateT [PredicateFailure s] m ()
forall a b. (a -> b) -> a -> b
$ PredicateFailure sub -> PredicateFailure s
forall sub super.
Embed sub super =>
PredicateFailure sub -> PredicateFailure super
wrapFailed (PredicateFailure sub -> PredicateFailure s)
-> [PredicateFailure sub] -> [PredicateFailure s]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[PredicateFailure sub]] -> [PredicateFailure sub]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[PredicateFailure sub]]
sfails
State sub -> a
next (State sub -> a)
-> StateT [PredicateFailure s] m (State sub)
-> StateT [PredicateFailure s] m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> State sub -> StateT [PredicateFailure s] m (State sub)
forall (f :: * -> *) a. Applicative f => a -> f a
pure State sub
ss
applySTSInternal ::
forall s m rtype.
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
AssertionPolicy ->
RuleInterpreter ->
RuleContext rtype s ->
m (State s, [[PredicateFailure s]])
applySTSInternal :: AssertionPolicy
-> RuleInterpreter
-> RuleContext rtype s
-> m (State s, [[PredicateFailure s]])
applySTSInternal AssertionPolicy
ap RuleInterpreter
goRule RuleContext rtype s
ctx =
[(State s, [PredicateFailure s])]
-> (State s, [[PredicateFailure s]])
forall (t :: * -> *) a a. Foldable t => [(a, t a)] -> (a, [t a])
successOrFirstFailure ([(State s, [PredicateFailure s])]
-> (State s, [[PredicateFailure s]]))
-> m [(State s, [PredicateFailure s])]
-> m (State s, [[PredicateFailure s]])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SRuleType rtype
-> RuleContext rtype s -> m [(State s, [PredicateFailure s])]
applySTSInternal' SRuleType rtype
forall (t :: RuleType). RuleTypeRep t => SRuleType t
rTypeRep RuleContext rtype s
ctx
where
successOrFirstFailure :: [(a, t a)] -> (a, [t a])
successOrFirstFailure [(a, t a)]
xs =
case ((a, t a) -> Bool) -> [(a, t a)] -> Maybe (a, t a)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (t a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (t a -> Bool) -> ((a, t a) -> t a) -> (a, t a) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, t a) -> t a
forall a b. (a, b) -> b
snd) [(a, t a)]
xs of
Maybe (a, t a)
Nothing ->
case [(a, t a)]
xs of
[] -> String -> (a, [t a])
forall a. HasCallStack => String -> a
error String
"applySTSInternal was called with an empty set of rules"
(a
s, t a
_) : [(a, t a)]
_ -> (a
s, (a, t a) -> t a
forall a b. (a, b) -> b
snd ((a, t a) -> t a) -> [(a, t a)] -> [t a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(a, t a)]
xs)
Just (a
s, t a
_) -> (a
s, [])
applySTSInternal' ::
SRuleType rtype ->
RuleContext rtype s ->
m [(State s, [PredicateFailure s])]
applySTSInternal' :: SRuleType rtype
-> RuleContext rtype s -> m [(State s, [PredicateFailure s])]
applySTSInternal' SRuleType rtype
SInitial RuleContext rtype s
env =
RuleContext 'Initial s
-> F (Clause s 'Initial) (State s)
-> m (State s, [PredicateFailure s])
RuleInterpreter
goRule RuleContext rtype s
RuleContext 'Initial s
env (F (Clause s 'Initial) (State s)
-> m (State s, [PredicateFailure s]))
-> [F (Clause s 'Initial) (State s)]
-> m [(State s, [PredicateFailure s])]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
`traverse` [F (Clause s 'Initial) (State s)]
forall a. STS a => [InitialRule a]
initialRules
applySTSInternal' SRuleType rtype
STransition RuleContext rtype s
jc = do
!()
_ <-
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when
(AssertionPolicy -> Bool
assertPre AssertionPolicy
ap)
( [Assertion s] -> (Assertion s -> m ()) -> m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
sfor_ (STS s => [Assertion s]
forall a. STS a => [Assertion a]
assertions @s)
((Assertion s -> m ()) -> m ()) -> (Assertion s -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$! \case
PreCondition String
msg TRC s -> Bool
cond ->
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when
(Bool -> Bool
not (TRC s -> Bool
cond RuleContext rtype s
TRC s
jc))
( AssertionViolation s -> m ()
forall a e. Exception e => e -> a
throw
(AssertionViolation s -> m ()) -> AssertionViolation s -> m ()
forall a b. (a -> b) -> a -> b
$! AssertionViolation :: forall sts.
String
-> String -> TRC sts -> Maybe (State sts) -> AssertionViolation sts
AssertionViolation
{ avSTS :: String
avSTS = TypeRep -> String
forall a. Show a => a -> String
show (TypeRep -> String) -> TypeRep -> String
forall a b. (a -> b) -> a -> b
$ Proxy s -> TypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (Proxy s
forall k (t :: k). Proxy t
Proxy @s),
avMsg :: String
avMsg = String
msg,
avCtx :: TRC s
avCtx = RuleContext rtype s
TRC s
jc,
avState :: Maybe (State s)
avState = Maybe (State s)
forall a. Maybe a
Nothing
}
)
Assertion s
_ -> () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
)
[(State s, [PredicateFailure s])]
res <- RuleContext 'Transition s
-> F (Clause s 'Transition) (State s)
-> m (State s, [PredicateFailure s])
RuleInterpreter
goRule RuleContext rtype s
RuleContext 'Transition s
jc (F (Clause s 'Transition) (State s)
-> m (State s, [PredicateFailure s]))
-> [F (Clause s 'Transition) (State s)]
-> m [(State s, [PredicateFailure s])]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
`traverse` [F (Clause s 'Transition) (State s)]
forall a. STS a => [TransitionRule a]
transitionRules
!()
_ <- case (AssertionPolicy -> Bool
assertPost AssertionPolicy
ap, [(State s, [PredicateFailure s])]
-> (State s, [[PredicateFailure s]])
forall (t :: * -> *) a a. Foldable t => [(a, t a)] -> (a, [t a])
successOrFirstFailure [(State s, [PredicateFailure s])]
res) of
(Bool
True, (State s
st, [])) ->
[Assertion s] -> (Assertion s -> m ()) -> m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
sfor_ (STS s => [Assertion s]
forall a. STS a => [Assertion a]
assertions @s)
((Assertion s -> m ()) -> m ()) -> (Assertion s -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$! ( \case
PostCondition String
msg TRC s -> State s -> Bool
cond ->
if Bool -> Bool
not (TRC s -> State s -> Bool
cond RuleContext rtype s
TRC s
jc State s
st)
then
AssertionViolation s -> m ()
forall a e. Exception e => e -> a
throw
(AssertionViolation s -> m ()) -> AssertionViolation s -> m ()
forall a b. (a -> b) -> a -> b
$! AssertionViolation :: forall sts.
String
-> String -> TRC sts -> Maybe (State sts) -> AssertionViolation sts
AssertionViolation
{ avSTS :: String
avSTS = TypeRep -> String
forall a. Show a => a -> String
show (TypeRep -> String) -> TypeRep -> String
forall a b. (a -> b) -> a -> b
$ Proxy s -> TypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (Proxy s
forall k (t :: k). Proxy t
Proxy @s),
avMsg :: String
avMsg = String
msg,
avCtx :: TRC s
avCtx = RuleContext rtype s
TRC s
jc,
avState :: Maybe (State s)
avState = State s -> Maybe (State s)
forall a. a -> Maybe a
Just State s
st
}
else () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Assertion s
_ -> () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
)
(Bool, (State s, [[PredicateFailure s]]))
_ -> () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
[(State s, [PredicateFailure s])]
-> m [(State s, [PredicateFailure s])]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(State s, [PredicateFailure s])]
-> m [(State s, [PredicateFailure s])])
-> [(State s, [PredicateFailure s])]
-> m [(State s, [PredicateFailure s])]
forall a b. (a -> b) -> a -> b
$! [(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
(Threshold a -> Threshold a -> Bool)
-> (Threshold a -> Threshold a -> Bool) -> Eq (Threshold a)
forall a. Eq a => Threshold a -> Threshold a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Threshold a -> Threshold a -> Bool
$c/= :: forall a. Eq a => Threshold a -> Threshold a -> Bool
== :: Threshold a -> Threshold a -> Bool
$c== :: forall a. Eq a => Threshold a -> Threshold a -> Bool
Eq, Eq (Threshold a)
Eq (Threshold a)
-> (Threshold a -> Threshold a -> Ordering)
-> (Threshold a -> Threshold a -> Bool)
-> (Threshold a -> Threshold a -> Bool)
-> (Threshold a -> Threshold a -> Bool)
-> (Threshold a -> Threshold a -> Bool)
-> (Threshold a -> Threshold a -> Threshold a)
-> (Threshold a -> Threshold a -> Threshold a)
-> Ord (Threshold a)
Threshold a -> Threshold a -> Bool
Threshold a -> Threshold a -> Ordering
Threshold a -> Threshold a -> Threshold a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (Threshold a)
forall a. Ord a => Threshold a -> Threshold a -> Bool
forall a. Ord a => Threshold a -> Threshold a -> Ordering
forall a. Ord a => Threshold a -> Threshold a -> Threshold a
min :: Threshold a -> Threshold a -> Threshold a
$cmin :: forall a. Ord a => Threshold a -> Threshold a -> Threshold a
max :: Threshold a -> Threshold a -> Threshold a
$cmax :: forall a. Ord a => Threshold a -> Threshold a -> Threshold a
>= :: Threshold a -> Threshold a -> Bool
$c>= :: forall a. Ord a => Threshold a -> Threshold a -> Bool
> :: Threshold a -> Threshold a -> Bool
$c> :: forall a. Ord a => Threshold a -> Threshold a -> Bool
<= :: Threshold a -> Threshold a -> Bool
$c<= :: forall a. Ord a => Threshold a -> Threshold a -> Bool
< :: Threshold a -> Threshold a -> Bool
$c< :: forall a. Ord a => Threshold a -> Threshold a -> Bool
compare :: Threshold a -> Threshold a -> Ordering
$ccompare :: forall a. Ord a => Threshold a -> Threshold a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (Threshold a)
Ord, Int -> Threshold a -> ShowS
[Threshold a] -> ShowS
Threshold a -> String
(Int -> Threshold a -> ShowS)
-> (Threshold a -> String)
-> ([Threshold a] -> ShowS)
-> Show (Threshold a)
forall a. Show a => Int -> Threshold a -> ShowS
forall a. Show a => [Threshold a] -> ShowS
forall a. Show a => Threshold a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Threshold a] -> ShowS
$cshowList :: forall a. Show a => [Threshold a] -> ShowS
show :: Threshold a -> String
$cshow :: forall a. Show a => Threshold a -> String
showsPrec :: Int -> Threshold a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Threshold a -> ShowS
Show, Typeable (Threshold a)
DataType
Constr
Typeable (Threshold a)
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Threshold a -> c (Threshold a))
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Threshold a))
-> (Threshold a -> Constr)
-> (Threshold a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Threshold a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Threshold a)))
-> ((forall b. Data b => b -> b) -> Threshold a -> Threshold a)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Threshold a -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Threshold a -> r)
-> (forall u. (forall d. Data d => d -> u) -> Threshold a -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> Threshold a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a))
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a))
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a))
-> Data (Threshold a)
Threshold a -> DataType
Threshold a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (Threshold a))
(forall b. Data b => b -> b) -> Threshold a -> Threshold a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Threshold a -> c (Threshold a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Threshold a)
forall a. Data a => Typeable (Threshold a)
forall a. Data a => Threshold a -> DataType
forall a. Data a => Threshold a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> Threshold a -> Threshold a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Threshold a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> Threshold a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Threshold a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Threshold a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Threshold a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Threshold a -> c (Threshold a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Threshold a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Threshold a))
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Threshold a -> u
forall u. (forall d. Data d => d -> u) -> Threshold a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Threshold a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Threshold a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Threshold a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Threshold a -> c (Threshold a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Threshold a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Threshold a))
$cThreshold :: Constr
$tThreshold :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a)
gmapMp :: (forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a)
gmapM :: (forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Threshold a -> m (Threshold a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> Threshold a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Threshold a -> u
gmapQ :: (forall d. Data d => d -> u) -> Threshold a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> Threshold a -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Threshold a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Threshold a -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Threshold a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Threshold a -> r
gmapT :: (forall b. Data b => b -> b) -> Threshold a -> Threshold a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Threshold a -> Threshold a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Threshold a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Threshold a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Threshold a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Threshold a))
dataTypeOf :: Threshold a -> DataType
$cdataTypeOf :: forall a. Data a => Threshold a -> DataType
toConstr :: Threshold a -> Constr
$ctoConstr :: forall a. Data a => Threshold a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Threshold a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Threshold a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Threshold a -> c (Threshold a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Threshold a -> c (Threshold a)
$cp1Data :: forall a. Data a => Typeable (Threshold a)
Data, Typeable, Context -> Threshold a -> IO (Maybe ThunkInfo)
Proxy (Threshold a) -> String
(Context -> Threshold a -> IO (Maybe ThunkInfo))
-> (Context -> Threshold a -> IO (Maybe ThunkInfo))
-> (Proxy (Threshold a) -> String)
-> NoThunks (Threshold a)
forall a.
NoThunks a =>
Context -> Threshold a -> IO (Maybe ThunkInfo)
forall a. NoThunks a => Proxy (Threshold a) -> String
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
showTypeOf :: Proxy (Threshold a) -> String
$cshowTypeOf :: forall a. NoThunks a => Proxy (Threshold a) -> String
wNoThunks :: Context -> Threshold a -> IO (Maybe ThunkInfo)
$cwNoThunks :: forall a.
NoThunks a =>
Context -> Threshold a -> IO (Maybe ThunkInfo)
noThunks :: Context -> Threshold a -> IO (Maybe ThunkInfo)
$cnoThunks :: forall a.
NoThunks a =>
Context -> Threshold a -> IO (Maybe ThunkInfo)
NoThunks)
straverse_ :: (Foldable t, Applicative f) => (a -> f b) -> t a -> f ()
straverse_ :: (a -> f b) -> t a -> f ()
straverse_ a -> f b
f = (a -> f () -> f ()) -> f () -> t a -> f ()
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> f () -> f ()
c (() -> f ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
where
c :: a -> f () -> f ()
c !a
x !f ()
k = (f b -> f () -> f ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> f ()
k) (f b -> f ()) -> f b -> f ()
forall a b. (a -> b) -> a -> b
$! a -> f b
f a
x
{-# INLINE c #-}
sfor_ :: (Foldable t, Applicative f) => t a -> (a -> f b) -> f ()
{-# INLINE sfor_ #-}
sfor_ :: t a -> (a -> f b) -> f ()
sfor_ = ((a -> f b) -> t a -> f ()) -> t a -> (a -> f b) -> f ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> f b) -> t a -> f ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
straverse_