protocol commands

definitions/src/Simplex/Messaging/Protocol.hs

@@ -1,5 +1,4 @@
 {-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE EmptyCase #-}
 {-# LANGUAGE FlexibleContexts #-}
@@ -8,13 +7,13 @@
 {-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NoStarIsType #-}
-{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeInType #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 module Simplex.Messaging.Protocol where
@@ -125,14 +124,87 @@ st2 = SPending :<==> SNew :<==| SConfirmed
 -- stBad = SPending :<==> SConfirmed :<==| SConfirmed
 
 
--- data Command (res :: Type)
---              (ps :: (Participant, Participant))
---              (AllConnState r b s)
---              (AllConnState r b s) :: Type where
+data Command res (from :: Participant) (to :: Participant) state state' :: Type where
+  CreateConn   :: Prf HasState 'Sender s
+               => CreateConnRequest
+               -> Command CreateConnResponse
+                    'Recipient 'Broker
+                    ('None <==> 'None <==| s)
+                    ('New <==> 'New  <==| s)
 
---   CreateConn  :: Prf HasState 'Sender s
---               => NewConnectionReqBody
---               -> Command NewConnectionResBody
---                     ('Recipient, 'Broker)
---                     ('None <==> 'None <==| s)
---                     ('New <==> 'New  <==| s)
+  Subscribe    :: Command () 'Recipient 'Broker state state -- TODO
+
+  SendInvite   :: Prf HasState 'Broker s
+               => String -- invitation - TODO
+               -> Command ()
+                    'Recipient 'Sender
+                    ('New <==> s <==| 'None)
+                    ('Pending <==> s <==| 'New)
+
+  ConfirmConn  :: Prf HasState 'Recipient s
+               => SecureConnRequest
+               -> Command ()
+                    'Sender 'Broker
+                    (s <==> 'New <==| 'New)
+                    (s <==> 'New <==| 'Confirmed)
+
+  PushConfirm  :: Prf HasState 'Sender s
+               => Command SecureConnRequest
+                    'Broker 'Recipient
+                    ('Pending <==> 'New <==| s)
+                    ('Confirmed <==> 'New <==| s)
+
+  SecureConn   :: Prf HasState 'Sender s
+               => SecureConnRequest
+               -> Command ()
+                    'Recipient 'Broker
+                    ('Confirmed <==> 'New <==| s)
+                    ('Secured <==> 'Secured <==| s)
+
+  SendWelcome  :: Prf HasState 'Recipient s
+               => Command ()
+                    'Sender 'Broker
+                    (s <==> 'Secured <==| 'Confirmed)
+                    (s <==> 'Secured <==| 'Secured)
+
+  PushWelcome  :: Prf HasState 'Sender s
+               => Command ()
+                    'Broker 'Recipient
+                    ('Secured <==> 'Secured <==| s)
+                    ('Secured <==> 'Secured <==| s)
+
+  SendMsg      :: Prf HasState 'Recipient s
+               => SendMessageRequest
+               -> Command ()
+                    'Sender 'Broker
+                    (s <==> 'Secured <==| 'Secured)
+                    (s <==> 'Secured <==| 'Secured)
+
+  PushMsg      :: Prf HasState 'Sender s
+               => Command MessagesResponse -- TODO, has to be a single message
+                    'Broker 'Recipient
+                    ('Secured <==> 'Secured <==| s)
+                    ('Secured <==> 'Secured <==| s)
+
+  DeleteMsg    :: Prf HasState 'Sender s   -- TODO needs message ID parameter
+               => Command ()
+                    'Recipient 'Broker
+                    ('Secured <==> 'Secured <==| s)
+                    ('Secured <==> 'Secured <==| s)
+
+  Return       :: a -> Command a from to state state
+
+  (:>>)        :: Command a from1 to1 s1 s2
+               -> Command b from2 to2 s2 s3
+               -> Command b from1 to2 s1 s3
+
+  (:>>=)       :: Command a from1 to1 s1 s2
+               -> (a -> Command b from2 to2 s2 s3)
+               -> Command b from1 to2 s1 s3
+
+
+infix 5 &:
+(&:) :: Sing from
+     -> Command a from to s1 s2
+     -> Command a from to s1 s2
+(&:) _ c = c

definitions/src/Simplex/Messaging/ServerAPI.hs

@@ -25,11 +25,11 @@ type ServerAPI =
   :<|> DeleteMessage
   :<|> SendMessage
 
-type CreateConnection = "connection" :> ReqBody '[JSON] NewConnectionReqBody
-                                     :> PostCreated '[JSON] NewConnectionResBody
+type CreateConnection = "connection" :> ReqBody '[JSON] CreateConnRequest
+                                     :> PostCreated '[JSON] CreateConnResponse
 
 type SecureConnection = "connection" :> Capture "connectionId" Base64EncodedString
-                                     :> ReqBody '[JSON] SecureConnectionReqBody
+                                     :> ReqBody '[JSON] SecureConnRequest
                                      :> Put '[JSON] NoContent
 
 type DeleteConnection = "connection" :> Capture "connectionId" Base64EncodedString
@@ -37,14 +37,14 @@ type DeleteConnection = "connection" :> Capture "connectionId" Base64EncodedStri
 
 type GetMessages      = "connection" :> Capture "connectionId" Base64EncodedString :>
                         "messages"   :> QueryParam "fromMessageId" (Maybe Base64EncodedString)
-                                     :> Get '[JSON] MessagesResBody
+                                     :> Get '[JSON] MessagesResponse
 
 type DeleteMessage    = "connection" :> Capture "connectionId" Base64EncodedString :>
                         "messages"   :> Capture "messageId" Base64EncodedString
                                      :> Delete '[JSON] NoContent
 
 type SendMessage      = "connection" :> Capture "senderConnectionId" Base64EncodedString :>
-                        "messages"   :> ReqBody '[JSON] SendMessageReqBody
+                        "messages"   :> ReqBody '[JSON] SendMessageRequest
                                      :> PostCreated '[JSON] NoContent
 
 -- API docs
@@ -106,14 +106,14 @@ instance ToParam (QueryParam "fromMessageId" (Maybe Base64EncodedString)) where
                   "if set, the server will respond with the messages received starting from the message with server message ID (unique per server) passed in this parameter."
                   Normal
 
-instance ToSample NewConnectionReqBody where
-  toSamples _ = singleSample $ NewConnectionReqBody "BODbZxmtKUUF1l8pj4nVjQ"
+instance ToSample CreateConnRequest where
+  toSamples _ = singleSample $ CreateConnRequest "BODbZxmtKUUF1l8pj4nVjQ"
 
-instance ToSample NewConnectionResBody where
-  toSamples _ = singleSample $ NewConnectionResBody "Qxz93A" "N9pA3g"
+instance ToSample CreateConnResponse where
+  toSamples _ = singleSample $ CreateConnResponse "Qxz93A" "N9pA3g"
 
-instance ToSample SecureConnectionReqBody where
-  toSamples _ = singleSample $ SecureConnectionReqBody "XPaVEVNunkYKqqK0dnAT5Q"
+instance ToSample SecureConnRequest where
+  toSamples _ = singleSample $ SecureConnRequest "XPaVEVNunkYKqqK0dnAT5Q"
 
 dummyMessage :: Message
 dummyMessage = Message
@@ -122,13 +122,13 @@ dummyMessage = Message
                 , msg = "OQLMXoEA4iv-aR46puPJuY1Rdoc1KY0gfq8oElJwtAs"
                 }
 
-instance ToSample MessagesResBody where
-  toSamples _ = singleSample $ MessagesResBody
+instance ToSample MessagesResponse where
+  toSamples _ = singleSample $ MessagesResponse
                                 { messages = [dummyMessage]
                                 , nextMessageId = Nothing
                                 }
 
-instance ToSample SendMessageReqBody where
-  toSamples _ = singleSample $ SendMessageReqBody
+instance ToSample SendMessageRequest where
+  toSamples _ = singleSample $ SendMessageRequest
                                 { msg = "OQLMXoEA4iv-aR46puPJuY1Rdoc1KY0gfq8oElJwtAs"
                                 }

definitions/src/Simplex/Messaging/Types.hs

@@ -7,16 +7,16 @@ import ClassyPrelude
 import Data.Aeson
 import GHC.Generics()
 
-newtype NewConnectionReqBody = NewConnectionReqBody
+newtype CreateConnRequest = CreateConnRequest
   { recipientKey :: Key
   } deriving (Show, Generic, ToJSON, FromJSON)
 
-data NewConnectionResBody = NewConnectionResBody
+data CreateConnResponse = CreateConnResponse
   { recipientId :: String
   , senderId    :: String
   } deriving (Show, Generic, ToJSON, FromJSON)
 
-newtype SecureConnectionReqBody = SecureConnectionReqBody
+newtype SecureConnRequest = SecureConnRequest
   { senderKey :: Key
   } deriving (Show, Generic, ToJSON, FromJSON)
 
@@ -26,12 +26,12 @@ data Message = Message
   , msg  :: Base64EncodedString
   } deriving (Show, Generic, ToJSON, FromJSON)
 
-data MessagesResBody = MessagesResBody
+data MessagesResponse = MessagesResponse
   { messages      :: [Message]
   , nextMessageId :: Maybe Base64EncodedString
   } deriving (Show, Generic, ToJSON, FromJSON)
 
-newtype SendMessageReqBody = SendMessageReqBody
+newtype SendMessageRequest = SendMessageRequest
   { msg :: Base64EncodedString
   } deriving (Show, Generic, ToJSON, FromJSON)