typed-fsm 0.1.0.1 → 0.2.0.0

raw patch · 6 files changed

+187/−106 lines, 6 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• src/TypedFsm.hs +6/−2
• src/TypedFsm/Driver.hs +0/−102
• src/TypedFsm/Driver/Common.hs +45/−0
• src/TypedFsm/Driver/General.hs +49/−0
• src/TypedFsm/Driver/Op.hs +83/−0
• typed-fsm.cabal +4/−2

@@ -43,8 +43,12 @@   module TypedFsm.Core,    -- * Running FSM-  module TypedFsm.Driver,+  module TypedFsm.Driver.Common,+  module TypedFsm.Driver.General,+  module TypedFsm.Driver.Op, ) where  import TypedFsm.Core-import TypedFsm.Driver+import TypedFsm.Driver.Common+import TypedFsm.Driver.General+import TypedFsm.Driver.Op

@@ -1,102 +0,0 @@-{-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE LambdaCase #-}--{- | Running FSM--The core function is `runOp`, and the other functions are to make it work properly.--}-module TypedFsm.Driver where--import Control.Monad.State as S (MonadState (get), StateT)-import Data.Dependent.Map (DMap)-import Data.Dependent.Map qualified as D-import Data.GADT.Compare (GCompare, GOrdering (..))-import Data.IFunctor (At (..))-import Data.Ord.Singletons (SOrd (sCompare), SOrdering (..))-import Data.Singletons (Sing, SingI (..), SingKind (..))-import TypedFsm.Core (Operate (..), StateTransMsg (Msg))-import Unsafe.Coerce (unsafeCoerce)--data SomeOperate ts m a-  = forall (i :: ts) (o :: ts).-    (SingI i) =>-    SomeOperate (Operate m (At a o) i)--getSomeOperateSt :: (SingKind ts) => SomeOperate ts m a -> Demote ts-getSomeOperateSt (SomeOperate (_ :: Operate m (At a o) i)) = fromSing $ sing @i--{- | 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--}-data Result ps m a-  = Finish a-  | Cont (SomeOperate ps m a)-  | forall t. NotMatchGenMsg (Sing (t :: ps))--{- | `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`.--}-type Op ps state m a o i = Operate (StateT state m) (At a (o :: ps)) (i :: ps)--newtype GenMsg ps state event from-  = GenMsg (state -> event -> Maybe (SomeMsg ps from))--type State2GenMsg ps state event = DMap (Sing @ps) (GenMsg ps state event)--data SomeMsg ps from-  = forall (to :: ps).-    (SingI to) =>-    SomeMsg (Msg ps from to)--type SomeOp ps state m a = SomeOperate ps (StateT state m) a--sOrdToGCompare-  :: forall n (a :: n) (b :: n)-   . (SOrd n)-  => Sing a -> Sing b -> GOrdering a b-sOrdToGCompare a b = case sCompare a b of-  SEQ -> unsafeCoerce GEQ-  SLT -> GLT-  SGT -> GGT--runOp-  :: forall ps event state m a (input :: ps) (output :: ps)-   . ( SingI input-     , GCompare (Sing @ps)-     )-  => (Monad m)-  => State2GenMsg ps state event-  -> [event]-  -> Operate (StateT state m) (At a output) input-  -> (StateT state m) (Result ps (StateT state m) a)-runOp dmp evns = \case-  IReturn (At a) -> pure (Finish a)-  LiftM m -> m Prelude.>>= runOp dmp evns-  In f -> do-    let singInput = sing @input-    case D.lookup singInput dmp of-      Nothing -> pure (NotMatchGenMsg singInput)-      Just (GenMsg genMsg) -> loop evns-       where-        loop [] = pure $ Cont $ SomeOperate (In f)-        loop (et : evns') = do-          state' <- get-          case genMsg state' et of-            Nothing -> loop evns'-            Just (SomeMsg msg) -> runOp dmp evns' (f msg)

@@ -0,0 +1,45 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# OPTIONS_GHC -Wno-unused-do-bind #-}++module TypedFsm.Driver.Common where++import Data.IFunctor (At (..))+import Data.Singletons (Sing, SingI (..), SingKind (..))+import TypedFsm.Core (Operate (..), StateTransMsg (Msg))+import Unsafe.Coerce (unsafeCoerce)++data SomeOperate ts m a+  = forall (i :: ts) (o :: ts).+    (SingI i) =>+    SomeOperate (Operate m (At a o) i)++getSomeOperateSingeton :: (SingKind ts) => SomeOperate ts m a -> Sing ts+getSomeOperateSingeton (SomeOperate (_ :: Operate m ia i)) =+  unsafeCoerce $ sing @i++getSomeOperateSt :: (SingKind ts) => SomeOperate ts m a -> Demote ts+getSomeOperateSt (SomeOperate (_ :: Operate m ia i)) = fromSing $ sing @i++data SomeMsg ps from+  = forall (to :: ps).+    (SingI to) =>+    SomeMsg (Msg ps from to)++data AnyMsg ps+  = forall (from :: ps) (to :: ps).+    (SingI from, SingI to) =>+    AnyMsg (Msg ps from to)++{- | Reuslt of run FSM++* Finish, return val a+* A wrapper for SomeOperate that returns the remaining computation when there is not enough input+* Error happened+-}+data Result ps e m a+  = Finish a+  | Cont (SomeOperate ps m a)+  | ErrorInfo e

@@ -0,0 +1,49 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# OPTIONS_GHC -Wno-unused-do-bind #-}++-- | Running FSM+module TypedFsm.Driver.General where++import Data.Bool.Singletons (SBool (..))+import Data.Eq.Singletons (SEq (..))+import Data.IFunctor (At (..))+import Data.Singletons (SingI (..))+import TypedFsm.Core (Operate (..), StateTransMsg (Msg))+import TypedFsm.Driver.Common+import Unsafe.Coerce (unsafeCoerce)++anyToSomeMsg+  :: forall ps input+   . (SingI input, SEq ps)+  => AnyMsg ps -> Maybe (SomeMsg ps input)+anyToSomeMsg (AnyMsg (msg :: Msg ps from to)) =+  case sing @from %== sing @input of+    -- (from == input) ~ True+    -- ==> from ~ input+    STrue -> unsafeCoerce (Just (SomeMsg msg))+    SFalse -> Nothing++newtype UnexpectMsg ps = UnexpectMsg (AnyMsg ps)++runOperate+  :: forall ps m a (input :: ps) (output :: ps)+   . ( Monad m+     , SingI input+     , SEq ps+     )+  => [AnyMsg ps]+  -> Operate m (At a output) input+  -> m (Result ps (UnexpectMsg ps) m a)+runOperate anyMsgs = \case+  IReturn (At a) -> pure (Finish a)+  LiftM m -> m >>= (runOperate anyMsgs)+  In f -> loop anyMsgs+   where+    loop [] = pure $ Cont $ SomeOperate (In f)+    loop (anyMsg : evns') = do+      case anyToSomeMsg @_ @input anyMsg of+        Nothing -> pure (ErrorInfo $ UnexpectMsg anyMsg)+        Just (SomeMsg msg) -> runOperate evns' (f msg)

@@ -0,0 +1,83 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# OPTIONS_GHC -Wno-unused-do-bind #-}++{- | Running FSM++The core function is `runOp`, and the other functions are to make it work properly.+-}+module TypedFsm.Driver.Op where++import Control.Monad.State as S (MonadState (get), StateT)+import Data.Dependent.Map (DMap)+import Data.Dependent.Map qualified as D+import Data.GADT.Compare (GCompare, GOrdering (..))+import Data.IFunctor (At (..))+import Data.Ord.Singletons (SOrd (sCompare), SOrdering (..))+import Data.Singletons (Sing, SingI (..), SomeSing (..))+import TypedFsm.Core (Operate (..))+import TypedFsm.Driver.Common+import Unsafe.Coerce (unsafeCoerce)++{- | `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`.+-}+type Op ps state m a o i = Operate (StateT state m) (At a (o :: ps)) (i :: ps)++type SomeOp ps state m a = SomeOperate ps (StateT state m) a++newtype GenMsg ps state event from+  = GenMsg (state -> event -> Maybe (SomeMsg ps from))++type State2GenMsg ps state event = DMap (Sing @ps) (GenMsg ps state event)++sOrdToGCompare+  :: forall n (a :: n) (b :: n)+   . (SOrd n)+  => Sing a -> Sing b -> GOrdering a b+sOrdToGCompare a b = case sCompare a b of+  SEQ -> unsafeCoerce GEQ+  SLT -> GLT+  SGT -> GGT++newtype NotFoundGenMsg ps = NotFoundGenMsg (SomeSing ps)++runOp+  :: forall ps event state m a (input :: ps) (output :: ps)+   . ( SingI input+     , GCompare (Sing @ps)+     )+  => (Monad m)+  => State2GenMsg ps state event+  -> [event]+  -> Operate (StateT state m) (At a output) input+  -> (StateT state m) (Result ps (NotFoundGenMsg ps) (StateT state m) a)+runOp dmp evns = \case+  IReturn (At a) -> pure (Finish a)+  LiftM m -> m >>= runOp dmp evns+  In f -> do+    let singInput = sing @input+    case D.lookup singInput dmp of+      Nothing -> pure (ErrorInfo $ NotFoundGenMsg $ SomeSing singInput)+      Just (GenMsg genMsg) -> loop evns+       where+        loop [] = pure $ Cont $ SomeOperate (In f)+        loop (et : evns') = do+          state' <- get+          case genMsg state' et of+            Nothing -> loop evns'+            Just (SomeMsg msg) -> runOp dmp evns' (f msg)

@@ -20,7 +20,7 @@ -- PVP summary:     +-+------- breaking API changes --                  | | +----- non-breaking API additions --                  | | | +--- code changes with no API change-version:            0.1.0.1+version:            0.2.0.0  -- A short (one-line) description of the package. synopsis: A framework for strongly typed FSM@@ -70,7 +70,9 @@     -- Modules exported by the library.     exposed-modules: TypedFsm                    , TypedFsm.Core-                   , TypedFsm.Driver+                   , TypedFsm.Driver.Common+                   , TypedFsm.Driver.Op+                   , TypedFsm.Driver.General                    , Data.IFunctor      -- Modules included in this library but not exported.