{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
{-# OPTIONS_GHC -fno-warn-unused-top-binds #-}
module Control.Protocol.Example
( MyProtocol,
MyCommand (..),
scenario,
Party (..),
ChannelState (..),
)
where
import Control.Protocol
import Control.XMonad.Do
import Data.Singletons.TH
import Prelude hiding ((>>), (>>=))
$( singletons
[d|
data Party = Recipient | Broker | Sender
deriving (Show, Eq)
|]
)
data ChannelState
= None
| Ready
| Busy
deriving (Show, Eq)
data MyCommand :: Command Party ChannelState where
Create :: MyCommand '(Recipient, None, Ready) '(Broker, None, Ready) ()
Notify :: MyCommand '(Recipient, Ready, Ready) '(Sender, None, Ready) ()
Send :: String -> MyCommand '(Sender, Ready, Ready) '(Broker, Ready, Busy) ()
Forward :: MyCommand '(Broker, Busy, Ready) '(Recipient, Ready, Ready) String
type MyProtocol = Protocol MyCommand '[Recipient, Broker, Sender]
r :: Sing Recipient
r = SRecipient
b :: Sing Broker
b = SBroker
s :: Sing Sender
s = SSender
scenario :: String -> MyProtocol '[None, None, None] '[Ready, Ready, Ready] String
scenario str = do
r ->: b $ Create
r ->: s $ Notify
s ->: b $ Send str
b ->: r $ Forward