{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE RecordWildCards     #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE TypeInType          #-}


-- This is already implied by the -Wall in the .cabal file, but lets just be
-- completely explicit about it too, since we rely on the completeness
-- checking in the cases below for the completeness of our proofs.
{-# OPTIONS_GHC -Wincomplete-patterns #-}

-- | Proofs about the typed protocol framework.
--
-- It also provides helpful testing utilities.
--
module Network.TypedProtocol.Proofs
  ( -- * About these proofs
    -- $about
    -- * Connect proof
    connect
  , TerminalStates (..)
    -- * Pipelining proofs
    -- | Additional proofs specific to the pipelining features
  , connectPipelined
  , forgetPipelined
    -- ** Pipeline proof helpers
  , Queue (..)
  , enqueue
    -- ** Auxilary functions
  , pipelineInterleaving
  ) where

import           Data.Void (absurd)
import           Network.TypedProtocol.Core
import           Network.TypedProtocol.Pipelined

-- $about
--
-- Typed languages such as Haskell can embed proofs. In total languages this
-- is straightforward: a value inhabiting a type is a proof of the property
-- corresponding to the type.
--
-- In languages like Haskell that have ⊥ as a value of every type, things
-- are slightly more complicated. We have to demonstrate that the value that
-- inhabits the type of interest is not ⊥ which we can do by evaluation.
--
-- This idea crops up frequently in advanced type level programming in Haskell.
-- For example @Refl@ proofs that two types are equal have to have a runtime
-- representation that is evaluated to demonstrate it is not ⊥ before it
-- can be relied upon.
--
-- The proofs here are about the nature of typed protocols in this framework.
-- The 'connect' and 'connectPipelined' proofs rely on a few lemmas about
-- the individual protocol. See 'AgencyProofs'.




-- | The 'connect' function takes two peers that agree on a protocol and runs
-- them in lock step, until (and if) they complete.
--
-- The 'connect' function serves a few purposes.
--
-- * The fact we can define this function at at all proves some minimal
-- sanity property of the typed protocol framework.
--
-- * It demonstrates that all protocols defined in the framework can be run
-- with synchronous communication rather than requiring buffered communication.
--
-- * It is useful for testing peer implementations against each other in a
-- minimalistic setting.
--
connect :: forall ps (pr :: PeerRole) (st :: ps) m a b.
           (Monad m, Protocol ps)
        => Peer ps pr st m a
        -> Peer ps (FlipAgency pr) st m b
        -> m (a, b, TerminalStates ps)
connect :: Peer ps pr st m a
-> Peer ps (FlipAgency pr) st m b -> m (a, b, TerminalStates ps)
connect = Peer ps pr st m a
-> Peer ps (FlipAgency pr) st m b -> m (a, b, TerminalStates ps)
forall (st' :: ps).
Peer ps pr st' m a
-> Peer ps (FlipAgency pr) st' m b -> m (a, b, TerminalStates ps)
go
  where
    go :: forall (st' :: ps).
          Peer ps pr st' m a
       -> Peer ps (FlipAgency pr) st' m b
       -> m (a, b, TerminalStates ps)
    go :: Peer ps pr st' m a
-> Peer ps (FlipAgency pr) st' m b -> m (a, b, TerminalStates ps)
go (Done NobodyHasAgency st'
stA a
a)    (Done NobodyHasAgency st'
stB b
b)    = (a, b, TerminalStates ps) -> m (a, b, TerminalStates ps)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, b
b, NobodyHasAgency st' -> NobodyHasAgency st' -> TerminalStates ps
forall ps (st :: ps).
NobodyHasAgency st -> NobodyHasAgency st -> TerminalStates ps
TerminalStates NobodyHasAgency st'
stA NobodyHasAgency st'
stB)
    go (Effect m (Peer ps pr st' m a)
a )      Peer ps (FlipAgency pr) st' m b
b              = m (Peer ps pr st' m a)
a m (Peer ps pr st' m a)
-> (Peer ps pr st' m a -> m (a, b, TerminalStates ps))
-> m (a, b, TerminalStates ps)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Peer ps pr st' m a
a' -> Peer ps pr st' m a
-> Peer ps (FlipAgency pr) st' m b -> m (a, b, TerminalStates ps)
forall (st' :: ps).
Peer ps pr st' m a
-> Peer ps (FlipAgency pr) st' m b -> m (a, b, TerminalStates ps)
go Peer ps pr st' m a
a' Peer ps (FlipAgency pr) st' m b
b
    go  Peer ps pr st' m a
a              (Effect m (Peer ps (FlipAgency pr) st' m b)
b)      = m (Peer ps (FlipAgency pr) st' m b)
b m (Peer ps (FlipAgency pr) st' m b)
-> (Peer ps (FlipAgency pr) st' m b -> m (a, b, TerminalStates ps))
-> m (a, b, TerminalStates ps)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Peer ps (FlipAgency pr) st' m b
b' -> Peer ps pr st' m a
-> Peer ps (FlipAgency pr) st' m b -> m (a, b, TerminalStates ps)
forall (st' :: ps).
Peer ps pr st' m a
-> Peer ps (FlipAgency pr) st' m b -> m (a, b, TerminalStates ps)
go Peer ps pr st' m a
a  Peer ps (FlipAgency pr) st' m b
b'
    go (Yield WeHaveAgency pr st'
_ Message ps st' st'
msg Peer ps pr st' m a
a) (Await TheyHaveAgency (FlipAgency pr) st'
_ forall (st' :: ps).
Message ps st' st' -> Peer ps (FlipAgency pr) st' m b
b)     = Peer ps pr st' m a
-> Peer ps (FlipAgency pr) st' m b -> m (a, b, TerminalStates ps)
forall (st' :: ps).
Peer ps pr st' m a
-> Peer ps (FlipAgency pr) st' m b -> m (a, b, TerminalStates ps)
go  Peer ps pr st' m a
a     (Message ps st' st' -> Peer ps (FlipAgency pr) st' m b
forall (st' :: ps).
Message ps st' st' -> Peer ps (FlipAgency pr) st' m b
b Message ps st' st'
msg)
    go (Await TheyHaveAgency pr st'
_ forall (st' :: ps). Message ps st' st' -> Peer ps pr st' m a
a)     (Yield TheyHaveAgency pr st'
_ Message ps st' st'
msg Peer ps (FlipAgency pr) st' m b
b) = Peer ps pr st' m a
-> Peer ps (FlipAgency pr) st' m b -> m (a, b, TerminalStates ps)
forall (st' :: ps).
Peer ps pr st' m a
-> Peer ps (FlipAgency pr) st' m b -> m (a, b, TerminalStates ps)
go (Message ps st' st' -> Peer ps pr st' m a
forall (st' :: ps). Message ps st' st' -> Peer ps pr st' m a
a Message ps st' st'
msg) Peer ps (FlipAgency pr) st' m b
b

    -- By appealing to the proofs about agency for this protocol we can
    -- show that these other cases are impossible
    go (Yield (ClientAgency ClientHasAgency st'
stA) Message ps st' st'
_ Peer ps pr st' m a
_) (Yield (ServerAgency ServerHasAgency st'
stB) Message ps st' st'
_ Peer ps (FlipAgency pr) st' m b
_) =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (ClientHasAgency st' -> ServerHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
ClientHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_ClientAndServerHaveAgency ClientHasAgency st'
stA ServerHasAgency st'
stB)

    go (Yield (ServerAgency ServerHasAgency st'
stA) Message ps st' st'
_ Peer ps pr st' m a
_) (Yield (ClientAgency ClientHasAgency st'
stB) Message ps st' st'
_ Peer ps (FlipAgency pr) st' m b
_) =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (ClientHasAgency st' -> ServerHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
ClientHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_ClientAndServerHaveAgency ClientHasAgency st'
stB ServerHasAgency st'
stA)

    go (Await (ServerAgency ServerHasAgency st'
stA) forall (st' :: ps). Message ps st' st' -> Peer ps pr st' m a
_)   (Await (ClientAgency ClientHasAgency st'
stB) forall (st' :: ps).
Message ps st' st' -> Peer ps (FlipAgency pr) st' m b
_)   =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (ClientHasAgency st' -> ServerHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
ClientHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_ClientAndServerHaveAgency ClientHasAgency st'
stB ServerHasAgency st'
stA)

    go (Await (ClientAgency ClientHasAgency st'
stA) forall (st' :: ps). Message ps st' st' -> Peer ps pr st' m a
_)   (Await (ServerAgency ServerHasAgency st'
stB) forall (st' :: ps).
Message ps st' st' -> Peer ps (FlipAgency pr) st' m b
_)   =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (ClientHasAgency st' -> ServerHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
ClientHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_ClientAndServerHaveAgency ClientHasAgency st'
stA ServerHasAgency st'
stB)

    go (Done  NobodyHasAgency st'
stA a
_)            (Yield (ServerAgency ServerHasAgency st'
stB) Message ps st' st'
_ Peer ps (FlipAgency pr) st' m b
_) =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (NobodyHasAgency st' -> ServerHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
NobodyHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_NobodyAndServerHaveAgency NobodyHasAgency st'
stA ServerHasAgency st'
stB)

    go (Done  NobodyHasAgency st'
stA a
_)            (Yield (ClientAgency ClientHasAgency st'
stB) Message ps st' st'
_ Peer ps (FlipAgency pr) st' m b
_) =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (NobodyHasAgency st' -> ClientHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
NobodyHasAgency st -> ClientHasAgency st -> Void
exclusionLemma_NobodyAndClientHaveAgency NobodyHasAgency st'
stA ClientHasAgency st'
stB)

    go (Done  NobodyHasAgency st'
stA a
_)            (Await (ClientAgency ClientHasAgency st'
stB) forall (st' :: ps).
Message ps st' st' -> Peer ps (FlipAgency pr) st' m b
_)   =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (NobodyHasAgency st' -> ClientHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
NobodyHasAgency st -> ClientHasAgency st -> Void
exclusionLemma_NobodyAndClientHaveAgency NobodyHasAgency st'
stA ClientHasAgency st'
stB)

    go (Done  NobodyHasAgency st'
stA a
_)            (Await (ServerAgency ServerHasAgency st'
stB) forall (st' :: ps).
Message ps st' st' -> Peer ps (FlipAgency pr) st' m b
_)   =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (NobodyHasAgency st' -> ServerHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
NobodyHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_NobodyAndServerHaveAgency NobodyHasAgency st'
stA ServerHasAgency st'
stB)

    go (Yield (ClientAgency ClientHasAgency st'
stA) Message ps st' st'
_ Peer ps pr st' m a
_) (Done NobodyHasAgency st'
stB b
_)    =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (NobodyHasAgency st' -> ClientHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
NobodyHasAgency st -> ClientHasAgency st -> Void
exclusionLemma_NobodyAndClientHaveAgency NobodyHasAgency st'
stB ClientHasAgency st'
stA)

    go (Yield (ServerAgency ServerHasAgency st'
stA) Message ps st' st'
_ Peer ps pr st' m a
_) (Done NobodyHasAgency st'
stB b
_)    =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (NobodyHasAgency st' -> ServerHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
NobodyHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_NobodyAndServerHaveAgency NobodyHasAgency st'
stB ServerHasAgency st'
stA)

    go (Await (ServerAgency ServerHasAgency st'
stA) forall (st' :: ps). Message ps st' st' -> Peer ps pr st' m a
_)   (Done NobodyHasAgency st'
stB b
_)    =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (NobodyHasAgency st' -> ServerHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
NobodyHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_NobodyAndServerHaveAgency NobodyHasAgency st'
stB ServerHasAgency st'
stA)

    go (Await (ClientAgency ClientHasAgency st'
stA) forall (st' :: ps). Message ps st' st' -> Peer ps pr st' m a
_)   (Done NobodyHasAgency st'
stB b
_)    =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (NobodyHasAgency st' -> ClientHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
NobodyHasAgency st -> ClientHasAgency st -> Void
exclusionLemma_NobodyAndClientHaveAgency NobodyHasAgency st'
stB ClientHasAgency st'
stA)


-- | The terminal states for the protocol. Used in 'connect' and
-- 'connectPipelined' to return the states in which the peers terminated.
--
data TerminalStates ps where
     TerminalStates :: forall ps (st :: ps).
                       NobodyHasAgency st
                    -> NobodyHasAgency st
                    -> TerminalStates ps


-- | Analogous to 'connect' but for pipelined peers.
--
-- Since pipelining allows multiple possible interleavings, we provide a
-- @[Bool]@ parameter to control the choices. Each @True@ will trigger picking
-- the first choice in the @SenderCollect@ construct (if possible), leading
-- to more results outstanding. This can also be interpreted as a greater
-- pipeline depth, or more messages in-flight.
--
-- This can be exercised using a QuickCheck style generator.
--
connectPipelined :: forall ps (pr :: PeerRole) (st :: ps) m a b.
                    (Monad m, Protocol ps)
                 => [Bool] -- ^ Interleaving choices. [] gives no pipelining.
                 -> PeerPipelined ps pr st m a
                 -> Peer          ps (FlipAgency pr) st m b
                 -> m (a, b, TerminalStates ps)

connectPipelined :: [Bool]
-> PeerPipelined ps pr st m a
-> Peer ps (FlipAgency pr) st m b
-> m (a, b, TerminalStates ps)
connectPipelined [Bool]
cs0 (PeerPipelined PeerSender ps pr st 'Z c m a
peerA) Peer ps (FlipAgency pr) st m b
peerB =
    [Bool]
-> Queue 'Z c
-> PeerSender ps pr st 'Z c m a
-> Peer ps (FlipAgency pr) st m b
-> m (a, b, TerminalStates ps)
forall (st' :: ps) (n :: N) c.
[Bool]
-> Queue n c
-> PeerSender ps pr st' n c m a
-> Peer ps (FlipAgency pr) st' m b
-> m (a, b, TerminalStates ps)
goSender [Bool]
cs0 Queue 'Z c
forall a. Queue 'Z a
EmptyQ PeerSender ps pr st 'Z c m a
peerA Peer ps (FlipAgency pr) st m b
peerB
  where
    goSender :: forall (st' :: ps) n c.
                [Bool]
             -> Queue                      n c
             -> PeerSender ps pr st' n c m a
             -> Peer       ps (FlipAgency pr) st'     m b
             -> m (a, b, TerminalStates ps)

    goSender :: [Bool]
-> Queue n c
-> PeerSender ps pr st' n c m a
-> Peer ps (FlipAgency pr) st' m b
-> m (a, b, TerminalStates ps)
goSender [Bool]
_ Queue n c
EmptyQ (SenderDone NobodyHasAgency st'
stA a
a) (Done NobodyHasAgency st'
stB b
b) = (a, b, TerminalStates ps) -> m (a, b, TerminalStates ps)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, b
b, TerminalStates ps
terminals)
      where terminals :: TerminalStates ps
terminals = NobodyHasAgency st' -> NobodyHasAgency st' -> TerminalStates ps
forall ps (st :: ps).
NobodyHasAgency st -> NobodyHasAgency st -> TerminalStates ps
TerminalStates NobodyHasAgency st'
stA NobodyHasAgency st'
stB

    goSender [Bool]
cs Queue n c
q (SenderEffect m (PeerSender ps pr st' n c m a)
a) Peer ps (FlipAgency pr) st' m b
b  = m (PeerSender ps pr st' n c m a)
a m (PeerSender ps pr st' n c m a)
-> (PeerSender ps pr st' n c m a -> m (a, b, TerminalStates ps))
-> m (a, b, TerminalStates ps)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \PeerSender ps pr st' n c m a
a' -> [Bool]
-> Queue n c
-> PeerSender ps pr st' n c m a
-> Peer ps (FlipAgency pr) st' m b
-> m (a, b, TerminalStates ps)
forall (st' :: ps) (n :: N) c.
[Bool]
-> Queue n c
-> PeerSender ps pr st' n c m a
-> Peer ps (FlipAgency pr) st' m b
-> m (a, b, TerminalStates ps)
goSender [Bool]
cs Queue n c
q PeerSender ps pr st' n c m a
a' Peer ps (FlipAgency pr) st' m b
b
    goSender [Bool]
cs Queue n c
q PeerSender ps pr st' n c m a
a        (Effect m (Peer ps (FlipAgency pr) st' m b)
b) = m (Peer ps (FlipAgency pr) st' m b)
b m (Peer ps (FlipAgency pr) st' m b)
-> (Peer ps (FlipAgency pr) st' m b -> m (a, b, TerminalStates ps))
-> m (a, b, TerminalStates ps)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Peer ps (FlipAgency pr) st' m b
b' -> [Bool]
-> Queue n c
-> PeerSender ps pr st' n c m a
-> Peer ps (FlipAgency pr) st' m b
-> m (a, b, TerminalStates ps)
forall (st' :: ps) (n :: N) c.
[Bool]
-> Queue n c
-> PeerSender ps pr st' n c m a
-> Peer ps (FlipAgency pr) st' m b
-> m (a, b, TerminalStates ps)
goSender [Bool]
cs Queue n c
q PeerSender ps pr st' n c m a
a  Peer ps (FlipAgency pr) st' m b
b'

    goSender [Bool]
cs Queue n c
q (SenderYield WeHaveAgency pr st'
_ Message ps st' st'
msg PeerSender ps pr st' 'Z c m a
a) (Await TheyHaveAgency (FlipAgency pr) st'
_ forall (st' :: ps).
Message ps st' st' -> Peer ps (FlipAgency pr) st' m b
b) = [Bool]
-> Queue n c
-> PeerSender ps pr st' n c m a
-> Peer ps (FlipAgency pr) st' m b
-> m (a, b, TerminalStates ps)
forall (st' :: ps) (n :: N) c.
[Bool]
-> Queue n c
-> PeerSender ps pr st' n c m a
-> Peer ps (FlipAgency pr) st' m b
-> m (a, b, TerminalStates ps)
goSender [Bool]
cs Queue n c
q PeerSender ps pr st' n c m a
PeerSender ps pr st' 'Z c m a
a (Message ps st' st' -> Peer ps (FlipAgency pr) st' m b
forall (st' :: ps).
Message ps st' st' -> Peer ps (FlipAgency pr) st' m b
b Message ps st' st'
msg)
    goSender [Bool]
cs Queue n c
q (SenderAwait TheyHaveAgency pr st'
_ forall (st' :: ps).
Message ps st' st' -> PeerSender ps pr st' 'Z c m a
a) (Yield TheyHaveAgency pr st'
_ Message ps st' st'
msg Peer ps (FlipAgency pr) st' m b
b) = [Bool]
-> Queue n c
-> PeerSender ps pr st' n c m a
-> Peer ps (FlipAgency pr) st' m b
-> m (a, b, TerminalStates ps)
forall (st' :: ps) (n :: N) c.
[Bool]
-> Queue n c
-> PeerSender ps pr st' n c m a
-> Peer ps (FlipAgency pr) st' m b
-> m (a, b, TerminalStates ps)
goSender [Bool]
cs Queue n c
q (Message ps st' st' -> PeerSender ps pr st' 'Z c m a
forall (st' :: ps).
Message ps st' st' -> PeerSender ps pr st' 'Z c m a
a Message ps st' st'
msg) Peer ps (FlipAgency pr) st' m b
b

    -- This does the receiver effects immediately, as if there were no
    -- pipelining.
    goSender [Bool]
cs Queue n c
q (SenderPipeline WeHaveAgency pr st'
_ Message ps st' st'
msg PeerReceiver ps pr st' st'' m c
r PeerSender ps pr st'' ('S n) c m a
a) (Await TheyHaveAgency (FlipAgency pr) st'
_ forall (st' :: ps).
Message ps st' st' -> Peer ps (FlipAgency pr) st' m b
b) =
      PeerReceiver ps pr st' st'' m c
-> Peer ps (FlipAgency pr) st' m b
-> m (Peer ps (FlipAgency pr) st'' m b, c)
forall (st' :: ps) (stdone :: ps) c.
PeerReceiver ps pr st' stdone m c
-> Peer ps (FlipAgency pr) st' m b
-> m (Peer ps (FlipAgency pr) stdone m b, c)
goReceiver PeerReceiver ps pr st' st'' m c
r (Message ps st' st' -> Peer ps (FlipAgency pr) st' m b
forall (st' :: ps).
Message ps st' st' -> Peer ps (FlipAgency pr) st' m b
b Message ps st' st'
msg) m (Peer ps (FlipAgency pr) st'' m b, c)
-> ((Peer ps (FlipAgency pr) st'' m b, c)
    -> m (a, b, TerminalStates ps))
-> m (a, b, TerminalStates ps)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(Peer ps (FlipAgency pr) st'' m b
b', c
x) -> [Bool]
-> Queue ('S n) c
-> PeerSender ps pr st'' ('S n) c m a
-> Peer ps (FlipAgency pr) st'' m b
-> m (a, b, TerminalStates ps)
forall (st' :: ps) (n :: N) c.
[Bool]
-> Queue n c
-> PeerSender ps pr st' n c m a
-> Peer ps (FlipAgency pr) st' m b
-> m (a, b, TerminalStates ps)
goSender [Bool]
cs (c -> Queue n c -> Queue ('S n) c
forall a (n :: N). a -> Queue n a -> Queue ('S n) a
enqueue c
x Queue n c
q) PeerSender ps pr st'' ('S n) c m a
a Peer ps (FlipAgency pr) st'' m b
b'

    -- However we make it possible to exercise the choice the environment has
    -- in the non-determinism of the pipeline interleaving of collecting
    -- results. Always picking the second continuation gives the fully serial
    -- order. Always picking the first leads to a maximal (and possibly
    -- unbounded) number of pending replies. By using a list of bools to
    -- control the choices here, we can test any other order:
    goSender (Bool
True:[Bool]
cs) Queue n c
q (SenderCollect (Just PeerSender ps pr st' ('S n) c m a
a) c -> PeerSender ps pr st' n c m a
_) Peer ps (FlipAgency pr) st' m b
b = [Bool]
-> Queue n c
-> PeerSender ps pr st' n c m a
-> Peer ps (FlipAgency pr) st' m b
-> m (a, b, TerminalStates ps)
forall (st' :: ps) (n :: N) c.
[Bool]
-> Queue n c
-> PeerSender ps pr st' n c m a
-> Peer ps (FlipAgency pr) st' m b
-> m (a, b, TerminalStates ps)
goSender [Bool]
cs Queue n c
q  PeerSender ps pr st' n c m a
PeerSender ps pr st' ('S n) c m a
a    Peer ps (FlipAgency pr) st' m b
b
    goSender (Bool
_:[Bool]
cs) (ConsQ c
x Queue n c
q) (SenderCollect Maybe (PeerSender ps pr st' ('S n) c m a)
_ c -> PeerSender ps pr st' n c m a
a) Peer ps (FlipAgency pr) st' m b
b = [Bool]
-> Queue n c
-> PeerSender ps pr st' n c m a
-> Peer ps (FlipAgency pr) st' m b
-> m (a, b, TerminalStates ps)
forall (st' :: ps) (n :: N) c.
[Bool]
-> Queue n c
-> PeerSender ps pr st' n c m a
-> Peer ps (FlipAgency pr) st' m b
-> m (a, b, TerminalStates ps)
goSender [Bool]
cs Queue n c
q (c -> PeerSender ps pr st' n c m a
a c
x) Peer ps (FlipAgency pr) st' m b
b
    goSender    []  (ConsQ c
x Queue n c
q) (SenderCollect Maybe (PeerSender ps pr st' ('S n) c m a)
_ c -> PeerSender ps pr st' n c m a
a) Peer ps (FlipAgency pr) st' m b
b = [Bool]
-> Queue n c
-> PeerSender ps pr st' n c m a
-> Peer ps (FlipAgency pr) st' m b
-> m (a, b, TerminalStates ps)
forall (st' :: ps) (n :: N) c.
[Bool]
-> Queue n c
-> PeerSender ps pr st' n c m a
-> Peer ps (FlipAgency pr) st' m b
-> m (a, b, TerminalStates ps)
goSender [] Queue n c
q (c -> PeerSender ps pr st' n c m a
a c
x) Peer ps (FlipAgency pr) st' m b
b

    -- Proofs that the remaining cases are impossible
    goSender [Bool]
_ Queue n c
_ (SenderDone NobodyHasAgency st'
stA a
_) (Yield (ServerAgency ServerHasAgency st'
stB) Message ps st' st'
_ Peer ps (FlipAgency pr) st' m b
_) =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (NobodyHasAgency st' -> ServerHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
NobodyHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_NobodyAndServerHaveAgency NobodyHasAgency st'
stA ServerHasAgency st'
stB)

    goSender [Bool]
_ Queue n c
_ (SenderDone NobodyHasAgency st'
stA a
_) (Yield (ClientAgency ClientHasAgency st'
stB) Message ps st' st'
_ Peer ps (FlipAgency pr) st' m b
_) =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (NobodyHasAgency st' -> ClientHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
NobodyHasAgency st -> ClientHasAgency st -> Void
exclusionLemma_NobodyAndClientHaveAgency NobodyHasAgency st'
stA ClientHasAgency st'
stB)

    goSender [Bool]
_ Queue n c
_ (SenderDone NobodyHasAgency st'
stA a
_) (Await (ClientAgency ClientHasAgency st'
stB) forall (st' :: ps).
Message ps st' st' -> Peer ps (FlipAgency pr) st' m b
_) =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (NobodyHasAgency st' -> ClientHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
NobodyHasAgency st -> ClientHasAgency st -> Void
exclusionLemma_NobodyAndClientHaveAgency NobodyHasAgency st'
stA ClientHasAgency st'
stB)

    goSender [Bool]
_ Queue n c
_ (SenderDone NobodyHasAgency st'
stA a
_) (Await (ServerAgency ServerHasAgency st'
stB) forall (st' :: ps).
Message ps st' st' -> Peer ps (FlipAgency pr) st' m b
_) =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (NobodyHasAgency st' -> ServerHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
NobodyHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_NobodyAndServerHaveAgency NobodyHasAgency st'
stA ServerHasAgency st'
stB)

    goSender [Bool]
_ Queue n c
_ (SenderYield (ClientAgency ClientHasAgency st'
stA) Message ps st' st'
_ PeerSender ps pr st' 'Z c m a
_) (Done NobodyHasAgency st'
stB b
_) =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (NobodyHasAgency st' -> ClientHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
NobodyHasAgency st -> ClientHasAgency st -> Void
exclusionLemma_NobodyAndClientHaveAgency NobodyHasAgency st'
stB ClientHasAgency st'
stA)

    goSender [Bool]
_ Queue n c
_ (SenderYield (ServerAgency ServerHasAgency st'
stA) Message ps st' st'
_ PeerSender ps pr st' 'Z c m a
_) (Done NobodyHasAgency st'
stB b
_) =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (NobodyHasAgency st' -> ServerHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
NobodyHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_NobodyAndServerHaveAgency NobodyHasAgency st'
stB ServerHasAgency st'
stA)

    goSender [Bool]
_ Queue n c
_ (SenderYield (ClientAgency ClientHasAgency st'
stA) Message ps st' st'
_ PeerSender ps pr st' 'Z c m a
_) (Yield (ServerAgency ServerHasAgency st'
stB) Message ps st' st'
_ Peer ps (FlipAgency pr) st' m b
_) =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (ClientHasAgency st' -> ServerHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
ClientHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_ClientAndServerHaveAgency ClientHasAgency st'
stA ServerHasAgency st'
stB)

    goSender [Bool]
_ Queue n c
_ (SenderYield (ServerAgency ServerHasAgency st'
stA) Message ps st' st'
_ PeerSender ps pr st' 'Z c m a
_) (Yield (ClientAgency ClientHasAgency st'
stB) Message ps st' st'
_ Peer ps (FlipAgency pr) st' m b
_) =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (ClientHasAgency st' -> ServerHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
ClientHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_ClientAndServerHaveAgency ClientHasAgency st'
stB ServerHasAgency st'
stA)

    goSender [Bool]
_ Queue n c
_ (SenderAwait (ClientAgency ClientHasAgency st'
stA) forall (st' :: ps).
Message ps st' st' -> PeerSender ps pr st' 'Z c m a
_) (Done NobodyHasAgency st'
stB b
_) =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (NobodyHasAgency st' -> ClientHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
NobodyHasAgency st -> ClientHasAgency st -> Void
exclusionLemma_NobodyAndClientHaveAgency NobodyHasAgency st'
stB ClientHasAgency st'
stA)

    goSender [Bool]
_ Queue n c
_ (SenderAwait (ServerAgency ServerHasAgency st'
stA) forall (st' :: ps).
Message ps st' st' -> PeerSender ps pr st' 'Z c m a
_) (Done NobodyHasAgency st'
stB b
_) =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (NobodyHasAgency st' -> ServerHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
NobodyHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_NobodyAndServerHaveAgency NobodyHasAgency st'
stB ServerHasAgency st'
stA)

    goSender [Bool]
_ Queue n c
_ (SenderAwait (ClientAgency ClientHasAgency st'
stA) forall (st' :: ps).
Message ps st' st' -> PeerSender ps pr st' 'Z c m a
_) (Await (ServerAgency ServerHasAgency st'
stB) forall (st' :: ps).
Message ps st' st' -> Peer ps (FlipAgency pr) st' m b
_) =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (ClientHasAgency st' -> ServerHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
ClientHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_ClientAndServerHaveAgency ClientHasAgency st'
stA ServerHasAgency st'
stB)

    goSender [Bool]
_ Queue n c
_ (SenderAwait (ServerAgency ServerHasAgency st'
stA) forall (st' :: ps).
Message ps st' st' -> PeerSender ps pr st' 'Z c m a
_) (Await (ClientAgency ClientHasAgency st'
stB) forall (st' :: ps).
Message ps st' st' -> Peer ps (FlipAgency pr) st' m b
_) =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (ClientHasAgency st' -> ServerHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
ClientHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_ClientAndServerHaveAgency ClientHasAgency st'
stB ServerHasAgency st'
stA)

    goSender [Bool]
_ Queue n c
_ (SenderPipeline (ClientAgency ClientHasAgency st'
stA) Message ps st' st'
_ PeerReceiver ps pr st' st'' m c
_ PeerSender ps pr st'' ('S n) c m a
_) (Done NobodyHasAgency st'
stB b
_) =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (NobodyHasAgency st' -> ClientHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
NobodyHasAgency st -> ClientHasAgency st -> Void
exclusionLemma_NobodyAndClientHaveAgency NobodyHasAgency st'
stB ClientHasAgency st'
stA)

    goSender [Bool]
_ Queue n c
_ (SenderPipeline (ServerAgency ServerHasAgency st'
stA) Message ps st' st'
_ PeerReceiver ps pr st' st'' m c
_ PeerSender ps pr st'' ('S n) c m a
_) (Done NobodyHasAgency st'
stB b
_) =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (NobodyHasAgency st' -> ServerHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
NobodyHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_NobodyAndServerHaveAgency NobodyHasAgency st'
stB ServerHasAgency st'
stA)

    goSender [Bool]
_ Queue n c
_ (SenderPipeline (ClientAgency ClientHasAgency st'
stA) Message ps st' st'
_ PeerReceiver ps pr st' st'' m c
_ PeerSender ps pr st'' ('S n) c m a
_) (Yield (ServerAgency ServerHasAgency st'
stB) Message ps st' st'
_ Peer ps (FlipAgency pr) st' m b
_) =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (ClientHasAgency st' -> ServerHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
ClientHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_ClientAndServerHaveAgency ClientHasAgency st'
stA ServerHasAgency st'
stB)

    goSender [Bool]
_ Queue n c
_ (SenderPipeline (ServerAgency ServerHasAgency st'
stA) Message ps st' st'
_ PeerReceiver ps pr st' st'' m c
_ PeerSender ps pr st'' ('S n) c m a
_) (Yield (ClientAgency ClientHasAgency st'
stB) Message ps st' st'
_ Peer ps (FlipAgency pr) st' m b
_) =
      Void -> m (a, b, TerminalStates ps)
forall a. Void -> a
absurd (ClientHasAgency st' -> ServerHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
ClientHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_ClientAndServerHaveAgency ClientHasAgency st'
stB ServerHasAgency st'
stA)


    goReceiver :: forall (st' :: ps) (stdone :: ps) c.
                  PeerReceiver ps pr st' stdone m c
               -> Peer         ps (FlipAgency pr) st'        m b
               -> m (Peer      ps (FlipAgency pr)     stdone m b, c)

    goReceiver :: PeerReceiver ps pr st' stdone m c
-> Peer ps (FlipAgency pr) st' m b
-> m (Peer ps (FlipAgency pr) stdone m b, c)
goReceiver (ReceiverDone c
x)    Peer ps (FlipAgency pr) st' m b
b         = (Peer ps (FlipAgency pr) st' m b, c)
-> m (Peer ps (FlipAgency pr) st' m b, c)
forall (m :: * -> *) a. Monad m => a -> m a
return (Peer ps (FlipAgency pr) st' m b
b, c
x)
    goReceiver (ReceiverEffect m (PeerReceiver ps pr st' stdone m c)
a)  Peer ps (FlipAgency pr) st' m b
b         = m (PeerReceiver ps pr st' stdone m c)
a m (PeerReceiver ps pr st' stdone m c)
-> (PeerReceiver ps pr st' stdone m c
    -> m (Peer ps (FlipAgency pr) stdone m b, c))
-> m (Peer ps (FlipAgency pr) stdone m b, c)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \PeerReceiver ps pr st' stdone m c
a' -> PeerReceiver ps pr st' stdone m c
-> Peer ps (FlipAgency pr) st' m b
-> m (Peer ps (FlipAgency pr) stdone m b, c)
forall (st' :: ps) (stdone :: ps) c.
PeerReceiver ps pr st' stdone m c
-> Peer ps (FlipAgency pr) st' m b
-> m (Peer ps (FlipAgency pr) stdone m b, c)
goReceiver PeerReceiver ps pr st' stdone m c
a' Peer ps (FlipAgency pr) st' m b
b
    goReceiver  PeerReceiver ps pr st' stdone m c
a                 (Effect m (Peer ps (FlipAgency pr) st' m b)
b) = m (Peer ps (FlipAgency pr) st' m b)
b m (Peer ps (FlipAgency pr) st' m b)
-> (Peer ps (FlipAgency pr) st' m b
    -> m (Peer ps (FlipAgency pr) stdone m b, c))
-> m (Peer ps (FlipAgency pr) stdone m b, c)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Peer ps (FlipAgency pr) st' m b
b' -> PeerReceiver ps pr st' stdone m c
-> Peer ps (FlipAgency pr) st' m b
-> m (Peer ps (FlipAgency pr) stdone m b, c)
forall (st' :: ps) (stdone :: ps) c.
PeerReceiver ps pr st' stdone m c
-> Peer ps (FlipAgency pr) st' m b
-> m (Peer ps (FlipAgency pr) stdone m b, c)
goReceiver PeerReceiver ps pr st' stdone m c
a  Peer ps (FlipAgency pr) st' m b
b'

    goReceiver (ReceiverAwait TheyHaveAgency pr st'
_ forall (st' :: ps).
Message ps st' st' -> PeerReceiver ps pr st' stdone m c
a) (Yield TheyHaveAgency pr st'
_ Message ps st' st'
msg Peer ps (FlipAgency pr) st' m b
b) = PeerReceiver ps pr st' stdone m c
-> Peer ps (FlipAgency pr) st' m b
-> m (Peer ps (FlipAgency pr) stdone m b, c)
forall (st' :: ps) (stdone :: ps) c.
PeerReceiver ps pr st' stdone m c
-> Peer ps (FlipAgency pr) st' m b
-> m (Peer ps (FlipAgency pr) stdone m b, c)
goReceiver (Message ps st' st' -> PeerReceiver ps pr st' stdone m c
forall (st' :: ps).
Message ps st' st' -> PeerReceiver ps pr st' stdone m c
a Message ps st' st'
msg) Peer ps (FlipAgency pr) st' m b
b


    -- Proofs that the remaining cases are impossible
    goReceiver (ReceiverAwait (ServerAgency ServerHasAgency st'
stA) forall (st' :: ps).
Message ps st' st' -> PeerReceiver ps pr st' stdone m c
_) (Done  NobodyHasAgency st'
stB b
_) =
      Void -> m (Peer ps 'AsServer stdone m b, c)
forall a. Void -> a
absurd (NobodyHasAgency st' -> ServerHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
NobodyHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_NobodyAndServerHaveAgency NobodyHasAgency st'
stB ServerHasAgency st'
stA)

    goReceiver (ReceiverAwait (ClientAgency ClientHasAgency st'
stA) forall (st' :: ps).
Message ps st' st' -> PeerReceiver ps pr st' stdone m c
_) (Done  NobodyHasAgency st'
stB b
_) =
      Void -> m (Peer ps 'AsClient stdone m b, c)
forall a. Void -> a
absurd (NobodyHasAgency st' -> ClientHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
NobodyHasAgency st -> ClientHasAgency st -> Void
exclusionLemma_NobodyAndClientHaveAgency NobodyHasAgency st'
stB ClientHasAgency st'
stA)

    goReceiver (ReceiverAwait (ServerAgency ServerHasAgency st'
stA) forall (st' :: ps).
Message ps st' st' -> PeerReceiver ps pr st' stdone m c
_) (Await (ClientAgency ClientHasAgency st'
stB) forall (st' :: ps).
Message ps st' st' -> Peer ps (FlipAgency pr) st' m b
_) =
      Void -> m (Peer ps 'AsServer stdone m b, c)
forall a. Void -> a
absurd (ClientHasAgency st' -> ServerHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
ClientHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_ClientAndServerHaveAgency ClientHasAgency st'
stB ServerHasAgency st'
stA)

    goReceiver (ReceiverAwait (ClientAgency ClientHasAgency st'
stA) forall (st' :: ps).
Message ps st' st' -> PeerReceiver ps pr st' stdone m c
_) (Await (ServerAgency ServerHasAgency st'
stB) forall (st' :: ps).
Message ps st' st' -> Peer ps (FlipAgency pr) st' m b
_) =
      Void -> m (Peer ps 'AsClient stdone m b, c)
forall a. Void -> a
absurd (ClientHasAgency st' -> ServerHasAgency st' -> Void
forall ps (st :: ps).
Protocol ps =>
ClientHasAgency st -> ServerHasAgency st -> Void
exclusionLemma_ClientAndServerHaveAgency ClientHasAgency st'
stA ServerHasAgency st'
stB)


-- | Prove that we have a total conversion from pipelined peers to regular
-- peers. This is a sanity property that shows that pipelining did not give
-- us extra expressiveness or to break the protocol state machine.
--
forgetPipelined
  :: forall ps (pr :: PeerRole) (st :: ps) m a.
     Functor m
  => PeerPipelined ps pr st m a
  -> Peer          ps pr st m a
forgetPipelined :: PeerPipelined ps pr st m a -> Peer ps pr st m a
forgetPipelined (PeerPipelined PeerSender ps pr st 'Z c m a
peer) = Queue 'Z c -> PeerSender ps pr st 'Z c m a -> Peer ps pr st m a
forall (st' :: ps) (n :: N) c.
Queue n c -> PeerSender ps pr st' n c m a -> Peer ps pr st' m a
goSender Queue 'Z c
forall a. Queue 'Z a
EmptyQ PeerSender ps pr st 'Z c m a
peer
  where
    goSender :: forall st' n c.
                Queue                n c
             -> PeerSender ps pr st' n c m a
             -> Peer       ps pr st'     m a

    goSender :: Queue n c -> PeerSender ps pr st' n c m a -> Peer ps pr st' m a
goSender Queue n c
EmptyQ (SenderDone     NobodyHasAgency st'
st     a
k) = NobodyHasAgency st' -> a -> Peer ps pr st' m a
forall ps (st :: ps) a (pr :: PeerRole) (m :: * -> *).
NobodyHasAgency st -> a -> Peer ps pr st m a
Done NobodyHasAgency st'
st a
k
    goSender Queue n c
q      (SenderEffect          m (PeerSender ps pr st' n c m a)
k) = m (Peer ps pr st' m a) -> Peer ps pr st' m a
forall (m :: * -> *) ps (pr :: PeerRole) (st :: ps) a.
m (Peer ps pr st m a) -> Peer ps pr st m a
Effect (Queue n c -> PeerSender ps pr st' n c m a -> Peer ps pr st' m a
forall (st' :: ps) (n :: N) c.
Queue n c -> PeerSender ps pr st' n c m a -> Peer ps pr st' m a
goSender Queue n c
q (PeerSender ps pr st' n c m a -> Peer ps pr st' m a)
-> m (PeerSender ps pr st' n c m a) -> m (Peer ps pr st' m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (PeerSender ps pr st' n c m a)
k)
    goSender Queue n c
q      (SenderYield    WeHaveAgency pr st'
st Message ps st' st'
m   PeerSender ps pr st' 'Z c m a
k) = WeHaveAgency pr st'
-> Message ps st' st' -> Peer ps pr st' m a -> Peer ps pr st' m a
forall (pr :: PeerRole) ps (st :: ps) (st' :: ps) (m :: * -> *) a.
WeHaveAgency pr st
-> Message ps st st' -> Peer ps pr st' m a -> Peer ps pr st m a
Yield WeHaveAgency pr st'
st Message ps st' st'
m (Queue n c -> PeerSender ps pr st' n c m a -> Peer ps pr st' m a
forall (st' :: ps) (n :: N) c.
Queue n c -> PeerSender ps pr st' n c m a -> Peer ps pr st' m a
goSender Queue n c
q PeerSender ps pr st' n c m a
PeerSender ps pr st' 'Z c m a
k)
    goSender Queue n c
q      (SenderAwait    TheyHaveAgency pr st'
st     forall (st' :: ps).
Message ps st' st' -> PeerSender ps pr st' 'Z c m a
k) = TheyHaveAgency pr st'
-> (forall (st' :: ps). Message ps st' st' -> Peer ps pr st' m a)
-> Peer ps pr st' m a
forall (pr :: PeerRole) ps (st :: ps) (m :: * -> *) a.
TheyHaveAgency pr st
-> (forall (st' :: ps). Message ps st st' -> Peer ps pr st' m a)
-> Peer ps pr st m a
Await TheyHaveAgency pr st'
st   (Queue n c -> PeerSender ps pr st' n c m a -> Peer ps pr st' m a
forall (st' :: ps) (n :: N) c.
Queue n c -> PeerSender ps pr st' n c m a -> Peer ps pr st' m a
goSender Queue n c
q (PeerSender ps pr st' n c m a -> Peer ps pr st' m a)
-> (Message ps st' st' -> PeerSender ps pr st' n c m a)
-> Message ps st' st'
-> Peer ps pr st' m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Message ps st' st' -> PeerSender ps pr st' n c m a
forall (st' :: ps).
Message ps st' st' -> PeerSender ps pr st' 'Z c m a
k)
    goSender Queue n c
q      (SenderPipeline WeHaveAgency pr st'
st Message ps st' st'
m PeerReceiver ps pr st' st'' m c
r PeerSender ps pr st'' ('S n) c m a
k) = WeHaveAgency pr st'
-> Message ps st' st' -> Peer ps pr st' m a -> Peer ps pr st' m a
forall (pr :: PeerRole) ps (st :: ps) (st' :: ps) (m :: * -> *) a.
WeHaveAgency pr st
-> Message ps st st' -> Peer ps pr st' m a -> Peer ps pr st m a
Yield WeHaveAgency pr st'
st Message ps st' st'
m (Queue n c
-> PeerSender ps pr st'' ('S n) c m a
-> PeerReceiver ps pr st' st'' m c
-> Peer ps pr st' m a
forall (stCurrent :: ps) (stNext :: ps) (n :: N) c.
Queue n c
-> PeerSender ps pr stNext ('S n) c m a
-> PeerReceiver ps pr stCurrent stNext m c
-> Peer ps pr stCurrent m a
goReceiver Queue n c
q PeerSender ps pr st'' ('S n) c m a
k PeerReceiver ps pr st' st'' m c
r)
    goSender (ConsQ c
x Queue n c
q) (SenderCollect  Maybe (PeerSender ps pr st' ('S n) c m a)
_ c -> PeerSender ps pr st' n c m a
k) = Queue n c -> PeerSender ps pr st' n c m a -> Peer ps pr st' m a
forall (st' :: ps) (n :: N) c.
Queue n c -> PeerSender ps pr st' n c m a -> Peer ps pr st' m a
goSender Queue n c
q (c -> PeerSender ps pr st' n c m a
k c
x)
    -- Here by picking the second continuation in Collect we resolve the
    -- non-determinism by always picking the fully in-order non-pipelined
    -- data flow path.

    goReceiver :: forall stCurrent stNext n c.
                  Queue                        n  c
               -> PeerSender   ps pr stNext (S n) c   m a
               -> PeerReceiver ps pr stCurrent stNext m c
               -> Peer         ps pr stCurrent        m a

    goReceiver :: Queue n c
-> PeerSender ps pr stNext ('S n) c m a
-> PeerReceiver ps pr stCurrent stNext m c
-> Peer ps pr stCurrent m a
goReceiver Queue n c
q PeerSender ps pr stNext ('S n) c m a
s (ReceiverDone     c
x) = Queue ('S n) c
-> PeerSender ps pr stNext ('S n) c m a -> Peer ps pr stNext m a
forall (st' :: ps) (n :: N) c.
Queue n c -> PeerSender ps pr st' n c m a -> Peer ps pr st' m a
goSender (c -> Queue n c -> Queue ('S n) c
forall a (n :: N). a -> Queue n a -> Queue ('S n) a
enqueue c
x Queue n c
q) PeerSender ps pr stNext ('S n) c m a
s
    goReceiver Queue n c
q PeerSender ps pr stNext ('S n) c m a
s (ReceiverEffect   m (PeerReceiver ps pr stCurrent stNext m c)
k) = m (Peer ps pr stCurrent m a) -> Peer ps pr stCurrent m a
forall (m :: * -> *) ps (pr :: PeerRole) (st :: ps) a.
m (Peer ps pr st m a) -> Peer ps pr st m a
Effect (Queue n c
-> PeerSender ps pr stNext ('S n) c m a
-> PeerReceiver ps pr stCurrent stNext m c
-> Peer ps pr stCurrent m a
forall (stCurrent :: ps) (stNext :: ps) (n :: N) c.
Queue n c
-> PeerSender ps pr stNext ('S n) c m a
-> PeerReceiver ps pr stCurrent stNext m c
-> Peer ps pr stCurrent m a
goReceiver Queue n c
q PeerSender ps pr stNext ('S n) c m a
s (PeerReceiver ps pr stCurrent stNext m c
 -> Peer ps pr stCurrent m a)
-> m (PeerReceiver ps pr stCurrent stNext m c)
-> m (Peer ps pr stCurrent m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (PeerReceiver ps pr stCurrent stNext m c)
k)
    goReceiver Queue n c
q PeerSender ps pr stNext ('S n) c m a
s (ReceiverAwait TheyHaveAgency pr stCurrent
st forall (st' :: ps).
Message ps stCurrent st' -> PeerReceiver ps pr st' stNext m c
k) = TheyHaveAgency pr stCurrent
-> (forall (st' :: ps).
    Message ps stCurrent st' -> Peer ps pr st' m a)
-> Peer ps pr stCurrent m a
forall (pr :: PeerRole) ps (st :: ps) (m :: * -> *) a.
TheyHaveAgency pr st
-> (forall (st' :: ps). Message ps st st' -> Peer ps pr st' m a)
-> Peer ps pr st m a
Await TheyHaveAgency pr stCurrent
st (Queue n c
-> PeerSender ps pr stNext ('S n) c m a
-> PeerReceiver ps pr st' stNext m c
-> Peer ps pr st' m a
forall (stCurrent :: ps) (stNext :: ps) (n :: N) c.
Queue n c
-> PeerSender ps pr stNext ('S n) c m a
-> PeerReceiver ps pr stCurrent stNext m c
-> Peer ps pr stCurrent m a
goReceiver Queue n c
q PeerSender ps pr stNext ('S n) c m a
s (PeerReceiver ps pr st' stNext m c -> Peer ps pr st' m a)
-> (Message ps stCurrent st' -> PeerReceiver ps pr st' stNext m c)
-> Message ps stCurrent st'
-> Peer ps pr st' m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Message ps stCurrent st' -> PeerReceiver ps pr st' stNext m c
forall (st' :: ps).
Message ps stCurrent st' -> PeerReceiver ps pr st' stNext m c
k)


-- | A size indexed queue. This is useful for proofs, including
-- 'connectPipelined' but also as so-called @direct@ functions for running a
-- client and server wrapper directly against each other.
--
data Queue (n :: N) a where
  EmptyQ ::                   Queue  Z    a
  ConsQ  :: a -> Queue n a -> Queue (S n) a

-- | At an element to the end of a 'Queue'. This is not intended to be
-- efficient. It is only for proofs and tests.
--
enqueue :: a -> Queue n a -> Queue (S n) a
enqueue :: a -> Queue n a -> Queue ('S n) a
enqueue a
a  Queue n a
EmptyQ     = a -> Queue 'Z a -> Queue ('S 'Z) a
forall a (n :: N). a -> Queue n a -> Queue ('S n) a
ConsQ a
a Queue 'Z a
forall a. Queue 'Z a
EmptyQ
enqueue a
a (ConsQ a
b Queue n a
q) = a -> Queue ('S n) a -> Queue ('S ('S n)) a
forall a (n :: N). a -> Queue n a -> Queue ('S n) a
ConsQ a
b (a -> Queue n a -> Queue ('S n) a
forall a (n :: N). a -> Queue n a -> Queue ('S n) a
enqueue a
a Queue n a
q)


-- | A reference specification for interleaving of requests and responses
-- with pipelining, where the environment can choose whether a response is
-- available yet.
--
-- This also supports bounded choice where the maximum number of outstanding
-- in-flight responses is limted.
--
pipelineInterleaving :: Int    -- ^ Bound on outstanding responses
                     -> [Bool] -- ^ Pipelining choices
                     -> [req] -> [resp] -> [Either req resp]
pipelineInterleaving :: Int -> [Bool] -> [req] -> [resp] -> [Either req resp]
pipelineInterleaving Int
omax [Bool]
cs0 [req]
reqs0 [resp]
resps0 =
    Int -> [Bool] -> [(Int, req)] -> [(Int, resp)] -> [Either req resp]
go Int
0 [Bool]
cs0 ([Int] -> [req] -> [(Int, req)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] [req]
reqs0)
             ([Int] -> [resp] -> [(Int, resp)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] [resp]
resps0)
  where
    go :: Int -> [Bool] -> [(Int, req)] -> [(Int, resp)] -> [Either req resp]
go Int
o (Bool
c:[Bool]
cs) reqs :: [(Int, req)]
reqs@((Int
reqNo, req
req) :[(Int, req)]
reqs')
               resps :: [(Int, resp)]
resps@((Int
respNo,resp
resp):[(Int, resp)]
resps')
      | Int
respNo Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
reqNo = req -> Either req resp
forall a b. a -> Either a b
Left  req
req   Either req resp -> [Either req resp] -> [Either req resp]
forall a. a -> [a] -> [a]
: Int -> [Bool] -> [(Int, req)] -> [(Int, resp)] -> [Either req resp]
go (Int
oInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Bool
cBool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
:[Bool]
cs) [(Int, req)]
reqs' [(Int, resp)]
resps
      | Bool
c Bool -> Bool -> Bool
&& Int
o Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
omax   = req -> Either req resp
forall a b. a -> Either a b
Left  req
req   Either req resp -> [Either req resp] -> [Either req resp]
forall a. a -> [a] -> [a]
: Int -> [Bool] -> [(Int, req)] -> [(Int, resp)] -> [Either req resp]
go (Int
oInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)    [Bool]
cs  [(Int, req)]
reqs' [(Int, resp)]
resps
      | Bool
otherwise       = resp -> Either req resp
forall a b. b -> Either a b
Right resp
resp  Either req resp -> [Either req resp] -> [Either req resp]
forall a. a -> [a] -> [a]
: Int -> [Bool] -> [(Int, req)] -> [(Int, resp)] -> [Either req resp]
go (Int
oInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)    [Bool]
cs  [(Int, req)]
reqs  [(Int, resp)]
resps'

    go Int
o []     reqs :: [(Int, req)]
reqs@((Int
reqNo, req
req) :[(Int, req)]
reqs')
               resps :: [(Int, resp)]
resps@((Int
respNo,resp
resp):[(Int, resp)]
resps')
      | Int
respNo Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
reqNo = req -> Either req resp
forall a b. a -> Either a b
Left  req
req   Either req resp -> [Either req resp] -> [Either req resp]
forall a. a -> [a] -> [a]
: Int -> [Bool] -> [(Int, req)] -> [(Int, resp)] -> [Either req resp]
go (Int
oInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [] [(Int, req)]
reqs' [(Int, resp)]
resps
      | Bool
otherwise       = resp -> Either req resp
forall a b. b -> Either a b
Right resp
resp  Either req resp -> [Either req resp] -> [Either req resp]
forall a. a -> [a] -> [a]
: Int -> [Bool] -> [(Int, req)] -> [(Int, resp)] -> [Either req resp]
go (Int
oInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [] [(Int, req)]
reqs  [(Int, resp)]
resps'

    go Int
_ [Bool]
_ [] [(Int, resp)]
resps     = ((Int, resp) -> Either req resp)
-> [(Int, resp)] -> [Either req resp]
forall a b. (a -> b) -> [a] -> [b]
map (resp -> Either req resp
forall a b. b -> Either a b
Right (resp -> Either req resp)
-> ((Int, resp) -> resp) -> (Int, resp) -> Either req resp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, resp) -> resp
forall a b. (a, b) -> b
snd) [(Int, resp)]
resps
    go Int
_ [Bool]
_ ((Int, req)
_:[(Int, req)]
_) []     = [Char] -> [Either req resp]
forall a. HasCallStack => [Char] -> a
error [Char]
"pipelineInterleaving: not enough responses"