TypedFsm.Driver

Running FSM

The core function is runOp, and the other functions are to make it work properly.

Documentation

data SomeOperate ts (m :: Type -> Type) a

Constructors

SingI i => SomeOperate (Operate m (At a o) i)

getSomeOperateSt :: forall ts (m :: Type -> Type) a. SingKind ts => SomeOperate ts m a -> Demote ts

data Result ps (m :: Type -> Type) a

Reuslt of runOp

• Finish, return val a
• A wrapper for SomeOperate that returns the remaining computation when there is not enough input
• There is no corresponding GenMsg function defined for some FSM states

Constructors

Finish a

Cont (SomeOperate ps m a)

NotMatchGenMsg (Sing t)

type Op ps state (m :: Type -> Type) a (o :: ps) (i :: ps) = Operate (StateT state m) (At a o) i

Op adds new assumptions based on Operate: assume that the internal monad contains at least a state monad.

type Op ps state m a o i = Operate (StateT state m) (At a (o :: ps)) (i :: ps)

Op contains two states, ps and state.

ps represents the state of the state machine state represents the internal state.

The external event needs to be converted to Msg.

It is essentially a function `event -> Msg`, but this function is affected by both ps and state.

newtype GenMsg ps state event (from :: ps)

Constructors

GenMsg (state -> event -> Maybe (SomeMsg ps from))

type State2GenMsg ps state event = DMap (Sing :: ps -> Type) (GenMsg ps state event)

data SomeMsg ps (from :: ps)

Constructors

SingI to => SomeMsg (Msg ps from to)

type SomeOp ps state (m :: Type -> Type) a = SomeOperate ps (StateT state m) a

sOrdToGCompare :: forall n (a :: n) (b :: n). SOrd n => Sing a -> Sing b -> GOrdering a b

runOp :: forall ps event state (m :: Type -> Type) a (input :: ps) (output :: ps). (SingI input, GCompare (Sing :: ps -> Type), Monad m) => State2GenMsg ps state event -> [event] -> Operate (StateT state m) (At a output) input -> StateT state m (Result ps (StateT state m) a)