IntenseFinance/simplex-chat
3
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

refactor: group Command parameters, do syntax in scenarios

Browse Source
This commit is contained in:
Evgeny Poberezkin
2020-07-10 12:36:14 +01:00
parent 063b7286e2
commit b19b5be50e
5 changed files with 67 additions and 75 deletions
Download Patch File Download Diff File Expand all files Collapse all files

14
definitions/src/Simplex/Messaging/Broker.hs
View File

@@ -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

28
definitions/src/Simplex/Messaging/Client.hs
View File

@@ -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

4
definitions/src/Simplex/Messaging/PrintScenario.hs
View File

@@ -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

60
definitions/src/Simplex/Messaging/Protocol.hs
View File

@@ -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

36
definitions/src/Simplex/Messaging/Scenarios.hs
View File

@@ -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"