0 | ||| Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.
  1 | ||| Types used by Network.Socket.Raw and Network.Socket.
  2 | |||
  3 | ||| Original (C) SimonJF, MIT Licensed, 2014
  4 | ||| Modified (C) The Idris Community, 2015, 2016, 2019
  5 | module Network.Socket.Data
  6 |
  7 | import Data.List
  8 | import Data.List1
  9 | import Data.String
 10 |
 11 | -- ------------------------------------------------------------ [ Type Aliases ]
 12 |
 13 | public export
 14 | ByteLength : Type
 15 | ByteLength = Int
 16 |
 17 | public export
 18 | ResultCode : Type
 19 | ResultCode = Int
 20 |
 21 | ||| Protocol Number.
 22 | |||
 23 | ||| Generally good enough to just set it to 0.
 24 | public export
 25 | ProtocolNumber : Type
 26 | ProtocolNumber = Int
 27 |
 28 | ||| SocketError: Error thrown by a socket operation
 29 | public export
 30 | SocketError : Type
 31 | SocketError = Int
 32 |
 33 | ||| SocketDescriptor: Native C Socket Descriptor
 34 | public export
 35 | SocketDescriptor : Type
 36 | SocketDescriptor = Int
 37 |
 38 | public export
 39 | Port : Type
 40 | Port = Int
 41 |
 42 | -- --------------------------------------------------------------- [ Constants ]
 43 |
 44 | ||| Backlog used within listen() call -- number of incoming calls
 45 | export
 46 | BACKLOG : Int
 47 | BACKLOG = 20
 48 |
 49 | -- Repeat to avoid a dependency cycle
 50 | %foreign "C:idrnet_geteagain, libidris2_support, idris_net.h"
 51 | prim__idrnet_geteagain : PrimIO Int
 52 |
 53 | export
 54 | EAGAIN : Int
 55 | EAGAIN =
 56 |   -- I'm sorry
 57 |   -- maybe
 58 |   unsafePerformIO $ primIO $ prim__idrnet_geteagain
 59 |
 60 | -- ---------------------------------------------------------------- [ Error Code ]
 61 |
 62 | -- repeat without export to avoid dependency cycles
 63 | %foreign "C:idrnet_errno, libidris2_support, idris_net.h"
 64 | prim__idrnet_errno : PrimIO Int
 65 |
 66 | %foreign "C:isNull, libidris2_support, idris_support.h"
 67 | prim__idrnet_isNull : (ptr : AnyPtr) -> PrimIO Int
 68 |
 69 |
 70 | export
 71 | getErrno : HasIO io => io SocketError
 72 | getErrno = primIO $ prim__idrnet_errno
 73 |
 74 | export
 75 | nullPtr : HasIO io => AnyPtr -> io Bool
 76 | nullPtr p = do 0 <- primIO  $ prim__idrnet_isNull p
 77 |                | _ => pure True
 78 |                pure False
 79 |
 80 | -- -------------------------------------------------------------- [ Interfaces ]
 81 |
 82 | public export
 83 | interface ToCode a where
 84 |   toCode : a -> Int
 85 |
 86 | -- --------------------------------------------------------- [ Socket Families ]
 87 |
 88 | ||| Socket Families
 89 | |||
 90 | ||| The ones that people might actually use. We're not going to need US
 91 | ||| Government proprietary ones.
 92 | public export
 93 | data SocketFamily : Type where
 94 |   ||| Unspecified
 95 |   AF_UNSPEC : SocketFamily
 96 |
 97 |   ||| Unix type sockets
 98 |   AF_UNIX : SocketFamily
 99 |
100 |   ||| IP / UDP etc. IPv4
101 |   AF_INET : SocketFamily
102 |
103 |   |||  IP / UDP etc. IPv6
104 |   AF_INET6 : SocketFamily
105 |
106 | Show SocketFamily where
107 |   show AF_UNSPEC = "AF_UNSPEC"
108 |   show AF_UNIX   = "AF_UNIX"
109 |   show AF_INET   = "AF_INET"
110 |   show AF_INET6  = "AF_INET6"
111 |
112 | -- This is a bit of a hack to get the OS-dependent magic constants out of C and
113 | -- into Idris without having to faff around on the preprocessor on the Idris
114 | -- side.
115 | %foreign "C:idrnet_af_unspec, libidris2_support, idris_net.h"
116 | prim__idrnet_af_unspec : PrimIO Int
117 |
118 | %foreign "C:idrnet_af_unix, libidris2_support, idris_net.h"
119 | prim__idrnet_af_unix : PrimIO Int
120 |
121 | %foreign "C:idrnet_af_inet, libidris2_support, idris_net.h"
122 | prim__idrnet_af_inet : PrimIO Int
123 |
124 | %foreign "C:idrnet_af_inet6, libidris2_support, idris_net.h"
125 | prim__idrnet_af_inet6 : PrimIO Int
126 |
127 | export
128 | ToCode SocketFamily where
129 |   toCode AF_UNSPEC = unsafePerformIO $ primIO $ prim__idrnet_af_unspec
130 |   toCode AF_UNIX   = unsafePerformIO $ primIO $ prim__idrnet_af_unix
131 |   toCode AF_INET   = unsafePerformIO $ primIO $ prim__idrnet_af_inet
132 |   toCode AF_INET6  = unsafePerformIO $ primIO $ prim__idrnet_af_inet6
133 |
134 | export
135 | getSocketFamily : Int -> Maybe SocketFamily
136 | getSocketFamily i =
137 |     lookup i [ (toCode AF_UNSPEC, AF_UNSPEC)
138 |              , (toCode AF_UNIX, AF_UNIX)
139 |              , (toCode AF_INET, AF_INET)
140 |              , (toCode AF_INET6, AF_INET6)
141 |              ]
142 |
143 | -- ------------------------------------------------------------ [ Socket Types ]
144 |
145 | ||| Socket Types.
146 | public export
147 | data SocketType : Type where
148 |   ||| Not a socket, used in certain operations
149 |   NotASocket : SocketType
150 |
151 |   ||| TCP
152 |   Stream : SocketType
153 |
154 |   ||| UDP
155 |   Datagram : SocketType
156 |
157 |   ||| Raw sockets
158 |   RawSocket : SocketType
159 |
160 | export
161 | Show SocketType where
162 |   show NotASocket = "Not a socket"
163 |   show Stream     = "Stream"
164 |   show Datagram   = "Datagram"
165 |   show RawSocket  = "Raw"
166 |
167 | export
168 | ToCode SocketType where
169 |   toCode NotASocket = 0
170 |   toCode Stream     = 1
171 |   toCode Datagram   = 2
172 |   toCode RawSocket  = 3
173 |
174 | -- --------------------------------------------------------------- [ Addresses ]
175 |
176 | ||| Network Addresses
177 | public export
178 | data SocketAddress : Type where
179 |   IPv4Addr : Int -> Int -> Int -> Int -> SocketAddress
180 |
181 |   ||| Not implemented (yet)
182 |   IPv6Addr : SocketAddress
183 |
184 |   Hostname : String -> SocketAddress
185 |
186 |   ||| Used when there's a parse error
187 |   InvalidAddress : SocketAddress
188 |
189 | export
190 | Show SocketAddress where
191 |   show (IPv4Addr i1 i2 i3 i4) = concat $ intersperse "." (map show [i1, i2, i3, i4])
192 |   show IPv6Addr               = "NOT IMPLEMENTED YET"
193 |   show (Hostname host)        = host
194 |   show InvalidAddress         = "Invalid"
195 |
196 | ||| Parses a textual representation of an IPv4 address into a SocketAddress
197 | export
198 | parseIPv4 : String -> SocketAddress
199 | parseIPv4 str =
200 |     case splitted of
201 |       (i1 ::: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
202 |       _ => InvalidAddress
203 |   where
204 |     toInt' : String -> Integer
205 |     toInt' = cast
206 |
207 |     toInt : String -> Int
208 |     toInt s = fromInteger $ toInt' s
209 |
210 |     splitted : List1 Int
211 |     splitted = map toInt (split (\c => c == '.') str)
212 |
213 | -- --------------------------------------------------------- [ UDP Information ]
214 |
215 | -- TODO: Expand to non-string payloads
216 | public export
217 | record UDPRecvData where
218 |   constructor MkUDPRecvData
219 |   remote_addr : SocketAddress
220 |   remote_port : Port
221 |   recv_data   : String
222 |   data_len    : Int
223 |
224 | public export
225 | record UDPAddrInfo where
226 |   constructor MkUDPAddrInfo
227 |   remote_addr : SocketAddress
228 |   remote_port : Port
229 |
230 | -- ----------------------------------------------------------------- [ Sockets ]
231 | ||| The metadata about a socket
232 | public export
233 | record Socket where
234 |   constructor MkSocket
235 |   descriptor     : SocketDescriptor
236 |   family         : SocketFamily
237 |   socketType     : SocketType
238 |   protocolNumber : ProtocolNumber
239 |