diff --git a/definitions/src/Simplex/Messaging/PrintScenario.hs b/definitions/src/Simplex/Messaging/PrintScenario.hs index 95c6ddad19..1d207fa402 100644 --- a/definitions/src/Simplex/Messaging/PrintScenario.hs +++ b/definitions/src/Simplex/Messaging/PrintScenario.hs @@ -10,7 +10,7 @@ import Data.Singletons import Simplex.Messaging.Protocol import Simplex.Messaging.Types -printScenario :: Protocol rs bs ss rs' bs' ss' a -> IO () +printScenario :: Protocol s s' a -> IO () printScenario scn = ps 1 "" $ execWriter $ logScenario scn where ps :: Int -> String -> [(String, String)] -> IO () @@ -23,15 +23,13 @@ printScenario scn = ps 1 "" $ execWriter $ logScenario scn prt i' s = putStrLn s >> ps i' p' ls l' = " - " <> l -logScenario :: Protocol rs bs ss rs' bs' ss' a -> Writer [(String, String)] a +logScenario :: Protocol s s' a -> Writer [(String, String)] a logScenario (Start s) = tell [("", s)] -logScenario (p :>> c) = logScenario p >> logCommand c -logScenario (p :>>= f) = logScenario p >>= \x -> logCommand (f x) - -logCommand :: PartiesCommand from fs fs' to ts ts' a -> Writer [(String, String)] a -logCommand ((:->) from to cmd) = do +logScenario ((:->) 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" diff --git a/definitions/src/Simplex/Messaging/Protocol.hs b/definitions/src/Simplex/Messaging/Protocol.hs index fa3241c60e..055e64a2cc 100644 --- a/definitions/src/Simplex/Messaging/Protocol.hs +++ b/definitions/src/Simplex/Messaging/Protocol.hs @@ -67,7 +67,8 @@ data (to :: Party) (ts :: ConnState) (ts' :: ConnState) - (res :: Type) :: Type where + (res :: Type) :: Type + where CreateConn :: PublicKey -> Command Recipient None New Broker None New CreateConnResponse @@ -112,7 +113,8 @@ data data Connection (p :: Party) - (s :: ConnState) :: Type where + (s :: ConnState) :: Type + where Connection :: String -> Connection p s -- TODO replace with real type definition class Monad m => PartyProtocol m (p :: Party) where @@ -132,67 +134,54 @@ 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 AllowedStates from fs fs' to ts ts' = - ( HasState from fs, - HasState from fs', - HasState to ts, - HasState 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, + HasState from fs', + HasState to ts' + ) infix 6 :-> -data PartiesCommand from fs fs' to ts ts' res :: Type where - (:->) :: - AllowedStates from fs fs' to ts ts' => - Sing from -> - Sing to -> - Command from fs fs' to ts ts' res -> - PartiesCommand from fs fs' to ts ts' res +type ProtocolState = (ConnState, ConnState, ConnState) -$( promote - [d| - cConnSt :: Party -> ConnState -> ConnState -> ConnState -> ConnState - cConnSt p rs bs ss = case p of - Recipient -> rs - Broker -> bs - Sender -> ss +type family ConnSt (p :: Party) (s :: ProtocolState) :: ConnState where + ConnSt Recipient '(rs, _, _) = rs + ConnSt Broker '(_, bs, _) = bs + ConnSt Sender '(_, _, ss) = ss - pConnSt :: Party -> ConnState -> Party -> ConnState -> Party -> ConnState -> ConnState - pConnSt p ps from fs' to ts' - | p == from = fs' - | p == to = ts' - | otherwise = ps - |] - ) +type family ProtoSt (s :: ProtocolState) from fs' to ts' 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' where + PartySt from _ from fs' _ _ = fs' + PartySt to _ _ _ to ts' = ts' + PartySt p s _ _ _ _ = ConnSt p s infixl 4 :>> -data - Protocol - (rs :: ConnState) - (bs :: ConnState) - (ss :: ConnState) - (rs' :: ConnState) - (bs' :: ConnState) - (ss' :: ConnState) - (res :: Type) :: Type where - Start :: String -> Protocol rs bs ss rs' bs' ss' () +data Protocol (s :: ProtocolState) (s' :: ProtocolState) (a :: Type) :: Type where + Start :: String -> Protocol s s () + (:->) :: + 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 rs bs ss rs' bs' ss' a -> - PartiesCommand from (CConnSt from rs' bs' ss') fs' to (CConnSt to rs' bs' ss') ts' b -> - Protocol rs bs ss - (PConnSt Recipient rs' from fs' to ts') - (PConnSt Broker bs' from fs' to ts') - (PConnSt Sender ss' from fs' to ts') - b + Protocol s s' a -> + Protocol s' s'' b -> + Protocol s s'' b (:>>=) :: - Protocol rs bs ss rs' bs' ss' a -> - (a -> PartiesCommand from (CConnSt from rs' bs' ss') fs' to (CConnSt to rs' bs' ss') ts' b) -> - Protocol rs bs ss - (PConnSt Recipient rs' from fs' to ts') - (PConnSt Broker bs' from fs' to ts') - (PConnSt Sender ss' from fs' to ts') - b + Protocol s s' a -> + (a -> Protocol s' s'' b) -> + Protocol s s'' b infix 5 |$ diff --git a/definitions/src/Simplex/Messaging/Scenarios.hs b/definitions/src/Simplex/Messaging/Scenarios.hs index 3922e70e4d..4ac1634a4e 100644 --- a/definitions/src/Simplex/Messaging/Scenarios.hs +++ b/definitions/src/Simplex/Messaging/Scenarios.hs @@ -19,7 +19,7 @@ b = SBroker s :: Sing Sender s = SSender -establishConnection :: Protocol None None None Secured Secured Secured () +establishConnection :: Protocol '(None, None, None) '(Secured, Secured, Secured) () establishConnection = Start "Establish simplex messaging connection and send first message" :>> r :-> b |$ CreateConn "BODbZxmtKUUF1l8pj4nVjQ"