diff --git a/definitions/src/Simplex/Messaging/Broker.hs b/definitions/src/Simplex/Messaging/Broker.hs index e525a6152b..eacc340ed6 100644 --- a/definitions/src/Simplex/Messaging/Broker.hs +++ b/definitions/src/Simplex/Messaging/Broker.hs @@ -13,9 +13,9 @@ import Simplex.Messaging.Protocol instance Monad m => PartyProtocol m Broker where api :: - Command from fs fs' Broker ps ps' res -> - Connection Broker ps -> - ExceptT String m (res, Connection Broker ps') + Command from '(Broker, s, s') a -> + Connection Broker s -> + ExceptT String m (a, Connection Broker s') api (CreateConn _) = apiStub api (Subscribe _) = apiStub api (Unsubscribe _) = apiStub @@ -25,9 +25,9 @@ instance Monad m => PartyProtocol m Broker where api (DeleteMsg _ _) = apiStub action :: - Command Broker ps ps' to ts ts' res -> - Connection Broker ps -> - ExceptT String m res -> - ExceptT String m (Connection Broker ps') + Command '(Broker, s, s') to a -> + Connection Broker s -> + ExceptT String m a -> + ExceptT String m (Connection Broker s') action (PushConfirm _ _) = actionStub action (PushMsg _ _) = actionStub diff --git a/definitions/src/Simplex/Messaging/Client.hs b/definitions/src/Simplex/Messaging/Client.hs index 91f0117bec..4364cb82f2 100644 --- a/definitions/src/Simplex/Messaging/Client.hs +++ b/definitions/src/Simplex/Messaging/Client.hs @@ -13,17 +13,17 @@ import Simplex.Messaging.Protocol instance Monad m => PartyProtocol m Recipient where api :: - Command from fs fs' Recipient ps ps' res -> - Connection Recipient ps -> - ExceptT String m (res, Connection Recipient ps') + Command from '(Recipient, s, s') a -> + Connection Recipient s -> + ExceptT String m (a, Connection Recipient s') api (PushConfirm _ _) = apiStub api (PushMsg _ _) = apiStub action :: - Command Recipient ps ps' to ts ts' res -> - Connection Recipient ps -> - ExceptT String m res -> - ExceptT String m (Connection Recipient ps') + Command '(Recipient, s, s') to a -> + Connection Recipient s -> + ExceptT String m a -> + ExceptT String m (Connection Recipient s') action (CreateConn _) = actionStub action (Subscribe _) = actionStub action (Unsubscribe _) = actionStub @@ -33,15 +33,15 @@ instance Monad m => PartyProtocol m Recipient where instance Monad m => PartyProtocol m Sender where api :: - Command from fs fs' Sender ps ps' res -> - Connection Sender ps -> - ExceptT String m (res, Connection Sender ps') + Command from '(Sender, s, s') a -> + Connection Sender s -> + ExceptT String m (a, Connection Sender s') api (SendInvite _) = apiStub action :: - Command Sender ps ps' to ts ts' res -> - Connection Sender ps -> - ExceptT String m res -> - ExceptT String m (Connection Sender ps') + Command '(Sender, s, s') to a -> + Connection Sender s -> + ExceptT String m a -> + ExceptT String m (Connection Sender s') action (ConfirmConn _ _) = actionStub action (SendMsg _ _) = actionStub diff --git a/definitions/src/Simplex/Messaging/PrintScenario.hs b/definitions/src/Simplex/Messaging/PrintScenario.hs index 4842522c54..61bbeef338 100644 --- a/definitions/src/Simplex/Messaging/PrintScenario.hs +++ b/definitions/src/Simplex/Messaging/PrintScenario.hs @@ -34,7 +34,7 @@ logProtocol (ProtocolCmd from to cmd) = do tell [(party from, commandStr cmd <> " " <> party to)] mockCommand cmd -commandStr :: Command from fs fs' to ts ts' a -> String +commandStr :: Command from to a -> String commandStr (CreateConn _) = "creates connection in" commandStr (Subscribe cid) = "subscribes to connection " <> show cid <> " in" commandStr (Unsubscribe cid) = "unsubscribes from connection " <> show cid <> " in" @@ -46,7 +46,7 @@ commandStr (SendMsg cid _) = "sends message to connection " <> show cid <> " in" commandStr (PushMsg cid _) = "pushes message from connection " <> show cid <> " to" commandStr (DeleteMsg cid _) = "deletes message from connection " <> show cid <> " in" -mockCommand :: Monad m => Command from fs fs' to ts ts' a -> m a +mockCommand :: Monad m => Command from to a -> m a mockCommand (CreateConn _) = return CreateConnResponse diff --git a/definitions/src/Simplex/Messaging/Protocol.hs b/definitions/src/Simplex/Messaging/Protocol.hs index 3bdb6cb303..ecc677dff3 100644 --- a/definitions/src/Simplex/Messaging/Protocol.hs +++ b/definitions/src/Simplex/Messaging/Protocol.hs @@ -60,55 +60,48 @@ type Enabled rs bs = (bs == New || bs == Secured) ~ True ) -data - Command - (from :: Party) - (fs :: ConnState) - (fs' :: ConnState) - (to :: Party) - (ts :: ConnState) - (ts' :: ConnState) - (res :: Type) :: Type - where +type PartyCmd = (Party, ConnState, ConnState) + +data Command (from :: PartyCmd) (to :: PartyCmd) (a :: Type) :: Type where CreateConn :: PublicKey -> - Command Recipient None New Broker None New CreateConnResponse + Command '(Recipient, None, New) '(Broker, None, New) CreateConnResponse Subscribe :: Enabled rs bs => ConnId -> - Command Recipient rs rs Broker bs bs () + Command '(Recipient, rs, rs) '(Broker, bs, bs) () Unsubscribe :: Enabled rs bs => ConnId -> - Command Recipient rs rs Broker bs bs () + Command '(Recipient, rs, rs) '(Broker, bs, bs) () SendInvite :: Invitation -> - Command Recipient New Pending Sender None New () + Command '(Recipient, New, Pending) '(Sender, None, New) () ConfirmConn :: SenderConnId -> Encrypted -> - Command Sender New Confirmed Broker New New () + Command '(Sender, New, Confirmed) '(Broker, New, New) () PushConfirm :: ConnId -> Message -> - Command Broker New New Recipient Pending Confirmed () + Command '(Broker, New, New) '(Recipient, Pending, Confirmed) () SecureConn :: ConnId -> PublicKey -> - Command Recipient Confirmed Secured Broker New Secured () + Command '(Recipient, Confirmed, Secured) '(Broker, New, Secured) () SendMsg :: (ss == Confirmed || ss == Secured) ~ True => SenderConnId -> Encrypted -> - Command Sender ss Secured Broker Secured Secured () + Command '(Sender, ss, Secured) '(Broker, Secured, Secured) () PushMsg :: ConnId -> Message -> - Command Broker Secured Secured Recipient Secured Secured () + Command '(Broker, Secured, Secured) '(Recipient, Secured, Secured) () DeleteMsg :: ConnId -> MessageId -> - Command Recipient Secured Secured Broker Secured Secured () + Command '(Recipient, Secured, Secured) '(Broker, Secured, Secured) () -- connection type stub for all participants, TODO move from idris data @@ -120,19 +113,19 @@ data class Monad m => PartyProtocol m (p :: Party) where api :: - Command from fs fs' p ps ps' res -> - Connection p ps -> - ExceptT String m (res, Connection p ps') + Command from '(p, s, s') a -> + Connection p s -> + ExceptT String m (a, Connection p s') action :: - Command p ps ps' to ts ts' res -> - Connection p ps -> - ExceptT String m res -> - ExceptT String m (Connection p ps') + Command '(p, s, s') to a -> + Connection p s -> + ExceptT String m a -> + ExceptT String m (Connection p s') -apiStub :: Monad m => Connection p ps -> ExceptT String m (res, Connection p ps') +apiStub :: Monad m => Connection p s -> ExceptT String m (a, Connection p s') apiStub _ = throwE "api not implemented" -actionStub :: Monad m => Connection p ps -> ExceptT String m res -> ExceptT String m (Connection p ps') +actionStub :: Monad m => Connection p s -> ExceptT String m a -> ExceptT String m (Connection p s') actionStub _ _ = throwE "action not implemented" type family AllowedStates s from fs' to ts' :: Constraint where @@ -169,7 +162,7 @@ data ProtocolEff (s :: ProtocolState) (s' :: ProtocolState) (a :: Type) :: Type AllowedStates s from fs' to ts' => Sing from -> Sing to -> - Command from (ConnSt from s) fs' to (ConnSt to s) ts' a -> + Command '(from, ConnSt from s, fs') '(to, ConnSt to s, ts') a -> ProtocolEff s (ProtoSt s from fs' to ts') a type Protocol = XFree ProtocolEff @@ -180,14 +173,9 @@ infix 6 ->: AllowedStates s from fs' to ts' => Sing from -> Sing to -> - Command from (ConnSt from s) fs' to (ConnSt to s) ts' a -> + Command '(from, ConnSt from s, fs') '(to, ConnSt to s, ts') a -> Protocol s (ProtoSt s from fs' to ts') a (->:) f t c = xfree $ ProtocolCmd f t c start :: String -> Protocol s s () start = xfree . Start - -infix 5 |$ - -(|$) :: (a -> b) -> a -> b -f |$ x = f x diff --git a/definitions/src/Simplex/Messaging/Scenarios.hs b/definitions/src/Simplex/Messaging/Scenarios.hs index 6cd61bb1c3..36d91f2858 100644 --- a/definitions/src/Simplex/Messaging/Scenarios.hs +++ b/definitions/src/Simplex/Messaging/Scenarios.hs @@ -1,15 +1,19 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RebindableSyntax #-} {-# OPTIONS_GHC -fno-warn-missing-fields #-} {-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-} +{-# OPTIONS_GHC -fno-warn-unused-do-bind #-} module Simplex.Messaging.Scenarios where -import Control.XMonad +import Control.XMonad.Do import Data.Singletons +import Data.String import Simplex.Messaging.Protocol import Simplex.Messaging.Types +import Prelude hiding ((>>), (>>=)) r :: Sing Recipient r = SRecipient @@ -21,19 +25,19 @@ s :: Sing Sender s = SSender establishConnection :: Protocol '(None, None, None) '(Secured, Secured, Secured) () -establishConnection = +establishConnection = do start "Establish simplex messaging connection and send first message" - >>: r ->: b |$ CreateConn "BODbZxmtKUUF1l8pj4nVjQ" - >>: r ->: b |$ Subscribe "RU" - >>: r ->: s |$ SendInvite "invitation RU" -- invitation - TODo - >>: s ->: b |$ ConfirmConn "SU" "encrypted" - >>: b ->: r |$ PushConfirm "RU" Message {msgId = "abc", msg = "XPaVEVNunkYKqqK0dnAT5Q"} - >>: r ->: b |$ SecureConn "RU" "XPaVEVNunkYKqqK0dnAT5Q" - >>: r ->: b |$ DeleteMsg "RU" "abc" - >>: s ->: b |$ SendMsg "SU" "welcome" -- welcome message - >>: b ->: r |$ PushMsg "RU" Message {msgId = "def", msg = "welcome"} - >>: r ->: b |$ DeleteMsg "RU" "def" - >>: s ->: b |$ SendMsg "SU" "hello there" - >>: b ->: r |$ PushMsg "RU" Message {msgId = "ghi", msg = "hello there"} - >>: r ->: b |$ DeleteMsg "RU" "ghi" - >>: r ->: b |$ Unsubscribe "RU" + r ->: b $ CreateConn "BODbZxmtKUUF1l8pj4nVjQ" + r ->: b $ Subscribe "RU" + r ->: s $ SendInvite "invitation RU" -- invitation - TODo + s ->: b $ ConfirmConn "SU" "encrypted" + b ->: r $ PushConfirm "RU" Message {msgId = "abc", msg = "XPaVEVNunkYKqqK0dnAT5Q"} + r ->: b $ SecureConn "RU" "XPaVEVNunkYKqqK0dnAT5Q" + r ->: b $ DeleteMsg "RU" "abc" + s ->: b $ SendMsg "SU" "welcome" -- welcome message + b ->: r $ PushMsg "RU" Message {msgId = "def", msg = "welcome"} + r ->: b $ DeleteMsg "RU" "def" + s ->: b $ SendMsg "SU" "hello there" + b ->: r $ PushMsg "RU" Message {msgId = "ghi", msg = "hello there"} + r ->: b $ DeleteMsg "RU" "ghi" + r ->: b $ Unsubscribe "RU"