{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE GADTs          #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators  #-}

-- 'withInitiatorMode' and 'withResponderMode' are using redundant constraints.
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- | Singletons to work with 'MuxMode' kind.
--
module Ouroboros.Network.MuxMode
  ( SingMuxMode (..)
  , SingHasInitiator (..)
  , hasInitiatorMode
  , WithMuxMode (..)
  , WithMuxTuple
  , withInitiatorMode
  , withResponderMode
  , InResponderMode (..)
  ) where

import Network.Mux.Types as Mux


-- | Singletons for matching the 'MuxMode' at term level.
--
data SingMuxMode (mode :: Mux.Mode) where
    SingInitiatorMode          :: SingMuxMode InitiatorMode
    SingResponderMode          :: SingMuxMode ResponderMode
    SingInitiatorResponderMode :: SingMuxMode InitiatorResponderMode


-- | Singleton for to match the @'HasInitiator' mode ~ True@ constraint.
--
data SingHasInitiator (mode :: Mux.Mode) where
    SingHasInitiator :: HasInitiator mode ~ True
                  => SingHasInitiator mode

    SingNoInitiator  :: HasInitiator mode ~ False
                  => SingHasInitiator mode

hasInitiatorMode :: SingMuxMode mode
                 -> SingHasInitiator mode
hasInitiatorMode :: forall (mode :: Mode). SingMuxMode mode -> SingHasInitiator mode
hasInitiatorMode SingMuxMode mode
SingInitiatorMode          = SingHasInitiator mode
forall (mode :: Mode).
(HasInitiator mode ~ 'True) =>
SingHasInitiator mode
SingHasInitiator
hasInitiatorMode SingMuxMode mode
SingInitiatorResponderMode = SingHasInitiator mode
forall (mode :: Mode).
(HasInitiator mode ~ 'True) =>
SingHasInitiator mode
SingHasInitiator
hasInitiatorMode SingMuxMode mode
SingResponderMode          = SingHasInitiator mode
forall (mode :: Mode).
(HasInitiator mode ~ 'False) =>
SingHasInitiator mode
SingNoInitiator

data WithMuxMode (mode :: Mux.Mode) a b where
    WithInitiatorMode          :: a -> WithMuxMode InitiatorMode a b
    WithResponderMode          :: b -> WithMuxMode ResponderMode a b
    WithInitiatorResponderMode :: a -> b -> WithMuxMode InitiatorResponderMode a b


type WithMuxTuple mode a = WithMuxMode mode a a

withInitiatorMode :: HasInitiator mode ~ True
                  => WithMuxMode mode a b
                  -> a
withInitiatorMode :: forall (mode :: Mode) a b.
(HasInitiator mode ~ 'True) =>
WithMuxMode mode a b -> a
withInitiatorMode (WithInitiatorMode          a
a  ) = a
a
withInitiatorMode (WithInitiatorResponderMode a
a b
_) = a
a

withResponderMode :: HasResponder mode ~ True
                  => WithMuxMode mode a b
                  -> b
withResponderMode :: forall (mode :: Mode) a b.
(HasResponder mode ~ 'True) =>
WithMuxMode mode a b -> b
withResponderMode (WithResponderMode            b
b) = b
b
withResponderMode (WithInitiatorResponderMode a
_ b
b) = b
b


data InResponderMode (mode :: Mux.Mode) a where
    InResponderMode    :: HasResponder mode ~ True
                       => a
                       -> InResponderMode mode a

    NotInResponderMode :: InResponderMode mode a