{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wno-unused-do-bind #-}

{- | Running FSM

The core function is `runOp`, and the other functions are to make it work properly.
-}
module TypedFsm.Driver.Op 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 (..), SomeSing (..))
import TypedFsm.Core (Operate (..))
import TypedFsm.Driver.Common
import Unsafe.Coerce (unsafeCoerce)

{- | `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)

type SomeOp ps state m a = SomeOperate ps (StateT state m) a

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)

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

newtype NotFoundGenMsg ps = NotFoundGenMsg (SomeSing ps)

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 (NotFoundGenMsg 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 (NotFoundGenMsg ps) (StateT state m) a)
runOp State2GenMsg ps state event
dmp [event]
evns = \case
  IReturn (At a
a) -> Result ps (NotFoundGenMsg ps) (StateT state m) a
-> StateT
     state m (Result ps (NotFoundGenMsg ps) (StateT state m) a)
forall a. a -> StateT state m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> Result ps (NotFoundGenMsg ps) (StateT state m) a
forall ps e (m :: * -> *) a. a -> Result ps e 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 (NotFoundGenMsg ps) (StateT state m) a))
-> StateT
     state m (Result ps (NotFoundGenMsg 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
>>= State2GenMsg ps state event
-> [event]
-> Operate (StateT state m) (At a output) mode'
-> StateT
     state m (Result ps (NotFoundGenMsg 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 (NotFoundGenMsg 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 (NotFoundGenMsg ps) (StateT state m) a
-> StateT
     state m (Result ps (NotFoundGenMsg ps) (StateT state m) a)
forall a. a -> StateT state m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NotFoundGenMsg ps
-> Result ps (NotFoundGenMsg ps) (StateT state m) a
forall ps e (m :: * -> *) a. e -> Result ps e m a
ErrorInfo (NotFoundGenMsg ps
 -> Result ps (NotFoundGenMsg ps) (StateT state m) a)
-> NotFoundGenMsg ps
-> Result ps (NotFoundGenMsg ps) (StateT state m) a
forall a b. (a -> b) -> a -> b
$ SomeSing ps -> NotFoundGenMsg ps
forall ps. SomeSing ps -> NotFoundGenMsg ps
NotFoundGenMsg (SomeSing ps -> NotFoundGenMsg ps)
-> SomeSing ps -> NotFoundGenMsg ps
forall a b. (a -> b) -> a -> b
$ Sing input -> SomeSing ps
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing input
singInput)
      Just (GenMsg state -> event -> Maybe (SomeMsg ps input)
genMsg) -> [event]
-> StateT
     state m (Result ps (NotFoundGenMsg ps) (StateT state m) a)
loop [event]
evns
       where
        loop :: [event]
-> StateT
     state m (Result ps (NotFoundGenMsg ps) (StateT state m) a)
loop [] = Result ps (NotFoundGenMsg ps) (StateT state m) a
-> StateT
     state m (Result ps (NotFoundGenMsg ps) (StateT state m) a)
forall a. a -> StateT state m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Result ps (NotFoundGenMsg ps) (StateT state m) a
 -> StateT
      state m (Result ps (NotFoundGenMsg ps) (StateT state m) a))
-> Result ps (NotFoundGenMsg ps) (StateT state m) a
-> StateT
     state m (Result ps (NotFoundGenMsg ps) (StateT state m) a)
forall a b. (a -> b) -> a -> b
$ SomeOperate ps (StateT state m) a
-> Result ps (NotFoundGenMsg ps) (StateT state m) a
forall ps e (m :: * -> *) a. SomeOperate ps m a -> Result ps e m a
Cont (SomeOperate ps (StateT state m) a
 -> Result ps (NotFoundGenMsg ps) (StateT state m) a)
-> SomeOperate ps (StateT state m) a
-> Result ps (NotFoundGenMsg 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 (NotFoundGenMsg 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 (NotFoundGenMsg 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 (NotFoundGenMsg 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)