{-# LANGUAGE DataKinds                #-}
{-# LANGUAGE FlexibleContexts         #-}
{-# LANGUAGE FlexibleInstances        #-}
{-# LANGUAGE GADTs                    #-}
{-# LANGUAGE InstanceSigs             #-}
{-# LANGUAGE KindSignatures           #-}
{-# LANGUAGE PolyKinds                #-}
{-# LANGUAGE ScopedTypeVariables      #-}
{-# LANGUAGE StandaloneDeriving       #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications         #-}
{-# LANGUAGE TypeFamilies             #-}
{-# LANGUAGE TypeOperators            #-}
{-# LANGUAGE UndecidableInstances     #-}

module Network.TypedProtocol.Trans.Wedge where

import           Network.TypedProtocol.Core

import qualified Network.TypedProtocol.Peer.Client as Client
import qualified Network.TypedProtocol.PingPong.Type as PingPong


-- | A [wedge](https://hackage.haskell.org/package/smash-0.1.2/docs/Data-Wedge.html)
-- sum of two protocols.
--
-- One can interleave both protocols using protocol pipelining.  Termination
-- must be done by terminating one of the protocols.
--
data Wedge ps (stIdle :: ps) ps' (stIdle' :: ps') where
    StIdle :: Wedge ps stIdle ps' stIdle'
    StFst  :: ps  -> Wedge ps stIdle ps' stIdle'
    StSnd  :: ps' -> Wedge ps stIdle ps' stIdle'


data SingWedge (st ::  Wedge ps (stIdle :: ps) ps' (stIdle' :: ps')) where
    SingStIdle :: SingWedge StIdle
    SingStFst  :: StateToken st
               -> SingWedge (StFst st)
    SingStSnd  :: StateToken st'
               -> SingWedge (StSnd st')

instance Show (SingWedge StIdle) where
    show :: SingWedge 'StIdle -> String
show SingWedge 'StIdle
SingStIdle    = String
"SingStIdle"
instance Show (StateToken st) => Show (SingWedge (StFst st)) where
    show :: SingWedge ('StFst st) -> String
show (SingStFst StateToken st
s) = String
"SingStFst " String -> ShowS
forall a. [a] -> [a] -> [a]
++ StateToken st -> String
forall a. Show a => a -> String
show StateToken st
StateToken st
s
instance Show (StateToken st) => Show (SingWedge (StSnd st)) where
    show :: SingWedge ('StSnd st) -> String
show (SingStSnd StateToken st'
s) = String
"SingStSnd " String -> ShowS
forall a. [a] -> [a] -> [a]
++ StateToken st -> String
forall a. Show a => a -> String
show StateToken st
StateToken st'
s

instance StateTokenI StIdle where
    stateToken :: StateToken 'StIdle
stateToken = StateToken 'StIdle
SingWedge 'StIdle
forall {ps} {stIdle :: ps} {ps'} {stIdle' :: ps'}.
SingWedge 'StIdle
SingStIdle
instance StateTokenI st => StateTokenI (StFst st) where
    stateToken :: StateToken ('StFst st)
stateToken = StateToken st -> SingWedge ('StFst st)
forall {ps} {stIdle :: ps} {ps'} {stIdle' :: ps'} (st :: ps).
StateToken st -> SingWedge ('StFst st)
SingStFst (forall (st :: ps). StateTokenI st => StateToken st
forall {ps} (st :: ps). StateTokenI st => StateToken st
stateToken @st)
instance StateTokenI st => StateTokenI (StSnd st) where
    stateToken :: StateToken ('StSnd st)
stateToken = StateToken st -> SingWedge ('StSnd st)
forall {ps} {ps} {stIdle :: ps} {stIdle' :: ps} (st :: ps).
StateToken st -> SingWedge ('StSnd st)
SingStSnd (forall (st :: ps'). StateTokenI st => StateToken st
forall {ps} (st :: ps). StateTokenI st => StateToken st
stateToken @st)


-- | A Singleton type which allows to pick the starting protocol state.
--
data SingStart (st :: Wedge ps stIdle ps' stIdle') where
    AtFst :: SingStart (StFst stIdle)
    AtSnd :: SingStart (StSnd stIdle)


-- Note: This does not require @(Protocol ps, Protocol ps')@, ghc is not
-- requiring class constraints for associated type families / data types the
-- same way as for terms.
--
instance Protocol (Wedge ps (stIdle :: ps) ps' (stIdle' :: ps')) where

    data Message  (Wedge ps (stIdle :: ps) ps' (stIdle' :: ps')) from to where
      -- | Signal that starts one of the protocols.
      --
      MsgStart :: SingStart st
               -> Message (Wedge ps stIdle ps' stIdle')
                          StIdle st

      -- | Embed any @ps@ message.
      --
      MsgFst      :: Message ps  st st'
                  -> Message (Wedge ps stIdle ps' stIdle')
                             (StFst st) (StFst st')


      -- | Embed any @ps'@ message.
      MsgSnd      :: Message ps' st st'
                  -> Message (Wedge ps stIdle ps' stIdle')
                             (StSnd st) (StSnd st')

      -- | Switch from @ps@ to @ps'@.
      --
      MsgFstToSnd :: Message (Wedge ps stIdle ps' stIdle')
                             (StFst stIdle) (StSnd stIdle')

      -- | Switch from @ps'@ to @ps@.
      --
      MsgSndToFst :: Message (Wedge ps stIdle ps' stIdle')
                             (StSnd stIdle') (StFst stIdle)


    type StateAgency StIdle     = ClientAgency
    type StateAgency (StFst st) = StateAgency st
    type StateAgency (StSnd st) = StateAgency st

    type StateToken = SingWedge


type PingPong2 = Wedge PingPong.PingPong PingPong.StIdle
                       PingPong.PingPong PingPong.StIdle


pingPong2Client :: Client.Client PingPong2 NonPipelined StIdle m ()
pingPong2Client :: forall (m :: * -> *). Client PingPong2 'NonPipelined 'StIdle m ()
pingPong2Client =
    Message PingPong2 'StIdle ('StFst 'StIdle)
-> Client PingPong2 'NonPipelined ('StFst 'StIdle) m ()
-> Client PingPong2 'NonPipelined 'StIdle m ()
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a
       (st' :: ps).
(StateTokenI st, StateTokenI st', StateAgency st ~ 'ClientAgency,
 Outstanding pl ~ 'Z) =>
Message ps st st' -> Client ps pl st' m a -> Client ps pl st m a
Client.Yield (SingStart ('StFst 'StIdle)
-> Message PingPong2 'StIdle ('StFst 'StIdle)
forall ps (stIdle :: ps) ps' (stIdle' :: ps')
       (st :: Wedge ps stIdle ps' stIdle').
SingStart st -> Message (Wedge ps stIdle ps' stIdle') 'StIdle st
MsgStart SingStart ('StFst 'StIdle)
forall {ps} {stIdle :: ps} {ps'} {stIdle' :: ps'} (st :: ps).
SingStart ('StFst st)
AtFst)
  (Client PingPong2 'NonPipelined ('StFst 'StIdle) m ()
 -> Client PingPong2 'NonPipelined 'StIdle m ())
-> Client PingPong2 'NonPipelined ('StFst 'StIdle) m ()
-> Client PingPong2 'NonPipelined 'StIdle m ()
forall a b. (a -> b) -> a -> b
$ Message PingPong2 ('StFst 'StIdle) ('StFst 'StBusy)
-> Client PingPong2 'NonPipelined ('StFst 'StBusy) m ()
-> Client PingPong2 'NonPipelined ('StFst 'StIdle) m ()
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a
       (st' :: ps).
(StateTokenI st, StateTokenI st', StateAgency st ~ 'ClientAgency,
 Outstanding pl ~ 'Z) =>
Message ps st st' -> Client ps pl st' m a -> Client ps pl st m a
Client.Yield (Message PingPong 'StIdle 'StBusy
-> Message PingPong2 ('StFst 'StIdle) ('StFst 'StBusy)
forall ps (st :: ps) (st' :: ps) (stIdle :: ps) ps'
       (stIdle' :: ps').
Message ps st st'
-> Message (Wedge ps stIdle ps' stIdle') ('StFst st) ('StFst st')
MsgFst Message PingPong 'StIdle 'StBusy
PingPong.MsgPing)
  (Client PingPong2 'NonPipelined ('StFst 'StBusy) m ()
 -> Client PingPong2 'NonPipelined ('StFst 'StIdle) m ())
-> Client PingPong2 'NonPipelined ('StFst 'StBusy) m ()
-> Client PingPong2 'NonPipelined ('StFst 'StIdle) m ()
forall a b. (a -> b) -> a -> b
$ (forall (st' :: PingPong2).
 Message PingPong2 ('StFst 'StBusy) st'
 -> Client PingPong2 'NonPipelined st' m ())
-> Client PingPong2 'NonPipelined ('StFst 'StBusy) m ()
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
(StateTokenI st, StateAgency st ~ 'ServerAgency,
 Outstanding pl ~ 'Z) =>
(forall (st' :: ps). Message ps st st' -> Client ps pl st' m a)
-> Client ps pl st m a
Client.Await ((forall (st' :: PingPong2).
  Message PingPong2 ('StFst 'StBusy) st'
  -> Client PingPong2 'NonPipelined st' m ())
 -> Client PingPong2 'NonPipelined ('StFst 'StBusy) m ())
-> (forall (st' :: PingPong2).
    Message PingPong2 ('StFst 'StBusy) st'
    -> Client PingPong2 'NonPipelined st' m ())
-> Client PingPong2 'NonPipelined ('StFst 'StBusy) m ()
forall a b. (a -> b) -> a -> b
$ \(MsgFst Message PingPong st st'
R:MessagePingPongfromto st st'
PingPong.MsgPong) ->
    Message PingPong2 st' ('StSnd 'StIdle)
-> Client PingPong2 'NonPipelined ('StSnd 'StIdle) m ()
-> Client PingPong2 'NonPipelined st' m ()
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a
       (st' :: ps).
(StateTokenI st, StateTokenI st', StateAgency st ~ 'ClientAgency,
 Outstanding pl ~ 'Z) =>
Message ps st st' -> Client ps pl st' m a -> Client ps pl st m a
Client.Yield Message PingPong2 st' ('StSnd 'StIdle)
Message PingPong2 ('StFst 'StIdle) ('StSnd 'StIdle)
forall ps (stIdle :: ps) ps' (stIdle' :: ps').
Message
  (Wedge ps stIdle ps' stIdle') ('StFst stIdle) ('StSnd stIdle')
MsgFstToSnd
  (Client PingPong2 'NonPipelined ('StSnd 'StIdle) m ()
 -> Client PingPong2 'NonPipelined st' m ())
-> Client PingPong2 'NonPipelined ('StSnd 'StIdle) m ()
-> Client PingPong2 'NonPipelined st' m ()
forall a b. (a -> b) -> a -> b
$ Message PingPong2 ('StSnd 'StIdle) ('StSnd 'StBusy)
-> Client PingPong2 'NonPipelined ('StSnd 'StBusy) m ()
-> Client PingPong2 'NonPipelined ('StSnd 'StIdle) m ()
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a
       (st' :: ps).
(StateTokenI st, StateTokenI st', StateAgency st ~ 'ClientAgency,
 Outstanding pl ~ 'Z) =>
Message ps st st' -> Client ps pl st' m a -> Client ps pl st m a
Client.Yield (Message PingPong 'StIdle 'StBusy
-> Message PingPong2 ('StSnd 'StIdle) ('StSnd 'StBusy)
forall ps' (st :: ps') (st' :: ps') ps (stIdle :: ps)
       (stIdle' :: ps').
Message ps' st st'
-> Message (Wedge ps stIdle ps' stIdle') ('StSnd st) ('StSnd st')
MsgSnd Message PingPong 'StIdle 'StBusy
PingPong.MsgPing)
  (Client PingPong2 'NonPipelined ('StSnd 'StBusy) m ()
 -> Client PingPong2 'NonPipelined ('StSnd 'StIdle) m ())
-> Client PingPong2 'NonPipelined ('StSnd 'StBusy) m ()
-> Client PingPong2 'NonPipelined ('StSnd 'StIdle) m ()
forall a b. (a -> b) -> a -> b
$ (forall (st' :: PingPong2).
 Message PingPong2 ('StSnd 'StBusy) st'
 -> Client PingPong2 'NonPipelined st' m ())
-> Client PingPong2 'NonPipelined ('StSnd 'StBusy) m ()
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
(StateTokenI st, StateAgency st ~ 'ServerAgency,
 Outstanding pl ~ 'Z) =>
(forall (st' :: ps). Message ps st st' -> Client ps pl st' m a)
-> Client ps pl st m a
Client.Await ((forall (st' :: PingPong2).
  Message PingPong2 ('StSnd 'StBusy) st'
  -> Client PingPong2 'NonPipelined st' m ())
 -> Client PingPong2 'NonPipelined ('StSnd 'StBusy) m ())
-> (forall (st' :: PingPong2).
    Message PingPong2 ('StSnd 'StBusy) st'
    -> Client PingPong2 'NonPipelined st' m ())
-> Client PingPong2 'NonPipelined ('StSnd 'StBusy) m ()
forall a b. (a -> b) -> a -> b
$ \(MsgSnd Message PingPong st st'
R:MessagePingPongfromto st st'
PingPong.MsgPong) ->
  -- terminate, through the second protocol
    Message PingPong2 st' ('StSnd 'StDone)
-> Client PingPong2 'NonPipelined ('StSnd 'StDone) m ()
-> Client PingPong2 'NonPipelined st' m ()
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a
       (st' :: ps).
(StateTokenI st, StateTokenI st', StateAgency st ~ 'ClientAgency,
 Outstanding pl ~ 'Z) =>
Message ps st st' -> Client ps pl st' m a -> Client ps pl st m a
Client.Yield (Message PingPong 'StIdle 'StDone
-> Message PingPong2 ('StSnd 'StIdle) ('StSnd 'StDone)
forall ps' (st :: ps') (st' :: ps') ps (stIdle :: ps)
       (stIdle' :: ps').
Message ps' st st'
-> Message (Wedge ps stIdle ps' stIdle') ('StSnd st) ('StSnd st')
MsgSnd Message PingPong 'StIdle 'StDone
PingPong.MsgDone)
  (Client PingPong2 'NonPipelined ('StSnd 'StDone) m ()
 -> Client PingPong2 'NonPipelined st' m ())
-> Client PingPong2 'NonPipelined ('StSnd 'StDone) m ()
-> Client PingPong2 'NonPipelined st' m ()
forall a b. (a -> b) -> a -> b
$ () -> Client PingPong2 'NonPipelined ('StSnd 'StDone) m ()
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
(StateTokenI st, StateAgency st ~ 'NobodyAgency,
 Outstanding pl ~ 'Z) =>
a -> Client ps pl st m a
Client.Done ()


pingPong2Client' :: forall m. Client.Client PingPong2 (Pipelined Client.Z ()) StIdle m ()
pingPong2Client' :: forall (m :: * -> *).
Client PingPong2 ('Pipelined 'Z ()) 'StIdle m ()
pingPong2Client' =
    --
    -- Pipeline first protocol
    --

      Message PingPong2 'StIdle ('StFst 'StIdle)
-> Receiver PingPong2 ('StFst 'StIdle) ('StFst 'StIdle) m ()
-> Client PingPong2 ('Pipelined ('S 'Z) ()) ('StFst 'StIdle) m ()
-> Client PingPong2 ('Pipelined 'Z ()) 'StIdle m ()
forall ps (st :: ps) (n :: N) c (m :: * -> *) a (st' :: ps)
       (st'' :: ps).
(StateTokenI st, StateTokenI st',
 StateAgency st ~ 'ClientAgency) =>
Message ps st st'
-> Receiver ps st' st'' m c
-> Client ps ('Pipelined ('S n) c) st'' m a
-> Client ps ('Pipelined n c) st m a
Client.YieldPipelined (SingStart ('StFst 'StIdle)
-> Message PingPong2 'StIdle ('StFst 'StIdle)
forall ps (stIdle :: ps) ps' (stIdle' :: ps')
       (st :: Wedge ps stIdle ps' stIdle').
SingStart st -> Message (Wedge ps stIdle ps' stIdle') 'StIdle st
MsgStart SingStart ('StFst 'StIdle)
forall {ps} {stIdle :: ps} {ps'} {stIdle' :: ps'} (st :: ps).
SingStart ('StFst st)
AtFst)
                            (() -> Receiver PingPong2 ('StFst 'StIdle) ('StFst 'StIdle) m ()
forall ps (stdone :: ps) (m :: * -> *) c.
c -> Receiver ps stdone stdone m c
Client.ReceiverDone ())
    (Client PingPong2 ('Pipelined ('S 'Z) ()) ('StFst 'StIdle) m ()
 -> Client PingPong2 ('Pipelined 'Z ()) 'StIdle m ())
-> Client PingPong2 ('Pipelined ('S 'Z) ()) ('StFst 'StIdle) m ()
-> Client PingPong2 ('Pipelined 'Z ()) 'StIdle m ()
forall a b. (a -> b) -> a -> b
$ Message PingPong2 ('StFst 'StIdle) ('StFst 'StBusy)
-> Receiver PingPong2 ('StFst 'StBusy) ('StFst 'StIdle) m ()
-> Client
     PingPong2 ('Pipelined ('S ('S 'Z)) ()) ('StFst 'StIdle) m ()
-> Client PingPong2 ('Pipelined ('S 'Z) ()) ('StFst 'StIdle) m ()
forall ps (st :: ps) (n :: N) c (m :: * -> *) a (st' :: ps)
       (st'' :: ps).
(StateTokenI st, StateTokenI st',
 StateAgency st ~ 'ClientAgency) =>
Message ps st st'
-> Receiver ps st' st'' m c
-> Client ps ('Pipelined ('S n) c) st'' m a
-> Client ps ('Pipelined n c) st m a
Client.YieldPipelined (Message PingPong 'StIdle 'StBusy
-> Message PingPong2 ('StFst 'StIdle) ('StFst 'StBusy)
forall ps (st :: ps) (st' :: ps) (stIdle :: ps) ps'
       (stIdle' :: ps').
Message ps st st'
-> Message (Wedge ps stIdle ps' stIdle') ('StFst st) ('StFst st')
MsgFst Message PingPong 'StIdle 'StBusy
PingPong.MsgPing)
                            ((forall (st' :: PingPong2).
 Message PingPong2 ('StFst 'StBusy) st'
 -> Receiver PingPong2 st' ('StFst 'StIdle) m ())
-> Receiver PingPong2 ('StFst 'StBusy) ('StFst 'StIdle) m ()
forall ps (st :: ps) (stdone :: ps) (m :: * -> *) c.
(StateTokenI st, ActiveState st, StateAgency st ~ 'ServerAgency) =>
(forall (st' :: ps).
 Message ps st st' -> Receiver ps st' stdone m c)
-> Receiver ps st stdone m c
Client.ReceiverAwait (\(MsgFst Message PingPong st st'
R:MessagePingPongfromto st st'
PingPong.MsgPong) -> () -> Receiver PingPong2 st' st' m ()
forall ps (stdone :: ps) (m :: * -> *) c.
c -> Receiver ps stdone stdone m c
Client.ReceiverDone ()))

    --
    -- Pipeline second protocol
    --

    (Client
   PingPong2 ('Pipelined ('S ('S 'Z)) ()) ('StFst 'StIdle) m ()
 -> Client PingPong2 ('Pipelined ('S 'Z) ()) ('StFst 'StIdle) m ())
-> Client
     PingPong2 ('Pipelined ('S ('S 'Z)) ()) ('StFst 'StIdle) m ()
-> Client PingPong2 ('Pipelined ('S 'Z) ()) ('StFst 'StIdle) m ()
forall a b. (a -> b) -> a -> b
$ Message PingPong2 ('StFst 'StIdle) ('StSnd 'StIdle)
-> Receiver PingPong2 ('StSnd 'StIdle) ('StSnd 'StIdle) m ()
-> Client
     PingPong2 ('Pipelined ('S ('S ('S 'Z))) ()) ('StSnd 'StIdle) m ()
-> Client
     PingPong2 ('Pipelined ('S ('S 'Z)) ()) ('StFst 'StIdle) m ()
forall ps (st :: ps) (n :: N) c (m :: * -> *) a (st' :: ps)
       (st'' :: ps).
(StateTokenI st, StateTokenI st',
 StateAgency st ~ 'ClientAgency) =>
Message ps st st'
-> Receiver ps st' st'' m c
-> Client ps ('Pipelined ('S n) c) st'' m a
-> Client ps ('Pipelined n c) st m a
Client.YieldPipelined Message PingPong2 ('StFst 'StIdle) ('StSnd 'StIdle)
forall ps (stIdle :: ps) ps' (stIdle' :: ps').
Message
  (Wedge ps stIdle ps' stIdle') ('StFst stIdle) ('StSnd stIdle')
MsgFstToSnd
                            (() -> Receiver PingPong2 ('StSnd 'StIdle) ('StSnd 'StIdle) m ()
forall ps (stdone :: ps) (m :: * -> *) c.
c -> Receiver ps stdone stdone m c
Client.ReceiverDone ())
    (Client
   PingPong2 ('Pipelined ('S ('S ('S 'Z))) ()) ('StSnd 'StIdle) m ()
 -> Client
      PingPong2 ('Pipelined ('S ('S 'Z)) ()) ('StFst 'StIdle) m ())
-> Client
     PingPong2 ('Pipelined ('S ('S ('S 'Z))) ()) ('StSnd 'StIdle) m ()
-> Client
     PingPong2 ('Pipelined ('S ('S 'Z)) ()) ('StFst 'StIdle) m ()
forall a b. (a -> b) -> a -> b
$ Message PingPong2 ('StSnd 'StIdle) ('StSnd 'StBusy)
-> Receiver PingPong2 ('StSnd 'StBusy) ('StSnd 'StIdle) m ()
-> Client
     PingPong2
     ('Pipelined ('S ('S ('S ('S 'Z)))) ())
     ('StSnd 'StIdle)
     m
     ()
-> Client
     PingPong2 ('Pipelined ('S ('S ('S 'Z))) ()) ('StSnd 'StIdle) m ()
forall ps (st :: ps) (n :: N) c (m :: * -> *) a (st' :: ps)
       (st'' :: ps).
(StateTokenI st, StateTokenI st',
 StateAgency st ~ 'ClientAgency) =>
Message ps st st'
-> Receiver ps st' st'' m c
-> Client ps ('Pipelined ('S n) c) st'' m a
-> Client ps ('Pipelined n c) st m a
Client.YieldPipelined (Message PingPong 'StIdle 'StBusy
-> Message PingPong2 ('StSnd 'StIdle) ('StSnd 'StBusy)
forall ps' (st :: ps') (st' :: ps') ps (stIdle :: ps)
       (stIdle' :: ps').
Message ps' st st'
-> Message (Wedge ps stIdle ps' stIdle') ('StSnd st) ('StSnd st')
MsgSnd Message PingPong 'StIdle 'StBusy
PingPong.MsgPing)
                            ((forall (st' :: PingPong2).
 Message PingPong2 ('StSnd 'StBusy) st'
 -> Receiver PingPong2 st' ('StSnd 'StIdle) m ())
-> Receiver PingPong2 ('StSnd 'StBusy) ('StSnd 'StIdle) m ()
forall ps (st :: ps) (stdone :: ps) (m :: * -> *) c.
(StateTokenI st, ActiveState st, StateAgency st ~ 'ServerAgency) =>
(forall (st' :: ps).
 Message ps st st' -> Receiver ps st' stdone m c)
-> Receiver ps st stdone m c
Client.ReceiverAwait (\(MsgSnd Message PingPong st st'
R:MessagePingPongfromto st st'
PingPong.MsgPong) -> () -> Receiver PingPong2 st' st' m ()
forall ps (stdone :: ps) (m :: * -> *) c.
c -> Receiver ps stdone stdone m c
Client.ReceiverDone ()))

    --
    -- Collect responses from the first protocol
    --

    (Client
   PingPong2
   ('Pipelined ('S ('S ('S ('S 'Z)))) ())
   ('StSnd 'StIdle)
   m
   ()
 -> Client
      PingPong2 ('Pipelined ('S ('S ('S 'Z))) ()) ('StSnd 'StIdle) m ())
-> Client
     PingPong2
     ('Pipelined ('S ('S ('S ('S 'Z)))) ())
     ('StSnd 'StIdle)
     m
     ()
-> Client
     PingPong2 ('Pipelined ('S ('S ('S 'Z))) ()) ('StSnd 'StIdle) m ()
forall a b. (a -> b) -> a -> b
$ Maybe
  (Client
     PingPong2
     ('Pipelined ('S ('S ('S ('S 'Z)))) ())
     ('StSnd 'StIdle)
     m
     ())
-> (()
    -> Client
         PingPong2 ('Pipelined ('S ('S ('S 'Z))) ()) ('StSnd 'StIdle) m ())
-> Client
     PingPong2
     ('Pipelined ('S ('S ('S ('S 'Z)))) ())
     ('StSnd 'StIdle)
     m
     ()
forall ps (st :: ps) (n :: N) c (m :: * -> *) a.
(StateTokenI st, ActiveState st) =>
Maybe (Client ps ('Pipelined ('S n) c) st m a)
-> (c -> Client ps ('Pipelined n c) st m a)
-> Client ps ('Pipelined ('S n) c) st m a
Client.Collect Maybe
  (Client
     PingPong2
     ('Pipelined ('S ('S ('S ('S 'Z)))) ())
     ('StSnd 'StIdle)
     m
     ())
forall a. Maybe a
Nothing ((()
  -> Client
       PingPong2 ('Pipelined ('S ('S ('S 'Z))) ()) ('StSnd 'StIdle) m ())
 -> Client
      PingPong2
      ('Pipelined ('S ('S ('S ('S 'Z)))) ())
      ('StSnd 'StIdle)
      m
      ())
-> (()
    -> Client
         PingPong2 ('Pipelined ('S ('S ('S 'Z))) ()) ('StSnd 'StIdle) m ())
-> Client
     PingPong2
     ('Pipelined ('S ('S ('S ('S 'Z)))) ())
     ('StSnd 'StIdle)
     m
     ()
forall a b. (a -> b) -> a -> b
$ \() -> -- collect transition pushed by `MsgStartFst`
      Maybe
  (Client
     PingPong2 ('Pipelined ('S ('S ('S 'Z))) ()) ('StSnd 'StIdle) m ())
-> (()
    -> Client
         PingPong2 ('Pipelined ('S ('S 'Z)) ()) ('StSnd 'StIdle) m ())
-> Client
     PingPong2 ('Pipelined ('S ('S ('S 'Z))) ()) ('StSnd 'StIdle) m ()
forall ps (st :: ps) (n :: N) c (m :: * -> *) a.
(StateTokenI st, ActiveState st) =>
Maybe (Client ps ('Pipelined ('S n) c) st m a)
-> (c -> Client ps ('Pipelined n c) st m a)
-> Client ps ('Pipelined ('S n) c) st m a
Client.Collect Maybe
  (Client
     PingPong2 ('Pipelined ('S ('S ('S 'Z))) ()) ('StSnd 'StIdle) m ())
forall a. Maybe a
Nothing ((()
  -> Client
       PingPong2 ('Pipelined ('S ('S 'Z)) ()) ('StSnd 'StIdle) m ())
 -> Client
      PingPong2 ('Pipelined ('S ('S ('S 'Z))) ()) ('StSnd 'StIdle) m ())
-> (()
    -> Client
         PingPong2 ('Pipelined ('S ('S 'Z)) ()) ('StSnd 'StIdle) m ())
-> Client
     PingPong2 ('Pipelined ('S ('S ('S 'Z))) ()) ('StSnd 'StIdle) m ()
forall a b. (a -> b) -> a -> b
$ \() -> -- collect reply received with `MsgFst MsgPong`

    --
    -- Collect responses from the second protocol
    --

      Maybe
  (Client
     PingPong2 ('Pipelined ('S ('S 'Z)) ()) ('StSnd 'StIdle) m ())
-> (()
    -> Client PingPong2 ('Pipelined ('S 'Z) ()) ('StSnd 'StIdle) m ())
-> Client
     PingPong2 ('Pipelined ('S ('S 'Z)) ()) ('StSnd 'StIdle) m ()
forall ps (st :: ps) (n :: N) c (m :: * -> *) a.
(StateTokenI st, ActiveState st) =>
Maybe (Client ps ('Pipelined ('S n) c) st m a)
-> (c -> Client ps ('Pipelined n c) st m a)
-> Client ps ('Pipelined ('S n) c) st m a
Client.Collect Maybe
  (Client
     PingPong2 ('Pipelined ('S ('S 'Z)) ()) ('StSnd 'StIdle) m ())
forall a. Maybe a
Nothing ((()
  -> Client PingPong2 ('Pipelined ('S 'Z) ()) ('StSnd 'StIdle) m ())
 -> Client
      PingPong2 ('Pipelined ('S ('S 'Z)) ()) ('StSnd 'StIdle) m ())
-> (()
    -> Client PingPong2 ('Pipelined ('S 'Z) ()) ('StSnd 'StIdle) m ())
-> Client
     PingPong2 ('Pipelined ('S ('S 'Z)) ()) ('StSnd 'StIdle) m ()
forall a b. (a -> b) -> a -> b
$ \() -> -- collect transition pushed by MsgFstToSnd
      Maybe
  (Client PingPong2 ('Pipelined ('S 'Z) ()) ('StSnd 'StIdle) m ())
-> (()
    -> Client PingPong2 ('Pipelined 'Z ()) ('StSnd 'StIdle) m ())
-> Client PingPong2 ('Pipelined ('S 'Z) ()) ('StSnd 'StIdle) m ()
forall ps (st :: ps) (n :: N) c (m :: * -> *) a.
(StateTokenI st, ActiveState st) =>
Maybe (Client ps ('Pipelined ('S n) c) st m a)
-> (c -> Client ps ('Pipelined n c) st m a)
-> Client ps ('Pipelined ('S n) c) st m a
Client.Collect Maybe
  (Client PingPong2 ('Pipelined ('S 'Z) ()) ('StSnd 'StIdle) m ())
forall a. Maybe a
Nothing ((() -> Client PingPong2 ('Pipelined 'Z ()) ('StSnd 'StIdle) m ())
 -> Client PingPong2 ('Pipelined ('S 'Z) ()) ('StSnd 'StIdle) m ())
-> (()
    -> Client PingPong2 ('Pipelined 'Z ()) ('StSnd 'StIdle) m ())
-> Client PingPong2 ('Pipelined ('S 'Z) ()) ('StSnd 'StIdle) m ()
forall a b. (a -> b) -> a -> b
$ \() -> -- collect reply received with `MsgSnd MsgPong`

    --
    -- Terminate the protocol
    --

      Message PingPong2 ('StSnd 'StIdle) ('StSnd 'StDone)
-> Client PingPong2 ('Pipelined 'Z ()) ('StSnd 'StDone) m ()
-> Client PingPong2 ('Pipelined 'Z ()) ('StSnd 'StIdle) m ()
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a
       (st' :: ps).
(StateTokenI st, StateTokenI st', StateAgency st ~ 'ClientAgency,
 Outstanding pl ~ 'Z) =>
Message ps st st' -> Client ps pl st' m a -> Client ps pl st m a
Client.Yield (Message PingPong 'StIdle 'StDone
-> Message PingPong2 ('StSnd 'StIdle) ('StSnd 'StDone)
forall ps' (st :: ps') (st' :: ps') ps (stIdle :: ps)
       (stIdle' :: ps').
Message ps' st st'
-> Message (Wedge ps stIdle ps' stIdle') ('StSnd st) ('StSnd st')
MsgSnd Message PingPong 'StIdle 'StDone
PingPong.MsgDone)
    (Client PingPong2 ('Pipelined 'Z ()) ('StSnd 'StDone) m ()
 -> Client PingPong2 ('Pipelined 'Z ()) ('StSnd 'StIdle) m ())
-> Client PingPong2 ('Pipelined 'Z ()) ('StSnd 'StDone) m ()
-> Client PingPong2 ('Pipelined 'Z ()) ('StSnd 'StIdle) m ()
forall a b. (a -> b) -> a -> b
$ () -> Client PingPong2 ('Pipelined 'Z ()) ('StSnd 'StDone) m ()
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
(StateTokenI st, StateAgency st ~ 'NobodyAgency,
 Outstanding pl ~ 'Z) =>
a -> Client ps pl st m a
Client.Done ()