From bbb763655e49f458a4a15e782ac403f7ba894dde Mon Sep 17 00:00:00 2001 From: Evgeny Poberezkin <2769109+epoberezkin@users.noreply.github.com> Date: Fri, 8 May 2020 17:36:04 +0100 Subject: [PATCH] participants list (to be removed) --- specification/Simplex/Messaging/Protocol.idr | 92 ++++++++++++++----- specification/Simplex/Messaging/Scenarios.idr | 3 +- 2 files changed, 70 insertions(+), 25 deletions(-) diff --git a/specification/Simplex/Messaging/Protocol.idr b/specification/Simplex/Messaging/Protocol.idr index 4d07d32fd5..d58541e297 100644 --- a/specification/Simplex/Messaging/Protocol.idr +++ b/specification/Simplex/Messaging/Protocol.idr @@ -3,6 +3,11 @@ module Simplex.Messaging.Protocol %access public export data Participant = Recipient | Sender | Broker +Eq Participant where + (==) Recipient Recipient = True + (==) Sender Sender = True + (==) Broker Broker = True + (==) _ _ = False data Client : Participant -> Type where CRecipient : Client Recipient @@ -192,8 +197,7 @@ Message = String -- operator to define connection state change based on the result infixl 7 <==>, <==| -prefix 8 @@@ -prefix 6 ///, >>> +prefix 6 />>, >>> data RBConnState : Type where (<==>) : (recipient : ConnectionState) @@ -207,9 +211,9 @@ data AllConnState : Type where -> {auto prf : HasState Sender sender} -> AllConnState -(///) : AllConnState +(/>>) : AllConnState -> (AllConnState -> Result a -> AllConnState) -(///) s' = \s, x => case x of +(/>>) s' = \s, x => case x of OK _ => s' Deny => s Err _ => s @@ -218,10 +222,41 @@ data AllConnState : Type where -> (AllConnState -> Result a -> AllConnState) (>>>) s = \_, _ => s +infixl 8 &>, &>> +infixr 7 /// + +data Participants : Type where + (&>) : Participant -> Participant -> Participants + (&>>) : Participants -> Participant -> Participants + (///) : Participants -> Participants -> Participants + +firstParticipant : Participants -> Participant +firstParticipant (p &> _) = p +firstParticipant (ps &>> _) = firstParticipant ps +firstParticipant (ps /// _) = firstParticipant ps + +lastParticipant : Participants -> Participant +lastParticipant (_ &> p) = p +lastParticipant (_ &>> p) = p +lastParticipant (_ /// ps) = lastParticipant ps + +infixl 6 &++ +total (&++) : Participants -> Participants -> Participants +(&++) (x &> y) (z &> w) = if y == z then x &> y &>> w + else x &> y /// z &> w +(&++) (x &> y) (zs &>> w) = (x &> y &++ zs) &>> w +(&++) (x &> y) (zs /// ws) = (x &> y &++ zs) /// ws + +(&++) (xs &>> y) (z &> w) = if y == z then xs &>> y &>> w + else xs &>> y /// z &> w +(&++) (xs &>> y) (zs &>> w) = (xs &>> y &++ zs) &>> w +(&++) (xs &>> y) (zs /// ws) = (xs &>> y &++ zs) /// ws + +(&++) (xs /// ys) zs = xs /// (ys &++ zs) + data Command : (ty : Type) - -> (from : Participant) - -> (to : Participant) + -> Participants -> (state : AllConnState) -> ((state : AllConnState) -> Result ty -> AllConnState) -> Type where @@ -229,69 +264,78 @@ data Command : (ty : Type) CreateConn : (recipientBrokerKey : Key) -> {auto prf : HasState Sender s} -> Command BrkCreateConnRes - Recipient Broker + (Recipient &> Broker) (Null <==> (Null, 0) <==| s) (>>> New <==> (New, 0) <==| s) - Subscribe : Command () Recipient Broker state (>>> state) -- to improve + Subscribe : Command () (Recipient &> Broker) state (>>> state) -- to improve SendInvite : Invitation -> {auto prf : HasState Broker s} - -> Command () Recipient Sender + -> Command () + (Recipient &> Sender) (New <==> (s, n) <==| Null) (>>> Pending <==> (s, n) <==| New) ConfirmConn : (senderBrokerKey : Key) - -> Command () Sender Broker + -> Command () + (Sender &> Broker) (s <==> (New, n) <==| New) (>>> s <==> (New, 1 + n) <==| Confirmed) PushConfirm : {auto prf : HasState Sender s} - -> Command () Broker Recipient + -> Command () + (Broker &> Recipient) (Pending <==> (New, 1 + n) <==| s) (>>> Confirmed <==> (New, n) <==| s) SecureConn : (senderBrokerKey : Key) -> {auto prf : HasState Sender s} - -> Command () Recipient Broker + -> Command () + (Recipient &> Broker) (Confirmed <==> (New, n) <==| s) (>>> Secured <==> (Secured, n) <==| s) SendWelcome : {auto prf : HasState Broker bs} - -> Command () Sender Broker + -> Command () + (Sender &> Broker) (rs <==> (Secured, n) <==| Confirmed) (>>> rs <==> (Secured, 1 + n) <==| Secured) PushWelcome : {auto prf : HasState Sender s} - -> Command () Broker Recipient + -> Command () + (Broker &> Recipient) (Secured <==> (Secured, 1 + n) <==| s) (>>> Secured <==> (Secured, n) <==| s) SendMsg : Message - -> Command () Sender Broker + -> Command () + (Sender &> Broker) (rs <==> (Secured, n) <==| Secured) (>>> rs <==> (Secured, 1 + n) <==| Secured) PushMsg : {auto prf : HasState Sender s} - -> Command () Broker Recipient + -> Command () + (Broker &> Recipient) (Secured <==> (Secured, n) <==| s) (>>> Secured <==> (Secured, n) <==| s) DeleteMsg : {auto prf : HasState Sender s} - -> Command () Recipient Broker + -> Command () + (Recipient &> Broker) (Secured <==> (Secured, 1 + n) <==| s) (>>> Secured <==> (Secured, n) <==| s) - Pure : (res : Result a) -> Command a from to state state_fn - (>>=) : Command a from1 to1 state1 state2_fn - -> ((res : Result a) -> Command b from2 to2 (state2_fn state1 res) state3_fn) - -> Command b from1 to2 state1 state3_fn + Pure : (res : Result a) -> Command a ps state state_fn + (>>=) : Command a ps1 state1 state2_fn + -> ((res : Result a) -> Command b ps2 (state2_fn state1 res) state3_fn) + -> Command b (firstParticipant ps1 &> lastParticipant ps2) state1 state3_fn infix 5 &: (&:) : (p : Participant) - -> Command a from1 to1 state1 state2_fn - -> {auto prf : p = from1} - -> Command a from1 to1 state1 state2_fn + -> Command a ps state1 state2_fn + -> {auto prf : p = firstParticipant ps} + -> Command a ps state1 state2_fn (&:) _ c = c diff --git a/specification/Simplex/Messaging/Scenarios.idr b/specification/Simplex/Messaging/Scenarios.idr index 92a07ac3d2..82ebe9da1e 100644 --- a/specification/Simplex/Messaging/Scenarios.idr +++ b/specification/Simplex/Messaging/Scenarios.idr @@ -2,7 +2,8 @@ module Simplex.Messaging.Scenarios import Protocol -establishConnection : Command () Recipient Broker +establishConnection : Command () + (Recipient &> Broker) (Null <==> (Null, 0) <==| Null) (>>> Secured <==> (Secured, 0) <==| Secured) establishConnection = do