mirror of
https://github.com/simplex-chat/simplex-chat.git
synced 2026-05-25 20:44:38 +00:00
change scenario syntax
This commit is contained in:
Evgeny Poberezkin
@@ -1,26 +1,24 @@
|
||||
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
|
||||
{-# LANGUAGE ConstraintKinds #-}
|
||||
{-# LANGUAGE DeriveAnyClass #-}
|
||||
{-# LANGUAGE EmptyCase #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE InstanceSigs #-}
|
||||
{-# 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 TypeOperators #-}
|
||||
{-# LANGUAGE TypeInType #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
{-# LANGUAGE NoStarIsType #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE StandaloneDeriving #-}
|
||||
{-# LANGUAGE TemplateHaskell #-}
|
||||
{-# LANGUAGE TypeApplications #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE TypeInType #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
|
||||
module Simplex.Messaging.Protocol where
|
||||
|
||||
import Simplex.Messaging.Types
|
||||
|
||||
import ClassyPrelude
|
||||
import Data.Kind
|
||||
import Data.Singletons
|
||||
@@ -29,6 +27,7 @@ import Data.Singletons.TH
|
||||
import Data.Type.Predicate
|
||||
import Data.Type.Predicate.Auto
|
||||
import GHC.TypeLits
|
||||
import Simplex.Messaging.Types
|
||||
|
||||
$(singletons [d|
|
||||
data Participant = Recipient | Broker | Sender
|
||||
@@ -221,21 +220,34 @@ data Command a (from :: Participant) (to :: Participant)
|
||||
|
||||
Return :: a -> Command a from to state state ss ss n n
|
||||
|
||||
(:>>) :: Command a from1 to1 s1 s2 ss1 ss2 n1 n2
|
||||
-> Command b from2 to2 s2 s3 ss2 ss3 n2 n3
|
||||
-> Command b from1 to2 s1 s3 ss1 ss3 n1 n3
|
||||
|
||||
(:>>=) :: Command a from1 to1 s1 s2 ss1 ss2 n1 n2
|
||||
-> (a -> Command b from2 to2 s2 s3 ss2 ss3 n2 n3)
|
||||
-> Command b from1 to2 s1 s3 ss1 ss3 n1 n3
|
||||
|
||||
(:>>) :: Command a from1 to1 s1 s2 ss1 ss2 n1 n2
|
||||
-> Command b from2 to2 s2 s3 ss2 ss3 n2 n3
|
||||
-> Command b from1 to2 s1 s3 ss1 ss3 n1 n3
|
||||
|
||||
infix 6 ==>
|
||||
(==>) :: from -> to -> (from, to)
|
||||
from ==> to = (from, to)
|
||||
Fail :: String
|
||||
-> Command String from to state (None <==> None <==| None) ss ss n n
|
||||
|
||||
infix 5 &:
|
||||
(&:) :: (Sing from, Sing to)
|
||||
-> Command a from to s1 s2 ss1 ss2 n1 n2
|
||||
-> Command a from to s1 s2 ss1 ss2 n1 n2
|
||||
(&:) _ c = c
|
||||
-- redifine Monad operators to compose commands
|
||||
-- using `do` notation with RebindableSyntax extension
|
||||
(>>=) :: Command a from1 to1 s1 s2 ss1 ss2 n1 n2
|
||||
-> (a -> Command b from2 to2 s2 s3 ss2 ss3 n2 n3)
|
||||
-> Command b from1 to2 s1 s3 ss1 ss3 n1 n3
|
||||
(>>=) = (:>>=)
|
||||
|
||||
(>>) :: Command a from1 to1 s1 s2 ss1 ss2 n1 n2
|
||||
-> Command b from2 to2 s2 s3 ss2 ss3 n2 n3
|
||||
-> Command b from1 to2 s1 s3 ss1 ss3 n1 n3
|
||||
(>>) = (:>>)
|
||||
|
||||
fail :: String -> Command 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 a from to s s' ss ss' n n' -> Command a from to s s' ss ss' n n')
|
||||
(-->) _ _ = id
|
||||
|
||||
@@ -1,34 +1,44 @@
|
||||
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
|
||||
{-# LANGUAGE BlockArguments #-}
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
{-# OPTIONS_GHC -fno-warn-unused-do-bind #-}
|
||||
-- below warning appears because of hiding Monad operators from prelude exports
|
||||
{-# OPTIONS_GHC -fno-warn-dodgy-imports #-}
|
||||
{-# LANGUAGE BlockArguments #-}
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE RebindableSyntax #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
|
||||
module Simplex.Messaging.Scenarios where
|
||||
|
||||
import ClassyPrelude hiding ((>>=), (>>), fail)
|
||||
import Data.Singletons
|
||||
import Simplex.Messaging.Protocol
|
||||
import Simplex.Messaging.Types
|
||||
|
||||
import ClassyPrelude
|
||||
r :: Sing Recipient
|
||||
r = SRecipient
|
||||
|
||||
b :: Sing Broker
|
||||
b = SBroker
|
||||
|
||||
s :: Sing Sender
|
||||
s = SSender
|
||||
|
||||
establishConnection :: Command ()
|
||||
Recipient Broker
|
||||
(None <==> None <==| None)
|
||||
(Secured <==> Secured <==| Secured)
|
||||
False False 0 0
|
||||
establishConnection =
|
||||
SRecipient ==> SBroker &: CreateConn "123" :>>= -- recipient's public key for broker
|
||||
\CreateConnResponse{..} ->
|
||||
SRecipient ==> SBroker &: Subscribe :>>
|
||||
SRecipient ==> SSender &: SendInvite "invite" :>> -- TODO invitation object
|
||||
SSender ==> SBroker &: ConfirmConn "456" :>> -- sender's public key for broker"
|
||||
SBroker ==> SRecipient &: PushConfirm :>>=
|
||||
\senderKey ->
|
||||
SRecipient ==> SBroker &: SecureConn senderKey :>>
|
||||
SRecipient ==> SBroker &: DeleteMsg :>>
|
||||
SSender ==> SBroker &: SendWelcome :>>
|
||||
SBroker ==> SRecipient &: PushMsg :>>
|
||||
SRecipient ==> SBroker &: DeleteMsg :>>
|
||||
SSender ==> SBroker &: SendMsg "Hello" :>>
|
||||
SBroker ==> SRecipient &: PushMsg :>>
|
||||
SRecipient ==> SBroker &: DeleteMsg :>>
|
||||
SRecipient ==> SBroker &: Unsubscribe
|
||||
establishConnection = do -- it is commands composition, not Monad
|
||||
r --> b $ CreateConn "123" -- recipient's public key for broker
|
||||
r --> b $ Subscribe
|
||||
r --> s $ SendInvite "invite" -- TODO invitation object
|
||||
s --> b $ ConfirmConn "456" -- sender's public key for broker"
|
||||
key <- b --> r $ PushConfirm
|
||||
r --> b $ SecureConn key
|
||||
r --> b $ DeleteMsg
|
||||
s --> b $ SendWelcome
|
||||
b --> r $ PushMsg
|
||||
r --> b $ DeleteMsg
|
||||
s --> b $ SendMsg "Hello"
|
||||
b --> r $ PushMsg
|
||||
r --> b $ DeleteMsg
|
||||
r --> b $ Unsubscribe
|
||||
|
||||
@@ -1,7 +1,7 @@
|
||||
{-# OPTIONS_GHC -fno-warn-orphans #-}
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
|
||||
module Simplex.Messaging.ServerAPI
|
||||
( ServerAPI
|
||||
@@ -9,13 +9,12 @@ module Simplex.Messaging.ServerAPI
|
||||
, serverApiExtra
|
||||
) where
|
||||
|
||||
import Simplex.Messaging.Types as T
|
||||
|
||||
import ClassyPrelude
|
||||
import Control.Lens
|
||||
import Data.Function()
|
||||
import Servant
|
||||
import Servant.Docs
|
||||
import Simplex.Messaging.Types
|
||||
|
||||
type ServerAPI =
|
||||
CreateConnection
|
||||
@@ -117,7 +116,7 @@ instance ToSample SecureConnRequest where
|
||||
|
||||
dummyMessage :: Message
|
||||
dummyMessage = Message
|
||||
{ T.id = "p8PCiGPZ"
|
||||
{ connId = "p8PCiGPZ"
|
||||
, ts = "2020-03-15T19:58:33.695Z"
|
||||
, msg = "OQLMXoEA4iv-aR46puPJuY1Rdoc1KY0gfq8oElJwtAs"
|
||||
}
|
||||
|
||||
@@ -1,63 +0,0 @@
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE EmptyCase #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE InstanceSigs #-}
|
||||
{-# LANGUAGE LambdaCase #-}
|
||||
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||
{-# LANGUAGE PolyKinds #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE StandaloneDeriving #-}
|
||||
{-# LANGUAGE TypeApplications #-}
|
||||
{-# LANGUAGE TemplateHaskell #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
{-# OPTIONS_GHC -Wall #-}
|
||||
{-# OPTIONS_GHC -Werror=incomplete-patterns #-}
|
||||
|
||||
module Simplex.Messaging.Test where
|
||||
|
||||
import ClassyPrelude
|
||||
|
||||
import Data.Kind
|
||||
import Data.Singletons()
|
||||
import Data.Singletons.TH
|
||||
import Data.Type.Predicate
|
||||
import Data.Type.Predicate.Auto
|
||||
|
||||
$(singletons [d|
|
||||
data Participant = Recipient | Broker | Sender
|
||||
|
||||
data ConnectionState = 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
|
||||
|])
|
||||
|
||||
-- broker connection states
|
||||
data BrokerCS :: ConnectionState -> Type where
|
||||
BrkNew :: BrokerCS 'New
|
||||
BrkSecured :: BrokerCS 'Secured
|
||||
|
||||
instance Auto (TyPred BrokerCS) 'New where auto = autoTC
|
||||
instance Auto (TyPred BrokerCS) 'Secured where auto = autoTC
|
||||
|
||||
data RBState (rs :: ConnectionState) (bs :: ConnectionState) :: Type where
|
||||
RBState :: Auto (TyPred BrokerCS) bs
|
||||
=> Sing rs -> Sing bs -> RBState rs bs
|
||||
|
||||
data Box a = Num a => Box a
|
||||
|
||||
goodBoxSample :: Box Int
|
||||
goodBoxSample = Box 1
|
||||
|
||||
-- badBoxSample :: Box String
|
||||
-- badBox = Box "foo"
|
||||
|
||||
goodSt :: RBState 'New 'New
|
||||
goodSt = RBState SNew SNew
|
||||
|
||||
-- badSt :: RBState 'Pending 'Pending
|
||||
-- badSt = RBState SPending SPending
|
||||
@@ -1,5 +1,5 @@
|
||||
{-# LANGUAGE DeriveAnyClass #-}
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
|
||||
module Simplex.Messaging.Types where
|
||||
|
||||
@@ -29,9 +29,9 @@ instance IsString SecureConnRequest where
|
||||
|
||||
|
||||
data Message = Message
|
||||
{ id :: Base64EncodedString
|
||||
, ts :: TimeStamp
|
||||
, msg :: Base64EncodedString
|
||||
{ connId :: Base64EncodedString
|
||||
, ts :: TimeStamp
|
||||
, msg :: Base64EncodedString
|
||||
} deriving (Show, Generic, ToJSON, FromJSON)
|
||||
|
||||
data MessagesResponse = MessagesResponse
|
||||
|
||||
@@ -130,7 +130,7 @@ Also see [Simplex messaging protocol implementation](simplex-messaging-implement
|
||||
- Example (`application/json;charset=utf-8`, `application/json`):
|
||||
|
||||
```javascript
|
||||
{"messages":[{"ts":"2020-03-15T19:58:33.695Z","msg":"OQLMXoEA4iv-aR46puPJuY1Rdoc1KY0gfq8oElJwtAs","id":"p8PCiGPZ"}],"nextMessageId":null}
|
||||
{"messages":[{"ts":"2020-03-15T19:58:33.695Z","msg":"OQLMXoEA4iv-aR46puPJuY1Rdoc1KY0gfq8oElJwtAs","connId":"p8PCiGPZ"}],"nextMessageId":null}
|
||||
```
|
||||
|
||||
## DELETE /connection/:connectionId/messages/:messageId
|
||||
|
||||
Reference in New Issue
Block a user