Idris2Doc : Control.Linear.Network

Control.Linear.Network

dataAction : 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.

dataSocket : SocketState -> Type
Totality: total
Constructor: 
MkSocket : Socket -> Socketst
dataSocketState : 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 : {autoconArg : LinearIOio} -> (sock : Socket) -> (addr : SocketAddress) -> (port : Port) -> L1io (Res (MaybeSocketError) (\{lcase:0} => caselcaseof {Nothing => SocketReady; Just_ => SocketClosed}))
done : LinearIOio => (1 _ : SocketClosed) -> Lio ()
listen : LinearIOio => (1 _ : SocketBound) -> L1io (Res (MaybeSocketError) (\res => NextListen (isNothingres)))
newSocket : LinearIOio => SocketFamily -> SocketType -> ProtocolNumber -> ((1 _ : SocketReady) -> Lio ()) -> (SocketError -> Lio ()) -> Lio ()
recv : LinearIOio => (1 _ : SocketOpen) -> ByteLength -> L1io (Res (EitherSocketError (String, ResultCode)) (\res => NextReceive (isRightres)))
recvAll : LinearIOio => (1 _ : SocketOpen) -> L1io (Res (EitherSocketErrorString) (\res => NextReceive (isRightres)))
send : LinearIOio => (1 _ : SocketOpen) -> String -> L1io (Res (MaybeSocketError) (\res => NextSend (isNothingres)))