@@ -4,205 +4,14 @@
44||| Modified (C) The Idris Community, 2015, 2016
55module Network.Socket
66
7+import public Network.Socket.Types
8+import Network.Socket.Raw
9+
710%include C "idris_net.h"
811%include C "sys/types.h"
912%include C "sys/socket.h"
1013%include C "netdb.h"
1114
12−-- ------------------------------------------------------------ [ Type Aliases ]
13−
14−public export
15−ByteLength : Type
16−ByteLength = Int
17−
18−public export
19−ResultCode : Type
20−ResultCode = Int
21−
22−||| Protocol Number.
23−|||
24−||| Generally good enough to just set it to 0.
25−public export
26−ProtocolNumber : Type
27−ProtocolNumber = Int
28−
29−||| SocketError: Error thrown by a socket operation
30−public export
31−SocketError : Type
32−SocketError = Int
33−
34−||| SocketDescriptor: Native C Socket Descriptor
35−public export
36−SocketDescriptor : Type
37−SocketDescriptor = Int
38−
39−public export
40−Port : Type
41−Port = Int
42−
43−-- --------------------------------------------------------------- [ Constants ]
44−
45−||| Backlog used within listen() call -- number of incoming calls
46−public export
47−BACKLOG : Int
48−BACKLOG = 20
49−
50−-- FIXME: This *must* be pulled in from C
51−public export
52−EAGAIN : Int
53−EAGAIN = 11
54−
55−-- -------------------------------------------------------------- [ Interfaces ]
56−
57−export
58−interface ToCode a where
59− toCode : a -> Int
60−
61−-- --------------------------------------------------------- [ Socket Families ]
62−
63−||| Socket Families
64−|||
65−||| The ones that people might actually use. We're not going to need US
66−||| Government proprietary ones.
67−public export
68−data SocketFamily : Type where
69− ||| Unspecified
70− AF_UNSPEC : SocketFamily
71−
72− ||| IP / UDP etc. IPv4
73− AF_INET : SocketFamily
74−
75− ||| IP / UDP etc. IPv6
76− AF_INET6 : SocketFamily
77−
78−export
79−Show SocketFamily where
80− show AF_UNSPEC = "AF_UNSPEC"
81− show AF_INET = "AF_INET"
82− show AF_INET6 = "AF_INET6"
83−
84−export
85−ToCode SocketFamily where
86− toCode AF_UNSPEC = 0
87− toCode AF_INET = 2
88− toCode AF_INET6 = 10
89−
90−getSocketFamily : Int -> Maybe SocketFamily
91−getSocketFamily i =
92− Prelude.List.lookup i [ (0, AF_UNSPEC)
93− , (2, AF_INET)
94− , (10, AF_INET6)
95− ]
96−
97−-- ------------------------------------------------------------ [ Socket Types ]
98−||| Socket Types.
99−public export
100−data SocketType : Type where
101− ||| Not a socket, used in certain operations
102− NotASocket : SocketType
103−
104− ||| TCP
105− Stream : SocketType
106−
107− ||| UDP
108− Datagram : SocketType
109−
110− ||| Raw sockets
111− RawSocket : SocketType
112−
113−export
114−Show SocketType where
115− show NotASocket = "Not a socket"
116− show Stream = "Stream"
117− show Datagram = "Datagram"
118− show RawSocket = "Raw"
119−
120−export
121−ToCode SocketType where
122− toCode NotASocket = 0
123− toCode Stream = 1
124− toCode Datagram = 2
125− toCode RawSocket = 3
126−
127−-- ---------------------------------------------------------------- [ Pointers ]
128−
129−data RecvStructPtr = RSPtr Ptr
130−data RecvfromStructPtr = RFPtr Ptr
131−
132−export
133−data BufPtr = BPtr Ptr
134−
135−export
136−data SockaddrPtr = SAPtr Ptr
137−
138−-- --------------------------------------------------------------- [ Addresses ]
139−
140−||| Network Addresses
141−public export
142−data SocketAddress : Type where
143− IPv4Addr : Int -> Int -> Int -> Int -> SocketAddress
144−
145− ||| Not implemented (yet)
146− IPv6Addr : SocketAddress
147−
148− Hostname : String -> SocketAddress
149−
150− ||| Used when there's a parse error
151− InvalidAddress : SocketAddress
152−
153−export
154−Show SocketAddress where
155− show (IPv4Addr i1 i2 i3 i4) = concat $ Prelude.List.intersperse "." (map show [i1, i2, i3, i4])
156− show IPv6Addr = "NOT IMPLEMENTED YET"
157− show (Hostname host) = host
158− show InvalidAddress = "Invalid"
159−
160−-- --------------------------------------------------------- [ UDP Information ]
161−
162−-- TODO: Expand to non-string payloads
163−export
164−record UDPRecvData where
165− constructor MkUDPRecvData
166− remote_addr : SocketAddress
167− remote_port : Port
168− recv_data : String
169− data_len : Int
170−
171−export
172−record UDPAddrInfo where
173− constructor MkUDPAddrInfo
174− remote_addr : SocketAddress
175− remote_port : Port
176−
177−-- ---------------------------------------------------------- [ Socket Utilies ]
178−
179−||| Frees a given pointer
180−export
181−sock_free : BufPtr -> IO ()
182−sock_free (BPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr
183−
184−export
185−sockaddr_free : SockaddrPtr -> IO ()
186−sockaddr_free (SAPtr ptr) = foreign FFI_C "idrnet_free" (Ptr -> IO ()) ptr
187−
188−||| Allocates an amount of memory given by the ByteLength parameter.
189−|||
190−||| Used to allocate a mutable pointer to be given to the Recv functions.
191−export
192−sock_alloc : ByteLength -> IO BufPtr
193−sock_alloc bl = map BPtr $ foreign FFI_C "idrnet_malloc" (Int -> IO Ptr) bl
194−
195−-- ----------------------------------------------------------------- [ Sockets ]
196−||| The metadata about a socket
197−export
198−record Socket where
199− constructor MkSocket
200− descriptor : SocketDescriptor
201− family : SocketFamily
202− socketType : SocketType
203− protocolNumber : ProtocolNumber
204−
205−
20615-- ----------------------------------------------------- [ Network Socket API. ]
20716
20817||| Creates a UNIX socket with the given family, socket type and protocol