packages feed

typed-fsm 0.2.0.1 → 0.3.0.0

raw patch · 6 files changed

+41/−40 lines, 6 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

- TypedFsm.Core: [LiftM] :: forall {ps} (c :: ps) (mode' :: ps) (a :: Type -> Type) (b :: ps -> Type). (SingI c, SingI mode') => a (Operate a b mode') -> Operate a b c
+ TypedFsm.Core: [LiftM] :: forall {ps} (mode' :: ps) (a :: Type -> Type) (b :: ps -> Type) (c :: ps). Sing mode' -> a (Operate a b mode') -> Operate a b c
- TypedFsm.Driver.Common: AnyMsg :: Msg ps from to -> AnyMsg ps
+ TypedFsm.Driver.Common: AnyMsg :: Sing from -> Sing to -> Msg ps from to -> AnyMsg ps
- TypedFsm.Driver.Common: SomeMsg :: Msg ps from to -> SomeMsg ps (from :: ps)
+ TypedFsm.Driver.Common: SomeMsg :: Sing to -> Msg ps from to -> SomeMsg ps (from :: ps)
- TypedFsm.Driver.Common: SomeOperate :: Operate m (At a o) i -> SomeOperate ts (m :: Type -> Type) a
+ TypedFsm.Driver.Common: SomeOperate :: Sing i -> Operate m (At a o) i -> SomeOperate ts (m :: Type -> Type) a
- TypedFsm.Driver.General: anyToSomeMsg :: forall ps (input :: ps). (SingI input, SEq ps) => AnyMsg ps -> Maybe (SomeMsg ps input)
+ TypedFsm.Driver.General: anyToSomeMsg :: forall ps (input :: ps). SEq ps => Sing input -> AnyMsg ps -> Maybe (SomeMsg ps input)
- TypedFsm.Driver.General: runOperate :: forall ps m a (input :: ps) (output :: ps). (Monad m, SingI input, SEq ps) => UnexpectMsgHandler ps m -> [AnyMsg ps] -> Operate m (At a output) input -> m (Result ps (UnexpectMsg ps) m a)
+ TypedFsm.Driver.General: runOperate :: forall ps m a (input :: ps) (output :: ps). (Monad m, SEq ps) => UnexpectMsgHandler ps m -> [AnyMsg ps] -> Sing input -> Operate m (At a output) input -> m (Result ps (UnexpectMsg ps) m a)
- TypedFsm.Driver.Op: 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 (NotFoundGenMsg ps) (StateT state m) a)
+ TypedFsm.Driver.Op: runOp :: forall ps event state (m :: Type -> Type) a (input :: ps) (output :: ps). (GCompare (Sing :: ps -> Type), Monad m) => State2GenMsg ps state event -> [event] -> Sing input -> Operate (StateT state m) (At a output) input -> StateT state m (Result ps (NotFoundGenMsg ps) (StateT state m) a)

Files

CHANGELOG.md view
@@ -1,5 +1,11 @@ # Revision history for typed-fsm +## 0.3.0.0-- 2024-7-25+* Remove the SingI constraints from SomeMsg and AnyMsg.+* Modify the definition of LiftM and remove the SingI constraints.+* RunOperate and runOp both remove the SingI constraints.+* Reason for doing this: When explaining Ast, constraints can be easily converted into proofs, but proofs seem difficult to convert into constraints.+ ## 0.2.0.1-- 2024-7-22  * Fix getSomeOperateSing
src/TypedFsm/Core.hs view
@@ -12,7 +12,7 @@  )  import Data.Kind (Type)-import Data.Singletons (SingI)+import Data.Singletons (Sing, SingI (..))  -- | The state-transition type class class StateTransMsg ps where@@ -33,8 +33,8 @@ data Operate :: (Type -> Type) -> (ps -> Type) -> ps -> Type where   IReturn :: ia (mode :: ps) -> Operate m ia mode   LiftM-    :: (SingI mode, SingI mode')-    => m (Operate m ia mode')+    :: Sing mode'+    -> m (Operate m ia mode')     -> Operate m ia mode   In     :: forall ps m (from :: ps) ia@@ -44,13 +44,13 @@ instance (Functor m) => IFunctor (Operate m) where   imap f = \case     IReturn ia -> IReturn (f ia)-    LiftM f' -> LiftM (fmap (imap f) f')+    LiftM s f' -> LiftM s (fmap (imap f) f')     In cont -> In (imap f . cont) instance (Functor m) => IMonad (Operate m) where   ireturn = IReturn   ibind f = \case     IReturn ia -> (f ia)-    LiftM m -> LiftM (fmap (ibind f) m)+    LiftM s m -> LiftM s (fmap (ibind f) m)     In cont -> In (ibind f . cont)  -- | get messages from outside@@ -59,4 +59,4 @@  -- | lifts the internal `m a` to `Operate m (At a i) i' liftm :: forall ps m (mode :: ps) a. (Functor m, SingI mode) => m a -> Operate m (At a mode) mode-liftm m = LiftM (returnAt <$> m)+liftm m = LiftM sing (returnAt <$> m)
src/TypedFsm/Driver/Common.hs view
@@ -7,31 +7,28 @@ module TypedFsm.Driver.Common where  import Data.IFunctor (At (..))-import Data.Singletons (Sing, SingI (..), SingKind (..))+import Data.Singletons (Sing, 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)+    SomeOperate (Sing i) (Operate m (At a o) i)  getSomeOperateSing :: (SingKind ts) => SomeOperate ts m a -> Sing (r :: ts)-getSomeOperateSing (SomeOperate (_ :: Operate m ia i)) =-  unsafeCoerce $ sing @i+getSomeOperateSing (SomeOperate si (_ :: Operate m ia i)) =+  unsafeCoerce si  getSomeOperateSt :: (SingKind ts) => SomeOperate ts m a -> Demote ts-getSomeOperateSt (SomeOperate (_ :: Operate m ia i)) = fromSing $ sing @i+getSomeOperateSt (SomeOperate si (_ :: Operate m ia i)) = fromSing $ si  data SomeMsg ps from   = forall (to :: ps).-    (SingI to) =>-    SomeMsg (Msg ps from to)+    SomeMsg (Sing to) (Msg ps from to)  data AnyMsg ps   = forall (from :: ps) (to :: ps).-    (SingI from, SingI to) =>-    AnyMsg (Msg ps from to)+    AnyMsg (Sing from) (Sing to) (Msg ps from to)  {- | Reuslt of run FSM
src/TypedFsm/Driver/General.hs view
@@ -10,20 +10,20 @@ import Data.Bool.Singletons (SBool (..)) import Data.Eq.Singletons (SEq (..)) import Data.IFunctor (At (..))-import Data.Singletons (SingI (..))+import Data.Singletons (Sing) 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+   . (SEq ps)+  => Sing input -> AnyMsg ps -> Maybe (SomeMsg ps input)+anyToSomeMsg sinput (AnyMsg sfrom sto (msg :: Msg ps from to)) =+  case sfrom %== sinput of     -- (from == input) ~ True     -- ==> from ~ input-    STrue -> unsafeCoerce (Just (SomeMsg msg))+    STrue -> unsafeCoerce (Just (SomeMsg sto msg))     SFalse -> Nothing  newtype UnexpectMsg ps = UnexpectMsg (AnyMsg ps)@@ -36,23 +36,23 @@ runOperate   :: forall ps m a (input :: ps) (output :: ps)    . ( Monad m-     , SingI input      , SEq ps      )   => UnexpectMsgHandler ps m   -> [AnyMsg ps]+  -> Sing input   -> Operate m (At a output) input   -> m (Result ps (UnexpectMsg ps) m a)-runOperate unHandler anyMsgs = \case+runOperate unHandler anyMsgs sinput = \case   IReturn (At a) -> pure (Finish a)-  LiftM m -> m >>= (runOperate unHandler anyMsgs)+  LiftM singv m -> m >>= (runOperate unHandler anyMsgs singv)   In f -> loop anyMsgs    where-    loop [] = pure $ Cont $ SomeOperate (In f)+    loop [] = pure $ Cont $ SomeOperate sinput (In f)     loop (anyMsg : evns') = do-      case anyToSomeMsg @_ @input anyMsg of+      case anyToSomeMsg sinput anyMsg of         Nothing -> case unHandler of           Ignore -> loop evns'           IgnoreAndTrace trace -> trace anyMsg >> loop evns'           Terminal -> pure (ErrorInfo $ UnexpectMsg anyMsg)-        Just (SomeMsg msg) -> runOperate unHandler evns' (f msg)+        Just (SomeMsg sto msg) -> runOperate unHandler evns' sto (f msg)
src/TypedFsm/Driver/Op.hs view
@@ -16,7 +16,7 @@ import Data.GADT.Compare (GCompare, GOrdering (..)) import Data.IFunctor (At (..)) import Data.Ord.Singletons (SOrd (sCompare), SOrdering (..))-import Data.Singletons (Sing, SingI (..), SomeSing (..))+import Data.Singletons (Sing, SomeSing (..)) import TypedFsm.Core (Operate (..)) import TypedFsm.Driver.Common import Unsafe.Coerce (unsafeCoerce)@@ -58,26 +58,24 @@  runOp   :: forall ps event state m a (input :: ps) (output :: ps)-   . ( SingI input-     , GCompare (Sing @ps)-     )+   . (GCompare (Sing @ps))   => (Monad m)   => State2GenMsg ps state event   -> [event]+  -> Sing input   -> Operate (StateT state m) (At a output) input   -> (StateT state m) (Result ps (NotFoundGenMsg ps) (StateT state m) a)-runOp dmp evns = \case+runOp dmp evns sinput = \case   IReturn (At a) -> pure (Finish a)-  LiftM m -> m >>= runOp dmp evns+  LiftM sinput' m -> m >>= runOp dmp evns sinput'   In f -> do-    let singInput = sing @input-    case D.lookup singInput dmp of-      Nothing -> pure (ErrorInfo $ NotFoundGenMsg $ SomeSing singInput)+    case D.lookup sinput dmp of+      Nothing -> pure (ErrorInfo $ NotFoundGenMsg $ SomeSing sinput)       Just (GenMsg genMsg) -> loop evns        where-        loop [] = pure $ Cont $ SomeOperate (In f)+        loop [] = pure $ Cont $ SomeOperate sinput (In f)         loop (et : evns') = do           state' <- get           case genMsg state' et of             Nothing -> loop evns'-            Just (SomeMsg msg) -> runOp dmp evns' (f msg)+            Just (SomeMsg sto msg) -> runOp dmp evns' sto (f msg)
typed-fsm.cabal view
@@ -20,7 +20,7 @@ -- PVP summary:     +-+------- breaking API changes --                  | | +----- non-breaking API additions --                  | | | +--- code changes with no API change-version:            0.2.0.1+version:            0.3.0.0  -- A short (one-line) description of the package. synopsis: A framework for strongly typed FSM