Idris2Doc : Network.Socket.Data

Network.Socket.Data

Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.
Types used by Network.Socket.Raw and Network.Socket.

Original (C) SimonJF, MIT Licensed, 2014
Modified (C) The Idris Community, 2015, 2016, 2019

Definitions

ByteLength : Type
Visibility: public export
ResultCode : Type
Visibility: public export
ProtocolNumber : Type
  Protocol Number.

Generally good enough to just set it to 0.

Visibility: public export
SocketError : Type
  SocketError: Error thrown by a socket operation

Visibility: public export
SocketDescriptor : Type
  SocketDescriptor: Native C Socket Descriptor

Visibility: public export
Port : Type
Visibility: public export
BACKLOG : Int
  Backlog used within listen() call -- number of incoming calls

Visibility: export
EAGAIN : Int
Visibility: export
getErrno : HasIO io => io SocketError
Visibility: export
nullPtr : HasIO io => AnyPtr -> io Bool
Visibility: export
interface ToCode : Type -> Type
Parameters: a
Methods:
toCode : a -> Int

Implementations:
ToCode SocketFamily
ToCode SocketType
toCode : ToCode a => a -> Int
Visibility: public export
data SocketFamily : Type
  Socket Families

The ones that people might actually use. We're not going to need US
Government proprietary ones.

Totality: total
Visibility: public export
Constructors:
AF_UNSPEC : SocketFamily
  Unspecified
AF_UNIX : SocketFamily
  Unix type sockets
AF_INET : SocketFamily
  IP / UDP etc. IPv4
AF_INET6 : SocketFamily
   IP / UDP etc. IPv6

Hints:
Show SocketFamily
ToCode SocketFamily
getSocketFamily : Int -> Maybe SocketFamily
Visibility: export
data SocketType : Type
  Socket Types.

Totality: total
Visibility: public export
Constructors:
NotASocket : SocketType
  Not a socket, used in certain operations
Stream : SocketType
  TCP
Datagram : SocketType
  UDP
RawSocket : SocketType
  Raw sockets

Hints:
Show SocketType
ToCode SocketType
data SocketAddress : Type
  Network Addresses

Totality: total
Visibility: public export
Constructors:
IPv4Addr : Int -> Int -> Int -> Int -> SocketAddress
IPv6Addr : SocketAddress
  Not implemented (yet)
Hostname : String -> SocketAddress
InvalidAddress : SocketAddress
  Used when there's a parse error

Hint: 
Show SocketAddress
parseIPv4 : String -> SocketAddress
  Parses a textual representation of an IPv4 address into a SocketAddress

Visibility: export
record UDPRecvData : Type
Totality: total
Visibility: public export
Constructor: 
MkUDPRecvData : SocketAddress -> Port -> String -> Int -> UDPRecvData

Projections:
.data_len : UDPRecvData -> Int
.recv_data : UDPRecvData -> String
.remote_addr : UDPRecvData -> SocketAddress
.remote_port : UDPRecvData -> Port
.remote_addr : UDPRecvData -> SocketAddress
Visibility: public export
remote_addr : UDPRecvData -> SocketAddress
Visibility: public export
.remote_port : UDPRecvData -> Port
Visibility: public export
remote_port : UDPRecvData -> Port
Visibility: public export
.recv_data : UDPRecvData -> String
Visibility: public export
recv_data : UDPRecvData -> String
Visibility: public export
.data_len : UDPRecvData -> Int
Visibility: public export
data_len : UDPRecvData -> Int
Visibility: public export
record UDPAddrInfo : Type
Totality: total
Visibility: public export
Constructor: 
MkUDPAddrInfo : SocketAddress -> Port -> UDPAddrInfo

Projections:
.remote_addr : UDPAddrInfo -> SocketAddress
.remote_port : UDPAddrInfo -> Port
.remote_addr : UDPAddrInfo -> SocketAddress
Visibility: public export
remote_addr : UDPAddrInfo -> SocketAddress
Visibility: public export
.remote_port : UDPAddrInfo -> Port
Visibility: public export
remote_port : UDPAddrInfo -> Port
Visibility: public export
record Socket : Type
  The metadata about a socket

Totality: total
Visibility: public export
Constructor: 
MkSocket : SocketDescriptor -> SocketFamily -> SocketType -> ProtocolNumber -> Socket

Projections:
.descriptor : Socket -> SocketDescriptor
.family : Socket -> SocketFamily
.protocolNumber : Socket -> ProtocolNumber
.socketType : Socket -> SocketType
.descriptor : Socket -> SocketDescriptor
Visibility: public export
descriptor : Socket -> SocketDescriptor
Visibility: public export
.family : Socket -> SocketFamily
Visibility: public export
family : Socket -> SocketFamily
Visibility: public export
.socketType : Socket -> SocketType
Visibility: public export
socketType : Socket -> SocketType
Visibility: public export
.protocolNumber : Socket -> ProtocolNumber
Visibility: public export
protocolNumber : Socket -> ProtocolNumber
Visibility: public export