android-apps-mirrors/SimpleX-Chat
0
0
Fork 0
mirror of https://github.com/simplex-chat/simplex-chat.git synced 2025-06-28 20:29:53 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix types

Browse source
This commit is contained in:
Evgeny Poberezkin 2020-05-08 10:03:47 +01:00
parent bcd58117a2
commit 947d7676a2
1 changed files with 7 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

19
specification/Simplex/Messaging.idr
View file

@ -170,7 +170,7 @@ goodSndConn = SCSecured (record
newSndConn) newSndConn)
-- data types for protocol commands -- protocol commands that participants send in relation to specific connection
data Result : (a : Type) -> Type where 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
@ -184,9 +184,9 @@ record BrkCreateConnRes where
Message : Type Message : Type
Message = String Message = String
-- operator to define connection state change based on the result
-- operators to create connection state and state change based on the result
infixl 7 <==>, <==| infixl 7 <==>, <==|
prefix 8 @@@
prefix 6 /// prefix 6 ///
data RBConnState : Type where data RBConnState : Type where
@ -208,11 +208,6 @@ data AllConnState : Type where
Deny => s Deny => s
Err _ => 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) data Command : (ty : Type)
-> (from : Participant) -> (from : Participant)
-> (to : Participant) -> (to : Participant)
@ -227,7 +222,7 @@ data Command : (ty : Type)
(Null <==> Null <==| s) (Null <==> Null <==| s)
(/// New <==> New <==| s) (/// New <==> New <==| s)
Subscribe : Command () Recipient Broker state sameState -- to improve Subscribe : Command () Recipient Broker state (/// state) -- to improve
SendInvite : Invitation SendInvite : Invitation
-> {auto prf : HasState Broker s} -> {auto prf : HasState Broker s}
@ -260,7 +255,7 @@ data Command : (ty : Type)
PushWelcome : {auto prf : HasState Sender s} PushWelcome : {auto prf : HasState Sender s}
-> Command () Broker Recipient -> Command () Broker Recipient
(Secured <==> Secured <==| s) (Secured <==> Secured <==| s)
sameState (/// Secured <==> Secured <==| s)
SendMsg : Message SendMsg : Message
-> {auto prf : HasState Broker bs} -> {auto prf : HasState Broker bs}
@ -272,7 +267,7 @@ data Command : (ty : Type)
Deny => (rs <==> bs <==| Null)) Deny => (rs <==> bs <==| Null))
PushMsg : Message PushMsg : Message
-> {auto prf : BrokerCS bcState} -> {auto prf : HasState Sender s}
-> Command () Broker Recipient -> Command () Broker Recipient
(Secured <==> Secured <==| s) (Secured <==> Secured <==| s)
sameState (/// Secured <==> Secured <==| s)