Skip to content

Commit 1ca4aa7

Browse files
committed
typed-protocols: simplify evidence of termination in a terminal state
The simplest solution seem to add `StateAgency st ~ NobodyAgency` to the `Done` constructor. Which can be carried over to `TerminalStates`.
1 parent ce833a9 commit 1ca4aa7

File tree

4 files changed

+21
-43
lines changed

4 files changed

+21
-43
lines changed

typed-protocols-examples/test/Network/TypedProtocol/PingPong/Tests.hs

Lines changed: 2 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,6 @@ module Network.TypedProtocol.PingPong.Tests
1818

1919
import Network.TypedProtocol.Channel
2020
import Network.TypedProtocol.Codec
21-
import Network.TypedProtocol.Core
2221
import Network.TypedProtocol.Driver.Simple
2322
import Network.TypedProtocol.Proofs
2423

@@ -196,11 +195,7 @@ prop_connect (NonNegative n) =
196195
(pingPongClientPeer (pingPongClientCount n))
197196
(pingPongServerPeer pingPongServerCount))
198197

199-
of ((), n', TerminalStates SingDone
200-
ReflNobodyAgency
201-
SingDone
202-
ReflNobodyAgency) ->
203-
n == n'
198+
of ((), n', TerminalStates SingDone SingDone) -> n == n'
204199

205200

206201
--
@@ -219,11 +214,7 @@ connect_pipelined client cs =
219214
(connectPipelined cs []
220215
(pingPongClientPeerPipelined client)
221216
(promoteToPipelined $ pingPongServerPeer pingPongServerCount))
222-
223-
of (reqResps, n, TerminalStates SingDone
224-
ReflNobodyAgency
225-
SingDone
226-
ReflNobodyAgency) ->
217+
of (reqResps, n, TerminalStates SingDone SingDone) ->
227218
(n, reqResps)
228219

229220

typed-protocols-examples/test/Network/TypedProtocol/ReqResp/Tests.hs

Lines changed: 2 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,11 @@
1-
{-# LANGUAGE BangPatterns #-}
21
{-# LANGUAGE CPP #-}
32
{-# LANGUAGE DataKinds #-}
43
{-# LANGUAGE FlexibleInstances #-}
54
{-# LANGUAGE GADTs #-}
65
{-# LANGUAGE NamedFieldPuns #-}
76
{-# LANGUAGE PolyKinds #-}
87
{-# LANGUAGE ScopedTypeVariables #-}
9-
{-# LANGUAGE StandaloneKindSignatures #-}
108
{-# LANGUAGE TupleSections #-}
11-
{-# LANGUAGE TypeApplications #-}
12-
{-# LANGUAGE TypeOperators #-}
139

1410
-- orphaned arbitrary instances
1511
{-# OPTIONS_GHC -Wno-orphans #-}
@@ -19,7 +15,6 @@ module Network.TypedProtocol.ReqResp.Tests (tests) where
1915

2016
import Network.TypedProtocol.Channel
2117
import Network.TypedProtocol.Codec
22-
import Network.TypedProtocol.Core
2318
import Network.TypedProtocol.Driver.Simple
2419
import Network.TypedProtocol.Proofs
2520

@@ -163,10 +158,7 @@ prop_connect f xs =
163158
(reqRespClientPeer (reqRespClientMap xs))
164159
(reqRespServerPeer (reqRespServerMapAccumL (\a -> pure . f a) 0)))
165160

166-
of (c, s, TerminalStates SingDone
167-
ReflNobodyAgency
168-
SingDone
169-
ReflNobodyAgency) ->
161+
of (c, s, TerminalStates SingDone SingDone) ->
170162
(s, c) == mapAccumL f 0 xs
171163

172164

@@ -178,10 +170,7 @@ prop_connectPipelined cs f xs =
178170
(promoteToPipelined $ reqRespServerPeer
179171
(reqRespServerMapAccumL (\a -> pure . f a) 0)))
180172

181-
of (c, s, TerminalStates SingDone
182-
ReflNobodyAgency
183-
SingDone
184-
ReflNobodyAgency) ->
173+
of (c, s, TerminalStates SingDone SingDone) ->
185174
(s, c) == mapAccumL f 0 xs
186175

187176

typed-protocols/src/Network/TypedProtocol/Peer.hs

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -181,7 +181,9 @@ data Peer ps pr pl n st m a where
181181
--
182182
Done
183183
:: forall ps pr pl (st :: ps) m a.
184-
SingI st
184+
( SingI st
185+
, StateAgency st ~ NobodyAgency
186+
)
185187
=> NobodyHasAgencyProof pr st
186188
-- ^ (no) agency proof
187189
-> a

typed-protocols/src/Network/TypedProtocol/Proofs.hs

Lines changed: 14 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@
77
{-# LANGUAGE RankNTypes #-}
88
{-# LANGUAGE ScopedTypeVariables #-}
99
{-# LANGUAGE TypeFamilies #-}
10+
{-# LANGUAGE TypeOperators #-}
1011

1112

1213
-- This is already implied by the -Wall in the .cabal file, but lets just be
@@ -82,7 +83,7 @@ connect
8283
(Monad m, SingI pr)
8384
=> Peer ps pr NonPipelined Z initSt m a
8485
-> Peer ps (FlipAgency pr) NonPipelined Z initSt m b
85-
-> m (a, b, TerminalStates ps pr)
86+
-> m (a, b, TerminalStates ps)
8687
connect = go
8788
where
8889
singPeerRole :: Sing pr
@@ -91,14 +92,14 @@ connect = go
9192
go :: forall (st :: ps).
9293
Peer ps pr NonPipelined Z st m a
9394
-> Peer ps (FlipAgency pr) NonPipelined Z st m b
94-
-> m (a, b, TerminalStates ps pr)
95-
go (Done reflA a) (Done reflB b) = return (a, b, terminals)
95+
-> m (a, b, TerminalStates ps)
96+
go (Done ReflNobodyAgency a) (Done ReflNobodyAgency b) =
97+
return (a, b, terminals)
9698
where
97-
terminals :: TerminalStates ps pr
99+
terminals :: TerminalStates ps
98100
terminals = TerminalStates (sing :: Sing st)
99-
reflA
100101
(sing :: Sing st)
101-
reflB
102+
102103
go (Effect a ) b = a >>= \a' -> go a' b
103104
go a (Effect b) = b >>= \b' -> go a b'
104105
go (Yield _ msg a) (Await _ b) = go a (b msg)
@@ -134,18 +135,13 @@ connect = go
134135
-- | The terminal states for the protocol. Used in 'connect' and
135136
-- 'connectPipelined' to return the states in which the peers terminated.
136137
--
137-
data TerminalStates ps (pr :: PeerRole) where
138+
data TerminalStates ps where
138139
TerminalStates
139-
:: forall ps pr (st :: ps) (st' :: ps).
140-
Sing st
141-
-> ReflRelativeAgency (StateAgency st)
142-
NobodyHasAgency
143-
(Relative pr (StateAgency st))
144-
-> Sing st'
145-
-> ReflRelativeAgency (StateAgency st')
146-
NobodyHasAgency
147-
(Relative (FlipAgency pr) (StateAgency st'))
148-
-> TerminalStates ps pr
140+
:: forall ps (st :: ps).
141+
(StateAgency st ~ NobodyAgency)
142+
=> Sing st
143+
-> Sing st
144+
-> TerminalStates ps
149145

150146
--
151147
-- Remove Pipelining
@@ -248,7 +244,7 @@ connectPipelined
248244
-> [Bool]
249245
-> Peer ps pr ('Pipelined c) Z st m a
250246
-> Peer ps (FlipAgency pr) ('Pipelined c') Z st m b
251-
-> m (a, b, TerminalStates ps pr)
247+
-> m (a, b, TerminalStates ps)
252248
connectPipelined csA csB a b =
253249
connect (forgetPipelined csA a)
254250
(forgetPipelined csB b)

0 commit comments

Comments
 (0)