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

module TypedFsm.Driver.Common where

import Data.IFunctor (At (..))
import Data.Singletons (Sing, SingKind (..))
import TypedFsm.Core (Operate (..), StateTransMsg (Msg))
import Unsafe.Coerce (unsafeCoerce)

data SomeOperate ts m a
  = forall (i :: ts) (o :: ts).
    SomeOperate (Sing i) (Operate m (At a o) i)

getSomeOperateSing :: SomeOperate ts m a -> Sing (r :: ts)
getSomeOperateSing :: forall ts (m :: * -> *) a (r :: ts). SomeOperate ts m a -> Sing r
getSomeOperateSing (SomeOperate Sing i
si (Operate m (At a o) i
_ :: Operate m ia i)) =
  Sing i -> Sing r
forall a b. a -> b
unsafeCoerce Sing i
si

getSomeOperateSt :: (SingKind ts) => SomeOperate ts m a -> Demote ts
getSomeOperateSt :: forall ts (m :: * -> *) a.
SingKind ts =>
SomeOperate ts m a -> Demote ts
getSomeOperateSt (SomeOperate Sing i
si (Operate m (At a o) i
_ :: Operate m ia 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
$ Sing i
si

data SomeMsg ps from
  = forall (to :: ps).
    SomeMsg (Sing to) (Msg ps from to)

data AnyMsg ps
  = forall (from :: ps) (to :: ps).
    AnyMsg (Sing from) (Sing to) (Msg ps from to)

{- | Reuslt of run FSM

* Finish, return val a
* A wrapper for SomeOperate that returns the remaining computation when there is not enough input
* Error happened
-}
data Result ps e m a
  = Finish a
  | Cont (SomeOperate ps m a)
  | ErrorInfo e