{-# LANGUAGE BangPatterns        #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}



module Network.TypedProtocol.ReqResp2.Client where

import           Network.TypedProtocol.ReqResp2.Type

import           Network.TypedProtocol.Core
import           Network.TypedProtocol.Peer.Client


reqResp2Client :: forall req resp m.
                  ()
               => [Either req req]
               -> Client (ReqResp2 req resp) (Pipelined Z (Either resp resp)) StIdle m [Either resp resp]
reqResp2Client :: forall req resp (m :: * -> *).
[Either req req]
-> Client
     (ReqResp2 req resp)
     ('Pipelined 'Z (Either resp resp))
     'StIdle
     m
     [Either resp resp]
reqResp2Client = Nat 'Z
-> [Either req req]
-> Client
     (ReqResp2 req resp)
     ('Pipelined 'Z (Either resp resp))
     'StIdle
     m
     [Either resp resp]
forall (n :: N).
Nat n
-> [Either req req]
-> Client
     (ReqResp2 req resp)
     ('Pipelined n (Either resp resp))
     'StIdle
     m
     [Either resp resp]
send Nat 'Z
forall (n :: N). ('Z ~ n) => Nat n
Zero
  where
    -- pipeline all the requests, either through `MsgReq` or `MsgReq'`.
    send :: forall (n :: N).
            Nat n
         -> [Either req req] -- requests to send
         -> Client (ReqResp2 req resp) (Pipelined  n (Either resp resp)) StIdle m [Either resp resp]

    send :: forall (n :: N).
Nat n
-> [Either req req]
-> Client
     (ReqResp2 req resp)
     ('Pipelined n (Either resp resp))
     'StIdle
     m
     [Either resp resp]
send !Nat n
n (Left req
req : [Either req req]
reqs) =
      Message (ReqResp2 req resp) 'StIdle 'StBusy
-> Receiver
     (ReqResp2 req resp) 'StBusy 'StIdle m (Either resp resp)
-> Client
     (ReqResp2 req resp)
     ('Pipelined ('S n) (Either resp resp))
     'StIdle
     m
     [Either resp resp]
-> Client
     (ReqResp2 req resp)
     ('Pipelined n (Either resp resp))
     'StIdle
     m
     [Either resp resp]
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
YieldPipelined (req -> Message (ReqResp2 req resp) 'StIdle 'StBusy
forall {k1} req1 (resp :: k1).
req1 -> Message (ReqResp2 req1 resp) 'StIdle 'StBusy
MsgReq  req
req) Receiver (ReqResp2 req resp) 'StBusy 'StIdle m (Either resp resp)
receiver (Nat ('S n)
-> [Either req req]
-> Client
     (ReqResp2 req resp)
     ('Pipelined ('S n) (Either resp resp))
     'StIdle
     m
     [Either resp resp]
forall (n :: N).
Nat n
-> [Either req req]
-> Client
     (ReqResp2 req resp)
     ('Pipelined n (Either resp resp))
     'StIdle
     m
     [Either resp resp]
send (Nat n -> Nat ('S n)
forall (m :: N) (n :: N). (m ~ 'S n) => Nat n -> Nat m
Succ Nat n
n) [Either req req]
reqs)

    send !Nat n
n (Right req
req : [Either req req]
reqs) =
      Message (ReqResp2 req resp) 'StIdle 'StBusy'
-> Receiver
     (ReqResp2 req resp) 'StBusy' 'StIdle m (Either resp resp)
-> Client
     (ReqResp2 req resp)
     ('Pipelined ('S n) (Either resp resp))
     'StIdle
     m
     [Either resp resp]
-> Client
     (ReqResp2 req resp)
     ('Pipelined n (Either resp resp))
     'StIdle
     m
     [Either resp resp]
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
YieldPipelined (req -> Message (ReqResp2 req resp) 'StIdle 'StBusy'
forall {k1} req1 (resp :: k1).
req1 -> Message (ReqResp2 req1 resp) 'StIdle 'StBusy'
MsgReq' req
req) Receiver (ReqResp2 req resp) 'StBusy' 'StIdle m (Either resp resp)
receiver' (Nat ('S n)
-> [Either req req]
-> Client
     (ReqResp2 req resp)
     ('Pipelined ('S n) (Either resp resp))
     'StIdle
     m
     [Either resp resp]
forall (n :: N).
Nat n
-> [Either req req]
-> Client
     (ReqResp2 req resp)
     ('Pipelined n (Either resp resp))
     'StIdle
     m
     [Either resp resp]
send (Nat n -> Nat ('S n)
forall (m :: N) (n :: N). (m ~ 'S n) => Nat n -> Nat m
Succ Nat n
n) [Either req req]
reqs)

    send !Nat n
n [] = Nat n
-> [Either resp resp]
-> Client
     (ReqResp2 req resp)
     ('Pipelined n (Either resp resp))
     'StIdle
     m
     [Either resp resp]
forall (n :: N).
Nat n
-> [Either resp resp]
-> Client
     (ReqResp2 req resp)
     ('Pipelined n (Either resp resp))
     'StIdle
     m
     [Either resp resp]
collect Nat n
n []


    receiver :: Receiver (ReqResp2 req resp) StBusy StIdle m (Either resp resp)
    receiver :: Receiver (ReqResp2 req resp) 'StBusy 'StIdle m (Either resp resp)
receiver = (forall (st' :: ReqResp2 req resp).
 Message (ReqResp2 req resp) 'StBusy st'
 -> Receiver (ReqResp2 req resp) st' 'StIdle m (Either resp resp))
-> Receiver
     (ReqResp2 req resp) 'StBusy 'StIdle m (Either resp resp)
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
ReceiverAwait (\(MsgResp resp1
resp) -> Either resp resp
-> Receiver (ReqResp2 req resp) st' st' m (Either resp resp)
forall ps (stdone :: ps) (m :: * -> *) c.
c -> Receiver ps stdone stdone m c
ReceiverDone (resp -> Either resp resp
forall a b. a -> Either a b
Left resp
resp1
resp))


    receiver' :: Receiver (ReqResp2 req resp) StBusy' StIdle m (Either resp resp)
    receiver' :: Receiver (ReqResp2 req resp) 'StBusy' 'StIdle m (Either resp resp)
receiver' = (forall (st' :: ReqResp2 req resp).
 Message (ReqResp2 req resp) 'StBusy' st'
 -> Receiver (ReqResp2 req resp) st' 'StIdle m (Either resp resp))
-> Receiver
     (ReqResp2 req resp) 'StBusy' 'StIdle m (Either resp resp)
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
ReceiverAwait (\(MsgResp' resp1
resp) -> Either resp resp
-> Receiver (ReqResp2 req resp) st' st' m (Either resp resp)
forall ps (stdone :: ps) (m :: * -> *) c.
c -> Receiver ps stdone stdone m c
ReceiverDone (resp -> Either resp resp
forall a b. b -> Either a b
Right resp
resp1
resp))


    -- collect all the responses
    collect :: Nat n
            -> [Either resp resp] -- all the responses received so far
            -> Client (ReqResp2 req resp) (Pipelined n (Either resp resp)) StIdle m [Either resp resp]

    collect :: forall (n :: N).
Nat n
-> [Either resp resp]
-> Client
     (ReqResp2 req resp)
     ('Pipelined n (Either resp resp))
     'StIdle
     m
     [Either resp resp]
collect Nat n
Zero ![Either resp resp]
resps = Message (ReqResp2 req resp) 'StIdle 'StDone
-> Client
     (ReqResp2 req resp)
     ('Pipelined n (Either resp resp))
     'StDone
     m
     [Either resp resp]
-> Client
     (ReqResp2 req resp)
     ('Pipelined n (Either resp resp))
     'StIdle
     m
     [Either resp resp]
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
Yield Message (ReqResp2 req resp) 'StIdle 'StDone
forall {k} {k1} (req :: k) (resp :: k1).
Message (ReqResp2 req resp) 'StIdle 'StDone
MsgDone ([Either resp resp]
-> Client
     (ReqResp2 req resp)
     ('Pipelined n (Either resp resp))
     'StDone
     m
     [Either resp resp]
forall ps (pl :: IsPipelined) (st :: ps) (m :: * -> *) a.
(StateTokenI st, StateAgency st ~ 'NobodyAgency,
 Outstanding pl ~ 'Z) =>
a -> Client ps pl st m a
Done ([Either resp resp] -> [Either resp resp]
forall a. [a] -> [a]
reverse [Either resp resp]
resps))

    collect (Succ Nat n
n) ![Either resp resp]
resps =
      Maybe
  (Client
     (ReqResp2 req resp)
     ('Pipelined ('S n) (Either resp resp))
     'StIdle
     m
     [Either resp resp])
-> (Either resp resp
    -> Client
         (ReqResp2 req resp)
         ('Pipelined n (Either resp resp))
         'StIdle
         m
         [Either resp resp])
-> Client
     (ReqResp2 req resp)
     ('Pipelined ('S n) (Either resp resp))
     'StIdle
     m
     [Either resp resp]
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
Collect Maybe
  (Client
     (ReqResp2 req resp)
     ('Pipelined ('S n) (Either resp resp))
     'StIdle
     m
     [Either resp resp])
forall a. Maybe a
Nothing ((Either resp resp
  -> Client
       (ReqResp2 req resp)
       ('Pipelined n (Either resp resp))
       'StIdle
       m
       [Either resp resp])
 -> Client
      (ReqResp2 req resp)
      ('Pipelined ('S n) (Either resp resp))
      'StIdle
      m
      [Either resp resp])
-> (Either resp resp
    -> Client
         (ReqResp2 req resp)
         ('Pipelined n (Either resp resp))
         'StIdle
         m
         [Either resp resp])
-> Client
     (ReqResp2 req resp)
     ('Pipelined ('S n) (Either resp resp))
     'StIdle
     m
     [Either resp resp]
forall a b. (a -> b) -> a -> b
$ \Either resp resp
c  -> Nat n
-> [Either resp resp]
-> Client
     (ReqResp2 req resp)
     ('Pipelined n (Either resp resp))
     'StIdle
     m
     [Either resp resp]
forall (n :: N).
Nat n
-> [Either resp resp]
-> Client
     (ReqResp2 req resp)
     ('Pipelined n (Either resp resp))
     'StIdle
     m
     [Either resp resp]
collect Nat n
n (Either resp resp
c Either resp resp -> [Either resp resp] -> [Either resp resp]
forall a. a -> [a] -> [a]
: [Either resp resp]
resps)