0 | module System.Posix.Socket.Struct
  1 |
  2 | import Data.Bits
  3 | import Data.C.Ptr
  4 | import Data.Vect
  5 | import Derive.Prelude
  6 | import System.Posix.Errno
  7 | import System.Posix.File.FileDesc
  8 | import System.Posix.Socket.Types
  9 |
 10 | %default total
 11 | %language ElabReflection
 12 |
 13 | --------------------------------------------------------------------------------
 14 | -- Socket
 15 | --------------------------------------------------------------------------------
 16 |
 17 | ||| A file descriptor representing a socket.
 18 | export
 19 | record Socket (d : Domain) where
 20 |   constructor S
 21 |   fd : Bits32
 22 |
 23 | export %inline
 24 | Cast (Socket d) Fd where cast = MkFd . fd
 25 |
 26 | export %inline
 27 | Cast CInt (Socket d) where cast = S . cast
 28 |
 29 | --------------------------------------------------------------------------------
 30 | -- SockaddrUn
 31 | --------------------------------------------------------------------------------
 32 |
 33 | %foreign "C:li_sockaddr_un, posix-idris"
 34 | prim__sockaddr_un: String -> PrimIO AnyPtr
 35 |
 36 | %foreign "C:sockaddr_un_path, posix-idris"
 37 | prim__sockaddr_un_path: AnyPtr -> PrimIO String
 38 |
 39 | export
 40 | record SSockaddrUn (s : Type) where
 41 |   constructor SUN
 42 |   ptr : AnyPtr
 43 |
 44 | public export
 45 | 0 SockaddrUn : Type
 46 | SockaddrUn = SSockaddrUn World
 47 |
 48 | export %inline
 49 | Struct SSockaddrUn where
 50 |   swrap   = SUN
 51 |   sunwrap = ptr
 52 |
 53 | export
 54 | SizeOf (SSockaddrUn s) where
 55 |   sizeof_ = sockaddr_un_size
 56 |
 57 | ||| Creates a `sockaddr_un` pointer and sets its `sun_path` value to
 58 | ||| the given path.
 59 | |||
 60 | ||| The allocated memory must be freed via `freeStruct`.
 61 | export %inline
 62 | sockaddrUn : (path : String) -> F1 s (SSockaddrUn s)
 63 | sockaddrUn path = mapF1 SUN $ ffi $ prim__sockaddr_un path
 64 |
 65 | export %inline
 66 | path : SSockaddrUn s -> F1 s String
 67 | path (SUN p) = ffi $ prim__sockaddr_un_path p
 68 |
 69 | --------------------------------------------------------------------------------
 70 | -- SockaddrIn
 71 | --------------------------------------------------------------------------------
 72 |
 73 | %foreign "C:li_sockaddr_in, posix-idris"
 74 | prim__sockaddr_in: Bits32 -> Bits16 -> PrimIO AnyPtr
 75 |
 76 | %foreign "C:sockaddr_in_port, posix-idris"
 77 | prim__sockaddr_in_port: AnyPtr -> PrimIO Bits16
 78 |
 79 | %foreign "C:sockaddr_in_addr, posix-idris"
 80 | prim__sockaddr_in_addr: AnyPtr -> PrimIO Bits32
 81 |
 82 | %foreign "C:sockaddr_in_addr_str, posix-idris"
 83 | prim__sockaddr_in_addr_str: AnyPtr -> PrimIO String
 84 |
 85 | public export
 86 | record IP4Addr where
 87 |   constructor IP4
 88 |   addr : Vect 4 Bits8
 89 |   port : Bits16
 90 |
 91 | %runElab derive "IP4Addr" [Show,Eq]
 92 |
 93 | export
 94 | ip4addr : Vect 4 Bits8 -> Bits32
 95 | ip4addr [w,x,y,z] =
 96 |   shiftL (cast w) 24 .|. shiftL (cast x) 16 .|. shiftL (cast y) 8 .|. cast z
 97 |
 98 | export
 99 | splitIp4Addr : Bits32 -> Vect 4 Bits8
100 | splitIp4Addr x =
101 |   [cast (shiftR x 24), cast (shiftR x 16), cast (shiftR x 8), cast x]
102 |
103 | export
104 | record SSockaddrIn (s : Type) where
105 |   constructor SIN
106 |   ptr : AnyPtr
107 |
108 | public export
109 | 0 SockaddrIn : Type
110 | SockaddrIn = SSockaddrIn World
111 |
112 | export %inline
113 | Struct SSockaddrIn where
114 |   swrap   = SIN
115 |   sunwrap = ptr
116 |
117 | export
118 | SizeOf (SSockaddrIn s) where
119 |   sizeof_ = sockaddr_in_size
120 |
121 | namespace SockaddrIn
122 |   export %inline
123 |   port : SSockaddrIn s -> F1 s Bits16
124 |   port (SIN p) = ffi $ prim__sockaddr_in_port p
125 |
126 |   export %inline
127 |   addr : SSockaddrIn s -> F1 s Bits32
128 |   addr (SIN p) = ffi $ prim__sockaddr_in_addr p
129 |
130 |   export
131 |   addrIP4Addr : SSockaddrIn s -> F1 s IP4Addr
132 |   addrIP4Addr a t =
133 |     let p  # t := SockaddrIn.port a t
134 |         ad # t := SockaddrIn.addr a t
135 |      in IP4 (splitIp4Addr ad) p # t
136 |
137 |   export %inline
138 |   addrStr : SSockaddrIn s -> F1 s String
139 |   addrStr (SIN p) = ffi $ prim__sockaddr_in_addr_str p
140 |
141 | ||| Creates a `sockaddr_in` pointer and sets its `sun_path` value to
142 | |||
143 | ||| The allocated memory must be freed via `freeStruct`.
144 | export %inline
145 | sockaddrIn : IP4Addr -> F1 s (SSockaddrIn s)
146 | sockaddrIn (IP4 a p) = mapF1 SIN $ ffi $ prim__sockaddr_in (ip4addr a) p
147 |
148 | --------------------------------------------------------------------------------
149 | -- SockaddrIn6
150 | --------------------------------------------------------------------------------
151 |
152 | %foreign "C:li_sockaddr_in6, posix-idris"
153 | prim__sockaddr_in6: Bits16 -> PrimIO AnyPtr
154 |
155 | %foreign "C:sockaddr_in6_port, posix-idris"
156 | prim__sockaddr_in6_port: AnyPtr -> PrimIO Bits16
157 |
158 | %foreign "C:sockaddr_in6_addr, posix-idris"
159 | prim__sockaddr_in6_addr: AnyPtr -> AnyPtr
160 |
161 | %foreign "C:sockaddr_in6_addr_str, posix-idris"
162 | prim__sockaddr_in6_addr_str: AnyPtr -> PrimIO String
163 |
164 | public export
165 | record IP6Addr where
166 |   constructor IP6
167 |   addr : Vect 16 Bits8
168 |   port : Bits16
169 |
170 | %runElab derive "IP6Addr" [Show,Eq]
171 |
172 | export
173 | record SSockaddrIn6 (s : Type) where
174 |   constructor SIN6
175 |   ptr : AnyPtr
176 |
177 | export %inline
178 | Struct SSockaddrIn6 where
179 |   swrap   = SIN6
180 |   sunwrap = ptr
181 |
182 | public export
183 | 0 SockaddrIn6 : Type
184 | SockaddrIn6 = SSockaddrIn6 World
185 |
186 | export
187 | SizeOf (SSockaddrIn6 s) where
188 |   sizeof_ = sockaddr_in6_size
189 |
190 | namespace SockaddrIn6
191 |   export %inline
192 |   port : SSockaddrIn6 s -> F1 s Bits16
193 |   port (SIN6 p) = ffi $ prim__sockaddr_in6_port p
194 |
195 |   export %inline
196 |   addr6 : SSockaddrIn6 s -> CArray s 16 Bits8
197 |   addr6 (SIN6 p) = unsafeWrap (prim__sockaddr_in6_addr p)
198 |
199 |   export
200 |   addrIP6Addr : SSockaddrIn6 s -> F1 s IP6Addr
201 |   addrIP6Addr a t =
202 |     let p  # t  := SockaddrIn6.port a t
203 |         bs # t  := values [] (addr6 a) (#) 16 t
204 |         Just ad := toVect 16 bs | Nothing => IP6 (replicate 16 0) p # t
205 |      in IP6 ad p # t
206 |
207 |   export %inline
208 |   addrStr : SSockaddrIn6 s -> F1 s String
209 |   addrStr (SIN6 p) = ffi $ prim__sockaddr_in6_addr_str p
210 |
211 | ||| Creates a `sockaddr_in` pointer and sets its `sun_path` value to
212 | |||
213 | ||| The allocated memory must be freed via `freeStruct`.
214 | export
215 | sockaddrIn6 : IP6Addr -> F1 s (SSockaddrIn6 s)
216 | sockaddrIn6 (IP6 addr pr) t =
217 |   let res # t := ffi (prim__sockaddr_in6 pr) t
218 |       _   # t := writeVect (addr6 $ SIN6 res) addr t
219 |    in SIN6 res # t
220 |
221 | --------------------------------------------------------------------------------
222 | -- Conversions
223 | --------------------------------------------------------------------------------
224 |
225 | public export
226 | 0 Sockaddr : Domain -> Type
227 | Sockaddr AF_UNIX  = SockaddrUn
228 | Sockaddr AF_INET  = SockaddrIn
229 | Sockaddr AF_INET6 = SockaddrIn6
230 |
231 | public export
232 | 0 Addr : Domain -> Type
233 | Addr AF_UNIX  = String
234 | Addr AF_INET  = IP4Addr
235 | Addr AF_INET6 = IP6Addr
236 |
237 | export
238 | ptr : (d : _) -> Sockaddr d -> AnyPtr
239 | ptr AF_UNIX  x = x.ptr
240 | ptr AF_INET  x = x.ptr
241 | ptr AF_INET6 x = x.ptr
242 |
243 | export
244 | addrSize : (d : Domain) -> Bits32
245 | addrSize AF_UNIX  = sizeof SockaddrUn
246 | addrSize AF_INET  = sizeof SockaddrIn
247 | addrSize AF_INET6 = sizeof SockaddrIn6
248 |
249 | export
250 | sockaddr : (d : _) -> Addr d -> F1 World (Sockaddr d)
251 | sockaddr AF_UNIX  a = sockaddrUn a
252 | sockaddr AF_INET  a = sockaddrIn a
253 | sockaddr AF_INET6 a = sockaddrIn6 a
254 |