||| 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, 2019module Network.Socket.Data import Data.Listimport Data.Strings -- ------------------------------------------------------------ [ Type Aliases ] %cg chez "libidris_net" public exportByteLength : TypeByteLength = Int public exportResultCode : TypeResultCode = Int ||| Protocol Number.|||||| Generally good enough to just set it to 0.public exportProtocolNumber : TypeProtocolNumber = Int ||| SocketError: Error thrown by a socket operationpublic exportSocketError : TypeSocketError = Int ||| SocketDescriptor: Native C Socket Descriptorpublic exportSocketDescriptor : TypeSocketDescriptor = Int public exportPort : TypePort = Int -- --------------------------------------------------------------- [ Constants ] ||| Backlog used within listen() call -- number of incoming callsexportBACKLOG : IntBACKLOG = 20 exportEAGAIN : IntEAGAIN =  -- I'm sorry  -- maybe  unsafePerformIO $ cCall Int "idrnet_geteagain" [] -- ---------------------------------------------------------------- [ Error Code ] exportgetErrno : IO SocketErrorgetErrno = cCall Int "idrnet_errno" [] exportnullPtr : AnyPtr -> IO BoolnullPtr p = cCall Bool "isNull" [p] -- -------------------------------------------------------------- [ Interfaces ] public exportinterface ToCode a where  toCode : a -> Int -- --------------------------------------------------------- [ Socket Families ] ||| Socket Families|||||| The ones that people might actually use. We're not going to need US||| Government proprietary ones.public exportdata SocketFamily : Type where  ||| Unspecified  AF_UNSPEC : SocketFamily   ||| Unix type sockets  AF_UNIX : SocketFamily   ||| IP / UDP etc. IPv4  AF_INET : SocketFamily   |||  IP / UDP etc. IPv6  AF_INET6 : SocketFamily Show SocketFamily where  show AF_UNSPEC = "AF_UNSPEC"  show AF_UNIX   = "AF_UNIX"  show AF_INET   = "AF_INET"  show AF_INET6  = "AF_INET6" exportToCode SocketFamily where  -- Don't know how to read a constant value from C code in idris2...  -- gotta to hardcode those for now  toCode AF_UNSPEC = 0 -- unsafePerformIO (cMacro "#AF_UNSPEC" Int)  toCode AF_UNIX   = 1  toCode AF_INET   = 2  toCode AF_INET6  = 10 exportgetSocketFamily : Int -> Maybe SocketFamilygetSocketFamily i =    lookup i [ (toCode AF_UNSPEC, AF_UNSPEC)             , (toCode AF_UNIX, AF_UNIX)             , (toCode AF_INET, AF_INET)             , (toCode AF_INET6, AF_INET6)             ] -- ------------------------------------------------------------ [ Socket Types ] ||| Socket Types.public exportdata SocketType : Type where  ||| Not a socket, used in certain operations  NotASocket : SocketType   ||| TCP  Stream : SocketType   ||| UDP  Datagram : SocketType   ||| Raw sockets  RawSocket : SocketType exportShow SocketType where  show NotASocket = "Not a socket"  show Stream     = "Stream"  show Datagram   = "Datagram"  show RawSocket  = "Raw" exportToCode SocketType where  toCode NotASocket = 0  toCode Stream     = 1  toCode Datagram   = 2  toCode RawSocket  = 3 -- --------------------------------------------------------------- [ Addresses ] ||| Network Addressespublic exportdata SocketAddress : Type where  IPv4Addr : Int -> Int -> Int -> Int -> SocketAddress   ||| Not implemented (yet)  IPv6Addr : SocketAddress   Hostname : String -> SocketAddress   ||| Used when there's a parse error  InvalidAddress : SocketAddress exportShow SocketAddress where  show (IPv4Addr i1 i2 i3 i4) = concat $ intersperse "." (map show [i1, i2, i3, i4])  show IPv6Addr               = "NOT IMPLEMENTED YET"  show (Hostname host)        = host  show InvalidAddress         = "Invalid" ||| Parses a textual representation of an IPv4 address into a SocketAddressexportparseIPv4 : String -> SocketAddressparseIPv4 str =    case splitted of      (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4      otherwise                   => InvalidAddress  where    toInt' : String -> Integer    toInt' = cast     toInt : String -> Int    toInt s = fromInteger $ toInt' s     splitted : List Int    splitted = map toInt (split (\c => c == '.') str) -- --------------------------------------------------------- [ UDP Information ] -- TODO: Expand to non-string payloadspublic exportrecord UDPRecvData where  constructor MkUDPRecvData  remote_addr : SocketAddress  remote_port : Port  recv_data   : String  data_len    : Int public exportrecord UDPAddrInfo where  constructor MkUDPAddrInfo  remote_addr : SocketAddress  remote_port : Port -- ----------------------------------------------------------------- [ Sockets ]||| The metadata about a socketpublic exportrecord Socket where  constructor MkSocket  descriptor     : SocketDescriptor  family         : SocketFamily  socketType     : SocketType  protocolNumber : ProtocolNumber