diff --git a/definitions/src/Control/Protocol.hs b/definitions/src/Control/Protocol.hs index 55ad516e88..7549bba628 100644 --- a/definitions/src/Control/Protocol.hs +++ b/definitions/src/Control/Protocol.hs @@ -1,6 +1,9 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} @@ -11,7 +14,7 @@ module Control.Protocol ProtocolCmd (..), Command, (->:), - comment, + interpret, ) where @@ -23,7 +26,6 @@ import GHC.TypeLits (ErrorMessage (..), TypeError) type Command party state = (party, state, state) -> (party, state, state) -> Type -> Type data ProtocolCmd (cmd :: Command p k) (parties :: [p]) (s :: [k]) (s' :: [k]) (a :: Type) where - Comment :: String -> ProtocolCmd cmd ps s s () ProtocolCmd :: Sing (from :: p) -> Sing (to :: p) -> @@ -41,15 +43,34 @@ infix 6 ->: Protocol cmd ps s (Inj ps (Inj ps s from fs') to ts') a (->:) f t c = xfree $ ProtocolCmd f t c -comment :: String -> Protocol ps cmd s s () -comment = xfree . Comment +interpret :: + forall m cmd ps s s' a. + Monad m => + (forall from to b. (Sing (P from) -> Sing (P to) -> cmd from to b -> m b)) -> + Protocol cmd ps s s' a -> + m a +interpret runCommand = loop + where + loop :: forall s1 s2 b. Protocol cmd ps s1 s2 b -> m b + loop = \case + Pure x -> return x + Bind c f -> do + x <- run c + loop (f x) + run :: forall s1 s2 b. ProtocolCmd cmd ps s1 s2 b -> m b + run (ProtocolCmd from to cmd) = runCommand from to cmd +type family P (partyCmd :: (party, s, s)) where + P '(p, _, _) = p + +-- extracts the state of one party from the list of states type family Prj (parties :: [pk]) (state :: [k]) (party :: pk) :: k where Prj (p ': _) (s ': _) p = s Prj (_ ': ps) (_ ': ss) p = Prj ps ss p Prj '[] _ p = TypeError (NoParty p) Prj _ '[] p = TypeError (NoParty p :$$: StateError) +-- updates the state of some party in the list of states type family Inj (parties :: [pk]) (state :: [k]) (p :: pk) (s' :: k) :: [k] where Inj (p ': _) (_ ': ss) p s' = s' ': ss Inj (_ ': ps) (s ': ss) p s' = s ': Inj ps ss p s' diff --git a/definitions/src/Simplex/Messaging/PrintScenario.hs b/definitions/src/Simplex/Messaging/PrintScenario.hs index e941fc5a13..a4bfb1090a 100644 --- a/definitions/src/Simplex/Messaging/PrintScenario.hs +++ b/definitions/src/Simplex/Messaging/PrintScenario.hs @@ -4,13 +4,13 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} +{-# LANGUAGE LambdaCase #-} {-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-} module Simplex.Messaging.PrintScenario where import Control.Monad.Writer -import Control.Protocol -import Control.XFreer +import Control.Protocol (interpret) import Data.Singletons import Simplex.Messaging.Protocol import Simplex.Messaging.Types @@ -21,7 +21,6 @@ printScenario scn = ps 1 "" $ execWriter $ logScenario scn ps :: Int -> String -> [(String, String)] -> IO () ps _ _ [] = return () ps i p ((p', l) : ls) - | p' == "" = part i $ "\n" <> l <> "\n" | p' /= p = part (i + 1) $ show i <> ". " <> p' <> ":\n" <> prefix l | otherwise = part i $ prefix l where @@ -29,45 +28,43 @@ printScenario scn = ps 1 "" $ execWriter $ logScenario scn prefix s = " - " <> s logScenario :: MonadWriter [(String, String)] m => SimplexProtocol s s' a -> m a -logScenario (Pure x) = return x -logScenario (Bind p f) = logProtocol p >>= \x -> logScenario (f x) - -logProtocol :: MonadWriter [(String, String)] m => SimplexProtocolCmd s s' a -> m a -logProtocol (Comment s) = tell [("", s)] -logProtocol (ProtocolCmd from to cmd) = do +logScenario = interpret $ \from to cmd -> do tell [(party from, commandStr cmd <> " " <> party to)] mockCommand cmd commandStr :: SimplexCommand 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" -commandStr (SendInvite _) = "sends out-of band invitation to " -commandStr (ConfirmConn cid _) = "confirms connection " <> show cid <> " in" -commandStr (PushConfirm cid _) = "pushes confirmation for " <> show cid <> " to" -commandStr (SecureConn cid _) = "secures connection " <> show cid <> " in" -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" +commandStr = \case + CreateConn _ -> "creates connection in" + Subscribe cid -> "subscribes to connection " <> show cid <> " in" + Unsubscribe cid -> "unsubscribes from connection " <> show cid <> " in" + SendInvite _ -> "sends out-of band invitation to " + ConfirmConn cid _ -> "confirms connection " <> show cid <> " in" + PushConfirm cid _ -> "pushes confirmation for " <> show cid <> " to" + SecureConn cid _ -> "secures connection " <> show cid <> " in" + SendMsg cid _ -> "sends message to connection " <> show cid <> " in" + PushMsg cid _ -> "pushes message from connection " <> show cid <> " to" + DeleteMsg cid _ -> "deletes message from connection " <> show cid <> " in" mockCommand :: Monad m => SimplexCommand from to a -> m a -mockCommand (CreateConn _) = - return - CreateConnResponse - { recipientId = "Qxz93A", - senderId = "N9pA3g" - } -mockCommand (Subscribe _) = return () -mockCommand (Unsubscribe _) = return () -mockCommand (SendInvite _) = return () -mockCommand (ConfirmConn _ _) = return () -mockCommand (PushConfirm _ _) = return () -mockCommand (SecureConn _ _) = return () -mockCommand (SendMsg _ _) = return () -mockCommand (PushMsg _ _) = return () -mockCommand (DeleteMsg _ _) = return () +mockCommand = \case + (CreateConn _) -> + return + CreateConnResponse + { recipientId = "Qxz93A", + senderId = "N9pA3g" + } + Subscribe _ -> return () + Unsubscribe _ -> return () + SendInvite _ -> return () + ConfirmConn _ _ -> return () + PushConfirm _ _ -> return () + SecureConn _ _ -> return () + SendMsg _ _ -> return () + PushMsg _ _ -> return () + DeleteMsg _ _ -> return () party :: Sing (p :: Party) -> String -party SRecipient = "Alice (recipient)" -party SBroker = "Alice's server (broker)" -party SSender = "Bob (sender)" +party = \case + SRecipient -> "Alice (recipient)" + SBroker -> "Alice's server (broker)" + SSender -> "Bob (sender)" diff --git a/definitions/src/Simplex/Messaging/Protocol.hs b/definitions/src/Simplex/Messaging/Protocol.hs index 5685148863..5df6765ed4 100644 --- a/definitions/src/Simplex/Messaging/Protocol.hs +++ b/definitions/src/Simplex/Messaging/Protocol.hs @@ -25,8 +25,6 @@ import Simplex.Messaging.Types type SimplexProtocol = Protocol SimplexCommand '[Recipient, Broker, Sender] -type SimplexProtocolCmd = ProtocolCmd SimplexCommand '[Recipient, Broker, Sender] - data SimplexCommand :: Command Party ConnState where CreateConn :: PublicKey -> diff --git a/definitions/src/Simplex/Messaging/Scenarios.hs b/definitions/src/Simplex/Messaging/Scenarios.hs index 908e1ae076..233ea51c7e 100644 --- a/definitions/src/Simplex/Messaging/Scenarios.hs +++ b/definitions/src/Simplex/Messaging/Scenarios.hs @@ -25,9 +25,9 @@ b = SBroker s :: Sing Sender s = SSender +-- Establish simplex messaging connection and send first message establishConnection :: SimplexProtocol '[None, None, None] '[Secured, Secured, Secured] () establishConnection = do - comment "## Establish simplex messaging connection and send first message" r ->: b $ CreateConn "BODbZxmtKUUF1l8pj4nVjQ" r ->: b $ Subscribe "RU" r ->: s $ SendInvite "invitation RU" -- invitation - TODo @@ -38,7 +38,7 @@ establishConnection = do s ->: b $ SendMsg "SU" "welcome" -- welcome message b ->: r $ PushMsg "RU" Message {msgId = "def", msg = "welcome"} r ->: b $ DeleteMsg "RU" "def" - comment "The connection is established (\"Secured\"), sending the message" + -- The connection is established ("Secured"), sending the message s ->: b $ SendMsg "SU" "hello there" b ->: r $ PushMsg "RU" Message {msgId = "ghi", msg = "hello there"} r ->: b $ DeleteMsg "RU" "ghi"