{-# 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, 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)
   . (GCompare (Sing @ps))
  => (Monad m)
  => State2GenMsg ps state event
  -> [event]
  -> Sing input
  -> 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).
(GCompare Sing, Monad m) =>
State2GenMsg ps state event
-> [event]
-> Sing input
-> 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 Sing input
sinput = \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 Sing mode'
sinput' 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]
-> Sing mode'
-> 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).
(GCompare Sing, Monad m) =>
State2GenMsg ps state event
-> [event]
-> Sing input
-> 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 Sing mode'
sinput'
  In Msg ps input ~> Operate (StateT state m) (At a output)
f -> do
    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
sinput 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
sinput)
      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
$ Sing input
-> Operate (StateT state m) (At a output) input
-> SomeOperate ps (StateT state 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 (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 Sing to
sto Msg ps input to
msg) -> State2GenMsg ps state event
-> [event]
-> Sing to
-> 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).
(GCompare Sing, Monad m) =>
State2GenMsg ps state event
-> [event]
-> Sing input
-> 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' Sing to
sto (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)