{-# 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 #-}

-- | Small step state transition systems.
module Control.State.Transition.Extended
  ( RuleType (..),
    RuleTypeRep,
    RuleContext,
    IRC (..),
    TRC (..),
    Rule,
    TransitionRule,
    InitialRule,
    Assertion (..),
    AssertionViolation (..),
    STS (..),
    Embed (..),
    (?!),
    (?!:),
    failBecause,
    judgmentContext,
    trans,
    liftSTS,
    -- * Apply STS
    AssertionPolicy (..),
    ValidationPolicy (..),
    ApplySTSOpts (..),
    applySTSOpts,
    applySTS,
    applySTSIndifferently,
    reapplySTS,

    -- * Random thing
    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

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

class RuleTypeRep t where
  rTypeRep :: SRuleType t

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

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

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

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

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

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

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

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

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

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

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

instance
  (STS sts) =>
  Exception (AssertionViolation sts)

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

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

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

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

  type BaseM a = Identity

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

  -- | Rules governing transition under this system.
  initialRules :: [InitialRule a]

  transitionRules :: [TransitionRule a]

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

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

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

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 ->
    -- Subsequent computation with state introduced
    (State sub -> a) ->
    Clause sts rtype a
  Predicate ::
    Either e a ->
    -- Type of failure to return if the predicate fails
    (e -> PredicateFailure sts) ->
    a ->
    Clause sts rtype a

deriving instance Functor (Clause sts rtype)

type Rule sts rtype = F (Clause sts rtype)

-- | Oh noes!
--
--   This takes a condition (a boolean expression) and a failure and results in
--   a clause which will throw that failure if the condition fails.
(?!) :: Bool -> PredicateFailure sts -> Rule sts ctx ()
Bool
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 ()
?!)

-- | Oh noes with an explanation
--
--   We interpret this as "What?" "No!" "Because:"
(?!:) :: 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

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

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

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

-- | Control which predicates are evaluated during rule processing.
data ValidationPolicy
  = ValidateAll
  | ValidateNone
  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
  { -- | Enable assertions during STS processing.
    --   If this option is enabled, STS processing will terminate on violation
    --   of an assertion.
    ApplySTSOpts -> AssertionPolicy
asoAssertions :: AssertionPolicy,
    -- | Validation policy
    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])

-- | Apply an STS with options. Note that this returns both the final state and
-- the list of predicate failures.
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

-- | Re-apply an STS.
--
--   It is assumed that the caller of this function has previously applied this
--   STS, and can guarantee that it completed successfully. No predicates will
--   be checked when calling this function.
reapplySTS ::
  forall s m rtype.
  (STS s, RuleTypeRep rtype, m ~ BaseM s) =>
  RuleContext rtype s ->
  m (State s)
reapplySTS :: RuleContext rtype s -> m (State s)
reapplySTS RuleContext rtype s
ctx =
  ApplySTSOpts
-> 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
        }

-- | Apply a rule even if its predicates fail.
--
--   If the rule successfully applied, the list of predicate failures will be
--   empty.
applyRuleInternal ::
  forall s m rtype.
  (STS s, RuleTypeRep rtype, m ~ BaseM s) =>
  ValidationPolicy ->
  -- | Interpreter for subsystems
  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 ->
  -- | Interpreter for rules
  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
      -- We only care about running postconditions if the state transition was
      -- successful.
      !()
_ <- 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

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

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

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

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