{-# 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 (Sing)
import TypedFsm.Core (Operate (..), StateTransMsg (Msg))
import TypedFsm.Driver.Common
import Unsafe.Coerce (unsafeCoerce)

anyToSomeMsg
  :: forall ps input
   . (SEq ps)
  => Sing input -> AnyMsg ps -> Maybe (SomeMsg ps input)
anyToSomeMsg :: forall ps (input :: ps).
SEq ps =>
Sing input -> AnyMsg ps -> Maybe (SomeMsg ps input)
anyToSomeMsg Sing input
sinput (AnyMsg Sing from
sfrom Sing to
sto (Msg ps from to
msg :: Msg ps from to)) =
  case Sing from
sfrom Sing from -> Sing input -> Sing (Apply (Apply (==@#@$) from) input)
forall (t1 :: ps) (t2 :: ps).
Sing t1 -> Sing t2 -> Sing (Apply (Apply (==@#@$) t1) t2)
forall a (t1 :: a) (t2 :: a).
SEq a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply (==@#@$) t1) t2)
%== Sing input
sinput of
    -- (from == input) ~ True
    -- ==> from ~ input
    Sing (Apply (Apply (==@#@$) from) input)
SBool (from == input)
STrue -> Maybe (SomeMsg ps from) -> Maybe (SomeMsg ps input)
forall a b. a -> b
unsafeCoerce (SomeMsg ps from -> Maybe (SomeMsg ps from)
forall a. a -> Maybe a
Just (Sing to -> Msg ps from to -> SomeMsg ps from
forall ps (from :: ps) (to :: ps).
Sing to -> Msg ps from to -> SomeMsg ps from
SomeMsg Sing to
sto Msg ps from to
msg))
    Sing (Apply (Apply (==@#@$) from) input)
SBool (from == input)
SFalse -> Maybe (SomeMsg ps input)
forall a. Maybe a
Nothing

newtype UnexpectMsg ps = UnexpectMsg (AnyMsg ps)

data UnexpectMsgHandler ps m
  = Ignore
  | IgnoreAndTrace (AnyMsg ps -> m ())
  | Terminal

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)
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)
runOperate UnexpectMsgHandler ps m
unHandler [AnyMsg ps]
anyMsgs Sing input
sinput = \case
  IReturn (At a
a) -> Result ps (UnexpectMsg ps) m a
-> m (Result ps (UnexpectMsg ps) m a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> Result ps (UnexpectMsg ps) m a
forall ps e (m :: * -> *) a. a -> Result ps e m a
Finish a
a)
  LiftM Sing mode'
singv m (Operate m (At a output) mode')
m -> m (Operate m (At a output) mode')
m m (Operate m (At a output) mode')
-> (Operate m (At a output) mode'
    -> m (Result ps (UnexpectMsg ps) m a))
-> m (Result ps (UnexpectMsg ps) m a)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (UnexpectMsgHandler ps m
-> [AnyMsg ps]
-> Sing mode'
-> Operate m (At a output) mode'
-> m (Result ps (UnexpectMsg ps) m a)
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)
runOperate UnexpectMsgHandler ps m
unHandler [AnyMsg ps]
anyMsgs Sing mode'
singv)
  In Msg ps input ~> Operate m (At a output)
f -> [AnyMsg ps] -> m (Result ps (UnexpectMsg ps) m a)
loop [AnyMsg ps]
anyMsgs
   where
    loop :: [AnyMsg ps] -> m (Result ps (UnexpectMsg ps) m a)
loop [] = Result ps (UnexpectMsg ps) m a
-> m (Result ps (UnexpectMsg ps) m a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Result ps (UnexpectMsg ps) m a
 -> m (Result ps (UnexpectMsg ps) m a))
-> Result ps (UnexpectMsg ps) m a
-> m (Result ps (UnexpectMsg ps) m a)
forall a b. (a -> b) -> a -> b
$ SomeOperate ps m a -> Result ps (UnexpectMsg ps) m a
forall ps e (m :: * -> *) a. SomeOperate ps m a -> Result ps e m a
Cont (SomeOperate ps m a -> Result ps (UnexpectMsg ps) m a)
-> SomeOperate ps m a -> Result ps (UnexpectMsg ps) m a
forall a b. (a -> b) -> a -> b
$ Sing input -> Operate m (At a output) input -> SomeOperate ps m a
forall ts (m :: * -> *) a (i :: ts) (o :: ts).
Sing i -> Operate m (At a o) i -> SomeOperate ts m a
SomeOperate Sing input
sinput ((Msg ps input ~> Operate m (At a output))
-> Operate m (At a output) input
forall ps (a :: * -> *) (c :: ps) (b :: ps -> *).
(Msg ps c ~> Operate a b) -> Operate a b c
In Msg ps input x -> Operate m (At a output) x
Msg ps input ~> Operate m (At a output)
f)
    loop (AnyMsg ps
anyMsg : [AnyMsg ps]
evns') = do
      case Sing input -> AnyMsg ps -> Maybe (SomeMsg ps input)
forall ps (input :: ps).
SEq ps =>
Sing input -> AnyMsg ps -> Maybe (SomeMsg ps input)
anyToSomeMsg Sing input
sinput AnyMsg ps
anyMsg of
        Maybe (SomeMsg ps input)
Nothing -> case UnexpectMsgHandler ps m
unHandler of
          UnexpectMsgHandler ps m
Ignore -> [AnyMsg ps] -> m (Result ps (UnexpectMsg ps) m a)
loop [AnyMsg ps]
evns'
          IgnoreAndTrace AnyMsg ps -> m ()
trace -> AnyMsg ps -> m ()
trace AnyMsg ps
anyMsg m ()
-> m (Result ps (UnexpectMsg ps) m a)
-> m (Result ps (UnexpectMsg ps) m a)
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [AnyMsg ps] -> m (Result ps (UnexpectMsg ps) m a)
loop [AnyMsg ps]
evns'
          UnexpectMsgHandler ps m
Terminal -> Result ps (UnexpectMsg ps) m a
-> m (Result ps (UnexpectMsg ps) m a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UnexpectMsg ps -> Result ps (UnexpectMsg ps) m a
forall ps e (m :: * -> *) a. e -> Result ps e m a
ErrorInfo (UnexpectMsg ps -> Result ps (UnexpectMsg ps) m a)
-> UnexpectMsg ps -> Result ps (UnexpectMsg ps) m a
forall a b. (a -> b) -> a -> b
$ AnyMsg ps -> UnexpectMsg ps
forall ps. AnyMsg ps -> UnexpectMsg ps
UnexpectMsg AnyMsg ps
anyMsg)
        Just (SomeMsg Sing to
sto Msg ps input to
msg) -> UnexpectMsgHandler ps m
-> [AnyMsg ps]
-> Sing to
-> Operate m (At a output) to
-> m (Result ps (UnexpectMsg ps) m a)
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)
runOperate UnexpectMsgHandler ps m
unHandler [AnyMsg ps]
evns' Sing to
sto (Msg ps input to -> Operate m (At a output) to
Msg ps input ~> Operate m (At a output)
f Msg ps input to
msg)