{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
module Network.TypedProtocol.PingPong.Examples where
import Network.TypedProtocol.PingPong.Client
import Network.TypedProtocol.PingPong.Server
import Network.TypedProtocol.Peer.Client
pingPongServerStandard
:: Applicative m
=> PingPongServer m ()
pingPongServerStandard :: forall (m :: * -> *). Applicative m => PingPongServer m ()
pingPongServerStandard =
PingPongServer {
recvMsgPing :: m (PingPongServer m ())
recvMsgPing = PingPongServer m () -> m (PingPongServer m ())
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure PingPongServer m ()
forall (m :: * -> *). Applicative m => PingPongServer m ()
pingPongServerStandard,
recvMsgDone :: ()
recvMsgDone = ()
}
pingPongServerCount
:: Applicative m
=> PingPongServer m Int
pingPongServerCount :: forall (m :: * -> *). Applicative m => PingPongServer m Int
pingPongServerCount = Int -> PingPongServer m Int
forall {m :: * -> *} {a}.
(Applicative m, Enum a) =>
a -> PingPongServer m a
go Int
0
where
go :: a -> PingPongServer m a
go !a
c = PingPongServer {
recvMsgPing :: m (PingPongServer m a)
recvMsgPing = PingPongServer m a -> m (PingPongServer m a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PingPongServer m a -> m (PingPongServer m a))
-> PingPongServer m a -> m (PingPongServer m a)
forall a b. (a -> b) -> a -> b
$ a -> PingPongServer m a
go (a -> a
forall a. Enum a => a -> a
succ a
c),
recvMsgDone :: a
recvMsgDone = a
c
}
pingPongClientFlood :: Applicative m => PingPongClient m a
pingPongClientFlood :: forall (m :: * -> *) a. Applicative m => PingPongClient m a
pingPongClientFlood = m (PingPongClient m a) -> PingPongClient m a
forall (m :: * -> *) a.
m (PingPongClient m a) -> PingPongClient m a
SendMsgPing (PingPongClient m a -> m (PingPongClient m a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure PingPongClient m a
forall (m :: * -> *) a. Applicative m => PingPongClient m a
pingPongClientFlood)
pingPongClientCount :: Applicative m => Int -> PingPongClient m ()
pingPongClientCount :: forall (m :: * -> *). Applicative m => Int -> PingPongClient m ()
pingPongClientCount Int
0 = () -> PingPongClient m ()
forall a (m :: * -> *). a -> PingPongClient m a
SendMsgDone ()
pingPongClientCount Int
n = m (PingPongClient m ()) -> PingPongClient m ()
forall (m :: * -> *) a.
m (PingPongClient m a) -> PingPongClient m a
SendMsgPing (PingPongClient m () -> m (PingPongClient m ())
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> PingPongClient m ()
forall (m :: * -> *). Applicative m => Int -> PingPongClient m ()
pingPongClientCount (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)))
pingPongClientPipelinedMax
:: forall m. Monad m
=> Int
-> PingPongClientPipelined Int m [Either Int Int]
pingPongClientPipelinedMax :: forall (m :: * -> *).
Monad m =>
Int -> PingPongClientPipelined Int m [Either Int Int]
pingPongClientPipelinedMax Int
c =
PingPongClientIdle 'Z Int m [Either Int Int]
-> PingPongClientPipelined Int m [Either Int Int]
forall c (m :: * -> *) a.
PingPongClientIdle 'Z c m a -> PingPongClientPipelined c m a
PingPongClientPipelined ([Either Int Int]
-> Nat 'Z -> Int -> PingPongClientIdle 'Z Int m [Either Int Int]
forall (o :: N).
[Either Int Int]
-> Nat o -> Int -> PingPongClientIdle o Int m [Either Int Int]
go [] Nat 'Z
forall (n :: N). ('Z ~ n) => Nat n
Zero Int
0)
where
go :: [Either Int Int] -> Nat o -> Int
-> PingPongClientIdle o Int m [Either Int Int]
go :: forall (o :: N).
[Either Int Int]
-> Nat o -> Int -> PingPongClientIdle o Int m [Either Int Int]
go [Either Int Int]
acc Nat o
o Int
n | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
c
= m Int
-> PingPongClientIdle ('S o) Int m [Either Int Int]
-> PingPongClientIdle o Int m [Either Int Int]
forall (m :: * -> *) c (n :: N) a.
m c
-> PingPongClientIdle ('S n) c m a -> PingPongClientIdle n c m a
SendMsgPingPipelined
(Int -> m Int
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
n)
([Either Int Int]
-> Nat ('S o)
-> Int
-> PingPongClientIdle ('S o) Int m [Either Int Int]
forall (o :: N).
[Either Int Int]
-> Nat o -> Int -> PingPongClientIdle o Int m [Either Int Int]
go (Int -> Either Int Int
forall a b. a -> Either a b
Left Int
n Either Int Int -> [Either Int Int] -> [Either Int Int]
forall a. a -> [a] -> [a]
: [Either Int Int]
acc) (Nat o -> Nat ('S o)
forall (m :: N) (n :: N). (m ~ 'S n) => Nat n -> Nat m
Succ Nat o
o) (Int -> Int
forall a. Enum a => a -> a
succ Int
n))
go [Either Int Int]
acc Nat o
Zero Int
_ = [Either Int Int] -> PingPongClientIdle 'Z Int m [Either Int Int]
forall a c (m :: * -> *). a -> PingPongClientIdle 'Z c m a
SendMsgDonePipelined ([Either Int Int] -> [Either Int Int]
forall a. [a] -> [a]
reverse [Either Int Int]
acc)
go [Either Int Int]
acc (Succ Nat n
o) Int
n = Maybe (PingPongClientIdle ('S n) Int m [Either Int Int])
-> (Int -> PingPongClientIdle n Int m [Either Int Int])
-> PingPongClientIdle ('S n) Int m [Either Int Int]
forall (n1 :: N) c (m :: * -> *) a.
Maybe (PingPongClientIdle ('S n1) c m a)
-> (c -> PingPongClientIdle n1 c m a)
-> PingPongClientIdle ('S n1) c m a
CollectPipelined
Maybe (PingPongClientIdle ('S n) Int m [Either Int Int])
forall a. Maybe a
Nothing
(\Int
n' -> [Either Int Int]
-> Nat n -> Int -> PingPongClientIdle n Int m [Either Int Int]
forall (o :: N).
[Either Int Int]
-> Nat o -> Int -> PingPongClientIdle o Int m [Either Int Int]
go (Int -> Either Int Int
forall a b. b -> Either a b
Right Int
n' Either Int Int -> [Either Int Int] -> [Either Int Int]
forall a. a -> [a] -> [a]
: [Either Int Int]
acc) Nat n
o Int
n)
pingPongClientPipelinedMin
:: forall m. Monad m
=> Int
-> PingPongClientPipelined Int m [Either Int Int]
pingPongClientPipelinedMin :: forall (m :: * -> *).
Monad m =>
Int -> PingPongClientPipelined Int m [Either Int Int]
pingPongClientPipelinedMin Int
c =
PingPongClientIdle 'Z Int m [Either Int Int]
-> PingPongClientPipelined Int m [Either Int Int]
forall c (m :: * -> *) a.
PingPongClientIdle 'Z c m a -> PingPongClientPipelined c m a
PingPongClientPipelined ([Either Int Int]
-> Nat 'Z -> Int -> PingPongClientIdle 'Z Int m [Either Int Int]
forall (o :: N).
[Either Int Int]
-> Nat o -> Int -> PingPongClientIdle o Int m [Either Int Int]
go [] Nat 'Z
forall (n :: N). ('Z ~ n) => Nat n
Zero Int
0)
where
go :: [Either Int Int] -> Nat o -> Int
-> PingPongClientIdle o Int m [Either Int Int]
go :: forall (o :: N).
[Either Int Int]
-> Nat o -> Int -> PingPongClientIdle o Int m [Either Int Int]
go [Either Int Int]
acc (Succ Nat n
o) Int
n = Maybe (PingPongClientIdle ('S n) Int m [Either Int Int])
-> (Int -> PingPongClientIdle n Int m [Either Int Int])
-> PingPongClientIdle ('S n) Int m [Either Int Int]
forall (n1 :: N) c (m :: * -> *) a.
Maybe (PingPongClientIdle ('S n1) c m a)
-> (c -> PingPongClientIdle n1 c m a)
-> PingPongClientIdle ('S n1) c m a
CollectPipelined
(if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
c then PingPongClientIdle ('S n) Int m [Either Int Int]
-> Maybe (PingPongClientIdle ('S n) Int m [Either Int Int])
forall a. a -> Maybe a
Just ([Either Int Int]
-> Nat ('S n)
-> Int
-> PingPongClientIdle ('S n) Int m [Either Int Int]
forall (o :: N).
[Either Int Int]
-> Nat o -> Int -> PingPongClientIdle o Int m [Either Int Int]
ping [Either Int Int]
acc (Nat n -> Nat ('S n)
forall (m :: N) (n :: N). (m ~ 'S n) => Nat n -> Nat m
Succ Nat n
o) Int
n)
else Maybe (PingPongClientIdle ('S n) Int m [Either Int Int])
forall a. Maybe a
Nothing)
(\Int
n' -> [Either Int Int]
-> Nat n -> Int -> PingPongClientIdle n Int m [Either Int Int]
forall (o :: N).
[Either Int Int]
-> Nat o -> Int -> PingPongClientIdle o Int m [Either Int Int]
go (Int -> Either Int Int
forall a b. b -> Either a b
Right Int
n' Either Int Int -> [Either Int Int] -> [Either Int Int]
forall a. a -> [a] -> [a]
: [Either Int Int]
acc) Nat n
o Int
n)
go [Either Int Int]
acc Nat o
Zero Int
n | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
c
= [Either Int Int]
-> Nat o -> Int -> PingPongClientIdle o Int m [Either Int Int]
forall (o :: N).
[Either Int Int]
-> Nat o -> Int -> PingPongClientIdle o Int m [Either Int Int]
ping [Either Int Int]
acc Nat o
forall (n :: N). ('Z ~ n) => Nat n
Zero Int
n
go [Either Int Int]
acc Nat o
Zero Int
_ = [Either Int Int] -> PingPongClientIdle 'Z Int m [Either Int Int]
forall a c (m :: * -> *). a -> PingPongClientIdle 'Z c m a
SendMsgDonePipelined ([Either Int Int] -> [Either Int Int]
forall a. [a] -> [a]
reverse [Either Int Int]
acc)
ping :: [Either Int Int] -> Nat o -> Int
-> PingPongClientIdle o Int m [Either Int Int]
ping :: forall (o :: N).
[Either Int Int]
-> Nat o -> Int -> PingPongClientIdle o Int m [Either Int Int]
ping [Either Int Int]
acc Nat o
o Int
n = m Int
-> PingPongClientIdle ('S o) Int m [Either Int Int]
-> PingPongClientIdle o Int m [Either Int Int]
forall (m :: * -> *) c (n :: N) a.
m c
-> PingPongClientIdle ('S n) c m a -> PingPongClientIdle n c m a
SendMsgPingPipelined
(Int -> m Int
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
n)
([Either Int Int]
-> Nat ('S o)
-> Int
-> PingPongClientIdle ('S o) Int m [Either Int Int]
forall (o :: N).
[Either Int Int]
-> Nat o -> Int -> PingPongClientIdle o Int m [Either Int Int]
go (Int -> Either Int Int
forall a b. a -> Either a b
Left Int
n Either Int Int -> [Either Int Int] -> [Either Int Int]
forall a. a -> [a] -> [a]
: [Either Int Int]
acc) (Nat o -> Nat ('S o)
forall (m :: N) (n :: N). (m ~ 'S n) => Nat n -> Nat m
Succ Nat o
o) (Int -> Int
forall a. Enum a => a -> a
succ Int
n))
pingPongClientPipelinedLimited
:: forall m. Monad m
=> Int -> Int
-> PingPongClientPipelined Int m [Either Int Int]
pingPongClientPipelinedLimited :: forall (m :: * -> *).
Monad m =>
Int -> Int -> PingPongClientPipelined Int m [Either Int Int]
pingPongClientPipelinedLimited Int
omax Int
c =
PingPongClientIdle 'Z Int m [Either Int Int]
-> PingPongClientPipelined Int m [Either Int Int]
forall c (m :: * -> *) a.
PingPongClientIdle 'Z c m a -> PingPongClientPipelined c m a
PingPongClientPipelined ([Either Int Int]
-> Nat 'Z -> Int -> PingPongClientIdle 'Z Int m [Either Int Int]
forall (o :: N).
[Either Int Int]
-> Nat o -> Int -> PingPongClientIdle o Int m [Either Int Int]
go [] Nat 'Z
forall (n :: N). ('Z ~ n) => Nat n
Zero Int
0)
where
go :: [Either Int Int] -> Nat o -> Int
-> PingPongClientIdle o Int m [Either Int Int]
go :: forall (o :: N).
[Either Int Int]
-> Nat o -> Int -> PingPongClientIdle o Int m [Either Int Int]
go [Either Int Int]
acc (Succ Nat n
o) Int
n = Maybe (PingPongClientIdle ('S n) Int m [Either Int Int])
-> (Int -> PingPongClientIdle n Int m [Either Int Int])
-> PingPongClientIdle ('S n) Int m [Either Int Int]
forall (n1 :: N) c (m :: * -> *) a.
Maybe (PingPongClientIdle ('S n1) c m a)
-> (c -> PingPongClientIdle n1 c m a)
-> PingPongClientIdle ('S n1) c m a
CollectPipelined
(if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
c Bool -> Bool -> Bool
&& Nat ('S n) -> Int
forall (n :: N). Nat n -> Int
int (Nat n -> Nat ('S n)
forall (m :: N) (n :: N). (m ~ 'S n) => Nat n -> Nat m
Succ Nat n
o) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
omax
then PingPongClientIdle ('S n) Int m [Either Int Int]
-> Maybe (PingPongClientIdle ('S n) Int m [Either Int Int])
forall a. a -> Maybe a
Just ([Either Int Int]
-> Nat ('S n)
-> Int
-> PingPongClientIdle ('S n) Int m [Either Int Int]
forall (o :: N).
[Either Int Int]
-> Nat o -> Int -> PingPongClientIdle o Int m [Either Int Int]
ping [Either Int Int]
acc (Nat n -> Nat ('S n)
forall (m :: N) (n :: N). (m ~ 'S n) => Nat n -> Nat m
Succ Nat n
o) Int
n)
else Maybe (PingPongClientIdle ('S n) Int m [Either Int Int])
forall a. Maybe a
Nothing)
(\Int
n' -> [Either Int Int]
-> Nat n -> Int -> PingPongClientIdle n Int m [Either Int Int]
forall (o :: N).
[Either Int Int]
-> Nat o -> Int -> PingPongClientIdle o Int m [Either Int Int]
go (Int -> Either Int Int
forall a b. b -> Either a b
Right Int
n' Either Int Int -> [Either Int Int] -> [Either Int Int]
forall a. a -> [a] -> [a]
: [Either Int Int]
acc) Nat n
o Int
n)
go [Either Int Int]
acc Nat o
Zero Int
n | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
c
= [Either Int Int]
-> Nat o -> Int -> PingPongClientIdle o Int m [Either Int Int]
forall (o :: N).
[Either Int Int]
-> Nat o -> Int -> PingPongClientIdle o Int m [Either Int Int]
ping [Either Int Int]
acc Nat o
forall (n :: N). ('Z ~ n) => Nat n
Zero Int
n
go [Either Int Int]
acc Nat o
Zero Int
_ = [Either Int Int] -> PingPongClientIdle 'Z Int m [Either Int Int]
forall a c (m :: * -> *). a -> PingPongClientIdle 'Z c m a
SendMsgDonePipelined ([Either Int Int] -> [Either Int Int]
forall a. [a] -> [a]
reverse [Either Int Int]
acc)
ping :: [Either Int Int] -> Nat o -> Int
-> PingPongClientIdle o Int m [Either Int Int]
ping :: forall (o :: N).
[Either Int Int]
-> Nat o -> Int -> PingPongClientIdle o Int m [Either Int Int]
ping [Either Int Int]
acc Nat o
o Int
n = m Int
-> PingPongClientIdle ('S o) Int m [Either Int Int]
-> PingPongClientIdle o Int m [Either Int Int]
forall (m :: * -> *) c (n :: N) a.
m c
-> PingPongClientIdle ('S n) c m a -> PingPongClientIdle n c m a
SendMsgPingPipelined
(Int -> m Int
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
n)
([Either Int Int]
-> Nat ('S o)
-> Int
-> PingPongClientIdle ('S o) Int m [Either Int Int]
forall (o :: N).
[Either Int Int]
-> Nat o -> Int -> PingPongClientIdle o Int m [Either Int Int]
go (Int -> Either Int Int
forall a b. a -> Either a b
Left Int
n Either Int Int -> [Either Int Int] -> [Either Int Int]
forall a. a -> [a] -> [a]
: [Either Int Int]
acc) (Nat o -> Nat ('S o)
forall (m :: N) (n :: N). (m ~ 'S n) => Nat n -> Nat m
Succ Nat o
o) (Int -> Int
forall a. Enum a => a -> a
succ Int
n))
int :: Nat n -> Int
int :: forall (n :: N). Nat n -> Int
int Nat n
Zero = Int
0
int (Succ Nat n
n) = Int -> Int
forall a. Enum a => a -> a
succ (Nat n -> Int
forall (n :: N). Nat n -> Int
int Nat n
n)