refactor: make Protocol a freer parameterized monad
This commit is contained in:
@@ -18,26 +18,15 @@ ghc-options:
|
||||
- -Wincomplete-record-updates
|
||||
- -Wincomplete-uni-patterns
|
||||
|
||||
# default-extensions:
|
||||
# - BlockArguments
|
||||
# - DuplicateRecordFields
|
||||
# - LambdaCase
|
||||
# - NamedFieldPuns
|
||||
# - NoImplicitPrelude
|
||||
# - OverloadedStrings
|
||||
# - RecordWildCards
|
||||
|
||||
dependencies:
|
||||
- aeson
|
||||
- base >= 4.7 && < 5
|
||||
- classy-prelude
|
||||
- decidable
|
||||
- freer-indexed
|
||||
- lens
|
||||
- mtl
|
||||
- singletons
|
||||
- servant-docs
|
||||
- servant-server
|
||||
- template-haskell
|
||||
- transformers
|
||||
|
||||
library:
|
||||
|
||||
@@ -6,6 +6,7 @@
|
||||
module Simplex.Messaging.PrintScenario where
|
||||
|
||||
import Control.Monad.Writer
|
||||
import Control.XFreer
|
||||
import Data.Singletons
|
||||
import Simplex.Messaging.Protocol
|
||||
import Simplex.Messaging.Types
|
||||
@@ -24,12 +25,14 @@ printScenario scn = ps 1 "" $ execWriter $ logScenario scn
|
||||
l' = " - " <> l
|
||||
|
||||
logScenario :: Protocol s s' a -> Writer [(String, String)] a
|
||||
logScenario (Start s) = tell [("", s)]
|
||||
logScenario ((:->) from to cmd) = do
|
||||
logScenario (Pure x) = return x
|
||||
logScenario (Bind p f) = logProtocol p >>= \x -> logScenario (f x)
|
||||
|
||||
logProtocol :: ProtocolEff s s' a -> Writer [(String, String)] a
|
||||
logProtocol (Start s) = tell [("", s)]
|
||||
logProtocol (ProtocolCmd from to cmd) = do
|
||||
tell [(party from, commandStr cmd <> " " <> party to)]
|
||||
mockCommand cmd
|
||||
logScenario (p :>> c) = logScenario p >> logScenario c
|
||||
logScenario (p :>>= f) = logScenario p >>= \x -> logScenario (f x)
|
||||
|
||||
commandStr :: Command from fs fs' to ts ts' a -> String
|
||||
commandStr (CreateConn _) = "creates connection in"
|
||||
|
||||
@@ -21,6 +21,7 @@
|
||||
module Simplex.Messaging.Protocol where
|
||||
|
||||
import Control.Monad.Trans.Except
|
||||
import Control.XFreer
|
||||
import Data.Kind
|
||||
import Data.Singletons
|
||||
import Data.Singletons.TH
|
||||
@@ -134,8 +135,8 @@ apiStub _ = throwE "api not implemented"
|
||||
actionStub :: Monad m => Connection p ps -> ExceptT String m res -> ExceptT String m (Connection p ps')
|
||||
actionStub _ _ = throwE "action not implemented"
|
||||
|
||||
type family AllowedStates' s from fs' to ts' :: Constraint where
|
||||
AllowedStates' '(rs, bs, ss) from fs' to ts' =
|
||||
type family AllowedStates s from fs' to ts' :: Constraint where
|
||||
AllowedStates '(rs, bs, ss) from fs' to ts' =
|
||||
( HasState Recipient rs,
|
||||
HasState Broker bs,
|
||||
HasState Sender ss,
|
||||
@@ -143,8 +144,6 @@ type family AllowedStates' s from fs' to ts' :: Constraint where
|
||||
HasState to ts'
|
||||
)
|
||||
|
||||
infix 6 :->
|
||||
|
||||
type ProtocolState = (ConnState, ConnState, ConnState)
|
||||
|
||||
type family ConnSt (p :: Party) (s :: ProtocolState) :: ConnState where
|
||||
@@ -164,24 +163,29 @@ type family PartySt (p :: Party) (s :: ProtocolState) from fs' to ts' where
|
||||
PartySt to _ _ _ to ts' = ts'
|
||||
PartySt p s _ _ _ _ = ConnSt p s
|
||||
|
||||
infixl 4 :>>
|
||||
|
||||
data Protocol (s :: ProtocolState) (s' :: ProtocolState) (a :: Type) :: Type where
|
||||
Start :: String -> Protocol s s ()
|
||||
(:->) ::
|
||||
AllowedStates' s from fs' to ts' =>
|
||||
data ProtocolEff (s :: ProtocolState) (s' :: ProtocolState) (a :: Type) :: Type where
|
||||
Start :: String -> ProtocolEff s s ()
|
||||
ProtocolCmd ::
|
||||
AllowedStates s from fs' 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
|
||||
(:>>) ::
|
||||
Protocol s s' a ->
|
||||
Protocol s' s'' b ->
|
||||
Protocol s s'' b
|
||||
(:>>=) ::
|
||||
Protocol s s' a ->
|
||||
(a -> Protocol s' s'' b) ->
|
||||
Protocol s s'' b
|
||||
ProtocolEff s (ProtoSt s from fs' to ts') a
|
||||
|
||||
type Protocol = XFree ProtocolEff
|
||||
|
||||
infix 6 ->:
|
||||
|
||||
(->:) ::
|
||||
AllowedStates s from fs' 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
|
||||
|
||||
infix 5 |$
|
||||
|
||||
|
||||
@@ -6,6 +6,7 @@
|
||||
|
||||
module Simplex.Messaging.Scenarios where
|
||||
|
||||
import Control.XMonad
|
||||
import Data.Singletons
|
||||
import Simplex.Messaging.Protocol
|
||||
import Simplex.Messaging.Types
|
||||
@@ -21,18 +22,18 @@ s = SSender
|
||||
|
||||
establishConnection :: Protocol '(None, None, None) '(Secured, Secured, Secured) ()
|
||||
establishConnection =
|
||||
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"
|
||||
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"
|
||||
|
||||
@@ -29,7 +29,7 @@ resolver: lts-15.11
|
||||
# - auto-update
|
||||
# - wai
|
||||
packages:
|
||||
- .
|
||||
- .
|
||||
# Dependency packages to be pulled from upstream that are not in the resolver.
|
||||
# These entries can reference officially published versions as well as
|
||||
# forks / in-progress versions pinned to a git hash. For example:
|
||||
@@ -40,10 +40,7 @@ packages:
|
||||
# commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a
|
||||
#
|
||||
extra-deps:
|
||||
- decidable-0.3.0.0@sha256:34857003b57139a047c9ab7944c313c227d9db702a8dcefa1478966257099423,1774
|
||||
- functor-products-0.1.1.0@sha256:2bea36b6106b5756be6b81b3a5bfe7b41db1cf45fb63c19a1f04b572ba90fd0c,1456
|
||||
- vinyl-0.12.1@sha256:03f5e246fae2434250987bbfe708015dc6e23f60c20739c34738acde1383b96c,3921
|
||||
|
||||
- freer-indexed-0.1.0.0@sha256:b247be91b8ad2154fe1a514dec7c6a2553281d89325f0bc213d1d832d4c1a0e9,3007
|
||||
# Override default flag values for local packages and extra-deps
|
||||
# flags: {}
|
||||
|
||||
|
||||
Reference in New Issue
Block a user