
   0 | module System.UV.Raw.Pointer
   1 | 
   2 | import Data.Buffer
   3 | import Derive.Prelude
   4 | import System.UV.Raw.Util
   5 | import public System.FFI
   6 | import public System.UV.Data.Pointer
   7 | 
   8 | %language ElabReflection
   9 | %default total
  10 | 
  11 | --------------------------------------------------------------------------------
  12 | -- Buffers and Loops
  13 | --------------------------------------------------------------------------------
  14 | 
  15 | export
  16 | data Buf : Type where
  17 | 
  18 | export
  19 | data Loop : Type where
  20 | 
  21 | ||| Convert a `Ptr Char` to an Idris string.
  22 | |||
  23 | ||| Note: Users must make sure that the given pointer points at a
  24 | ||| zero-terminated byte array. As an alternative, consider converting
  25 | ||| a `Ptr Bits8`.
  26 | export %inline
  27 | getString : Ptr Char -> String
  28 | getString p = prim__getString (believe_me p)
  29 | 
  30 | ||| Like `getString` but returns `Nothing` in case the given pointer is the
  31 | ||| null pointer.
  32 | export %inline
  33 | getStringMay : Ptr Char -> Maybe String
  34 | getStringMay p =
  35 |   case prim__nullPtr p of
  36 |     0 => Just $ getString p
  37 |     _ => Nothing
  38 | 
  39 | --------------------------------------------------------------------------------
  40 | -- FFI
  41 | --------------------------------------------------------------------------------
  42 | 
  43 | %foreign "scheme:blodwen-new-buffer"
  44 |          "RefC:newBuffer"
  45 |          "node:lambda:s=>Buffer.alloc(s)"
  46 | prim__newBuffer : Bits32 -> PrimIO Buffer
  47 | 
  48 | %foreign (idris_uv "uv_set_buf_len")
  49 | uv_set_buf_len : Ptr Buf -> Bits32 -> PrimIO ()
  50 | 
  51 | %foreign (idris_uv "uv_set_buf_base")
  52 | uv_set_buf_base : Ptr Buf -> Ptr Bits8 -> PrimIO ()
  53 | 
  54 | %foreign (idris_uv "uv_get_buf_len")
  55 | uv_get_buf_len : Ptr Buf -> PrimIO Bits32
  56 | 
  57 | %foreign (idris_uv "uv_get_buf_base")
  58 | uv_get_buf_base : Ptr Buf -> PrimIO (Ptr Bits8)
  59 | 
  60 | %foreign (idris_uv "uv_copy_buf")
  61 | uv_copy_to_buf : Ptr Bits8 -> Buffer -> Bits32 -> PrimIO ()
  62 | 
  63 | %foreign (idris_uv "uv_copy_from_buf")
  64 | uv_copy_from_buf : Buffer -> Ptr Bits8 -> (size, offset : Bits32) -> PrimIO ()
  65 | 
  66 | %foreign "scheme:blodwen-buffer-getstring"
  67 | uv_get_string : Ptr Bits8 -> (offset, len : Bits32) -> PrimIO String
  68 | 
  69 | --------------------------------------------------------------------------------
  70 | -- Handles
  71 | --------------------------------------------------------------------------------
  72 | 
  73 | export
  74 | data Async : Type where
  75 | 
  76 | export
  77 | data Check : Type where
  78 | 
  79 | export
  80 | data FsEvent : Type where
  81 | 
  82 | export
  83 | data FsPoll : Type where
  84 | 
  85 | export
  86 | data Handle : Type where
  87 | 
  88 | export
  89 | data Idle : Type where
  90 | 
  91 | export
  92 | data Pipe : Type where
  93 | 
  94 | export
  95 | data Poll : Type where
  96 | 
  97 | export
  98 | data Prepare : Type where
  99 | 
 100 | export
 101 | data Process : Type where
 102 | 
 103 | export
 104 | data Stream : Type where
 105 | 
 106 | export
 107 | data Tcp : Type where
 108 | 
 109 | export
 110 | data Timer : Type where
 111 | 
 112 | export
 113 | data Tty : Type where
 114 | 
 115 | export
 116 | data Udp : Type where
 117 | 
 118 | export
 119 | data Signal : Type where
 120 | 
 121 | --------------------------------------------------------------------------------
 122 | -- Reqs
 123 | --------------------------------------------------------------------------------
 124 | 
 125 | export
 126 | data Req : Type where
 127 | 
 128 | export
 129 | data Connect : Type where
 130 | 
 131 | export
 132 | data Write : Type where
 133 | 
 134 | export
 135 | data Shutdown : Type where
 136 | 
 137 | export
 138 | data UpdSend : Type where
 139 | 
 140 | export
 141 | data Fs : Type where
 142 | 
 143 | export
 144 | data Work : Type where
 145 | 
 146 | export
 147 | data GetAddrInfo : Type where
 148 | 
 149 | export
 150 | data GetNameInfo : Type where
 151 | 
 152 | --------------------------------------------------------------------------------
 153 | -- Sock Addresses
 154 | --------------------------------------------------------------------------------
 155 | 
 156 | export
 157 | data AddrInfo : Type where
 158 | 
 159 | export
 160 | data SockAddr : Type where
 161 | 
 162 | export
 163 | data SockAddrIn : Type where
 164 | 
 165 | export
 166 | data SockAddrIn6 : Type where
 167 | 
 168 | --------------------------------------------------------------------------------
 169 | -- Allocation
 170 | --------------------------------------------------------------------------------
 171 | 
 172 | ||| Proof that we have an associated size for a pointer type. This
 173 | ||| allows us to allocate the correct amount of memory when we need a
 174 | ||| new pointer of the given type (see `mallocPtr` and `mallocPtrs`).
 175 | public export
 176 | data PSize : (a : Type) -> (s : Bits32) -> Type where
 177 |   [search a]
 178 |   ASYNC          : PSize Async SZ_ASYNC
 179 |   CHECK          : PSize Check SZ_CHECK
 180 |   FS_EVENT       : PSize FsEvent SZ_FS_EVENT
 181 |   FS_POLL        : PSize FsPoll SZ_FS_POLL
 182 |   HANDLE         : PSize Handle SZ_HANDLE
 183 |   IDLE           : PSize Idle SZ_IDLE
 184 |   NAMEDPIPE      : PSize Pipe SZ_NAMED_PIPE
 185 |   POLL           : PSize Poll SZ_POLL
 186 |   PREPARE        : PSize Prepare SZ_PREPARE
 187 |   PROCESS        : PSize Process SZ_PROCESS
 188 |   STREAM         : PSize Stream SZ_STREAM
 189 |   TCP            : PSize Tcp SZ_TCP
 190 |   TIMER          : PSize Timer SZ_TIMER
 191 |   TTY            : PSize Tty SZ_TTY
 192 |   UDP            : PSize Udp SZ_UDP
 193 |   SIGNAL         : PSize Signal SZ_SIGNAL
 194 |   REQ            : PSize Req SZ_REQ
 195 |   CONNECT        : PSize Connect SZ_CONNECT
 196 |   WRITE          : PSize Write SZ_WRITE
 197 |   SHUTDOWN       : PSize Shutdown SZ_SHUTDOWN
 198 |   FS             : PSize Fs SZ_FS
 199 |   WORK           : PSize Work SZ_WORK
 200 |   GETADDRINFO    : PSize GetAddrInfo SZ_GETADDRINFO
 201 |   GETNAMEINFO    : PSize GetNameInfo SZ_GETNAMEINFO
 202 |   ADDRINFO       : PSize AddrInfo SZ_ADDRINFO
 203 |   SOCKADDR       : PSize SockAddr SZ_SOCKADDR
 204 |   SOCKADDRIN     : PSize SockAddrIn SZ_SOCKADDR_IN
 205 |   SOCKADDRIN6    : PSize SockAddrIn6 SZ_SOCKADDR_IN6
 206 |   BUF            : PSize Buf SZ_BUF
 207 |   LOOP           : PSize Loop SZ_LOOP
 208 |   BYTE           : PSize Bits8 1
 209 |   CHAR           : PSize Char 1
 210 | 
 211 | %runElab deriveIndexed "PSize" [Show]
 212 | 
 213 | ||| Allocates a pointer for a type of a known pointer size.
 214 | export %inline
 215 | mallocPtr :
 216 |      {auto has : HasIO io}
 217 |   -> {s : _}
 218 |   -> (0 a : Type)
 219 |   -> {auto 0 prf : PSize a s}
 220 |   -> io (Ptr a)
 221 | mallocPtr _ = prim__castPtr <$> malloc (cast s)
 222 | 
 223 | ||| Allocates an array of pointers for a type of a known pointer size.
 224 | export %inline
 225 | mallocPtrs :
 226 |      {auto has : HasIO io}
 227 |   -> {s : _}
 228 |   -> (0 a : Type)
 229 |   -> {auto 0 prf : PSize a s}
 230 |   -> (numPtrs : Bits32)
 231 |   -> io (Ptr a)
 232 | mallocPtrs _ numPtrs = prim__castPtr <$> malloc (cast $ s * numPtrs)
 233 | 
 234 | ||| Frees a typed pointer.
 235 | export %inline
 236 | freePtr : HasIO io => Ptr t -> io ()
 237 | freePtr = free . prim__forgetPtr
 238 | 
 239 | --------------------------------------------------------------------------------
 240 | -- Safe Casts
 241 | --------------------------------------------------------------------------------
 242 | 
 243 | ||| Pointers to some types are subtypes of pointers to other types:
 244 | ||| Their structure is laid out in such a way that they can be used
 245 | ||| where the other pointer type is expected.
 246 | |||
 247 | ||| For instance, every libuv handle can be used where a `uv_handle_t`
 248 | ||| (represented as `Ptr Handle` in Idris) is expected.
 249 | |||
 250 | ||| This data type is a proof of such a subtyping relation. Use `castPtr`
 251 | ||| to safely convert pointers.
 252 | public export
 253 | data PCast : Type -> Type -> Type where
 254 |   Self                 : PCast t t
 255 |   AsyncHandle          : PCast Async Handle
 256 |   CheckHandle          : PCast Check Handle
 257 |   Fs_eventHandle       : PCast FsEvent Handle
 258 |   Fs_pollHandle        : PCast FsPoll Handle
 259 |   IdleHandle           : PCast Idle Handle
 260 |   NamedpipeHandle      : PCast Pipe Handle
 261 |   PollHandle           : PCast Poll Handle
 262 |   PrepareHandle        : PCast Prepare Handle
 263 |   ProcessHandle        : PCast Process Handle
 264 |   StreamHandle         : PCast Stream Handle
 265 |   TcpHandle            : PCast Tcp Handle
 266 |   TimerHandle          : PCast Timer Handle
 267 |   TtyHandle            : PCast Tty Handle
 268 |   UdpHandle            : PCast Udp Handle
 269 |   SignalHandle         : PCast Signal Handle
 270 |   StreamStream         : PCast Stream Stream
 271 |   TcpStream            : PCast Tcp Stream
 272 |   PipeStream           : PCast Pipe Stream
 273 |   TtyStream            : PCast Tty Stream
 274 |   IP4Addr              : PCast SockAddrIn SockAddr
 275 |   RevIP4Addr           : PCast SockAddr SockAddrIn
 276 |   IP6Addr              : PCast SockAddrIn6 SockAddr
 277 |   ConnectReq           : PCast Connect Req
 278 |   WriteReq             : PCast Write Req
 279 |   ShutdownReq          : PCast Shutdown Req
 280 |   UpdSendReq           : PCast UpdSend Req
 281 |   FsReq                : PCast Fs Req
 282 |   WorkReq              : PCast Work Req
 283 |   GetAddrInfoReq       : PCast GetAddrInfo Req
 284 |   GetNameInfoReq       : PCast GetNameInfo Req
 285 |   ByteChar             : PCast Bits8 Char
 286 |   CharByte             : PCast Char Bits8
 287 | 
 288 | export
 289 | castPtr : (0 _ : PCast s t) => Ptr s -> Ptr t
 290 | castPtr = believe_me
 291 | 
 292 | --------------------------------------------------------------------------------
 293 | -- Buffers
 294 | --------------------------------------------------------------------------------
 295 | 
 296 | export %inline
 297 | newBuffer : HasIO io => Bits32 -> io Buffer
 298 | newBuffer s = primIO $ prim__newBuffer s
 299 | 
 300 | export %inline
 301 | setBufLen : HasIO io => Ptr Buf -> Bits32 -> io ()
 302 | setBufLen p s = primIO $ uv_set_buf_len p s
 303 | 
 304 | export %inline
 305 | getBufLen : HasIO io => Ptr Buf -> io Bits32
 306 | getBufLen p = primIO $ uv_get_buf_len p
 307 | 
 308 | export %inline
 309 | setBufBase : HasIO io => Ptr Buf -> Ptr Bits8 -> io ()
 310 | setBufBase p s = primIO $ uv_set_buf_base p s
 311 | 
 312 | export %inline
 313 | getBufBase : HasIO io => Ptr Buf -> io (Ptr Bits8)
 314 | getBufBase p = primIO $ uv_get_buf_base p
 315 | 
 316 | export
 317 | initBuf : HasIO io => Ptr Buf -> Ptr Bits8 -> Bits32 -> io ()
 318 | initBuf pbuf pcs len = do
 319 |   setBufBase pbuf pcs
 320 |   setBufLen pbuf len
 321 | 
 322 | ||| Frees the memory allocated for a `uv_buf_t`'s `base` field.
 323 | export %inline
 324 | freeBufBase : HasIO io => Ptr Buf -> io ()
 325 | freeBufBase buf = getBufBase buf >>= freePtr
 326 | 
 327 | ||| Copy the given number of bytes from a byte array to an Idris-managed
 328 | ||| buffer.
 329 | export
 330 | copyToBuffer : HasIO io => Ptr Bits8 -> Buffer -> Bits32 -> io ()
 331 | copyToBuffer p buf x = primIO $ uv_copy_to_buf p buf x
 332 | 
 333 | ||| Copy the given number of bytes from a byte array to an Idris-managed
 334 | ||| buffer.
 335 | export
 336 | copyBufToBuffer : HasIO io => Ptr Buf -> Buffer -> Bits32 -> io ()
 337 | copyBufToBuffer p buf s = getBufBase p >>= \x => copyToBuffer x buf s
 338 | 
 339 | ||| Copy the given number of bytes an Idris-managed
 340 | ||| buffer to a `Ptr Char`
 341 | export
 342 | copyFromBuffer : HasIO io => Buffer -> (size, offset : Bits32) -> io (Ptr Bits8)
 343 | copyFromBuffer buf size offset = do
 344 |   pchar <- mallocPtrs Bits8 size
 345 |   primIO $ uv_copy_from_buf buf pchar size offset
 346 |   pure pchar
 347 |