Idris2Doc : Control.Linear.Network

Control.Linear.Network

data Action : SocketState -> Type
  Define the domain of SocketState transitions.
  Label every such transition.

  Totality: total
  Constructors:
  
Bind : Action Ready
  
Listen : Action Bound
  
Accept : Action Listening
  
Send : Action Open
  
Receive : Action Open
  
Close : Action st
Next : Action st -> Bool -> Type
  For every label of a SocketState transition
  and a success value of the transition,
  define its result.

  
data Socket : SocketState -> Type
  Totality: total
  Constructor: 
MkSocket : Socket -> Socket st
data SocketState : Type
  Totality: total
  Constructors:
  
Ready : SocketState
  
Bound : SocketState
  
Listening : SocketState
  
Open : SocketState
  
Closed : SocketState
accept : LinearIO io => (1 _ : Socket Listening) -> L1 io (Res (Maybe SocketError) (\res => Next Accept (isNothing res)))
  
bind : LinearIO io => (1 _ : Socket Ready) -> Maybe SocketAddress -> Port -> L1 io (Res (Maybe SocketError) (\res => Next Bind (isNothing res)))
  
close : LinearIO io => (1 _ : Socket st) -> L1 io (Socket Closed)
  
connect : {auto conArg : LinearIO io} -> (sock : Socket) -> (addr : SocketAddress) -> (port : Port) -> L1 io (Res (Maybe SocketError) (\{lcase:0} => case lcase of {Nothing => Socket Ready; Just _ => Socket Closed}))
  
done : LinearIO io => (1 _ : Socket Closed) -> L io ()
  
listen : LinearIO io => (1 _ : Socket Bound) -> L1 io (Res (Maybe SocketError) (\res => Next Listen (isNothing res)))
  
newSocket : LinearIO io => SocketFamily -> SocketType -> ProtocolNumber -> ((1 _ : Socket Ready) -> L io ()) -> (SocketError -> L io ()) -> L io ()
  
recv : LinearIO io => (1 _ : Socket Open) -> ByteLength -> L1 io (Res (Either SocketError (String, ResultCode)) (\res => Next Receive (isRight res)))
  
recvAll : LinearIO io => (1 _ : Socket Open) -> L1 io (Res (Either SocketError String) (\res => Next Receive (isRight res)))
  
send : LinearIO io => (1 _ : Socket Open) -> String -> L1 io (Res (Maybe SocketError) (\res => Next Send (isNothing res)))