{-# 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 :: forall ps (input :: ps).
(SingI input, SEq ps) =>
AnyMsg ps -> Maybe (SomeMsg ps input)
anyToSomeMsg (AnyMsg (Msg ps from to
msg :: Msg ps from to)) =
  case forall (a :: ps). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @from 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)
%== forall (a :: ps). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @input 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 (Msg ps from to -> SomeMsg ps from
forall ps (from :: ps) (to :: ps).
SingI to =>
Msg ps from to -> SomeMsg ps from
SomeMsg 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)

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 :: 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 [AnyMsg ps]
anyMsgs = \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 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
>>= ([AnyMsg ps]
-> Operate m (At a output) mode'
-> m (Result ps (UnexpectMsg ps) m a)
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 [AnyMsg ps]
anyMsgs)
  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
$ Operate m (At a output) input -> SomeOperate ps m a
forall ts (m :: * -> *) a (i :: ts) (o :: ts).
SingI i =>
Operate m (At a o) i -> SomeOperate ts m a
SomeOperate ((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 forall ps (input :: ps).
(SingI input, SEq ps) =>
AnyMsg ps -> Maybe (SomeMsg ps input)
anyToSomeMsg @_ @input AnyMsg ps
anyMsg of
        Maybe (SomeMsg ps input)
Nothing -> 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 Msg ps input to
msg) -> [AnyMsg ps]
-> Operate m (At a output) to -> m (Result ps (UnexpectMsg ps) m a)
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 [AnyMsg ps]
evns' (Msg ps input to -> Operate m (At a output) to
Msg ps input ~> Operate m (At a output)
f Msg ps input to
msg)