{-# 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, 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)

getSomeOperateSingeton :: (SingKind ts) => SomeOperate ts m a -> Sing ts
getSomeOperateSingeton :: forall ts (m :: * -> *) a.
SingKind ts =>
SomeOperate ts m a -> Sing ts
getSomeOperateSingeton (SomeOperate (Operate m (At a o) i
_ :: Operate m ia i)) =
  Sing i -> Sing ts
forall a b. a -> b
unsafeCoerce (Sing i -> Sing ts) -> Sing i -> Sing 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

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 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
$ forall (a :: ts). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @i

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

data AnyMsg ps
  = forall (from :: ps) (to :: ps).
    (SingI from, SingI to) =>
    AnyMsg (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