{-# 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 :: forall ts (m :: * -> *) a.
SingKind ts =>
SomeOperate ts m a -> Demote ts
getSomeOperateSt (SomeOperate (Operate m (At a o) i
_ :: Operate m (At a o) i)) = Sing i -> Demote ts
forall (a :: ts). Sing a -> Demote ts
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing (Sing i -> Demote ts) -> Sing i -> Demote ts
forall a b. (a -> b) -> a -> b
$ forall (a :: ts). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
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 :: forall n (a :: n) (b :: n).
SOrd n =>
Sing a -> Sing b -> GOrdering a b
sOrdToGCompare Sing a
a Sing b
b = case Sing a -> Sing b -> Sing (Apply (Apply CompareSym0 a) b)
forall (t1 :: n) (t2 :: n).
Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)
forall a (t1 :: a) (t2 :: a).
SOrd a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)
sCompare Sing a
a Sing b
b of
  Sing (Apply (Apply CompareSym0 a) b)
SOrdering (Compare a b)
SEQ -> GOrdering Any Any -> GOrdering a b
forall a b. a -> b
unsafeCoerce GOrdering Any Any
forall {k} (a :: k). GOrdering a a
GEQ
  Sing (Apply (Apply CompareSym0 a) b)
SOrdering (Compare a b)
SLT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
  Sing (Apply (Apply CompareSym0 a) b)
SOrdering (Compare a b)
SGT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
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 :: forall ps event state (m :: * -> *) a (input :: ps) (output :: ps).
(SingI input, GCompare Sing, 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 State2GenMsg ps state event
dmp [event]
evns = \case
  IReturn (At a
a) -> Result ps (StateT state m) a
-> StateT state m (Result ps (StateT state m) a)
forall a. a -> StateT state m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> Result ps (StateT state m) a
forall ps (m :: * -> *) a. a -> Result ps m a
Finish a
a)
  LiftM StateT state m (Operate (StateT state m) (At a output) mode')
m -> StateT state m (Operate (StateT state m) (At a output) mode')
m StateT state m (Operate (StateT state m) (At a output) mode')
-> (Operate (StateT state m) (At a output) mode'
    -> StateT state m (Result ps (StateT state m) a))
-> StateT state m (Result ps (StateT state m) a)
forall a b.
StateT state m a -> (a -> StateT state m b) -> StateT state m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
Prelude.>>= State2GenMsg ps state event
-> [event]
-> Operate (StateT state m) (At a output) mode'
-> StateT state m (Result ps (StateT state m) a)
forall ps event state (m :: * -> *) a (input :: ps) (output :: ps).
(SingI input, GCompare Sing, 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 State2GenMsg ps state event
dmp [event]
evns
  In Msg ps input ~> Operate (StateT state m) (At a output)
f -> do
    let singInput :: Sing input
singInput = forall (a :: ps). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @input
    case Sing input
-> State2GenMsg ps state event
-> Maybe (GenMsg ps state event input)
forall {k1} (k2 :: k1 -> *) (f :: k1 -> *) (v :: k1).
GCompare k2 =>
k2 v -> DMap k2 f -> Maybe (f v)
D.lookup Sing input
singInput State2GenMsg ps state event
dmp of
      Maybe (GenMsg ps state event input)
Nothing -> Result ps (StateT state m) a
-> StateT state m (Result ps (StateT state m) a)
forall a. a -> StateT state m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sing input -> Result ps (StateT state m) a
forall ps (m :: * -> *) a (t :: ps). Sing t -> Result ps m a
NotMatchGenMsg Sing input
singInput)
      Just (GenMsg state -> event -> Maybe (SomeMsg ps input)
genMsg) -> [event] -> StateT state m (Result ps (StateT state m) a)
loop [event]
evns
       where
        loop :: [event] -> StateT state m (Result ps (StateT state m) a)
loop [] = Result ps (StateT state m) a
-> StateT state m (Result ps (StateT state m) a)
forall a. a -> StateT state m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Result ps (StateT state m) a
 -> StateT state m (Result ps (StateT state m) a))
-> Result ps (StateT state m) a
-> StateT state m (Result ps (StateT state m) a)
forall a b. (a -> b) -> a -> b
$ SomeOperate ps (StateT state m) a -> Result ps (StateT state m) a
forall ps (m :: * -> *) a. SomeOperate ps m a -> Result ps m a
Cont (SomeOperate ps (StateT state m) a -> Result ps (StateT state m) a)
-> SomeOperate ps (StateT state m) a
-> Result ps (StateT state m) a
forall a b. (a -> b) -> a -> b
$ Operate (StateT state m) (At a output) input
-> SomeOperate ps (StateT state 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 (StateT state m) (At a output))
-> Operate (StateT state 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 (StateT state m) (At a output) x
Msg ps input ~> Operate (StateT state m) (At a output)
f)
        loop (event
et : [event]
evns') = do
          state' <- StateT state m state
forall s (m :: * -> *). MonadState s m => m s
get
          case genMsg state' et of
            Maybe (SomeMsg ps input)
Nothing -> [event] -> StateT state m (Result ps (StateT state m) a)
loop [event]
evns'
            Just (SomeMsg Msg ps input to
msg) -> State2GenMsg ps state event
-> [event]
-> Operate (StateT state m) (At a output) to
-> StateT state m (Result ps (StateT state m) a)
forall ps event state (m :: * -> *) a (input :: ps) (output :: ps).
(SingI input, GCompare Sing, 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 State2GenMsg ps state event
dmp [event]
evns' (Msg ps input to -> Operate (StateT state m) (At a output) to
Msg ps input ~> Operate (StateT state m) (At a output)
f Msg ps input to
msg)