packages feed

typed-fsm (empty) → 0.1.0.0

raw patch · 18 files changed

+1477/−0 lines, 18 filesdep +basedep +containersdep +dependent-map

Dependencies added: base, containers, dependent-map, dependent-sum, linear, microlens, microlens-mtl, microlens-th, mtl, sdl2, sdl2-ttf, singletons-base, stm, typed-fsm, unordered-containers

Files

+ CHANGELOG.md view
@@ -0,0 +1,5 @@+# Revision history for typed-fsm++## 0.1.0.0 -- YYYY-mm-dd++* First version. Released on an unsuspecting world.
+ LICENSE view
@@ -0,0 +1,21 @@+MIT License++Copyright (c) 2024 Yang Miao++Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in all+copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE+SOFTWARE.
+ examples/ATM/EventToMsg.hs view
@@ -0,0 +1,57 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE ViewPatterns #-}++module EventToMsg where++import Data.Data (Proxy (..))+import qualified Data.Dependent.Map as D+import Data.Dependent.Sum+import Data.Singletons (SingI)+import Lens.Micro+import Type+import TypedFsm.Driver+import Utils++scEventHandler+  :: (SingI n, Less3 n)+  => Proxy n+  -> GenMsg ATMSt InternalState MyEvent (CardInserted n)+scEventHandler _ =+  GenMsg+    ( \ist event -> case event of+        MyMouseLeftButtonClick (fmap fromIntegral -> p) ->+          if+            | (ist ^. ejectLabel . rect) `contains` p -> Just (SomeMsg CIEject)+            | (ist ^. checkPinLabel . rect) `contains` p -> Just (SomeMsg (CheckPIN 1234))+            | (ist ^. checkPinErrorLabel . rect) `contains` p -> Just (SomeMsg (CheckPIN 1))+            | otherwise -> Nothing+    )++atmDepMap :: State2GenMsg ATMSt InternalState MyEvent+atmDepMap =+  D.fromList+    [ SReady+        :=> GenMsg+          ( \ist event -> case event of+              MyMouseLeftButtonClick (fmap fromIntegral -> p) ->+                ( if+                    | (ist ^. insCardLabel . rect) `contains` p -> Just (SomeMsg InsertCard)+                    | (ist ^. exitLabel . rect) `contains` p -> Just (SomeMsg ExitATM)+                    | otherwise -> Nothing+                )+          )+    , SCardInserted SZ :=> scEventHandler Proxy+    , SCardInserted (SS SZ) :=> scEventHandler Proxy+    , SCardInserted (SS (SS SZ)) :=> scEventHandler Proxy+    , SSession+        :=> GenMsg+          ( \ist event -> case event of+              MyMouseLeftButtonClick (fmap fromIntegral -> p) ->+                if+                  | (ist ^. ejectLabel . rect) `contains` p -> Just (SomeMsg SEject)+                  | (ist ^. getAmountLabel . rect) `contains` p -> Just (SomeMsg GetAmount)+                  | (ist ^. dispenseLabel . rect) `contains` p -> Just (SomeMsg (Dispense 100))+                  | otherwise -> Nothing+          )+    ]
+ examples/ATM/Handler.hs view
@@ -0,0 +1,92 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}++module Handler where++import Control.Monad.State+import Data.IFunctor (At (..), IMonad (..), returnAt)+import qualified Data.IFunctor as I+import Data.Singletons (SingI (sing))+import Lens.Micro.Mtl (use, (-=), (.=))+import Type+import TypedFsm.Core+import TypedFsm.Driver++checkResult+  :: forall n+   . (SingI n, Less3 n)+  => Int+  -> Operate (StateT InternalState IO) CheckPINResult (CheckPin n)+checkResult i = I.do+  At userPin <- liftm $ use pin+  if i == userPin+    then LiftM $ pure (ireturn Correct)+    else LiftM $ pure (ireturn (Incorrect @n))++checkPinFun+  :: forall (n :: N)+   . (SingI n)+  => Int+  -> Operate (StateT InternalState IO) CheckPINResult (CheckPin (n :: N))+checkPinFun i = I.do+  case sing @n of+    SS SZ -> checkResult i+    SS (SS SZ) -> checkResult i+    sn@(SS (SS (SS SZ))) -> I.do+      At userPin <- liftm $ use pin+      if i == userPin+        then LiftM $ pure (ireturn Correct)+        else LiftM $ do+          liftIO $ putStrLn "-> test 3 times, eject card!"+          pure (ireturn (EjectCard sn))+    _ -> error "np"++readyHandler :: Op ATMSt InternalState IO () Exit Ready+readyHandler = I.do+  msg <- getInput+  case msg of+    InsertCard -> cardInsertedHandler+    ExitATM -> returnAt ()++cardInsertedHandler+  :: (SingI n)+  => Op ATMSt InternalState IO () Exit (CardInserted n)+cardInsertedHandler = I.do+  msg <- getInput+  case msg of+    CIEject -> I.do+      readyHandler+    CheckPIN i -> I.do+      res <- checkPinFun i+      case res of+        EjectCard _ -> readyHandler+        Incorrect -> cardInsertedHandler+        Correct -> I.do+          liftm $ amountLabel . label .= ("Amount: -- ")+          sessionHandler++sessionHandler :: Op ATMSt InternalState IO () Exit Session+sessionHandler = I.do+  msg <- getInput+  case msg of+    GetAmount -> I.do+      liftm $ do+        am <- use amount+        amountLabel . label .= ("Amount: " <> show am)+        liftIO $ putStrLn ("-> User Amount: " <> show am)+      sessionHandler+    Dispense i -> I.do+      liftm $ do+        amount -= i -- need to check amount is enough?+        liftIO $ putStrLn ("-> Use dispense " ++ show i)+        am <- use amount+        amountLabel . label .= ("Now Amount: " <> show am)+        liftIO $ putStrLn ("-> Now User Amount: " <> show am)+      sessionHandler+    SEject -> readyHandler
+ examples/ATM/Main.hs view
@@ -0,0 +1,79 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}+{-# OPTIONS_GHC -Wno-unused-do-bind #-}++module Main where++import Control.Concurrent (threadDelay)+import Control.Monad.IO.Class (liftIO)+import Control.Monad.State (StateT (runStateT))+import qualified Control.Monad.State as M+import EventToMsg+import Handler+import Lens.Micro ((^.))+import SDL+import qualified SDL.Font as Font+import Type+import TypedFsm.Driver+import Utils++main :: IO ()+main = do+  initialize [InitVideo]+  Font.initialize+  font <- Font.load "data/fonts/SourceCodePro-Regular.otf" 20+  window <- createWindow "test" defaultWindow+  renderer <- createRenderer window (-1) defaultRenderer+  ccref <- initCharCache++  runStateT+    (appLoop (DrawEnv renderer font ccref) (SomeOperate readyHandler))+    initInternState+  destroyWindow window++appLoop :: DrawEnv -> SomeOp ATMSt InternalState IO () -> StateT InternalState IO ()+appLoop de@(DrawEnv renderer _font _ccref) (SomeOperate fun) = do+  events <- pollEvents+  -- liftIO $ print events+  v <- runOp atmDepMap (makeMyEvent events) fun+  case v of+    Finish _ -> pure ()+    NotMatchGenMsg si -> liftIO $ putStrLn $ "error: not match GenMsg " ++ show si+    Cont fun1 -> do+      let atmSt = getSomeOperateSt fun1+      rendererDrawColor renderer $= V4 0 0 0 255+      clear renderer++      rendererDrawColor renderer $= V4 255 0 155 255+      liftIO $ drawStrings de [show atmSt] (10, 30)++      ist <- M.get+      case atmSt of+        Ready -> do+          liftIO $ drawLabel de (ist ^. insCardLabel)+          liftIO $ drawLabel de (ist ^. exitLabel)+        CardInserted _n -> do+          liftIO $ drawLabel de (ist ^. checkPinLabel)+          liftIO $ drawLabel de (ist ^. checkPinErrorLabel)+          liftIO $ drawLabel de (ist ^. ejectLabel)+        Session -> do+          liftIO $ drawLabel de (ist ^. amountLabel)+          liftIO $ drawLabel de (ist ^. getAmountLabel)+          liftIO $ drawLabel de (ist ^. dispenseLabel)+          liftIO $ drawLabel de (ist ^. ejectLabel)+        CheckPin _n -> pure ()+        Exit -> pure ()++      present renderer+      liftIO $ threadDelay (1000000 `div` 30)+      appLoop de fun1
+ examples/ATM/Type.hs view
@@ -0,0 +1,144 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wall #-}++module Type where++import Data.GADT.Compare (GCompare (..), GEq (..))+import Data.Int (Int32)+import Data.Kind (Constraint, Type)+import Data.Singletons.Base.TH+import Data.Type.Equality (TestEquality (testEquality))+import GHC.TypeError (TypeError)+import GHC.TypeLits (ErrorMessage (..))+import Lens.Micro.TH (makeLenses)+import SDL+import TypedFsm.Core (StateTransMsg (..))+import TypedFsm.Driver (sOrdToGCompare)++$( singletons+    [d|+      data N = Z | S N+        deriving (Show, Eq, Ord)++      data ATMSt+        = Ready+        | CardInserted N+        | CheckPin N+        | Session+        | Exit+        deriving (Show, Eq, Ord)+      |]+ )++satmToatm :: SATMSt s -> ATMSt+satmToatm = fromSing++instance GEq SN where+  geq = testEquality++instance GEq SATMSt where+  geq = testEquality++instance GCompare SN where+  gcompare = sOrdToGCompare++instance GCompare SATMSt where+  gcompare = sOrdToGCompare++type family Less3 (n :: N) :: Constraint where+  Less3 Z = ()+  Less3 (S Z) = ()+  Less3 (S (S Z)) = ()+  Less3 _ = TypeError (Text "test must less 3")++data CheckPINResult :: ATMSt -> Type where+  EjectCard :: (n ~ S (S (S Z))) => SN n -> CheckPINResult Ready+  Incorrect :: (SingI n, Less3 n) => CheckPINResult (CardInserted n)+  Correct :: CheckPINResult Session++instance StateTransMsg ATMSt where+  data Msg ATMSt from to where+    ExitATM :: Msg ATMSt Ready Exit+    InsertCard :: Msg ATMSt Ready (CardInserted Z)+    CIEject :: Msg ATMSt (CardInserted n) Ready+    ---------------+    CheckPIN :: Int -> Msg ATMSt (CardInserted n) (CheckPin (S n))+    ---------------+    GetAmount :: Msg ATMSt Session Session+    Dispense :: Int -> Msg ATMSt Session Session+    SEject :: Msg ATMSt Session Ready++----------------------------------+type Point' = Point V2 Int++pattern Point :: a -> a -> Point V2 a+pattern Point x y = P (V2 x y)+{-# COMPLETE Point #-}++newtype MyEvent = MyMouseLeftButtonClick (Point V2 Int32)+  deriving (Show, Eq, Ord)++data Rect = Rect+  { _rx :: Int+  , _ry :: Int+  , _width :: Int+  , _height :: Int+  }+  deriving (Show)++data Label = Label+  { _rect :: Rect+  , _label :: String+  }+  deriving (Show)++----------------------------------++data InternalState = InternalState+  { _pin :: Int+  , _amount :: Int+  , _amountLabel :: Label+  , _insCardLabel :: Label+  , _exitLabel :: Label+  , _checkPinLabel :: Label+  , _checkPinErrorLabel :: Label+  , _getAmountLabel :: Label+  , _dispenseLabel :: Label+  , _ejectLabel :: Label+  }+  deriving (Show)++initInternState :: InternalState+initInternState =+  InternalState+    { _pin = 1234+    , _amount = 1000+    , _amountLabel = Label (Rect 10 130 100 30) "null"+    , _insCardLabel = (Label (Rect 10 230 100 30) "Insert Card")+    , _exitLabel = (Label (Rect 10 270 100 30) "EXIT")+    , _checkPinLabel = (Label (Rect 10 230 100 30) "checkPin 1234")+    , _checkPinErrorLabel = (Label (Rect 10 274 100 30) "checkPin 1 error")+    , _getAmountLabel = (Label (Rect 10 230 100 30) "GetAmount")+    , _dispenseLabel = (Label (Rect 130 230 100 30) "Dispense 100")+    , _ejectLabel = (Label (Rect 10 330 100 30) "Eject")+    }++Lens.Micro.TH.makeLenses ''Rect+Lens.Micro.TH.makeLenses ''Label+Lens.Micro.TH.makeLenses ''InternalState
+ examples/ATM/Utils.hs view
@@ -0,0 +1,91 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE QualifiedDo #-}++module Utils where++import Control.Monad+import Data.HashMap.Strict (HashMap)+import qualified Data.HashMap.Strict as H+import Data.IORef+import Linear+import SDL+import SDL.Font (Font)+import qualified SDL.Font as Font+import Type++type CharCache = HashMap Char Texture+type CharCacheRef = IORef CharCache++data DrawEnv = DrawEnv+  { _renderer :: Renderer+  , _font :: Font+  , _charCacheRef :: CharCacheRef+  }++eventToKP :: Event -> Maybe MyEvent+eventToKP e = case eventPayload e of+  MouseButtonEvent (MouseButtonEventData _ Pressed _ _ _ pos) ->+    Just $ MyMouseLeftButtonClick pos+  _ -> Nothing++makeMyEvent :: [Event] -> [MyEvent]+makeMyEvent events =+  let fun b a =+        case eventToKP a of+          Nothing -> b+          Just a' -> a' : b+   in reverse (foldl' fun [] events)++pattern KBE+  :: InputMotion+  -> Keycode+  -> Bool+  -> Maybe Window+  -> Scancode+  -> KeyModifier+  -> EventPayload+pattern KBE press keycode repeat a d f =+  KeyboardEvent+    (KeyboardEventData a press repeat (Keysym d keycode f))++initCharCache :: IO CharCacheRef+initCharCache = newIORef H.empty++getCharTexure :: Renderer -> Font -> CharCacheRef -> Char -> IO Texture+getCharTexure r font cref c = do+  cc <- readIORef cref+  case H.lookup c cc of+    Nothing -> do+      surf <- Font.blendedGlyph font (V4 0 255 0 255) c+      text <- createTextureFromSurface r surf+      freeSurface surf+      modifyIORef' cref (H.insert c text)+      pure text+    Just t -> pure t++drawString :: DrawEnv -> String -> (Int, Int) -> IO ()+drawString (DrawEnv r font cref) st (x', y') = do+  let go _ _ [] = pure ()+      go x y (t : ts) = do+        TextureInfo _ _ w h <- queryTexture t+        copy r t Nothing (Just (Rectangle (P (V2 x y)) (V2 w h)))+        go (x + w) y ts+  txts <- mapM (getCharTexure r font cref) st+  go (fromIntegral x') (fromIntegral y') txts++drawStrings :: DrawEnv -> [String] -> (Int, Int) -> IO ()+drawStrings de sts (x, y) = do+  forM_ (zip [0 ..] sts) $ \(i, st) -> do+    drawString de st (x, y + i * 20)++drawLabel :: DrawEnv -> Label -> IO ()+drawLabel de@(DrawEnv{_renderer}) (Label (Rect x y w h) st) = do+  drawRect _renderer (Just (Rectangle (P (V2 (fromIntegral x) (fromIntegral y))) (V2 (fromIntegral w) (fromIntegral h))))+  drawString de st (x, y)++contains :: Rect -> Point' -> Bool+contains (Rect rx1 ry1 w h) (Point x y) =+  (rx1 <= x && x <= rx1 + w) && (ry1 <= y && y <= ry1 + h)
+ examples/motion/EventToMsg.hs view
@@ -0,0 +1,48 @@+{-# LANGUAGE ViewPatterns #-}++module EventToMsg where++import qualified Data.Dependent.Map as D+import Data.Dependent.Sum+import Type+import TypedFsm.Driver+import Utils++mouseDepMap :: State2GenMsg Motion MotionState MyEvent+mouseDepMap =+  D.fromList+    [ SIdle+        :=> GenMsg+          ( \(MotionState rect' _ _ _) event -> case event of+              MyQuit -> Just (SomeMsg ExitMotion)+              MyMouseMotion (fmap fromIntegral -> p) tms ->+                if rect' `contains` p+                  then Just $ SomeMsg (MoveIn p tms)+                  else Nothing+              _ -> Nothing+          )+    , SOver+        :=> GenMsg+          ( \(MotionState rect' _ _ _) event -> case event of+              MyQuit -> Just (SomeMsg ExitMotion)+              MyMouseMotion (fmap fromIntegral -> p) tms ->+                if rect' `contains` p+                  then Just $ SomeMsg (InMove p tms)+                  else Just $ SomeMsg MoveOut+              MyTimeout -> Just $ SomeMsg TimeoutH+          )+    , SHover+        :=> GenMsg+          ( \(MotionState rect' _ (Point mx my) _) event -> case event of+              MyQuit -> Just (SomeMsg ExitMotion)+              MyMouseMotion (fmap fromIntegral -> p@(Point x y)) tms ->+                if rect' `contains` p+                  then+                    if abs (mx - x) < 30 && abs (my - y) < 30+                      then Nothing+                      else+                        Just $ SomeMsg (HInMove p tms)+                  else Just $ SomeMsg HMoveOut+              _ -> Nothing+          )+    ]
+ examples/motion/Handler.hs view
@@ -0,0 +1,82 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE NumericUnderscores #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE TypeFamilies #-}+{-# OPTIONS_GHC -Wall #-}++module Handler where++import Control.Concurrent.STM (atomically)+import Control.Concurrent.STM.TChan+import Control.Monad.State+import Data.IFunctor (At (..), returnAt)+import qualified Data.IFunctor as I+import GHC.Event+import Lens.Micro.Mtl+import SDL+import Type+import TypedFsm.Core+import TypedFsm.Driver++timeoutSize :: Int+timeoutSize = 400_000++myRegisterTimeout :: StateT MotionState IO (TimerManager, TimeoutKey)+myRegisterTimeout = do+  chan <- use channel+  liftIO $ do+    tm <- getSystemTimerManager+    tk <- registerTimeout tm timeoutSize (atomically $ writeTChan chan ())+    pure (tm, tk)++idelHandler :: Op Motion MotionState IO () Exit Idle+idelHandler = I.do+  msg <- getInput+  case msg of+    ExitMotion -> returnAt ()+    MoveIn pos tms -> I.do+      At tp <- liftm $ do+        mousePos .= pos+        (tm, tk) <- myRegisterTimeout+        pure (tm, tk, tms)+      overHandler tp++overHandler :: (TimerManager, TimeoutKey, Timestamp) -> Op Motion MotionState IO () Exit Over+overHandler (tm, tk, oldtms) = I.do+  msg <- getInput+  case msg of+    ExitMotion -> returnAt ()+    MoveOut -> I.do+      liftm $ liftIO $ unregisterTimeout tm tk+      idelHandler+    InMove pos tms -> I.do+      liftm $ do+        mousePos .= pos+      if tms - oldtms > 40+        then I.do+          liftm $ liftIO $ updateTimeout tm tk timeoutSize+          overHandler (tm, tk, tms)+        else overHandler (tm, tk, oldtms)+    TimeoutH -> I.do+      liftm $ do+        liftIO $ unregisterTimeout tm tk+        pos <- use mousePos+        onHover .= Just (pos, [show oldtms, show pos])+      hoverHandler++hoverHandler :: Op Motion MotionState IO () Exit Hover+hoverHandler = I.do+  msg <- getInput+  case msg of+    ExitMotion -> returnAt ()+    HInMove pos tms -> I.do+      At tp <- liftm $ do+        mousePos .= pos+        onHover .= Nothing+        (tm, tk) <- myRegisterTimeout+        pure (tm, tk, tms)+      overHandler tp+    HMoveOut -> I.do+      liftm $ onHover .= Nothing+      idelHandler
+ examples/motion/Main.hs view
@@ -0,0 +1,85 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# OPTIONS_GHC -Wno-unused-do-bind #-}++module Main where++import Control.Concurrent (threadDelay)+import Control.Concurrent.STM (atomically)+import Control.Concurrent.STM.TChan+import Control.Monad.IO.Class (liftIO)+import Control.Monad.State (StateT (runStateT))+import qualified Control.Monad.State as M+import EventToMsg+import Handler+import SDL+import qualified SDL.Font as Font+import Type+import TypedFsm.Driver+import Utils++main :: IO ()+main = do+  initialize [InitVideo]+  Font.initialize+  font <- Font.load "data/fonts/SourceCodePro-Regular.otf" 20+  window <- createWindow "test" defaultWindow+  renderer <- createRenderer window (-1) defaultRenderer+  ccref <- initCharCache+  chan <- newTChanIO @()++  runStateT+    (appLoop (DrawEnv renderer font ccref) chan mouseDepMap (SomeOperate idelHandler))+    (MotionState (Rect 100 100 400 400) chan (Point 0 0) Nothing)++  destroyWindow window++creatRect :: (Integral p1, Integral p2, Integral p3, Integral p4, Num a) => p1 -> p2 -> p3 -> p4 -> Rectangle a+creatRect x y w h =+  Rectangle+    (P (V2 (fromIntegral x) (fromIntegral y)))+    (V2 (fromIntegral w) (fromIntegral h))++appLoop+  :: DrawEnv+  -> TChan ()+  -> State2GenMsg Motion MotionState MyEvent+  -> SomeOp Motion MotionState IO ()+  -> StateT MotionState IO ()+appLoop de@(DrawEnv renderer _font _ccref) chan depMap (SomeOperate fun) = do+  events <- pollEvents+  ma <- liftIO (atomically $ tryReadTChan chan)+  v <- runOp depMap (makeMyEvent ma events) fun+  case v of+    Finish _ -> pure ()+    NotMatchGenMsg si -> liftIO $ putStrLn $ "error: not match GenMsg " ++ show si+    Cont fun1 -> do+      rendererDrawColor renderer $= V4 0 0 0 255+      clear renderer++      let motionState = getSomeOperateSt fun1+      liftIO $ drawStrings de [show motionState] (10, 30)++      MotionState (Rect x y w h) _ _ mOnhove <- M.get+      rendererDrawColor renderer $= V4 255 0 155 255+      drawRect renderer $ Just (creatRect x y w h)++      liftIO $+        case mOnhove of+          Nothing -> pure ()+          Just (Point x' y', st) -> do+            rendererDrawColor renderer $= V4 100 155 144 255+            fillRect renderer $ Just (creatRect x' y' (300 :: Int) (-100 :: Int))+            drawStrings de st (fromIntegral x', fromIntegral y' - 60)++      present renderer+      liftIO $ threadDelay (1000000 `div` 30)++      appLoop de chan depMap fun1
+ examples/motion/Type.hs view
@@ -0,0 +1,94 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE NumericUnderscores #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ViewPatterns #-}++module Type where++import Control.Concurrent.STM.TChan+import Data.GADT.Compare (GCompare (..), GEq (..))+import Data.Int (Int32)+import Data.Singletons.Base.TH+import Data.Type.Equality (TestEquality (testEquality))+import Lens.Micro.TH+import SDL+import TypedFsm.Core+import TypedFsm.Driver++$( singletons+    [d|+      data Motion+        = Idle+        | Over+        | Hover+        | Exit+        deriving (Show, Eq, Ord)+      |]+ )++instance GEq SMotion where+  geq = testEquality++instance GCompare SMotion where+  gcompare = sOrdToGCompare++smTom :: SMotion m -> Motion+smTom = fromSing++----------------------------------+type Point' = Point V2 Int++pattern Point :: a -> a -> Point V2 a+pattern Point x y = P (V2 x y)+{-# COMPLETE Point #-}++instance StateTransMsg Motion where+  data Msg Motion from to where+    ExitMotion :: Msg Motion s Exit+    -----------------+    MoveIn :: Point' -> Timestamp -> Msg Motion Idle Over+    -----------------+    MoveOut :: Msg Motion Over Idle+    InMove :: Point' -> Timestamp -> Msg Motion Over Over+    TimeoutH :: Msg Motion Over Hover+    -----------------+    HInMove :: Point' -> Timestamp -> Msg Motion Hover Over+    HMoveOut :: Msg Motion Hover Idle++data Rect = Rect+  { _rx :: Int+  , _ry :: Int+  , _width :: Int+  , _height :: Int+  }+  deriving (Show)++data MotionState = MotionState+  { _rect :: Rect+  , _channel :: TChan ()+  , _mousePos :: Point'+  , _onHover :: Maybe (Point', [String])+  }++data MyEvent+  = MyMouseMotion (Point V2 Int32) Timestamp+  | MyTimeout+  | MyQuit+  deriving (Show, Eq, Ord)++----------------------------------++makeLenses ''MotionState
+ examples/motion/Utils.hs view
@@ -0,0 +1,91 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE QualifiedDo #-}++module Utils where++import Control.Monad+import Data.HashMap.Strict (HashMap)+import qualified Data.HashMap.Strict as H+import Data.IORef+import Linear+import SDL+import SDL.Font (Font)+import qualified SDL.Font as Font+import Type++type CharCache = HashMap Char Texture+type CharCacheRef = IORef CharCache++data DrawEnv = DrawEnv+  { _renderer :: Renderer+  , _font :: Font+  , _charCacheRef :: CharCacheRef+  }++eventToKP :: Event -> Maybe MyEvent+eventToKP e = case eventPayload e of+  QuitEvent -> Just MyQuit+  KBE Pressed KeycodeQ _ _ _ _ -> Just MyQuit+  KBE Pressed KeycodeEscape _ _ _ _ -> Just MyQuit+  MouseMotionEvent (MouseMotionEventData _ _ _ pos _) ->+    Just $ MyMouseMotion pos (eventTimestamp e)+  _ -> Nothing++makeMyEvent :: Maybe () -> [Event] -> [MyEvent]+makeMyEvent ma events =+  let fun b a =+        case eventToKP a of+          Nothing -> b+          Just a' -> a' : b+      res = reverse (foldl' fun [] events)+   in case ma of+        Nothing -> res+        Just _ -> MyTimeout : res++pattern KBE+  :: InputMotion+  -> Keycode+  -> Bool+  -> Maybe Window+  -> Scancode+  -> KeyModifier+  -> EventPayload+pattern KBE press keycode repeat a d f =+  KeyboardEvent+    (KeyboardEventData a press repeat (Keysym d keycode f))++initCharCache :: IO CharCacheRef+initCharCache = newIORef H.empty++getCharTexure :: Renderer -> Font -> CharCacheRef -> Char -> IO Texture+getCharTexure r font cref c = do+  cc <- readIORef cref+  case H.lookup c cc of+    Nothing -> do+      surf <- Font.blendedGlyph font (V4 0 255 0 255) c+      text <- createTextureFromSurface r surf+      freeSurface surf+      modifyIORef' cref (H.insert c text)+      pure text+    Just t -> pure t++drawString :: DrawEnv -> String -> (Int, Int) -> IO ()+drawString (DrawEnv r font cref) st (x', y') = do+  let go _ _ [] = pure ()+      go x y (t : ts) = do+        TextureInfo _ _ w h <- queryTexture t+        copy r t Nothing (Just (Rectangle (P (V2 x y)) (V2 w h)))+        go (x + w) y ts+  txts <- mapM (getCharTexure r font cref) st+  go (fromIntegral x') (fromIntegral y') txts++drawStrings :: DrawEnv -> [String] -> (Int, Int) -> IO ()+drawStrings de sts (x, y) = do+  forM_ (zip [0 ..] sts) $ \(i, st) -> do+    drawString de st (x, y + i * 20)++contains :: Rect -> Point' -> Bool+contains (Rect rx ry w h) (Point x y) =+  (rx <= x && x <= rx + w) && (ry <= y && y <= ry + h)
+ examples/turnstile/Main.hs view
@@ -0,0 +1,104 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_GHC -Wno-unused-do-bind #-}++module Main where++import Control.Monad (void)+import Control.Monad.State+import qualified Data.Dependent.Map as D+import Data.Dependent.Sum+import Data.GADT.Compare (GCompare (..), GEq (..))+import Data.IFunctor as I+import Data.Singletons.Base.TH+import Data.Type.Equality (TestEquality (testEquality))+import TypedFsm++$(singletons [d|data TurnSt = Locked | Unlocked | Exit deriving (Show, Eq, Ord)|])++instance StateTransMsg TurnSt where+  data Msg TurnSt from to where+    Coin :: Msg TurnSt Locked Unlocked+    Push :: Msg TurnSt Unlocked Locked+    ExitTurnSt :: Msg TurnSt Locked Exit++instance GEq STurnSt where+  geq = testEquality++instance GCompare STurnSt where+  gcompare = sOrdToGCompare++lockedHandler :: Op TurnSt Int IO () Exit Locked+lockedHandler = I.do+  msg <- getInput+  case msg of+    Coin -> I.do+      liftm $ do+        liftIO $ putStrLn "Coin, internal int add one"+        modify' (+ 1)+        v <- get+        liftIO $ putStrLn $ "Now coin: " ++ show v+      unlockedHandler+    ExitTurnSt -> I.do+      liftm $ liftIO $ putStrLn "Exit turnSt"++unlockedHandler :: Op TurnSt Int IO () Exit Unlocked+unlockedHandler = I.do+  msg <- getInput+  case msg of+    Push -> I.do+      liftm $ do+        liftIO $ putStrLn "Push"+      lockedHandler++eventDepMap :: State2GenMsg TurnSt Int String+eventDepMap =+  D.fromList+    [ SLocked+        :=> GenMsg+          ( \_ ev -> case ev of+              "coin" -> Just $ SomeMsg Coin+              "exit" -> Just $ SomeMsg ExitTurnSt+              _ -> Nothing+          )+    , SUnlocked+        :=> GenMsg+          ( \_ ev -> case ev of+              "push" -> Just $ SomeMsg Push+              _ -> Nothing+          )+    ]++loop+  :: Result TurnSt (StateT Int IO) ()+  -> StateT Int IO ()+loop res = do+  case res of+    Finish _ -> liftIO $ putStrLn "Finish"+    NotMatchGenMsg singst -> liftIO $ putStrLn $ "NotMatch GenMSg: " ++ show singst+    Cont sop@(SomeOperate op) -> do+      st <- liftIO $ do+        putStrLn $ "current state: " ++ show (getSomeOperateSt sop)+        putStrLn "input command:"+        getLine+      nres <- runOp eventDepMap [st] op+      loop nres++main :: IO ()+main = do+  putStrLn "start loop"+  void $ runStateT (loop (Cont $ SomeOperate lockedHandler)) 0
+ src/Data/IFunctor.hs view
@@ -0,0 +1,99 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}++{- | Introducing McBride Indexed Monads++Here's Edward Kmett's [introduction to Indexed Monads](https://stackoverflow.com/questions/28690448/what-is-indexed-monad).++As he said, there are at least three indexed monads:+++* Bob Atkey++@+class IMonad m where+  ireturn  ::  a -> m i i a+  ibind    ::  m i j a -> (a -> m j k b) -> m i k b+@++* Conor McBride++@+type a ~> b = forall i. a i -> b i++class IMonad m where+  ireturn :: a ~> m a+  ibind :: (a ~> m b) -> (m a ~> m b)+@++* Dominic Orchard++No detailed description, just a link to this [lecture](https://github.com/dorchard/effect-monad/blob/master/docs/ixmonad-fita14.pdf)。++I use  the McBride Indexed Monad, the earliest paper [here](https://personal.cis.strath.ac.uk/conor.mcbride/Kleisli.pdf).++The following is my understanding of (\~>): through GADT, let the value contain type information,+and then use ((\~>), pattern match) to pass the type to subsequent functions++@+data V = A | B++data SV :: V -> Type where  -- GADT, let the value contain type information+   SA :: SV A+   SB :: SV B++data SV1 :: V -> Type where+   SA1 :: SV1 A+   SB1 :: SV1 B++fun :: SV ~> SV1     -- type f ~> g = forall x. f x -> g x+fun sv = case sv of  -- x is arbitrary but f, g must have the same x+     SA -> SA1       -- Pass concrete type state to subsequent functions via pattern matching+     SB -> SB1+++class (IFunctor m) => IMonad m where+  ireturn :: a ~> m a+  ibind :: (a ~> m b)  -- The type information contained in a will be passed to (m b),+                       -- which is exactly what we need: external input has an impact on the type!+        -> m a ~> m b+@+-}+module Data.IFunctor where++import Data.Data+import Data.Kind++infixr 0 ~>++type f ~> g = forall x. f x -> g x++class IFunctor f where+  imap :: (a ~> b) -> f a ~> f b++class (IFunctor m) => IMonad m where+  ireturn :: a ~> m a+  ibind :: (a ~> m b) -> m a ~> m b++class (IMonad m) => IMonadFail m where+  fail :: String -> m a ix++data At :: Type -> k -> k -> Type where+  At :: a -> At a k k+  deriving (Typeable)++(>>=) :: (IMonad (m :: (x -> Type) -> x -> Type)) => m a ix -> (a ~> m b) -> m b ix+m >>= f = ibind f m++{- | (>>)++Note: (>>) can only be used if the type of left `m` is `m (At a j) i`.+-}+(>>) :: (IMonad (m :: (x -> Type) -> x -> Type)) => m (At a j) i -> m b j -> m b i+m >> f = ibind (\(At _) -> f) m++returnAt :: (IMonad m) => a -> m (At a k) k+returnAt = ireturn . At
+ src/TypedFsm.hs view
@@ -0,0 +1,50 @@+{- | This package defines the typed-fsm framework. This module re-exports+the public API.++FSM stands for [Finite State Machine](https://en.wikipedia.org/wiki/Finite-state_machine).++The typed-fsm is used to define and execute FSM.++Advantages of type-fsm:++* Focus on the right message.+* Top-to-bottom design for easy refactoring.+* Conducive to building complex state machine systems:+** Type guarantees will not produce incorrect function calls when written.+** With the help of the type system, we can define many state processing functions and then call each other recursively with confidence.+* There is a sanity check. If you miss some items for pattern matching, the compiler will issue a warning, and there will also be a warning for invalid items.+++In order to use do syntax, the `QualifiedDo` extension is required.++The QualifiedDo extension allows us to overload only the two operators (>>=) and (>>).++Prior to ghc 9.10.1, this extension had [serious issues](https://gitlab.haskell.org/ghc/ghc/-/issues/21206),+But this [MR](https://gitlab.haskell.org/ghc/ghc/-/merge_requests/10140) fixes these problems! !++The latest ghc 9.10.1 contains this MR. So this library requires you to update the ghc version to 9.10.1.++Using typed-fsm will go through the following five steps:++1. Define status+2. Define state transfer messages+3. Build status processing function+4. Construct functions from events to messages in different states+5. Running status processing function++Here are some examples:++1. [turnstile](https://github.com/sdzx-1/typed-fsm/tree/main/examples/turnstile)+2. [mouse motion](https://github.com/sdzx-1/typed-fsm/tree/main/examples/motion)+3. [atm](https://github.com/sdzx-1/typed-fsm/tree/main/examples/ATM)+-}+module TypedFsm (+  -- * Defining and implementing FSM+  module TypedFsm.Core,++  -- * Running FSM+  module TypedFsm.Driver,+) where++import TypedFsm.Core+import TypedFsm.Driver
+ src/TypedFsm/Core.hs view
@@ -0,0 +1,62 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TypeFamilies #-}++module TypedFsm.Core where++import Data.IFunctor (+  At (..),+  IFunctor (..),+  IMonad (..),+  returnAt,+  type (~>),+ )++import Data.Kind (Type)+import Data.Singletons (SingI)++-- | The state-transition type class+class StateTransMsg ps where+  data Msg ps (st :: ps) (st' :: ps)++{- | Core AST++Essentially all we do is build this AST and then interpret it.++`Operate m ia st` is an instance of `IMonad`, and it contains an `m` internally+++Typed-fsm only contains two core functions: `getInput`, `liftm`.+We use these two functions to build Operate.++The overall behavior is as follows: constantly reading messages from the outside and converting them into internal monads action.+-}+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')+    -> Operate m ia mode+  In+    :: forall ps m (from :: ps) ia+     . (Msg ps from ~> Operate m ia)+    -> Operate m ia from++instance (Functor m) => IFunctor (Operate m) where+  imap f = \case+    IReturn ia -> IReturn (f ia)+    LiftM f' -> LiftM (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)+    In cont -> In (ibind f . cont)++-- | get messages from outside+getInput :: forall ps m (from :: ps). (Functor m) => Operate m (Msg ps from) from+getInput = In ireturn++-- | 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)
+ src/TypedFsm/Driver.hs view
@@ -0,0 +1,102 @@+{-# 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)
+ typed-fsm.cabal view
@@ -0,0 +1,171 @@+cabal-version:      3.0+-- The cabal-version field refers to the version of the .cabal specification,+-- and can be different from the cabal-install (the tool) version and the++-- version used must be equal or greater than the version stated in this field.+-- Starting from the specification version 2.2, the cabal-version field must be+-- the first thing in the cabal file.++-- Initial package description 'typed-fsm' generated by+-- 'cabal init'. For further documentation, see:+--   http://haskell.org/cabal/users-guide/++-- The name of the package.+name:               typed-fsm++-- The package version.++-- guiding when and how versions should be incremented.+-- https://pvp.haskell.org+-- PVP summary:     +-+------- breaking API changes+--                  | | +----- non-breaking API additions+--                  | | | +--- code changes with no API change+version:            0.1.0.0++-- A short (one-line) description of the package.+synopsis: A framework for strongly typed FSM++-- A longer description of the package.+description:+  FSM stands for [Finite State Machine](https://en.wikipedia.org/wiki/Finite-state_machine).+  The typed-fsm is used to define and execute FSM.++  Advantages of type-fsm:++  * Focus on the right message.+  * Top-to-bottom design for easy refactoring.+  * Conducive to building complex state machine systems:+  ** Type guarantees will not produce incorrect function calls when written.+  ** With the help of the type system, we can define many state processing functions and then call each other recursively with confidence.+  * There is a sanity check. If you miss some items for pattern matching, the compiler will issue a warning, and there will also be a warning for invalid items.+-- The license under which the package is released.+license:            MIT++-- The file containing the license text.+license-file:       LICENSE++-- The package author(s).+author:             sdzx-1++-- An email address to which users can send suggestions, bug reports, and patches.+maintainer:         shangdizhixia1993@163.com+-- A copyright notice.+-- copyright:+category:           Control+build-type:         Simple++-- Extra doc files to be distributed with the package, such as a CHANGELOG or a README.+extra-doc-files:    CHANGELOG.md++-- Extra source files to be distributed with the package, such as examples, or a tutorial module.+-- extra-source-files:++flag BuildExample+  description: Build examples+  default: False++common warnings+    ghc-options: -Wall++library+    -- Import common warning flags.+    import:           warnings++    -- Modules exported by the library.+    exposed-modules: TypedFsm+                   , TypedFsm.Core+                   , TypedFsm.Driver+                   , Data.IFunctor++    -- Modules included in this library but not exported.+    -- other-modules:++    -- LANGUAGE extensions used by modules in this package.+    -- other-extensions:++    -- Other library packages from which modules are imported.+    build-depends: base >=4.20.0.0 && < 5+                 , dependent-map ^>= 0.4.0.0+                 , dependent-sum ^>= 0.7.2.0+                 , mtl ^>= 2.3.1+                 , singletons-base ^>= 3.4++    -- Directories containing source files.+    hs-source-dirs:   src++    -- Base language which the package is written in.+    default-language: GHC2021++executable motion+  if !flag(BuildExample)+    buildable: False+  build-depends: base >=4.20.0.0+               , typed-fsm+               , sdl2 ^>= 2.5.5.0+               , sdl2-ttf ^>= 2.1.3+               , mtl >= 2.3.1+               , stm ^>= 2.5.3.1+               , linear ^>= 1.22+               , unordered-containers ^>= 0.2.20+               , dependent-map >= 0.4.0.0+               , dependent-sum >= 0.7.2.0+               , containers ^>= 0.7 +               , microlens ^>= 0.4.0.0+               , microlens-mtl ^>= 0.2.0.3+               , microlens-th ^>= 0.4.3.15+               , singletons-base >= 3.4+  main-is: Main.hs+  default-language: Haskell2010+  hs-source-dirs: examples/motion+  other-modules: Utils+               , Handler+               , Type+               , EventToMsg+  ghc-options: -threaded -Wall++executable atm+  if !flag(BuildExample)+    buildable: False+  build-depends: base >=4.20.0.0+               , typed-fsm+               , unordered-containers ^>= 0.2.20+               , dependent-map >= 0.4.0.0+               , dependent-sum >= 0.7.2.0+               , containers ^>= 0.7+               , microlens ^>= 0.4.0.0+               , microlens-mtl ^>= 0.2.0.3+               , microlens-th ^>= 0.4.3.15+               , mtl >= 2.3.1+               , sdl2 ^>= 2.5.5.0+               , sdl2-ttf ^>= 2.1.3+               , mtl >= 2.3.1+               , stm ^>= 2.5.3.1+               , linear ^>= 1.22+               , unordered-containers+               , singletons-base >= 3.4+  main-is: Main.hs+  default-language: Haskell2010+  hs-source-dirs: examples/ATM+  other-modules: Type+               , Handler+               , EventToMsg+               , Utils+  ghc-options: -Wall++executable turnstile+  if !flag(BuildExample)+    buildable: False+  build-depends: base >=4.20.0.0+               , typed-fsm+               , dependent-map >= 0.4.0.0+               , dependent-sum >= 0.7.2.0+               , mtl >= 2.3.1+               , singletons-base >= 3.4+  main-is: Main.hs+  default-language: Haskell2010+  hs-source-dirs: examples/turnstile+  ghc-options: -Wall++source-repository head+  type:     git+  location: https://github.com/sdzx-1/typed-fsm