{-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE PolyKinds #-} module Network.TypedProtocol.ReqResp.Type where import Network.TypedProtocol.Core data ReqResp req resp where StIdle :: ReqResp req resp StBusy :: ReqResp req resp StDone :: ReqResp req resp instance Protocol (ReqResp req resp) where data Message (ReqResp req resp) from to where MsgReq :: req -> Message (ReqResp req resp) StIdle StBusy MsgResp :: resp -> Message (ReqResp req resp) StBusy StIdle MsgDone :: Message (ReqResp req resp) StIdle StDone data ClientHasAgency st where TokIdle :: ClientHasAgency StIdle data ServerHasAgency st where TokBusy :: ServerHasAgency StBusy data NobodyHasAgency st where TokDone :: NobodyHasAgency StDone exclusionLemma_ClientAndServerHaveAgency :: ClientHasAgency st -> ServerHasAgency st -> Void exclusionLemma_ClientAndServerHaveAgency ClientHasAgency st TokIdle ServerHasAgency st tok = case ServerHasAgency st tok of {} exclusionLemma_NobodyAndClientHaveAgency :: NobodyHasAgency st -> ClientHasAgency st -> Void exclusionLemma_NobodyAndClientHaveAgency NobodyHasAgency st TokDone ClientHasAgency st tok = case ClientHasAgency st tok of {} exclusionLemma_NobodyAndServerHaveAgency :: NobodyHasAgency st -> ServerHasAgency st -> Void exclusionLemma_NobodyAndServerHaveAgency NobodyHasAgency st TokDone ServerHasAgency st tok = case ServerHasAgency st tok of {} deriving instance (Show req, Show resp) => Show (Message (ReqResp req resp) from to) deriving instance (Eq req, Eq resp) => Eq (Message (ReqResp req resp) from to) instance Show (ClientHasAgency (st :: ReqResp req resp)) where show :: ClientHasAgency st -> String show ClientHasAgency st TokIdle = String "TokIdle" instance Show (ServerHasAgency (st :: ReqResp req resp)) where show :: ServerHasAgency st -> String show ServerHasAgency st TokBusy = String "TokBusy"