Control.Linear.Network

Reexports

Definitions

data SocketState : Type

Totality: total
Visibility: public export
Constructors:

Ready : SocketState

Bound : SocketState

Listening : SocketState

Open : SocketState

Closed : SocketState

data Action : SocketState -> Type

  Define the domain of SocketState transitions.
  Label every such transition.

Totality: total
Visibility: public export
Constructors:

Bind : Action Ready

Listen : Action Bound

Accept : Action Listening

Connect : Action Ready

Send : Action Open

Receive : Action Open

Close : Action st

data Socket : SocketState -> Type

Totality: total
Visibility: export
Constructor: 

MkSocket : Socket -> Socket st

Next : Action st -> Bool -> Type

  For every label of a SocketState transition
  and a success value of the transition,
  define its result.

Visibility: public export

newSocket : LinearIO io => SocketFamily -> SocketType -> ProtocolNumber -> ((1 _ : Socket Ready) -> L io ()) -> (SocketError -> L io ()) -> L io ()

Visibility: export

close : LinearIO io => (1 _ : Socket st) -> L1 io (Socket Closed)

Visibility: export

done : LinearIO io => (1 _ : Socket Closed) -> L io ()

Visibility: export

bind : LinearIO io => (1 _ : Socket Ready) -> Maybe SocketAddress -> Port -> L1 io (Res (Maybe SocketError) (\res => Next Bind (isNothing res)))

Visibility: export

connect : LinearIO io => (1 _ : Socket Ready) -> SocketAddress -> Port -> L1 io (Res (Maybe SocketError) (\res => Next Connect (isNothing res)))

Visibility: export

listen : LinearIO io => (1 _ : Socket Bound) -> L1 io (Res (Maybe SocketError) (\res => Next Listen (isNothing res)))

Visibility: export

accept : LinearIO io => (1 _ : Socket Listening) -> L1 io (Res (Maybe SocketError) (\res => Next Accept (isNothing res)))

Visibility: export

send : LinearIO io => (1 _ : Socket Open) -> String -> L1 io (Res (Maybe SocketError) (\res => Next Send (isNothing res)))

Visibility: export

recv : LinearIO io => (1 _ : Socket Open) -> ByteLength -> L1 io (Res (Either SocketError (String, ResultCode)) (\res => Next Receive (isRight res)))

Visibility: export

recvAll : LinearIO io => (1 _ : Socket Open) -> L1 io (Res (Either SocketError String) (\res => Next Receive (isRight res)))

Visibility: export

sendBytes : LinearIO io => (1 _ : Socket Open) -> List Bits8 -> L1 io (Res (Maybe SocketError) (\res => Next Send (isNothing res)))

Visibility: export

recvBytes : LinearIO io => (1 _ : Socket Open) -> ByteLength -> L1 io (Res (Either SocketError (List Bits8)) (\res => Next Receive (isRight res)))

Visibility: export

recvAllBytes : LinearIO io => (1 _ : Socket Open) -> L1 io (Res (Either SocketError (List Bits8)) (\res => Next Receive (isRight res)))

Visibility: export