refactor protocol interpreter

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'

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)"

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 ->

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"