small-steps-1.1.0.0: Small step semantics
Safe HaskellSafe-Inferred
LanguageHaskell2010

Control.State.Transition.Simple

Description

Simple state transition system over the Identity monad.

Synopsis

Documentation

applySTSIndifferently ∷ ∀ s rtype. (STS s, RuleTypeRep rtype, Identity ~ BaseM s) ⇒ RuleContext rtype s → (State s, [PredicateFailure s]) Source #

applySTS ∷ ∀ s rtype. (STS s, RuleTypeRep rtype, BaseM s ~ Identity) ⇒ RuleContext rtype s → Either (NonEmpty (PredicateFailure s)) (State s) Source #

data STUB (e ∷ Type) (st ∷ Type) (si ∷ Type) (f ∷ Type) (m ∷ TypeType) Source #

A stub rule with no transitions to use as a placeholder

Instances

Instances details
(Eq f, Monad m, Show f, Typeable e, Typeable f, Typeable si, Typeable st, Typeable m) ⇒ STS (STUB e st si f m) Source # 
Instance details

Defined in Control.State.Transition.Extended

Associated Types

type State (STUB e st si f m) Source #

type Signal (STUB e st si f m) Source #

type Environment (STUB e st si f m) Source #

type BaseM (STUB e st si f m) ∷ TypeType Source #

type Event (STUB e st si f m) Source #

type PredicateFailure (STUB e st si f m) Source #

type BaseM (STUB e st si f m) Source # 
Instance details

Defined in Control.State.Transition.Extended

type BaseM (STUB e st si f m) = m
type Environment (STUB e st si f m) Source # 
Instance details

Defined in Control.State.Transition.Extended

type Environment (STUB e st si f m) = e
type Event (STUB e st si f m) Source # 
Instance details

Defined in Control.State.Transition.Extended

type Event (STUB e st si f m) = Void
type PredicateFailure (STUB e st si f m) Source # 
Instance details

Defined in Control.State.Transition.Extended

type PredicateFailure (STUB e st si f m) = f
type Signal (STUB e st si f m) Source # 
Instance details

Defined in Control.State.Transition.Extended

type Signal (STUB e st si f m) = si
type State (STUB e st si f m) Source # 
Instance details

Defined in Control.State.Transition.Extended

type State (STUB e st si f m) = st

newtype Threshold a Source #

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

Constructors

Threshold a 

Instances

Instances details
Data a ⇒ Data (Threshold a) Source # 
Instance details

Defined in Control.State.Transition.Extended

Methods

gfoldl ∷ (∀ d b. Data d ⇒ c (d → b) → d → c b) → (∀ g. g → c g) → Threshold a → c (Threshold a) Source #

gunfold ∷ (∀ b r. Data b ⇒ c (b → r) → c r) → (∀ r. r → c r) → Constr → c (Threshold a) Source #

toConstrThreshold a → Constr Source #

dataTypeOfThreshold a → DataType Source #

dataCast1Typeable t ⇒ (∀ d. Data d ⇒ c (t d)) → Maybe (c (Threshold a)) Source #

dataCast2Typeable t ⇒ (∀ d e. (Data d, Data e) ⇒ c (t d e)) → Maybe (c (Threshold a)) Source #

gmapT ∷ (∀ b. Data b ⇒ b → b) → Threshold a → Threshold a Source #

gmapQl ∷ (r → r' → r) → r → (∀ d. Data d ⇒ d → r') → Threshold a → r Source #

gmapQr ∷ ∀ r r'. (r' → r → r) → r → (∀ d. Data d ⇒ d → r') → Threshold a → r Source #

gmapQ ∷ (∀ d. Data d ⇒ d → u) → Threshold a → [u] Source #

gmapQiInt → (∀ d. Data d ⇒ d → u) → Threshold a → u Source #

gmapMMonad m ⇒ (∀ d. Data d ⇒ d → m d) → Threshold a → m (Threshold a) Source #

gmapMpMonadPlus m ⇒ (∀ d. Data d ⇒ d → m d) → Threshold a → m (Threshold a) Source #

gmapMoMonadPlus m ⇒ (∀ d. Data d ⇒ d → m d) → Threshold a → m (Threshold a) Source #

Show a ⇒ Show (Threshold a) Source # 
Instance details

Defined in Control.State.Transition.Extended

Eq a ⇒ Eq (Threshold a) Source # 
Instance details

Defined in Control.State.Transition.Extended

Methods

(==)Threshold a → Threshold a → Bool Source #

(/=)Threshold a → Threshold a → Bool Source #

Ord a ⇒ Ord (Threshold a) Source # 
Instance details

Defined in Control.State.Transition.Extended

NoThunks a ⇒ NoThunks (Threshold a) Source # 
Instance details

Defined in Control.State.Transition.Extended

type RuleInterpreter ep = ∀ 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])) Source #

type STSInterpreter ep = ∀ s m rtype. (STS s, RuleTypeRep rtype, m ~ BaseM s) ⇒ RuleContext rtype s → m (EventReturnType ep s (State s, [PredicateFailure s])) Source #

data ApplySTSOpts ep Source #

Constructors

ApplySTSOpts 

Fields

data ValidationPolicy Source #

Control which predicates are evaluated during rule processing.

data AssertionPolicy Source #

Control which assertions are enabled.

Constructors

AssertionsAll 
AssertionsPre

Only run preconditions

AssertionsPost

Only run postconditions

AssertionsOff 

type Label = String Source #

Label for a predicate. This can be used to control which predicates get run.

type Rule sts rtype = F (Clause sts rtype) Source #

class EventReturnTypeRep ert Source #

Minimal complete definition

eventReturnTypeRep

type family EventReturnType ep sts a ∷ Type where ... Source #

Equations

EventReturnType 'EventPolicyReturn sts a = (a, [Event sts]) 
EventReturnType _ _ a = a 

class (STS sub, BaseM sub ~ BaseM super) ⇒ Embed sub super where Source #

Embed one STS within another.

Minimal complete definition

wrapFailed

Methods

wrapFailedPredicateFailure sub → PredicateFailure super Source #

Wrap a predicate failure of the subsystem in a failure of the super-system.

wrapEventEvent sub → Event super Source #

default wrapEventCoercible (Event sub) (Event super) ⇒ Event sub → Event super Source #

Instances

Instances details
STS sts ⇒ Embed sts sts Source # 
Instance details

Defined in Control.State.Transition.Extended

class (Eq (PredicateFailure a), Show (PredicateFailure a), Monad (BaseM a), Typeable a) ⇒ STS a where Source #

State transition system.

Minimal complete definition

transitionRules

Associated Types

type State a ∷ Type Source #

Type of the state which the system transitions between.

type Signal a ∷ Type Source #

Signal triggering a state change.

type Environment a ∷ Type Source #

Environment type.

type BaseM a ∷ TypeType Source #

Monad into which to interpret the rules.

type BaseM a = Identity

type Event a ∷ Type Source #

Event type.

type Event a = Void

type PredicateFailure a ∷ Type Source #

Descriptive type for the possible failures which might cause a transition to fail.

As a convention, PredicateFailures 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 PredicateFailures 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.

Methods

initialRules ∷ [InitialRule a] Source #

Rules governing transition under this system.

default initialRulesDefault (State a) ⇒ [InitialRule a] Source #

transitionRules ∷ [TransitionRule a] Source #

assertions ∷ [Assertion a] Source #

Assertions about the transition system.

renderAssertionViolationAssertionViolation a → String Source #

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.

Instances

Instances details
(Eq f, Monad m, Show f, Typeable e, Typeable f, Typeable si, Typeable st, Typeable m) ⇒ STS (STUB e st si f m) Source # 
Instance details

Defined in Control.State.Transition.Extended

Associated Types

type State (STUB e st si f m) Source #

type Signal (STUB e st si f m) Source #

type Environment (STUB e st si f m) Source #

type BaseM (STUB e st si f m) ∷ TypeType Source #

type Event (STUB e st si f m) Source #

type PredicateFailure (STUB e st si f m) Source #

data AssertionViolation sts Source #

Constructors

AssertionViolation 

Fields

Instances

Instances details
STS sts ⇒ Show (AssertionViolation sts) Source # 
Instance details

Defined in Control.State.Transition.Extended

data Assertion sts Source #

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.

Constructors

PreCondition String (TRC sts → Bool)

Pre-condition. Checked before the rule fires.

PostCondition String (TRC sts → State sts → Bool)

Post-condition. Checked after the rule fires, and given access to the resultant state as well as the initial context.

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

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

type family RuleContext (t ∷ RuleType) = (ctx ∷ TypeType) | ctx → t where ... Source #

newtype TRC sts Source #

Context available to transition rules.

Constructors

TRC (Environment sts, State sts, Signal sts) 

Instances

Instances details
(Show (Environment sts), Show (State sts), Show (Signal sts)) ⇒ Show (TRC sts) Source # 
Instance details

Defined in Control.State.Transition.Extended

Methods

showsPrecIntTRC sts → ShowS Source #

showTRC sts → String Source #

showList ∷ [TRC sts] → ShowS Source #

newtype IRC sts Source #

Context available to initial rules.

Constructors

IRC (Environment sts) 

class RuleTypeRep t Source #

Minimal complete definition

rTypeRep

Instances

Instances details
RuleTypeRep 'Initial Source # 
Instance details

Defined in Control.State.Transition.Extended

Methods

rTypeRep ∷ SRuleType 'Initial

RuleTypeRep 'Transition Source # 
Instance details

Defined in Control.State.Transition.Extended

Methods

rTypeRep ∷ SRuleType 'Transition

data RuleType Source #

Constructors

Initial 
Transition 

mapEventReturn ∷ ∀ ep sts a b. EventReturnTypeRep ep ⇒ (a → b) → EventReturnType ep sts a → EventReturnType ep sts b Source #

Map over an arbitrary EventReturnType.

validateValidation (NonEmpty (PredicateFailure sts)) () → Rule sts ctx () Source #

Fail with PredicateFailure's in STS if Validation was unsuccessful.

validateTrans Source #

Arguments

∷ (e → PredicateFailure sts)

Transformation function for all errors

Validation (NonEmpty e) () 
Rule sts ctx () 

Same as validation, except with ability to transform opaque failures into PredicateFailures with a help of supplied function.

validateTransLabeled Source #

Arguments

∷ (e → PredicateFailure sts)

Transformation function for all errors

NonEmpty Label

Supply a list of labels to be used as filters when STS is executed

Validation (NonEmpty e) ()

Actual validations to be executed

Rule sts ctx () 

Same as validation, except with ability to translate opaque failures into PredicateFailures with a help of supplied function.

(?!)BoolPredicateFailure sts → Rule sts ctx () infix 1 Source #

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.

failBecausePredicateFailure sts → Rule sts ctx () Source #

failOnJustMaybe a → (a → PredicateFailure sts) → Rule sts ctx () Source #

Produce a predicate failure when condition contains a Just value, contents of which can be used inside the predicate failure

failureOnJustMaybe a → (a → e) → Validation (NonEmpty e) () Source #

Produce a failure when condition contains a Just value, contents of which can be used inside the failure

failOnNonEmptyFoldable f ⇒ f a → (NonEmpty a → PredicateFailure sts) → Rule sts ctx () Source #

Produce a predicate failure when supplied foldable is not empty, contents of which will be converted to a NonEmpty list and can be used inside the predicate failure.

failureOnNonEmptyFoldable f ⇒ f a → (NonEmpty a → e) → Validation (NonEmpty e) () Source #

Produce a failure when supplied foldable is not empty, contents of which will be converted to a NonEmpty list and theh can be used inside the failure.

(?!:)Either e () → (e → PredicateFailure sts) → Rule sts ctx () Source #

Oh noes with an explanation

We interpret this as "What?" "No!" "Because:"

labeledPredNonEmpty LabelBoolPredicateFailure sts → Rule sts ctx () Source #

Labeled predicate. This may be used to control which predicates are run using ValidateSuchThat.

labeledPredENonEmpty LabelEither e () → (e → PredicateFailure sts) → Rule sts ctx () Source #

Labeled predicate with an explanation

labeledNonEmpty LabelRule sts ctx () → Rule sts ctx () Source #

Labeled clause. This will only be executed if the interpreter is set to execute clauses with this label.

transEmbed sub super ⇒ RuleContext rtype sub → Rule super rtype (State sub) Source #

ifFailureFreeRule sts rtype a → Rule sts rtype a → Rule sts rtype a Source #

whenFailureFreeRule sts rtype () → Rule sts rtype () Source #

liftSTSSTS sts ⇒ BaseM sts a → Rule sts ctx a Source #

judgmentContextRule sts rtype (RuleContext rtype sts) Source #

Get the judgment context

applySTSOpts ∷ ∀ s m rtype ep. (STS s, RuleTypeRep rtype, m ~ BaseM s) ⇒ ApplySTSOpts ep → RuleContext rtype s → m (EventReturnType ep s (State s, [PredicateFailure s])) Source #

Apply an STS with options. Note that this returns both the final state and the list of predicate failures.

applySTSOptsEither ∷ ∀ 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))) Source #

reapplySTS ∷ ∀ s m rtype. (STS s, RuleTypeRep rtype, m ~ BaseM s) ⇒ RuleContext rtype s → m (State s) Source #

Re-apply an STS.

It is assumed that the caller of this function has previously applied this STS, and can guarantee that it completed successfully. No predicates or assertions will be checked when calling this function.

applyRuleInternal Source #

Arguments

∷ ∀ (ep ∷ EventPolicy) s m rtype result. (STS s, RuleTypeRep rtype, m ~ BaseM s) 
⇒ IsFailing

We need to know if the current STS incurred at least one PredicateFailure. This is necessary because applyRuleInternal is called recursively through the goSTS argument, which will not have access to any of the predicate failures occured in other branches of STS rule execusion tree.

SingEP ep 
ValidationPolicy 
→ (IsFailing → STSInterpreter ep)

Interpreter for subsystems

RuleContext rtype s 
Rule s rtype result 
→ m (EventReturnType ep s (result, [PredicateFailure s])) 

Apply a rule even if its predicates fail.

If the rule successfully applied, the list of predicate failures will be empty.

applySTSInternal Source #

Arguments

∷ ∀ s m rtype ep. (STS s, RuleTypeRep rtype, m ~ BaseM s) 
SingEP ep 
AssertionPolicy 
RuleInterpreter ep

Interpreter for rules

RuleContext rtype s 
ExceptT (AssertionViolation s) m (EventReturnType ep s (State s, [PredicateFailure s])) 

sfor_ ∷ (Foldable t, Applicative f) ⇒ t a → (a → f b) → f () Source #

sfor_ is straverse_ with its arguments flipped. For a version that doesn't ignore the results see for.

>>> sfor_ ([1..4] :: [Int]) print
1
2
3
4

tellEventEvent sts → Rule sts ctx () Source #

tellEvents ∷ [Event sts] → Rule sts ctx () Source #

runRule ∷ (STS s, RuleTypeRep rtype) ⇒ RuleContext rtype s → Rule s rtype result → BaseM s (result, [PredicateFailure s]) Source #

runRule :: RuleInterpreter 'EventPolicyDiscard run a rule given its context, to get a BaseM computation