diff --git a/definitions/src/Simplex/Messaging/Broker.hs b/definitions/src/Simplex/Messaging/Broker.hs index 16eadaf5a8..8b7965b93e 100644 --- a/definitions/src/Simplex/Messaging/Broker.hs +++ b/definitions/src/Simplex/Messaging/Broker.hs @@ -1,7 +1,12 @@ {-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-} -{-# OPTIONS_GHC -fno-warn-orphans #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} +{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeOperators #-} module Simplex.Messaging.Broker where @@ -9,35 +14,19 @@ import ClassyPrelude import Simplex.Messaging.Protocol import Simplex.Messaging.Types --- For some reason PrfCmd type-class requirement is not enforced here: --- if I change one of the connection states to one for which --- instance of PrfCmd does not exist (i.e. Command cannot be constructed), --- it compiles anyway. --- Creating Command instance here would prevent compilation --- in case the types are incorrect, as it is done in Client.hs -instance ProtocolFunc Broker CreateConnCmd - CreateConnRequest CreateConnResponse -- request response - None New Idle Idle -- connection states - where - protoFunc _ = bCreateConn + +instance Prf HasState Sender s + => ProtocolCommandOf Broker + CreateConnRequest CreateConnResponse + Recipient Broker + (None <==> None <==| s) + (New <==> New <==| s) + Idle Idle 0 0 + where + command = CreateConn + protoCmd = bCreateConn bCreateConn :: Connection Broker None Idle -> CreateConnRequest - -> Either String - (CreateConnResponse, Connection Broker New Idle) -bCreateConn (Connection str) _ = Right (CreateConnResponse "1" "2", Connection str) --- TODO stub - - --- below code should NOT compile, but it does -instance ProtocolFunc Broker CreateConnCmd - CreateConnRequest CreateConnResponse -- request response - None Secured Idle Idle -- "Secured" should not be allowed here, - where -- such command does not exist, so no instance of - protoFunc _ = bCreateConn' -- PrfCmd exist...? But it compiles. - -bCreateConn' :: Connection Broker None Idle - -> CreateConnRequest - -> Either String - (CreateConnResponse, Connection Broker Secured Idle) -bCreateConn' (Connection str) _ = Right (CreateConnResponse "1" "2", Connection str) + -> Either String (CreateConnResponse, Connection Broker New Idle) +bCreateConn = protoCmdStub diff --git a/definitions/src/Simplex/Messaging/Client.hs b/definitions/src/Simplex/Messaging/Client.hs index 96d4bbbf47..93d3fe81f5 100644 --- a/definitions/src/Simplex/Messaging/Client.hs +++ b/definitions/src/Simplex/Messaging/Client.hs @@ -1,8 +1,12 @@ {-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-} -{-# OPTIONS_GHC -fno-warn-orphans #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} +{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} module Simplex.Messaging.Client where @@ -10,16 +14,20 @@ import ClassyPrelude import Simplex.Messaging.Protocol import Simplex.Messaging.Types - -instance ProtocolAction Recipient CreateConnCmd - CreateConnRequest CreateConnResponse -- request responce - None New Idle Idle -- connection states - where - protoAction _ = \(Connection str) _ _ -> Connection str -- TODO stub +instance Prf HasState Sender s + => ProtocolActionOf Recipient + CreateConnRequest CreateConnResponse + Recipient Broker + (None <==> None <==| s) + (New <==> New <==| s) + Idle Idle 0 0 + where + action = CreateConn + protoAction = rCreateConn rCreateConn :: Connection Recipient None Idle -> CreateConnRequest -> Either String CreateConnResponse - -> Connection Recipient New Idle -rCreateConn = protoAction $ CreateConn @None + -> Either String (Connection Recipient New Idle) +rCreateConn = protoActionStub diff --git a/definitions/src/Simplex/Messaging/Protocol.hs b/definitions/src/Simplex/Messaging/Protocol.hs index b3883a8c0f..0ab9406642 100644 --- a/definitions/src/Simplex/Messaging/Protocol.hs +++ b/definitions/src/Simplex/Messaging/Protocol.hs @@ -1,4 +1,5 @@ {-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-} +{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE EmptyCase #-} @@ -41,7 +42,7 @@ $(singletons [d| | Drained -- (broker, recipient) drained (no messages) deriving (Show, ShowSing, Eq) - data ConnectionSubscription = Subscribed | Idle + data ConnSubscription = Subscribed | Idle |]) -- broker connection states @@ -96,7 +97,7 @@ data EstablishedState (s :: ConnectionState) :: Type where -- connection type stub for all participants, TODO move from idris data Connection (p :: Participant) (s :: ConnectionState) - (ss :: ConnectionSubscription) :: Type where + (ss :: ConnSubscription) :: Type where Connection :: String -> Connection p s ss -- TODO replace with real type definition @@ -112,19 +113,16 @@ data (<==>) (rs :: ConnectionState) (bs :: ConnectionState) :: Type where deriving instance Show (rs <==> bs) -data AllConnState (rs :: ConnectionState) - (bs :: ConnectionState) - (ss :: ConnectionState) :: Type where +data family (<==|) rb (ss :: ConnectionState) :: Type +data instance (<==|) (rs <==> bs) ss :: Type where (:<==|) :: Prf HasState Sender ss => rs <==> bs -> Sing ss - -> AllConnState rs bs ss + -> rs <==> bs <==| ss -deriving instance Show (AllConnState rs bs ss) - -type family (<==|) rb ss where - (rs <==> bs) <==| (ss :: ConnectionState) = AllConnState rs bs ss +deriving instance Show (rs <==> bs <==| ss) +-- example of states of connection for all participants -- recipient <==> broker <==| sender st2 :: Pending <==> New <==| Confirmed st2 = SPending :<==> SNew :<==| SConfirmed @@ -134,32 +132,16 @@ st2 = SPending :<==> SNew :<==| SConfirmed -- stBad = SPending :<==> SConfirmed :<==| SConfirmed --- data type with all available protocol commands -$(singletons [d| - data ProtocolCmd = CreateConnCmd - | SubscribeCmd - | UnsubscribeCmd - | SendInviteCmd - | ConfirmConnCmd - | PushConfirmCmd - | SecureConnCmd - | SendWelcomeCmd - | SendMsgCmd - | PushMsgCmd - | DeleteMsgCmd - | Comp -- result of composing multiple commands - |]) - infixl 4 :>>, :>>= -data Command (cmd :: ProtocolCmd) arg result +data Command arg result (from :: Participant) (to :: Participant) state state' - (ss :: ConnectionSubscription) (ss' :: ConnectionSubscription) + (ss :: ConnSubscription) (ss' :: ConnSubscription) (messages :: Nat) (messages' :: Nat) :: Type where CreateConn :: Prf HasState Sender s - => Command CreateConnCmd + => Command CreateConnRequest CreateConnResponse Recipient Broker (None <==> None <==| s) @@ -169,7 +151,7 @@ data Command (cmd :: ProtocolCmd) arg result Subscribe :: ( (r /= None && r /= Disabled) ~ True , (b /= None && b /= Disabled) ~ True , Prf HasState Sender s ) - => Command SubscribeCmd + => Command () () Recipient Broker (r <==> b <==| s) @@ -179,7 +161,7 @@ data Command (cmd :: ProtocolCmd) arg result Unsubscribe :: ( (r /= None && r /= Disabled) ~ True , (b /= None && b /= Disabled) ~ True , Prf HasState Sender s ) - => Command UnsubscribeCmd + => Command () () Recipient Broker (r <==> b <==| s) @@ -187,7 +169,7 @@ data Command (cmd :: ProtocolCmd) arg result Subscribed Idle n n SendInvite :: Prf HasState Broker s - => Command SendInviteCmd + => Command String () -- invitation - TODO Recipient Sender (New <==> s <==| None) @@ -195,7 +177,7 @@ data Command (cmd :: ProtocolCmd) arg result ss ss n n ConfirmConn :: Prf HasState Recipient s - => Command ConfirmConnCmd + => Command SecureConnRequest () Sender Broker (s <==> New <==| New) @@ -203,7 +185,7 @@ data Command (cmd :: ProtocolCmd) arg result ss ss n (n+1) PushConfirm :: Prf HasState Sender s - => Command PushConfirmCmd + => Command SecureConnRequest () Broker Recipient (Pending <==> New <==| s) @@ -211,7 +193,7 @@ data Command (cmd :: ProtocolCmd) arg result Subscribed Subscribed n n SecureConn :: Prf HasState Sender s - => Command SecureConnCmd + => Command SecureConnRequest () Recipient Broker (Confirmed <==> New <==| s) @@ -219,7 +201,7 @@ data Command (cmd :: ProtocolCmd) arg result ss ss n n SendWelcome :: Prf HasState Recipient s - => Command SendWelcomeCmd + => Command () () Sender Broker (s <==> Secured <==| Confirmed) @@ -227,7 +209,7 @@ data Command (cmd :: ProtocolCmd) arg result ss ss n (n+1) SendMsg :: Prf HasState Recipient s - => Command SendMsgCmd + => Command SendMessageRequest () Sender Broker (s <==> Secured <==| Secured) @@ -235,7 +217,7 @@ data Command (cmd :: ProtocolCmd) arg result ss ss n (n+1) PushMsg :: Prf HasState 'Sender s - => Command PushMsgCmd + => Command MessagesResponse () -- TODO, has to be a single message Broker Recipient (Secured <==> Secured <==| s) @@ -243,100 +225,93 @@ data Command (cmd :: ProtocolCmd) arg result Subscribed Subscribed n n DeleteMsg :: Prf HasState Sender s - => Command DeleteMsgCmd + => Command () () -- TODO needs message ID parameter Recipient Broker (Secured <==> Secured <==| s) (Secured <==> Secured <==| s) ss ss n (n-1) --- this command has to be removed - this is here to allow proof --- that any command can be constructed - AnyCmd :: Command cmd a b from to s1 s2 ss1 ss2 n1 n2 + Return :: b -> Command a b from to state state ss ss n n - Return :: b -> Command Comp a b from to state state ss ss n n + (:>>=) :: Command a b from1 to1 s1 s2 ss1 ss2 n1 n2 + -> (b -> Command b c from2 to2 s2 s3 ss2 ss3 n2 n3) + -> Command a c from1 to2 s1 s3 ss1 ss3 n1 n3 - (:>>=) :: Command cmd1 a b from1 to1 s1 s2 ss1 ss2 n1 n2 - -> (b -> Command cmd2 b c from2 to2 s2 s3 ss2 ss3 n2 n3) - -> Command Comp a c from1 to2 s1 s3 ss1 ss3 n1 n3 - - (:>>) :: Command cmd1 a b from1 to1 s1 s2 ss1 ss2 n1 n2 - -> Command cmd2 c d from2 to2 s2 s3 ss2 ss3 n2 n3 - -> Command Comp a d from1 to2 s1 s3 ss1 ss3 n1 n3 + (:>>) :: Command a b from1 to1 s1 s2 ss1 ss2 n1 n2 + -> Command c d from2 to2 s2 s3 ss2 ss3 n2 n3 + -> Command a d from1 to2 s1 s3 ss1 ss3 n1 n3 Fail :: String - -> Command Comp a String from to state (None <==> None <==| None) ss ss n n + -> Command a String from to state (None <==> None <==| None) ss ss n n -- redifine Monad operators to compose commands -- using `do` notation with RebindableSyntax extension -(>>=) :: Command cmd1 a b from1 to1 s1 s2 ss1 ss2 n1 n2 - -> (b -> Command cmd2 b c from2 to2 s2 s3 ss2 ss3 n2 n3) - -> Command Comp a c from1 to2 s1 s3 ss1 ss3 n1 n3 +(>>=) :: Command a b from1 to1 s1 s2 ss1 ss2 n1 n2 + -> (b -> Command b c from2 to2 s2 s3 ss2 ss3 n2 n3) + -> Command a c from1 to2 s1 s3 ss1 ss3 n1 n3 (>>=) = (:>>=) -(>>) :: Command cmd1 a b from1 to1 s1 s2 ss1 ss2 n1 n2 - -> Command cmd2 c d from2 to2 s2 s3 ss2 ss3 n2 n3 - -> Command Comp a d from1 to2 s1 s3 ss1 ss3 n1 n3 +(>>) :: Command a b from1 to1 s1 s2 ss1 ss2 n1 n2 + -> Command c d from2 to2 s2 s3 ss2 ss3 n2 n3 + -> Command a d from1 to2 s1 s3 ss1 ss3 n1 n3 (>>) = (:>>) -fail :: String -> Command Comp a String from to state (None <==> None <==| None) ss ss n n +fail :: String -> Command a String from to state (None <==> None <==| None) ss ss n n fail = Fail -- show and validate expexcted command participants infix 6 --> (-->) :: Sing from -> Sing to - -> ( Command cmd a b from to s s' ss ss' n n' - -> Command cmd a b from to s s' ss ss' n n' ) + -> ( Command a b from to s s' ss ss' n n' + -> Command a b from to s s' ss ss' n n' ) (-->) _ _ = id -- extract connection state of specfic participant type family PConnSt (p :: Participant) state where - PConnSt Recipient (AllConnState r b s) = r - PConnSt Broker (AllConnState r b s) = b - PConnSt Sender (AllConnState r b s) = s + PConnSt Recipient (r <==> b <==| s) = r + PConnSt Broker (r <==> b <==| s) = b + PConnSt Sender (r <==> b <==| s) = s -- Type classes to ensure consistency of types of implementations -- of participants actions/functions and connection state transitions (types) -- with types of protocol commands defined above. --- TODO for some reason this type class is not enforced - --- it still allows to construct invalid implementations. --- See comment in Broker.hs --- As done in Client.hs it type-checks, but it looks ugly -class PrfCmd cmd arg res from to s s' ss ss' n n' where - command :: Command cmd arg res from to s s' ss ss' n n' -instance Prf HasState Sender s - => PrfCmd CreateConnCmd - CreateConnRequest CreateConnResponse - Recipient Broker - (AllConnState None None s) - (AllConnState New New s) - Idle Idle 0 0 - where - command = CreateConn +class me ~ p => ProtocolCommandOf (me :: Participant) + arg res + (from :: Participant) (p :: Participant) + state state' + (ss :: ConnSubscription) (ss' :: ConnSubscription) + (n :: Nat) (n' :: Nat) + where + command :: Command arg res from p state state' ss ss' n n' + protoCmd :: Connection p (PConnSt p state) ss + -> arg + -> Either String (res, Connection p (PConnSt p state') ss') + +protoCmdStub :: Connection p ps ss + -> arg + -> Either String (res, Connection p ps' ss') +protoCmdStub _ _ = Left "Command not implemented" -class ProtocolFunc (p :: Participant) (cmd :: ProtocolCmd) arg res ps ps' ss ss' where - protoFunc :: ( PrfCmd cmd arg res from p s s' ss ss' n n' - , PConnSt p s ~ ps - , PConnSt p s' ~ ps' ) - => Command cmd arg res - from p -- participant receives this command - s s' ss ss' n n' - -> ( Connection p ps ss - -> arg - -> Either String (res, Connection p ps' ss') ) +class me ~ p => ProtocolActionOf (me :: Participant) + arg res + (p :: Participant) (to :: Participant) + state state' + (ss :: ConnSubscription) (ss' :: ConnSubscription) + (n :: Nat) (n' :: Nat) + where + action :: Command arg res p to state state' ss ss' n n' + protoAction :: Connection p (PConnSt p state) ss + -> arg + -> Either String res + -> Either String (Connection p (PConnSt p state') ss') -class ProtocolAction (p :: Participant) (cmd :: ProtocolCmd) arg res ps ps' ss ss' where - protoAction :: ( PrfCmd cmd arg res p to s s' ss ss' n n' - , PConnSt p s ~ ps - , PConnSt p s' ~ ps' ) - => Command cmd arg res - p to -- participant sends this command - s s' ss ss' n n' - -> ( Connection p ps ss - -> arg - -> Either String res - -> Connection p ps' ss' ) +protoActionStub :: Connection p ps ss + -> arg + -> Either String res + -> Either String (Connection p ps' ss') +protoActionStub _ _ _ = Left "Action not implemented" diff --git a/definitions/src/Simplex/Messaging/Scenarios.hs b/definitions/src/Simplex/Messaging/Scenarios.hs index 9c9b5f0e09..c60395aaf2 100644 --- a/definitions/src/Simplex/Messaging/Scenarios.hs +++ b/definitions/src/Simplex/Messaging/Scenarios.hs @@ -23,7 +23,7 @@ b = SBroker s :: Sing Sender s = SSender -establishConnection :: Command Comp +establishConnection :: Command CreateConnRequest () Recipient Broker (None <==> None <==| None) diff --git a/definitions/src/Simplex/Messaging/Test.hs b/definitions/src/Simplex/Messaging/Test.hs new file mode 100644 index 0000000000..42e9085b0d --- /dev/null +++ b/definitions/src/Simplex/Messaging/Test.hs @@ -0,0 +1,246 @@ +{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-} +{-# OPTIONS_GHC -freduction-depth=0 #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NoStarIsType #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module Simplex.Messaging.Test where + +import ClassyPrelude +import Data.Kind +import Data.Singletons +import Data.Singletons.ShowSing +import Data.Singletons.TH +import Data.Type.Predicate +import Data.Type.Predicate.Auto +import Simplex.Messaging.Types + +$(singletons [d| + data Participant = Recipient | Broker | Sender + + data ConnectionState = None -- (all) not available or removed from the broker + | New -- (participants: all) connection created (or received from sender) + | Pending -- (recipient) sent to sender out-of-band + | Confirmed -- (recipient) confirmed by sender with the broker + | Secured -- (all) secured with the broker + | Disabled -- (broker, recipient) disabled with the broker by recipient + | Drained -- (broker, recipient) drained (no messages) + deriving (Show, ShowSing, Eq) + + data ConnSubscription = Subscribed | Idle + |]) + +-- broker connection states +type Prf1 t a = Auto (TyPred t) a + +data BrokerCS :: ConnectionState -> Type where + BrkNew :: BrokerCS New + BrkSecured :: BrokerCS Secured + BrkDisabled :: BrokerCS Disabled + BrkDrained :: BrokerCS Drained + BrkNone :: BrokerCS None + +instance Auto (TyPred BrokerCS) New where auto = autoTC +instance Auto (TyPred BrokerCS) Secured where auto = autoTC +instance Auto (TyPred BrokerCS) Disabled where auto = autoTC +instance Auto (TyPred BrokerCS) Drained where auto = autoTC +instance Auto (TyPred BrokerCS) None where auto = autoTC + +-- sender connection states +data SenderCS :: ConnectionState -> Type where + SndNew :: SenderCS New + SndConfirmed :: SenderCS Confirmed + SndSecured :: SenderCS Secured + SndNone :: SenderCS None + +instance Auto (TyPred SenderCS) New where auto = autoTC +instance Auto (TyPred SenderCS) Confirmed where auto = autoTC +instance Auto (TyPred SenderCS) Secured where auto = autoTC +instance Auto (TyPred SenderCS) None where auto = autoTC + +-- allowed participant connection states +data HasState (p :: Participant) (s :: ConnectionState) :: Type where + RcpHasState :: HasState Recipient s + BrkHasState :: Prf1 BrokerCS s => HasState Broker s + SndHasState :: Prf1 SenderCS s => HasState Sender s + +class Prf t p s where auto' :: t p s +instance Prf HasState Recipient s + where auto' = RcpHasState +instance Prf1 BrokerCS s => Prf HasState Broker s + where auto' = BrkHasState +instance Prf1 SenderCS s => Prf HasState Sender s + where auto' = SndHasState + + +-- connection type stub for all participants, TODO move from idris +data Connection (p :: Participant) + (s :: ConnectionState) + (ss :: ConnSubscription) :: Type where + Connection :: String -> Connection p s ss -- TODO replace with real type definition + + +-- data types for connection states of all participants +infixl 7 <==>, <==| -- types +infixl 7 :<==>, :<==| -- constructors + +data (<==>) (rs :: ConnectionState) (bs :: ConnectionState) :: Type where + (:<==>) :: (Prf HasState Recipient rs, Prf HasState Broker bs) + => Sing rs + -> Sing bs + -> rs <==> bs + +deriving instance Show (rs <==> bs) + +data family (<==|) rcpBrk (ss :: ConnectionState) :: Type +data instance (<==|) (rs <==> bs) ss :: Type where + (:<==|) :: Prf HasState Sender ss + => rs <==> bs + -> Sing ss + -> rs <==> bs <==| ss + +deriving instance Show (rs <==> bs <==| ss) + +-- type family (<==|) rb ss where +-- (rs <==> bs) <==| (ss :: ConnectionState) = AllConnState rs bs ss + +-- recipient <==> broker <==| sender +st2 :: Pending <==> New <==| Confirmed +st2 = SPending :<==> SNew :<==| SConfirmed + +-- this must not type check +-- stBad :: 'Pending <==> 'Confirmed <==| 'Confirmed +-- stBad = SPending :<==> SConfirmed :<==| SConfirmed + + +-- data type with all available protocol commands +$(singletons [d| + data ProtocolCmd = CreateConnCmd + | SubscribeCmd + | Comp -- result of composing multiple commands + |]) + +data Command (cmd :: ProtocolCmd) arg result + (from :: Participant) (to :: Participant) + state state' + (ss :: ConnSubscription) (ss' :: ConnSubscription) + :: Type where + CreateConn :: Prf HasState Sender s + => Command CreateConnCmd + CreateConnRequest CreateConnResponse + Recipient Broker + (None <==> None <==| s) + (New <==> New <==| s) + Idle Idle + + Subscribe :: ( (r /= None && r /= Disabled) ~ True + , (b /= None && b /= Disabled) ~ True + , Prf HasState Sender s ) + => Command SubscribeCmd + () () + Recipient Broker + (r <==> b <==| s) + (r <==> b <==| s) + Idle Subscribed + +-- extract connection state of specfic participant +type family PConnSt (p :: Participant) state where + PConnSt Recipient (r <==> b <==| s) = r + PConnSt Broker (r <==> b <==| s) = b + PConnSt Sender (r <==> b <==| s) = s + + +-- Type classes to ensure consistency of types of implementations +-- of participants actions/functions and connection state transitions (types) +-- with types of protocol commands defined above. + +-- TODO for some reason this type class is not enforced - +-- it still allows to construct invalid implementations. +-- See comment in Broker.hs +-- As done in Client.hs it type-checks, but it looks ugly +-- class PrfCmd cmd arg res from to s1 s2 s3 s1' s2' s3' ss ss' where +-- command :: Command cmd arg res from to (AllConnState s1 s2 s3) (AllConnState s1' s2' s3') ss ss' +-- instance Prf HasState Sender s +-- => PrfCmd CreateConnCmd +-- CreateConnRequest CreateConnResponse +-- Recipient Broker +-- None None s +-- New New s +-- Idle Idle +-- where +-- command = CreateConn + +-- data Cmd cmd arg res from to ss ss' :: Type where +-- Cmd :: Command cmd arg res +-- from to +-- (AllConnState s1 s2 s3) +-- (AllConnState s1' s2' s3') +-- ss ss' +-- -> Cmd cmd arg res from to ss ss' + +class ProtocolFunc + (cmd :: ProtocolCmd) arg res + (from :: Participant) (p :: Participant) + state state' + (ss :: ConnSubscription) (ss' :: ConnSubscription) + where + pfCommand :: Command (cmd :: ProtocolCmd) arg res + (from :: Participant) (p :: Participant) + state state' + (ss :: ConnSubscription) (ss' :: ConnSubscription) + protoFunc :: Connection p (PConnSt p state) ss + -> arg + -> Either String (res, Connection p (PConnSt p state') ss') + + +-- For some reason PrfCmd type-class requirement is not enforced here: +-- if I change one of the connection states to one for which +-- instance of PrfCmd does not exist (i.e. Command cannot be constructed), +-- it compiles anyway. +-- Creating Command instance here would prevent compilation +-- in case the types are incorrect, as it is done in Client.hs +instance Prf HasState Sender s + => ProtocolFunc CreateConnCmd + CreateConnRequest CreateConnResponse + Recipient Broker + (None <==> None <==| s) + (New <==> New <==| s) + Idle Idle -- connection states + where + pfCommand = CreateConn + protoFunc = brkCreateConn + +brkCreateConn :: Connection Broker None Idle + -> CreateConnRequest + -> Either String (CreateConnResponse, Connection Broker New Idle) +brkCreateConn (Connection str) _ = Right (CreateConnResponse "1" "2", Connection str) +-- TODO stub + + +-- -- below code should NOT compile, but it does +-- instance ProtocolFunc Broker CreateConnCmd +-- CreateConnRequest CreateConnResponse -- request response +-- None New Idle Idle -- "Secured" should not be allowed here, +-- where -- such command does not exist, so no instance of +-- protoFunc _ = \(Connection str) _ -> Right (CreateConnResponse "1" "2", Connection str) -- PrfCmd exist...? But it compiles. + +-- bCreateConn' :: Connection Broker None Idle +-- -> CreateConnRequest +-- -> Either String +-- (CreateConnResponse, Connection Broker New Idle) +-- bCreateConn' = protoFunc $ CreateConn @None