{-# LANGUAGE DataKinds                #-}
{-# LANGUAGE FlexibleContexts         #-}
{-# LANGUAGE GADTs                    #-}
{-# LANGUAGE PatternSynonyms          #-}
{-# LANGUAGE PolyKinds                #-}
{-# LANGUAGE RankNTypes               #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeOperators            #-}

-- | Bidirectional patterns for @'Peer' ps 'AsClient'@.   The advantage of
-- these patterns is that they automatically provide the 'RelativeAgencyEq'
-- singleton.
--
module Network.TypedProtocol.Stateful.Peer.Client
  ( -- * Client type alias and its pattern synonyms
    Client
  , pattern Effect
  , pattern Yield
  , pattern Await
  , pattern Done
  ) where

import           Data.Kind (Type)

import           Network.TypedProtocol.Core
import           Network.TypedProtocol.Stateful.Peer (Peer)
import qualified Network.TypedProtocol.Stateful.Peer as TP


type Client :: forall ps
            -> ps
            -> (ps -> Type)
            -> (Type -> Type)
            -> Type
            -> Type
type Client ps st f m a = Peer ps AsClient st f m a


-- | Client role pattern for 'TP.Effect'.
--
pattern Effect :: forall ps st f m a.
                  m (Client ps st f m a)
               -- ^ monadic continuation
               -> Client ps st f m a
pattern $bEffect :: forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a.
m (Client ps st f m a) -> Client ps st f m a
$mEffect :: forall {r} {ps} {st :: ps} {f :: ps -> *} {m :: * -> *} {a}.
Client ps st f m a
-> (m (Client ps st f m a) -> r) -> ((# #) -> r) -> r
Effect mclient = TP.Effect mclient


-- | Client role pattern for 'TP.Yield'
--
pattern Yield :: forall ps st f m a.
                 ()
              => forall st'.
                 ( StateTokenI st
                 , StateTokenI st'
                 , StateAgency st ~ ClientAgency
                 )
              => f st
              -> f st'
              -> Message ps st st'
              -- ^ protocol message
              -> Client ps st' f m a
              -- ^ continuation
              -> Client ps st  f m a
pattern $bYield :: forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a (st' :: ps).
(StateTokenI st, StateTokenI st',
 StateAgency st ~ 'ClientAgency) =>
f st
-> f st'
-> Message ps st st'
-> Client ps st' f m a
-> Client ps st f m a
$mYield :: forall {r} {ps} {st :: ps} {f :: ps -> *} {m :: * -> *} {a}.
Client ps st f m a
-> (forall {st' :: ps}.
    (StateTokenI st, StateTokenI st',
     StateAgency st ~ 'ClientAgency) =>
    f st -> f st' -> Message ps st st' -> Client ps st' f m a -> r)
-> ((# #) -> r)
-> r
Yield f f' msg k = TP.Yield ReflClientAgency f f' msg k


-- | Client role pattern for 'TP.Await'
--
pattern Await :: forall ps st f m a.
                 ()
              => ( StateTokenI st
                 , StateAgency st ~ ServerAgency
                 )
              => (forall st'.
                     f st
                  -> Message ps st st'
                  -> ( Client ps st' f m a
                     , f st'
                     )
                 )
              -- ^ continuation
              -> Client ps st f m a
pattern $bAwait :: forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a.
(StateTokenI st, StateAgency st ~ 'ServerAgency) =>
(forall (st' :: ps).
 f st -> Message ps st st' -> (Client ps st' f m a, f st'))
-> Client ps st f m a
$mAwait :: forall {r} {ps} {st :: ps} {f :: ps -> *} {m :: * -> *} {a}.
Client ps st f m a
-> ((StateTokenI st, StateAgency st ~ 'ServerAgency) =>
    (forall (st' :: ps).
     f st -> Message ps st st' -> (Client ps st' f m a, f st'))
    -> r)
-> ((# #) -> r)
-> r
Await k = TP.Await ReflServerAgency k


-- | Client role pattern for 'TP.Done'
--
pattern Done :: forall ps st f m a.
                ()
             => ( StateTokenI st
                , StateAgency st ~ NobodyAgency
                )
             => a
             -- ^ protocol return value
             -> Client ps st f m a
pattern $bDone :: forall ps (st :: ps) (f :: ps -> *) (m :: * -> *) a.
(StateTokenI st, StateAgency st ~ 'NobodyAgency) =>
a -> Client ps st f m a
$mDone :: forall {r} {ps} {st :: ps} {f :: ps -> *} {m :: * -> *} {a}.
Client ps st f m a
-> ((StateTokenI st, StateAgency st ~ 'NobodyAgency) => a -> r)
-> ((# #) -> r)
-> r
Done a = TP.Done ReflNobodyAgency a


{-# COMPLETE Effect, Yield, Await, Done #-}