Skip to content

Commit fa0cc09

Browse files
cootcoot
committed
reqresp: example client & server
1 parent 5cbf746 commit fa0cc09

File tree

6 files changed

+395
-1
lines changed

6 files changed

+395
-1
lines changed

‎typed-protocols/examples/Network/TypedProtocol/ReqResp3/Client.hs‎

Lines changed: 111 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,111 @@
1+
{-# LANGUAGE ScopedTypeVariables #-}
2+
3+
module Network.TypedProtocol.ReqResp3.Client
4+
( clientPeer
5+
, clientPeer2
6+
) where
7+
8+
import Control.Monad (void)
9+
import Control.Concurrent.Class.MonadSTM.Strict
10+
11+
import Network.TypedProtocol.ReqResp
12+
import Network.TypedProtocol.ReqResp3.Type
13+
14+
data Result = ResInt Int | ResFib Int | ResStr String
15+
deriving (Show, Eq)
16+
17+
-- | A client which sends:
18+
--
19+
-- * m `ReqInt` requests, then
20+
-- * n `ReqFib` requests, then
21+
-- * o `ReqStr` requests.
22+
--
23+
clientPeer
24+
:: forall m. MonadSTM m
25+
=> Int
26+
-> Int
27+
-> Int
28+
-> Peer ReqType (AsClient Running) m [Result]
29+
clientPeer m0 n0 o0 = Effect $ clientInt m0 <$> newTVarIO []
30+
where
31+
clientInt
32+
:: Int
33+
-> StrictTVar m [Result]
34+
-> Peer ReqType (AsClient Running) m [Result]
35+
clientInt m v
36+
| m > 0
37+
= SendRequest
38+
MsgRequestInt
39+
(\case MsgResponseInt a -> void $ atomically $ modifyTVar v (ResInt a:))
40+
(clientInt (m - 1) v)
41+
| otherwise
42+
=
43+
clientFib n0 v
44+
45+
clientFib
46+
:: Int
47+
-> StrictTVar m [Result]
48+
-> Peer ReqType (AsClient Running) m [Result]
49+
clientFib m v
50+
| m > 0
51+
= SendRequest
52+
MsgRequestFib
53+
(\case MsgResponseFib a -> void $ atomically $ modifyTVar v (ResFib a:))
54+
(clientFib (m - 1) v)
55+
| otherwise
56+
= clientStr o0 v
57+
58+
clientStr
59+
:: Int
60+
-> StrictTVar m [Result]
61+
-> Peer ReqType (AsClient Running) m [Result]
62+
clientStr m v
63+
| m > 0
64+
= SendRequest
65+
MsgRequestStr
66+
(\case MsgResponseStr a -> void $ atomically $ modifyTVar v (ResStr a:))
67+
(clientStr (m - 1) v)
68+
| otherwise
69+
= clientTerminated v
70+
71+
clientTerminated
72+
:: StrictTVar m [Result]
73+
-> Peer ReqType (AsClient Running) m [Result]
74+
clientTerminated v =
75+
SendRequestDone
76+
MsgDone
77+
(Effect $ ClientDone <$> readTVarIO v)
78+
79+
80+
-- | A client which sends m batches of three requests: `ReqStr`, `ReqFib`,
81+
-- `ReqInt`.
82+
--
83+
clientPeer2
84+
:: forall m. MonadSTM m
85+
=> Int
86+
-> Peer ReqType (AsClient Running) m [Result]
87+
clientPeer2 m0 = Effect $ clientLoop m0 <$> newTVarIO []
88+
where
89+
clientLoop
90+
:: Int
91+
-> StrictTVar m [Result]
92+
-> Peer ReqType (AsClient Running) m [Result]
93+
clientLoop m v | m > 1 =
94+
SendRequest
95+
MsgRequestStr
96+
(\case MsgResponseStr s -> void $ atomically $ modifyTVar v (ResStr s :))
97+
$ SendRequest
98+
MsgRequestFib
99+
(\case MsgResponseFib f -> void $ atomically $ modifyTVar v (ResFib f :))
100+
$ SendRequest
101+
MsgRequestInt
102+
(\case MsgResponseInt i -> void $ atomically $ modifyTVar v (ResInt i :))
103+
(clientLoop (m - 1) v)
104+
105+
| otherwise
106+
= clientTerminated v
107+
108+
clientTerminated
109+
:: StrictTVar m [Result]
110+
-> Peer ReqType (AsClient Running) m [Result]
111+
clientTerminated v = Effect $ SendRequestDone MsgDone . ClientDone <$> readTVarIO v

‎typed-protocols/examples/Network/TypedProtocol/ReqResp3/Examples.hs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
module Network.TypedProtocol.ReqResp3.Examples where

‎typed-protocols/examples/Network/TypedProtocol/ReqResp3/Server.hs‎

Lines changed: 235 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,235 @@
1+
{-# LANGUAGE TypeOperators #-}
2+
3+
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
4+
5+
module Network.TypedProtocol.ReqResp3.Server where
6+
7+
import Prelude hiding (lookup)
8+
import Data.Type.NatMap
9+
import Network.TypedProtocol.ReqResp
10+
import Network.TypedProtocol.ReqResp3.Type
11+
12+
13+
-- | A server which collects all requests until the terminal request is sent,
14+
-- then responds to all `ReqInt` and then to all `ReqPrime` and finally all
15+
-- `ReqStr` requests.
16+
serverPeerMax
17+
:: forall m. Peer ReqType (AsServer Empty) m ()
18+
serverPeerMax =
19+
serverAwaitLoop SingEmpty
20+
where
21+
serverAwaitLoop
22+
:: forall (q :: NatMap (State ReqType)).
23+
Lookup Terminal q ~ Z
24+
=> SingNatMap q
25+
-> Peer ReqType (AsServer q) m ()
26+
serverAwaitLoop q =
27+
AwaitRequest $ \case
28+
MsgRequestInt ->
29+
case ( increment (SingActive SingReqInt) q
30+
-- Lookup Terminal (Increment (Active ReqInt) q) ≡ Lookup Terminal q
31+
, incrementLemma (\case{}) (SingActive SingReqInt) SingTerminal q
32+
) of
33+
(q', Refl) -> serverAwaitLoop q'
34+
MsgRequestFib ->
35+
case ( increment (SingActive SingReqFib) q
36+
, incrementLemma (\case{}) (SingActive SingReqFib) SingTerminal q
37+
) of
38+
(q', Refl) -> serverAwaitLoop q'
39+
MsgRequestStr ->
40+
case ( increment (SingActive SingReqStr) q
41+
-- Lookup Terminal (Increment (Active ReqStr) q) ≡ Lookup Terminal q
42+
, incrementLemma (\case{}) (SingActive SingReqStr) SingTerminal q
43+
) of
44+
(q', Refl) -> serverAwaitLoop q'
45+
MsgDone ->
46+
case ( increment SingTerminal q
47+
-- Lookup Terminal (Increment Terminal q) ≡ S (Lookup Terminal q)
48+
, incrementLemma2 SingTerminal q
49+
) of
50+
(q', Refl) ->
51+
case lookup (SingActive SingReqInt) q' of
52+
Succ _ -> serverSendInts q' 0
53+
Zero ->
54+
case lookup (SingActive SingReqFib) q' of
55+
Succ _ -> serverSendFibs q' 0 1
56+
Zero ->
57+
case lookup (SingActive SingReqStr) q' of
58+
Succ _ -> serverSendChars Refl q' 'a'
59+
Zero -> serverDone q'
60+
61+
62+
-- reply all `ReqInt` requests
63+
serverSendInts
64+
:: forall (q :: NatMap (State ReqType)) (n :: N).
65+
( Lookup (Active ReqInt) q ~ S n
66+
, Lookup Terminal q ~ S Z
67+
)
68+
=> SingNatMap q
69+
-> Int
70+
-> Peer ReqType (AsServer q) m ()
71+
serverSendInts q i =
72+
case ( decrement (SingActive SingReqInt) q
73+
-- lemmas
74+
, -- Lookup Terminal (Decrement (Active ReqInt) q) ≡ Lookup Terminal q
75+
decrementLemma
76+
(\case {}) -- Active ReqInt ≢ Terminal
77+
(SingActive SingReqInt)
78+
SingTerminal
79+
q
80+
, -- Lookup (Active ReqInt) q ≡ S n
81+
-- ⇒ Lookup (Active ReqInt) (Decrement (Active ReqInt) q) ≡ n
82+
decrementLemma2 (SingActive SingReqInt) q
83+
)of
84+
((q', Succ (Succ _)), Refl, Refl) ->
85+
SendResponse
86+
(MsgResponseInt i)
87+
(serverSendInts q' (i + 1))
88+
89+
((q', Succ Zero), Refl, Refl) ->
90+
SendResponse
91+
(MsgResponseInt i)
92+
(case lookup (SingActive SingReqFib) q' of
93+
Succ{} -> serverSendFibs q' 0 1
94+
Zero ->
95+
case lookup (SingActive SingReqStr) q' of
96+
Succ _ -> serverSendChars Refl q' 'a'
97+
Zero -> serverDone q'
98+
)
99+
100+
101+
-- reply all `ReqFib` requests, incrementally computing Fibonacci numbers
102+
serverSendFibs
103+
:: forall (q :: NatMap (State ReqType)) (n :: N).
104+
( Lookup (Active ReqFib) q ~ S n
105+
, Lookup (Active ReqInt) q ~ Z
106+
, Lookup Terminal q ~ S Z
107+
)
108+
=> SingNatMap q
109+
-> Int -- ^ current Fibonacci number
110+
-> Int -- ^ next Fibonacci number
111+
-> Peer ReqType (AsServer q) m ()
112+
serverSendFibs q fib fib' =
113+
case ( decrement (SingActive SingReqFib) q
114+
-- lemmas
115+
, -- Lookup Terminal (Decrement Active ReqFib q) ≡ Lookup Terminal q
116+
decrementLemma
117+
(\case {})
118+
(SingActive SingReqFib)
119+
SingTerminal
120+
q
121+
, -- Lookup (Active ReqFib) (Decrement (Active ReqInt) q) ≡ Lookup (Active ReqFib) q
122+
decrementLemma
123+
(\case {}) -- Active ReqFib ≢ Active ReqInt
124+
(SingActive SingReqFib)
125+
(SingActive SingReqInt)
126+
q
127+
, -- Lookup (Active ReqFib) q ≡ S n
128+
-- ⇒ Lookup (Active ReqFib) (Decrement (Active ReqFib) q) ≡ n
129+
decrementLemma2
130+
(SingActive SingReqFib)
131+
q
132+
) of
133+
((q', Succ (Succ _)), Refl, Refl, Refl) ->
134+
SendResponse
135+
(MsgResponseFib fib)
136+
(serverSendFibs q' fib (fib + fib'))
137+
138+
((q', Succ Zero), Refl, Refl, Refl) ->
139+
SendResponse
140+
(MsgResponseFib fib)
141+
-- TODO
142+
-- I shouldn't need to do the lookup
143+
(case lookup (SingActive SingReqStr) q' of
144+
Succ _ -> serverSendChars Refl q' 'a'
145+
Zero -> serverDone q')
146+
147+
148+
149+
-- reply all `ReqStr` requests
150+
serverSendChars
151+
:: forall (q :: NatMap (State ReqType)) (n :: N).
152+
( Lookup Terminal q ~ S Z
153+
, Lookup (Active ReqInt) q ~ Z
154+
, Lookup (Active ReqFib) q ~ Z
155+
, Lookup (Active ReqStr) q ~ S n
156+
)
157+
=> (Lookup (Active ReqInt) q :~: Z)
158+
-> SingNatMap q
159+
-> Char
160+
-> Peer ReqType (AsServer q) m ()
161+
serverSendChars Refl q c =
162+
case
163+
( decrement
164+
(SingActive SingReqStr)
165+
q
166+
167+
-- lemmas
168+
, -- Lookup (Active ReqInt) (Decrement (Active ReqStr) q) ≡ Lookup (Active ReqInt) q
169+
decrementLemma
170+
(\case {}) -- Active ReqStr ≢ Active ReqInt
171+
(SingActive SingReqStr)
172+
(SingActive SingReqInt)
173+
q
174+
, -- Lookup (Active ReqFib) (Decrement (Active ReqStr) q) ≡ Lookup (Active ReqFib) q
175+
decrementLemma
176+
(\case {}) -- Active ReqStr ≢ Active ReqFib
177+
(SingActive SingReqStr)
178+
(SingActive SingReqFib)
179+
q
180+
, -- Lookup Terminal (Decrement (Active ReqFib) q) ≡ Lookup Terminal q
181+
decrementLemma
182+
(\case {}) -- Active ReqStr ≢ Terminal
183+
(SingActive SingReqStr)
184+
SingTerminal
185+
q
186+
, -- Lookup (Active ReqStr) q ≡ S n
187+
-- ⇒ Lookup (Active ReqStr) (Decrement (Active ReqStr) q) ≡ n
188+
decrementLemma2
189+
(SingActive SingReqStr)
190+
q
191+
) of
192+
((q', Succ (Succ _)), Refl, Refl, Refl, _) ->
193+
SendResponse
194+
(MsgResponseStr [c])
195+
(case lookup (SingActive SingReqStr) q' of
196+
Succ _ -> serverSendChars Refl q' (succ c)
197+
Zero -> serverDone q'
198+
)
199+
200+
((q', Succ Zero), Refl, Refl, Refl, Refl) ->
201+
SendResponse
202+
(MsgResponseStr [c])
203+
(serverDone q')
204+
205+
-- terminate
206+
serverDone
207+
:: forall (q :: NatMap (State ReqType)).
208+
( Lookup Terminal q ~ S Z
209+
, Lookup (Active ReqInt) q ~ Z
210+
, Lookup (Active ReqFib) q ~ Z
211+
, Lookup (Active ReqStr) q ~ Z
212+
)
213+
=> SingNatMap q
214+
-> Peer ReqType (AsServer q) m ()
215+
serverDone q =
216+
case empty q of
217+
Refl -> ServerDone ()
218+
219+
-- NOTE: the instances are needed to eliminate some of the cases, but
220+
-- GHC is not smart enough to figure it out, and places a warning
221+
-- `Redundant constraints`, hence we use `-Wno-redundant-constraints`.
222+
empty :: forall (q :: NatMap (State ReqType)).
223+
( Lookup Terminal q ~ S Z
224+
, Lookup (Active ReqInt) q ~ Z
225+
, Lookup (Active ReqFib) q ~ Z
226+
, Lookup (Active ReqStr) q ~ Z
227+
)
228+
=> SingNatMap q
229+
-> q :~: (Cons (Terminal :-> S Z) Empty :: NatMap (State ReqType))
230+
empty (SingCons Refl SingTerminal (Succ Zero) SingEmpty) = Refl
231+
232+
empty (SingCons Refl SingTerminal (Succ Zero) (SingCons _ s _ _))
233+
= case s of {}
234+
empty (SingCons _ (SingActive a) _ _)
235+
= case a of {}

‎typed-protocols/test/Main.hs‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ import Test.Tasty
44

55
import Network.TypedProtocol.PingPong.Tests qualified as PingPong
66
import Network.TypedProtocol.ReqResp.Tests qualified as ReqResp
7+
import Network.TypedProtocol.ReqResp3.Tests qualified as ReqResp3
78

89
main :: IO ()
910
main = defaultMain tests
@@ -13,5 +14,6 @@ tests =
1314
testGroup "typed-protocols"
1415
[ PingPong.tests
1516
, ReqResp.tests
17+
, ReqResp3.tests
1618
]
1719

0 commit comments

Comments
 (0)