Idris2Doc : Control.Linear.Network

Control.Linear.Network

Action : SocketState -> Type
Define the domain of SocketState transitions.
Label every such transition.
Totality: total
Constructors:
Bind : ActionReady
Listen : ActionBound
Accept : ActionListening
Send : ActionOpen
Receive : ActionOpen
Close : Actionst
Next : Actionst -> Bool -> Type
For every label of a SocketState transition
and a success value of the transition,
define its result.
Socket : SocketState -> Type
Totality: total
Constructor: 
MkSocket : Socket -> Socketst
SocketState : Type
Totality: total
Constructors:
Ready : SocketState
Bound : SocketState
Listening : SocketState
Open : SocketState
Closed : SocketState
accept : LinearIOio => (1 _ : SocketListening) -> L1io (Res (MaybeSocketError) (\res => NextAccept (isNothingres)))
bind : LinearIOio => (1 _ : SocketReady) -> MaybeSocketAddress -> Port -> L1io (Res (MaybeSocketError) (\res => NextBind (isNothingres)))
close : LinearIOio => (1 _ : Socketst) -> L1io (SocketClosed)
connect : {auto {conArg:5945} : LinearIOio} -> (sock : Socket) -> (addr : SocketAddress) -> (port : Port) -> L1io (Res (MaybeSocketError) (\{lcase:0} => case{lcase:0}of {Nothing => SocketReady; Just{_:5974} => SocketClosed}))
done : LinearIOio => (1 _ : SocketClosed) -> LioUnit
listen : LinearIOio => (1 _ : SocketBound) -> L1io (Res (MaybeSocketError) (\res => NextListen (isNothingres)))
newSocket : LinearIOio => SocketFamily -> SocketType -> ProtocolNumber -> ((1 _ : SocketReady) -> LioUnit) -> (SocketError -> LioUnit) -> LioUnit
recv : LinearIOio => (1 _ : SocketOpen) -> ByteLength -> L1io (Res (EitherSocketError (String, ResultCode)) (\res => NextReceive (isRightres)))
recvAll : LinearIOio => (1 _ : SocketOpen) -> L1io (Res (EitherSocketError String) (\res => NextReceive (isRightres)))
send : LinearIOio => (1 _ : SocketOpen) -> String -> L1io (Res (MaybeSocketError) (\res => NextSend (isNothingres)))