From b5a04ad1785f37360c71d7a38b4acbb2d21b0f61 Mon Sep 17 00:00:00 2001 From: Evgeny Poberezkin <2769109+epoberezkin@users.noreply.github.com> Date: Sat, 11 Jul 2020 20:27:23 +0100 Subject: [PATCH] Control.Protocol (#35) * polysemy effects * exctract Protocol abstraction * refactor: use Control.Protocol * better type errors --- definitions/package.yaml | 4 + definitions/src/Control/Protocol.hs | 47 ++++++ .../src/Control/Protocol/Example/Command.hs | 48 ++++++ .../src/Control/Protocol/Example/Scenario.hs | 28 ++++ definitions/src/Control/Protocol/Internal.hs | 58 +++++++ definitions/src/Simplex/Messaging/Broker.hs | 25 +++- definitions/src/Simplex/Messaging/Client.hs | 46 +++++- definitions/src/Simplex/Messaging/Core.hs | 49 ++++++ .../src/Simplex/Messaging/PrintScenario.hs | 15 +- definitions/src/Simplex/Messaging/Protocol.hs | 141 ++++-------------- .../src/Simplex/Messaging/Scenarios.hs | 6 +- 11 files changed, 344 insertions(+), 123 deletions(-) create mode 100644 definitions/src/Control/Protocol.hs create mode 100644 definitions/src/Control/Protocol/Example/Command.hs create mode 100644 definitions/src/Control/Protocol/Example/Scenario.hs create mode 100644 definitions/src/Control/Protocol/Internal.hs create mode 100644 definitions/src/Simplex/Messaging/Core.hs diff --git a/definitions/package.yaml b/definitions/package.yaml index bebd52855..17be97b54 100644 --- a/definitions/package.yaml +++ b/definitions/package.yaml @@ -11,6 +11,8 @@ extra-source-files: - readme.md ghc-options: + # - -fplugin=Polysemy.Plugin + - -O2 - -Wall - -Wcompat - -Werror=incomplete-patterns @@ -23,6 +25,8 @@ dependencies: - aeson - base >= 4.7 && < 5 - freer-indexed + - polysemy + # - polysemy-plugin - lens - mtl - singletons diff --git a/definitions/src/Control/Protocol.hs b/definitions/src/Control/Protocol.hs new file mode 100644 index 000000000..d46052eab --- /dev/null +++ b/definitions/src/Control/Protocol.hs @@ -0,0 +1,47 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-} + +module Control.Protocol + ( Protocol, + ProtocolCmd (..), + Command, + PartyCmd (..), + type (|:), + (->:), + comment, + ) +where + +import Control.Protocol.Internal +import Control.XFreer +import Data.Kind +import Data.Singletons + +data PartyCmd p = forall s. Cmd p s s + +type Command p = PartyCmd p -> PartyCmd p -> Type -> Type + +data ProtocolCmd (cmd :: Command p) (parties :: [p]) (s :: DList) (s' :: DList) (a :: Type) where + Comment :: String -> ProtocolCmd cmd ps s s () + ProtocolCmd :: + Sing (from :: p) -> + Sing (to :: p) -> + cmd (Cmd from (PartySt ps s from) fs') (Cmd to (PartySt ps s to) ts') a -> + ProtocolCmd cmd ps s (ProtoSt ps s from fs' to ts') a + +type Protocol parties cmd = XFree (ProtocolCmd parties cmd) + +infix 6 ->: + +(->:) :: + Sing from -> + Sing to -> + cmd (Cmd from (PartySt ps s from) fs') (Cmd to (PartySt ps s to) ts') a -> + Protocol cmd ps s (ProtoSt ps s from fs' to ts') a +(->:) f t c = xfree $ ProtocolCmd f t c + +comment :: String -> Protocol ps cmd s s () +comment = xfree . Comment diff --git a/definitions/src/Control/Protocol/Example/Command.hs b/definitions/src/Control/Protocol/Example/Command.hs new file mode 100644 index 000000000..13816fa9b --- /dev/null +++ b/definitions/src/Control/Protocol/Example/Command.hs @@ -0,0 +1,48 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-} + +module Control.Protocol.Example.Command where + +import Control.Protocol +import Data.Singletons.TH + +$( singletons + [d| + data Party = Recipient | Broker | Sender + deriving (Show, Eq) + + data RState + = RNone + | RReady + deriving (Show, Eq) + + data BState + = BNone + | BEmpty + | BFull + deriving (Show, Eq) + + data SState + = SNone + | SReady + deriving (Show, Eq) + |] + ) + +data MyCommand :: Command Party where + Create :: MyCommand (Cmd Recipient RNone RReady) (Cmd Broker BNone BEmpty) () + Notify :: MyCommand (Cmd Recipient RReady RReady) (Cmd Sender SNone SReady) () + Send :: String -> MyCommand (Cmd Sender SReady SReady) (Cmd Broker BEmpty BFull) () + Forward :: MyCommand (Cmd Broker BFull BEmpty) (Cmd Recipient RReady RReady) String + +type MyProtocol = Protocol MyCommand '[Recipient, Broker, Sender] diff --git a/definitions/src/Control/Protocol/Example/Scenario.hs b/definitions/src/Control/Protocol/Example/Scenario.hs new file mode 100644 index 000000000..59db9cade --- /dev/null +++ b/definitions/src/Control/Protocol/Example/Scenario.hs @@ -0,0 +1,28 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE RebindableSyntax #-} +{-# LANGUAGE TypeOperators #-} +{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-} + +module Control.Protocol.Example.Scenario where + +import Control.Protocol +import Control.Protocol.Example.Command +import Control.XMonad.Do +import Data.Singletons +import Prelude hiding ((>>), (>>=)) + +r :: Sing Recipient +r = SRecipient + +b :: Sing Broker +b = SBroker + +s :: Sing Sender +s = SSender + +scenario :: String -> MyProtocol (RNone |: BNone |: SNone) (RReady |: BEmpty |: SReady) String +scenario str = do + r ->: b $ Create + r ->: s $ Notify + s ->: b $ Send str + b ->: r $ Forward diff --git a/definitions/src/Control/Protocol/Internal.hs b/definitions/src/Control/Protocol/Internal.hs new file mode 100644 index 000000000..cd90d3e0f --- /dev/null +++ b/definitions/src/Control/Protocol/Internal.hs @@ -0,0 +1,58 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-} + +module Control.Protocol.Internal + ( DList (..), + type (|:), + PartySt, + ProtoSt, + ) +where + +import GHC.TypeLits (ErrorMessage (..), TypeError) + +infixr 3 :|, |: + +data DList = DNil | forall a. a :| DList + +type family (|:) (s :: k1) (t :: k2) :: DList where + s |: DNil = s :| DNil + s |: (t :| ss) = s :| t :| ss + s |: t = s :| t :| DNil + +type family PartySt (parties :: [k]) (state :: DList) (party :: k) where + PartySt (p ': _) (s ':| _) p = s + PartySt (_ ': ps) (_ ':| ss) p = PartySt ps ss p + PartySt '[] DNil p = TypeError (NoParty p) + PartySt '[] _ p = TypeError (NoParty p :<>: PartyError) + PartySt _ DNil p = TypeError (NoParty p :<>: StateError) + +type family ProtoSt (parties :: [k]) (state :: DList) (from :: k) fs' (to :: k) ts' where + ProtoSt '[] DNil from _ to _ = TypeError (NoParties from to) + ProtoSt '[] _ from _ to _ = TypeError (NoParties from to :<>: PartyError) + ProtoSt _ DNil from _ to _ = TypeError (NoParties from to :<>: StateError) + ProtoSt (from ': ps) (_ ':| ss) from fs' to ts' = fs' ':| ProtoSt1 ps ss to ts' + ProtoSt (to ': ps) (_ ':| ss) from fs' to ts' = ts' ':| ProtoSt1 ps ss from fs' + ProtoSt (_ ': ps) (s ':| ss) from fs' to ts' = s ':| ProtoSt ps ss from fs' to ts' + +type family ProtoSt1 (parties :: [k]) (state :: DList) (p :: k) s' where + ProtoSt1 '[] DNil p _ = TypeError (NoParty p) + ProtoSt1 '[] _ p _ = TypeError (NoParty p :<>: PartyError) + ProtoSt1 _ DNil p _ = TypeError (NoParty p :<>: StateError) + ProtoSt1 (p ': _) (_ ':| ss) p s' = s' ':| ss + ProtoSt1 (_ ': ps) (s ':| ss) p s' = s ':| ProtoSt1 ps ss p s' + +type NoParties p1 p2 = + Text "Parties " :<>: ShowType p1 :<>: Text " and " :<>: ShowType p2 + :<>: Text " are not found." + +type NoParty p = Text "Party " :<>: ShowType p :<>: Text " is not found." + +type PartyError = Text "\nSpecified fewer protocol parties than states." + +type StateError = Text "\nSpecified fewer protocol states than parties." diff --git a/definitions/src/Simplex/Messaging/Broker.hs b/definitions/src/Simplex/Messaging/Broker.hs index eacc340ed..02d009ffa 100644 --- a/definitions/src/Simplex/Messaging/Broker.hs +++ b/definitions/src/Simplex/Messaging/Broker.hs @@ -1,19 +1,23 @@ {-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} {-# OPTIONS_GHC -fno-warn-orphans #-} {-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-} module Simplex.Messaging.Broker where import Control.Monad.Trans.Except +import Control.Protocol (PartyCmd (..)) +import Polysemy.Internal import Simplex.Messaging.Protocol instance Monad m => PartyProtocol m Broker where api :: - Command from '(Broker, s, s') a -> + SimplexCommand from (Cmd Broker s s') a -> Connection Broker s -> ExceptT String m (a, Connection Broker s') api (CreateConn _) = apiStub @@ -25,9 +29,26 @@ instance Monad m => PartyProtocol m Broker where api (DeleteMsg _ _) = apiStub action :: - Command '(Broker, s, s') to a -> + SimplexCommand (Cmd Broker s s') to a -> Connection Broker s -> ExceptT String m a -> ExceptT String m (Connection Broker s') action (PushConfirm _ _) = actionStub action (PushMsg _ _) = actionStub + +type SimplexBroker = SimplexParty Broker + +api' :: + Member SimplexBroker r => + SimplexCommand from (Cmd Broker s s') a -> + Connection Broker s -> + Sem r (Either String (a, Connection Broker s')) +api' cmd conn = send $ Api cmd conn + +action' :: + Member SimplexBroker r => + SimplexCommand (Cmd Broker s s') to a -> + Connection Broker s -> + Either String a -> + Sem r (Either String (Connection Broker s')) +action' cmd conn res = send $ Action cmd conn res diff --git a/definitions/src/Simplex/Messaging/Client.hs b/definitions/src/Simplex/Messaging/Client.hs index 4364cb82f..a478905a3 100644 --- a/definitions/src/Simplex/Messaging/Client.hs +++ b/definitions/src/Simplex/Messaging/Client.hs @@ -1,26 +1,30 @@ {-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} {-# OPTIONS_GHC -fno-warn-orphans #-} {-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-} module Simplex.Messaging.Client where import Control.Monad.Trans.Except +import Control.Protocol (PartyCmd (..)) +import Polysemy.Internal import Simplex.Messaging.Protocol instance Monad m => PartyProtocol m Recipient where api :: - Command from '(Recipient, s, s') a -> + SimplexCommand from (Cmd Recipient s s') a -> Connection Recipient s -> ExceptT String m (a, Connection Recipient s') api (PushConfirm _ _) = apiStub api (PushMsg _ _) = apiStub action :: - Command '(Recipient, s, s') to a -> + SimplexCommand (Cmd Recipient s s') to a -> Connection Recipient s -> ExceptT String m a -> ExceptT String m (Connection Recipient s') @@ -33,15 +37,49 @@ instance Monad m => PartyProtocol m Recipient where instance Monad m => PartyProtocol m Sender where api :: - Command from '(Sender, s, s') a -> + SimplexCommand from (Cmd Sender s s') a -> Connection Sender s -> ExceptT String m (a, Connection Sender s') api (SendInvite _) = apiStub action :: - Command '(Sender, s, s') to a -> + SimplexCommand (Cmd Sender s s') to a -> Connection Sender s -> ExceptT String m a -> ExceptT String m (Connection Sender s') action (ConfirmConn _ _) = actionStub action (SendMsg _ _) = actionStub + +type SimplexRecipient = SimplexParty Recipient + +type SimplexSender = SimplexParty Sender + +rApi :: + Member SimplexRecipient r => + SimplexCommand from (Cmd Recipient s s') a -> + Connection Recipient s -> + Sem r (Either String (a, Connection Recipient s')) +rApi cmd conn = send $ Api cmd conn + +rAction :: + Member SimplexRecipient r => + SimplexCommand (Cmd Recipient s s') to a -> + Connection Recipient s -> + Either String a -> + Sem r (Either String (Connection Recipient s')) +rAction cmd conn res = send $ Action cmd conn res + +sApi :: + Member SimplexSender r => + SimplexCommand from (Cmd Sender s s') a -> + Connection Sender s -> + Sem r (Either String (a, Connection Sender s')) +sApi cmd conn = send $ Api cmd conn + +sAction :: + Member SimplexSender r => + SimplexCommand (Cmd Sender s s') to a -> + Connection Sender s -> + Either String a -> + Sem r (Either String (Connection Sender s')) +sAction cmd conn res = send $ Action cmd conn res diff --git a/definitions/src/Simplex/Messaging/Core.hs b/definitions/src/Simplex/Messaging/Core.hs new file mode 100644 index 000000000..0eda9bb08 --- /dev/null +++ b/definitions/src/Simplex/Messaging/Core.hs @@ -0,0 +1,49 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-} + +module Simplex.Messaging.Core where + +import Data.Kind +import Data.Singletons.TH + +$( singletons + [d| + data Party = Recipient | Broker | Sender + deriving (Show, Eq) + + data ConnState + = None -- (all) not available or removed from the broker + | New -- (recipient, broker) connection created (or received from sender) + | Pending -- (recipient, sender) 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 + deriving (Show, Eq) + |] + ) + +type family HasState (p :: Party) (s :: ConnState) :: Constraint where + HasState Recipient _ = () + HasState Broker None = () + HasState Broker New = () + HasState Broker Secured = () + HasState Broker Disabled = () + HasState Sender None = () + HasState Sender New = () + HasState Sender Confirmed = () + HasState Sender Secured = () + +type family Enabled (rs :: ConnState) (bs :: ConnState) :: Constraint where + Enabled New New = () + Enabled Pending New = () + Enabled Confirmed New = () + Enabled Secured Secured = () diff --git a/definitions/src/Simplex/Messaging/PrintScenario.hs b/definitions/src/Simplex/Messaging/PrintScenario.hs index 6e1f64d2b..b74d9c818 100644 --- a/definitions/src/Simplex/Messaging/PrintScenario.hs +++ b/definitions/src/Simplex/Messaging/PrintScenario.hs @@ -1,17 +1,20 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} +{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-} module Simplex.Messaging.PrintScenario where import Control.Monad.Writer +import Control.Protocol import Control.XFreer import Data.Singletons import Simplex.Messaging.Protocol import Simplex.Messaging.Types -printScenario :: Protocol s s' a -> IO () +printScenario :: SimplexProtocol s s' a -> IO () printScenario scn = ps 1 "" $ execWriter $ logScenario scn where ps :: Int -> String -> [(String, String)] -> IO () @@ -24,17 +27,17 @@ printScenario scn = ps 1 "" $ execWriter $ logScenario scn prt i' s = putStrLn s >> ps i' p' ls l' = " - " <> l -logScenario :: Protocol s s' a -> Writer [(String, String)] a +logScenario :: SimplexProtocol s s' a -> Writer [(String, String)] a logScenario (Pure x) = return x logScenario (Bind p f) = logProtocol p >>= \x -> logScenario (f x) -logProtocol :: ProtocolCmd s s' a -> Writer [(String, String)] a -logProtocol (Start s) = tell [("", s)] +logProtocol :: ProtocolCmd SimplexCommand '[Recipient, Broker, Sender] s s' a -> Writer [(String, String)] a +logProtocol (Comment s) = tell [("", s)] logProtocol (ProtocolCmd from to cmd) = do tell [(party from, commandStr cmd <> " " <> party to)] mockCommand cmd -commandStr :: Command from to a -> String +commandStr :: SimplexCommand 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 +49,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 to a -> m a +mockCommand :: Monad m => SimplexCommand 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 a6a25c8a1..c583a7ac9 100644 --- a/definitions/src/Simplex/Messaging/Protocol.hs +++ b/definitions/src/Simplex/Messaging/Protocol.hs @@ -1,108 +1,70 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} -{-# LANGUAGE EmptyCase #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} -{-# LANGUAGE InstanceSigs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PolyKinds #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE NoStarIsType #-} {-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-} -module Simplex.Messaging.Protocol where +module Simplex.Messaging.Protocol + ( module Simplex.Messaging.Core, + module Simplex.Messaging.Protocol, + ) +where import Control.Monad.Trans.Except -import Control.XFreer +import Control.Protocol import Data.Kind -import Data.Singletons -import Data.Singletons.TH import Data.Type.Bool (type (||)) +import Data.Type.Equality (type (==)) +import Simplex.Messaging.Core import Simplex.Messaging.Types -$( singletons - [d| - data Party = Recipient | Broker | Sender - deriving (Show, Eq) +type SimplexProtocol = Protocol SimplexCommand '[Recipient, Broker, Sender] - data ConnState - = None -- (all) not available or removed from the broker - | New -- (recipient, broker) connection created (or received from sender) - | Pending -- (recipient, sender) 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 - deriving (Show, Eq) - |] - ) - -type family HasState (p :: Party) (s :: ConnState) :: Constraint where - HasState Recipient _ = () - HasState Broker None = () - HasState Broker New = () - HasState Broker Secured = () - HasState Broker Disabled = () - HasState Sender None = () - HasState Sender New = () - HasState Sender Confirmed = () - HasState Sender Secured = () - -type family Enabled (rs :: ConnState) (bs :: ConnState) :: Constraint where - Enabled New New = () - Enabled Pending New = () - Enabled Confirmed New = () - Enabled Secured Secured = () - -type PartyCmd = (Party, ConnState, ConnState) - -data Command (from :: PartyCmd) (to :: PartyCmd) (a :: Type) :: Type where +data SimplexCommand :: Command Party where CreateConn :: PublicKey -> - Command '(Recipient, None, New) '(Broker, None, New) CreateConnResponse + SimplexCommand (Cmd Recipient None New) (Cmd Broker None New) CreateConnResponse Subscribe :: Enabled rs bs => ConnId -> - Command '(Recipient, rs, rs) '(Broker, bs, bs) () + SimplexCommand (Cmd Recipient rs rs) (Cmd Broker bs bs) () Unsubscribe :: Enabled rs bs => ConnId -> - Command '(Recipient, rs, rs) '(Broker, bs, bs) () + SimplexCommand (Cmd Recipient rs rs) (Cmd Broker bs bs) () SendInvite :: Invitation -> - Command '(Recipient, New, Pending) '(Sender, None, New) () + SimplexCommand (Cmd Recipient New Pending) (Cmd Sender None New) () ConfirmConn :: SenderConnId -> Encrypted -> - Command '(Sender, New, Confirmed) '(Broker, New, New) () + SimplexCommand (Cmd Sender New Confirmed) (Cmd Broker New New) () PushConfirm :: ConnId -> Message -> - Command '(Broker, New, New) '(Recipient, Pending, Confirmed) () + SimplexCommand (Cmd Broker New New) (Cmd Recipient Pending Confirmed) () SecureConn :: ConnId -> PublicKey -> - Command '(Recipient, Confirmed, Secured) '(Broker, New, Secured) () + SimplexCommand (Cmd Recipient Confirmed Secured) (Cmd Broker New Secured) () SendMsg :: (ss == Confirmed || ss == Secured) ~ True => SenderConnId -> Encrypted -> - Command '(Sender, ss, Secured) '(Broker, Secured, Secured) () + SimplexCommand (Cmd Sender ss Secured) (Cmd Broker Secured Secured) () PushMsg :: ConnId -> Message -> - Command '(Broker, Secured, Secured) '(Recipient, Secured, Secured) () + SimplexCommand (Cmd Broker Secured Secured) (Cmd Recipient Secured Secured) () DeleteMsg :: ConnId -> MessageId -> - Command '(Recipient, Secured, Secured) '(Broker, Secured, Secured) () + SimplexCommand (Cmd Recipient Secured Secured) (Cmd Broker Secured Secured) () -- connection type stub for all participants, TODO move from idris data @@ -114,11 +76,11 @@ data class Monad m => PartyProtocol m (p :: Party) where api :: - Command from '(p, s, s') a -> + SimplexCommand from (Cmd p s s') a -> Connection p s -> ExceptT String m (a, Connection p s') action :: - Command '(p, s, s') to a -> + SimplexCommand (Cmd p s s') to a -> Connection p s -> ExceptT String m a -> ExceptT String m (Connection p s') @@ -129,52 +91,13 @@ apiStub _ = throwE "api not implemented" actionStub :: Monad m => Connection p s -> ExceptT String m a -> ExceptT String m (Connection p s') actionStub _ _ = throwE "action not implemented" -type ProtocolState = (ConnState, ConnState, ConnState) - -type family HasProtoSt (s :: ProtocolState) :: Constraint where - HasProtoSt '(rs, bs, ss) = - ( HasState Recipient rs, - HasState Broker bs, - HasState Sender ss - ) - -type family ConnSt (p :: Party) (s :: ProtocolState) :: ConnState where - ConnSt Recipient '(rs, _, _) = rs - ConnSt Broker '(_, bs, _) = bs - ConnSt Sender '(_, _, ss) = ss - -type family ProtoSt (s :: ProtocolState) from fs' to ts' :: ProtocolState where - ProtoSt s from fs' to ts' = - '( PartySt Recipient s from fs' to ts', - PartySt Broker s from fs' to ts', - PartySt Sender s from fs' to ts' - ) - -type family PartySt (p :: Party) (s :: ProtocolState) from fs' to ts' :: ConnState where - PartySt from _ from fs' _ _ = fs' - PartySt to _ _ _ to ts' = ts' - PartySt p s _ _ _ _ = ConnSt p s - -data ProtocolCmd (s :: ProtocolState) (s' :: ProtocolState) (a :: Type) :: Type where - Start :: String -> ProtocolCmd s s () - ProtocolCmd :: - (HasProtoSt s, HasState from fs', HasState to ts') => - Sing from -> - Sing to -> - Command '(from, ConnSt from s, fs') '(to, ConnSt to s, ts') a -> - ProtocolCmd s (ProtoSt s from fs' to ts') a - -type Protocol = XFree ProtocolCmd - -infix 6 ->: - -(->:) :: - (HasProtoSt s, HasState from fs', HasState to ts') => - Sing from -> - Sing to -> - 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 +data SimplexParty (p :: Party) m a where + Api :: + SimplexCommand from (Cmd p s s') x -> + Connection p s -> + SimplexParty p m (Either String (x, Connection p s')) + Action :: + SimplexCommand (Cmd p s s') to x -> + Connection p s -> + Either String x -> + SimplexParty p m (Either String (Connection p s')) diff --git a/definitions/src/Simplex/Messaging/Scenarios.hs b/definitions/src/Simplex/Messaging/Scenarios.hs index 36d91f285..b40a70fc2 100644 --- a/definitions/src/Simplex/Messaging/Scenarios.hs +++ b/definitions/src/Simplex/Messaging/Scenarios.hs @@ -2,12 +2,14 @@ {-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RebindableSyntax #-} +{-# LANGUAGE TypeOperators #-} {-# 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.Protocol import Control.XMonad.Do import Data.Singletons import Data.String @@ -24,9 +26,9 @@ b = SBroker s :: Sing Sender s = SSender -establishConnection :: Protocol '(None, None, None) '(Secured, Secured, Secured) () +establishConnection :: SimplexProtocol (None |: None |: None) (Secured |: Secured |: Secured) () establishConnection = do - start "Establish simplex messaging connection and send first message" + comment "Establish simplex messaging connection and send first message" r ->: b $ CreateConn "BODbZxmtKUUF1l8pj4nVjQ" r ->: b $ Subscribe "RU" r ->: s $ SendInvite "invitation RU" -- invitation - TODo