connection states for all participants stored in one type (r <==> b <==| s)

specification/Simplex/Messaging.idr

@@ -170,11 +170,11 @@ goodSndConn = SCSecured (record
                          newSndConn)
 
 
--- protocol commands that participants send
+-- data types for protocol commands
 data Result : (a : Type) -> Type where
-  OK : a -> Result a
+  OK   : a -> Result a
-  Deny  : Result a -- access restriction, not some arbitrary error
+  Deny : Result a -- access restriction, not some arbitrary error
-  Error : String -> Result a
+  Err  : String -> Result a -- another error
 
 record BrkCreateConnRes where
   constructor MkBrkCreateConnRes
@@ -184,83 +184,95 @@ record BrkCreateConnRes where
 Message : Type
 Message = String
 
-infix 10 /@
 
--- operator to define connection state change based on the result
+-- operators to create connection state and state change based on the result
-(/@) : ConnectionState
+infixl 7 <==>, <==|
-    -> ConnectionState
+prefix 6 ///
-    -> (Result a -> ConnectionState)
+
-(/@) okCS failCS = \x => case x of
+data RBConnState : Type where
-                           OK _ => okCS
+  (<==>) : (recipient : ConnectionState)
-                           Deny => failCS
+        -> (broker    : ConnectionState)
-                           Error _ => failCS
+        -> {auto prf  : HasState Broker broker}
+        -> RBConnState
+
+data AllConnState : Type where
+  (<==|) : (rcpBrk : RBConnState)
+        -> (sender : ConnectionState)
+        -> {auto prf : HasState Sender sender}
+        -> AllConnState
+
+(///) : AllConnState
+     -> (AllConnState -> Result a -> AllConnState)
+(///) s' = \s, x => case x of
+                      OK _  => s'
+                      Deny  => s
+                      Err _ => s
+
+sameState : (AllConnState -> Result a -> AllConnState)
+sameState s _ => s
 
 
+-- protocol commands that participants send in relation to a specific connection
 data Command : (ty : Type)
-            -> (act    : Participant)
+            -> (from : Participant)
-            -> (rcv    : Participant)
+            -> (to : Participant)
-            -> (actCS  : ConnectionState)
+            -> (state : AllConnState)
-            -> (rcvCS  : ConnectionState)
+            -> ((state : AllConnState) -> Result ty -> AllConnState)
-            -> (actCS' : ty -> ConnectionState)
-            -> (rcvCS' : ty -> ConnectionState)
-            -> {auto prf : HasState act actCS}
-            -> {auto prf : HasState rcv rcvCS}
             -> Type where
 
   CreateConn  : (recipientBrokerKey : Key)
-             -> Command (Result BrkCreateConnRes)
+             -> {auto prf : HasState Sender s}
+             -> Command BrkCreateConnRes
                   Recipient Broker
-                  Null      Null
+                  (Null <==> Null <==| s)
-                  (New /@ Null) (New /@ Null)
+                  (/// New <==> New  <==| s)
 
-  Subscribe   : (connId : String)
+  Subscribe   : Command () Recipient Broker state sameState -- to improve
-             -> {auto prf : BrokerCS state}
-             -> Command (Result ())
-                  Recipient Broker
-                  state     state
-                  (const state) (const state)
 
   SendInvite  : Invitation
-             -> Command ()
+             -> {auto prf : HasState Broker s}
-                  Recipient Sender
+             -> Command () Recipient Sender
-                  New       Null
+                  (New <==> s <==| Null)
-                  (const Pending) (const New)
+                  (/// Pending <==> s <==| New)
 
-  ConfirmConn : (connId : String)
+  ConfirmConn : (senderBrokerKey : Key)
-             -> (senderBrokerKey : Key)
+             -> Command () Sender Broker
+                  (s <==> New <==| New)
+                  (/// s <==> New <==| Confirmed)
+
+  PushConfirm : (senderBrokerKey : Key)
+             -> {auto prf : HasState Sender s}
+             -> Command () Broker Recipient
+                  (New <==> New <==| s)
+                  (/// Confirmed <==> New <==| s)
+
+  SecureConn  : (senderBrokerKey : Key)
+             -> {auto prf : HasState Sender s}
+             -> Command () Recipient Broker
+                  (Confirmed <==> New <==| s)
+                  (/// Secured <==> Secured <==| s)
+
+  SendWelcome : {auto prf : HasState Broker bs}
+             -> Command () Sender Broker
+                  (rs <==> bs <==| Confirmed)
+                  (/// rs <==> bs <==| Secured)
+
+  PushWelcome : {auto prf : HasState Sender s}
+             -> Command () Broker Recipient
+                  (Secured <==> Secured <==| s)
+                  sameState
+
+  SendMsg     : Message
+             -> {auto prf : HasState Broker bs}
+             -> Command () Sender Broker
+                  (rs <==> bs <==| Secured)
+                  (\state, x => case x of
+                                  OK _  => state
+                                  Err _ => state
+                                  Deny  => (rs <==> bs <==| Null))
+
+  PushMsg     : Message
              -> {auto prf : BrokerCS bcState}
-             -> Command (Result ())
+             -> Command () Broker Recipient
-                  Sender Broker
+                  (Secured <==> Secured <==| s)
-                  New    bcState
+                  sameState
-                  (Confirmed /@ New) (const bcState)
-
-  DeliverConfirmation : (connId : String)
-                     -> Command (Result ())
-                          Broker Recipient
-                          New    New
-                          (const New) (Confirmed /@ New)
-
-  SecureConn  : (connId : String)
-             -> (senderKey : Key)
-             -> Command (Result ())
-                  Recipient Broker
-                  Confirmed New
-                  (Secured /@ Confirmed) (Secured /@ New)
-
-  WelcomeMsg  : (connId : String)
-             -> {auto prf : BrokerCS bcState}
-             -> Command (Result ())
-                  Sender    Broker
-                  Confirmed bcState
-                  (const Confirmed) (const bcState)
-
-  SendMsg    : Message
-            -> {auto prf : BrokerCS bcState}
-            -> Command (Result ())
-                 Sender  Broker
-                 Secured bcState
-                 (\x => case x of
-                          OK _    => Secured
-                          Error _ => Secured
-                          Deny    => Null)
-                 (const bcState)