
   0 | module System.Posix.File.ReadRes
   1 | 
   2 | import Derive.Prelude
   3 | import Data.Linear.Token
   4 | 
   5 | import Data.Vect
   6 | import public Control.Monad.Resource
   7 | import public Data.Buffer
   8 | import public Data.Buffer.Core
   9 | import public Data.ByteString
  10 | import public Data.C.Ptr
  11 | import public System.Posix.Errno
  12 | 
  13 | %default total
  14 | %language ElabReflection
  15 | 
  16 | ||| Result of a (potentially non-blocking) read, typically from a pipe
  17 | ||| or socket.
  18 | public export
  19 | data ReadRes : Type -> Type where
  20 |   ||| The system call was interrupted by a signal.
  21 |   Interrupted : ReadRes a
  22 | 
  23 |   ||| There is currently no data avialable (this will only be a possible
  24 |   ||| outcome when reading in non-blocking mode).
  25 |   NoData      : ReadRes a
  26 | 
  27 |   ||| Tried to read from a closed connection or pipe.
  28 |   Closed      : ReadRes a
  29 | 
  30 |   ||| We reached the end of input.
  31 |   EOI         : ReadRes a
  32 | 
  33 |   ||| We got `n` bytes of data.
  34 |   Res         : (res : a) -> ReadRes a
  35 | 
  36 | %runElab derive "ReadRes" [Show,Eq]
  37 | 
  38 | export
  39 | Functor ReadRes where
  40 |   map f Interrupted = Interrupted
  41 |   map f NoData      = NoData
  42 |   map f Closed      = Closed
  43 |   map f EOI         = EOI
  44 |   map f (Res res)   = Res (f res)
  45 | 
  46 | export
  47 | Foldable ReadRes where
  48 |   foldr f v (Res r) = f r v
  49 |   foldr _ v _       = v
  50 | 
  51 | export
  52 | Traversable ReadRes where
  53 |   traverse f Interrupted = pure Interrupted
  54 |   traverse f NoData      = pure NoData
  55 |   traverse f Closed      = pure Closed
  56 |   traverse f EOI         = pure EOI
  57 |   traverse f (Res res)   = Res <$> f res
  58 | 
  59 | export
  60 | fromErr : Errno -> EPrim (ReadRes a)
  61 | fromErr err t =
  62 |   if      err == EAGAIN      then R NoData t
  63 |   else if err == EWOULDBLOCK then R NoData t
  64 |   else if err == EINTR       then R Interrupted t
  65 |   else if err == EPIPE       then R Closed t
  66 |   else                            E (inject err) t
  67 | 
  68 | --------------------------------------------------------------------------------
  69 | -- Read and Write Interfaces
  70 | --------------------------------------------------------------------------------
  71 | 
  72 | public export
  73 | record CPtr where
  74 |   constructor CP
  75 |   size : Bits32
  76 |   ptr  : AnyPtr
  77 | 
  78 | export
  79 | cptrOf1 : (0 a : Type) -> SizeOf a => Nat -> F1 World CPtr
  80 | cptrOf1 a n t =
  81 |   let sz := cast n * sizeof a
  82 |       p  := prim__malloc sz
  83 |    in CP sz (prim__malloc sz) # t
  84 | 
  85 | export %inline
  86 | cptrOf : HasIO io => (0 a : Type) -> SizeOf a => Nat -> io CPtr
  87 | cptrOf a = runIO . cptrOf1 a
  88 | 
  89 | export %inline
  90 | cptr1 : Nat -> F1 World CPtr
  91 | cptr1 = cptrOf1 Bits8
  92 | 
  93 | export %inline
  94 | cptr : HasIO io => Nat -> io CPtr
  95 | cptr = runIO . cptr1
  96 | 
  97 | export %inline
  98 | freePtr1 : CPtr -> F1' World
  99 | freePtr1 (CP _ p) = toF1 (prim__free p)
 100 | 
 101 | export %inline
 102 | ELift1 World f => Resource f CPtr where
 103 |   cleanup p = lift1 (freePtr1 p)
 104 | 
 105 | export %inline
 106 | freePtr : HasIO io => CPtr -> io ()
 107 | freePtr = runIO . freePtr1
 108 | 
 109 | public export
 110 | record Buf where
 111 |   constructor B
 112 |   size : Bits32
 113 |   buf  : Buffer
 114 | 
 115 | export %inline
 116 | buf : Bits32 -> F1 World Buf
 117 | buf sz t =
 118 |   let b # t := toF1 (prim__newBuf $ cast sz) t
 119 |    in B sz b # t
 120 | 
 121 | ||| Interface for wrapping or converting a freshly allocated buffer
 122 | ||| for reading, or an already allocated C-pointer for streaming
 123 | ||| data (typically from a file descriptor).
 124 | |||
 125 | ||| Please note that not all conversions are guaranteed to be
 126 | ||| lossless. For instance, converting a buffer to a (UTF-8) string
 127 | ||| will only be safe if the byte array does not end in the middle of
 128 | ||| a codepoint consisting of several bytes.
 129 | public export
 130 | interface FromBuf a where
 131 |   fromBuf : Buf -> F1 World a
 132 | 
 133 | public export
 134 | 0 EMBuffer : Type
 135 | EMBuffer = DPair Nat IOBuffer
 136 | 
 137 | public export
 138 | 0 EBuffer : Type
 139 | EBuffer = DPair Nat IBuffer
 140 | 
 141 | export %inline
 142 | FromBuf Buf where
 143 |   fromBuf buf t = buf # t
 144 | 
 145 | export %inline
 146 | FromBuf EMBuffer where
 147 |   fromBuf (B sz buf) t = (cast sz ** unsafeMBuffer buf) # t
 148 | 
 149 | export %inline
 150 | FromBuf EBuffer where
 151 |   fromBuf (B sz buf) t = (cast sz ** unsafeMakeBuffer buf) # t
 152 | 
 153 | export %inline
 154 | FromBuf ByteString where
 155 |   fromBuf (B sz buf) t = unsafeByteString (cast sz) buf # t
 156 | 
 157 | export %inline
 158 | FromBuf String where
 159 |   fromBuf buf t =
 160 |     let (n ** ib) # t := fromBuf {a = EBuffer} buf t
 161 |      in toString ib 0 n # t
 162 | 
 163 | export %inline
 164 | [DecimalString] FromBuf (Maybe Nat) where
 165 |   fromBuf b t =
 166 |     let bs # t := fromBuf {a=ByteString} b t
 167 |     in (parseDecimalNat bs) # t
 168 | 
 169 | export %inline
 170 | [HexadecimalString] FromBuf (Maybe Nat) where
 171 |   fromBuf b t =
 172 |     let bs # t := fromBuf {a=ByteString} b t
 173 |     in (parseHexadecimalNat bs) # t
 174 | 
 175 | export %inline
 176 | [OctalString] FromBuf (Maybe Nat) where
 177 |   fromBuf b t =
 178 |     let bs # t := fromBuf {a=ByteString} b t
 179 |     in (parseOctalNat bs) # t
 180 | 
 181 | export %inline
 182 | [BinaryString] FromBuf (Maybe Nat) where
 183 |   fromBuf b t =
 184 |     let bs # t := fromBuf {a=ByteString} b t
 185 |     in (parseBinaryNat bs) # t
 186 | 
 187 | export %inline
 188 | [IntegerString] FromBuf (Maybe Integer) where
 189 |   fromBuf b t =
 190 |     let bs # t := fromBuf {a=ByteString} b t
 191 |     in (parseInteger bs) # t
 192 | 
 193 | export %inline
 194 | [DoubleString] FromBuf (Maybe Double) where
 195 |   fromBuf b t =
 196 |     let bs # t := fromBuf {a=ByteString} b t
 197 |     in (parseDouble bs) # t
 198 | 
 199 | public export
 200 | 0 ECArrayIO : Type -> Type
 201 | ECArrayIO t = (n ** CArrayIO n t)
 202 | 
 203 | ||| Interface for converting a value for writing.
 204 | |||
 205 | ||| We distinguis between three situations:
 206 | |||
 207 | |||   a) The value is converted to a `ByteString`. In this case
 208 | |||      the value can be directly written and the runtime will take
 209 | |||      care of collecting its memory.
 210 | |||
 211 | |||   b) The value is converted to a `CPtr`, which has been allocated
 212 | |||      elsewhere. We are not responsible for freeing the pointer as
 213 | |||      it might be reused for streaming.
 214 | public export
 215 | interface ToBuf a where
 216 |   unsafeToBuf : a -> Either CPtr ByteString
 217 | 
 218 | export %inline
 219 | ToBuf ByteString where
 220 |   unsafeToBuf = Right
 221 | 
 222 | export %inline
 223 | ToBuf String where
 224 |   unsafeToBuf = Right . fromString
 225 | 
 226 | export %inline
 227 | {n : _} -> ToBuf (IBuffer n) where
 228 |   unsafeToBuf buf = Right $ unsafeByteString n (unsafeGetBuffer buf)
 229 | 
 230 | export %inline
 231 | {n : _} -> ToBuf (MBuffer t n) where
 232 |   unsafeToBuf buf = Right $ unsafeByteString n (unsafeFromMBuffer buf)
 233 | 
 234 | export %inline
 235 | ToBuf CPtr where
 236 |   unsafeToBuf = Left
 237 | 
 238 | export %inline
 239 | {n : _} -> SizeOf a => ToBuf (CArray t n a) where
 240 |   unsafeToBuf arr =
 241 |     Left (CP (cast n * sizeof a) (unsafeUnwrap arr))
 242 | 
 243 | export %inline
 244 | SizeOf a => ToBuf (ECArrayIO a) where
 245 |   unsafeToBuf (_ ** arr) = unsafeToBuf arr
 246 | 
 247 | export
 248 | {n : _} -> SizeOf a => SetPtr a => ToBuf (Vect n a) where
 249 |   unsafeToBuf vs =
 250 |     run1 $ \t =>
 251 |      let sz      := cast n * sizeof a
 252 |          buf # t := ffi (prim__newBuf $ cast sz) t
 253 |          arr # t := malloc1 a n t
 254 |          _   # t := writeVect arr vs t
 255 |          _   # t := ffi (prim__copy_pb (unsafeUnwrap arr) buf sz) t
 256 |          _   # t := free1 arr t
 257 |       in Right (unsafeByteString (cast sz) buf) # t
 258 | 
 259 | export %inline
 260 | SizeOf a => SetPtr a => ToBuf (List a) where
 261 |   unsafeToBuf vs = unsafeToBuf (Vect.fromList vs)
 262 | 
 263 | --------------------------------------------------------------------------------
 264 | -- Streaming Interfaces
 265 | --------------------------------------------------------------------------------
 266 | 
 267 | export %inline
 268 | [DStruct] Struct f => Deref (f World) where
 269 |   deref p = pure (swrap p)
 270 | 
 271 | public export
 272 | record Convert t where
 273 |   [noHints]
 274 |   constructor C
 275 |   0 source : Type
 276 |   {auto sof  : SizeOf source}
 277 |   {auto derf : Deref source}
 278 |   convert : source -> F1 World t
 279 | 
 280 | public export
 281 | convStruct :
 282 |      (0 f : Type -> Type)
 283 |   -> {auto iss : Struct f}
 284 |   -> {auto sof : SizeOf (f World)}
 285 |   -> (fun : f World -> F1 World t)
 286 |   -> Convert t
 287 | convStruct f fun = C (f World) {sof} {derf = DStruct} fun
 288 | 
 289 | ||| Interface for wrapping or converting a c-land pointer.
 290 | |||
 291 | ||| This is useful for streaming data from a file descriptor.
 292 | ||| Idris (garbage collected) values are generated by copying the given
 293 | ||| number of bytes.
 294 | |||
 295 | ||| Please note that not all conversions are guaranteed to be
 296 | ||| lossless. For instance, converting a buffer to a (UTF-8) string
 297 | ||| will only be safe if the byte array does not end in the middle of
 298 | ||| a codepoint consisting of several bytes.
 299 | public export
 300 | interface FromPtr a where
 301 |   fromPtr : CPtr -> F1 World a
 302 | 
 303 | export %inline
 304 | FromPtr CPtr where
 305 |   fromPtr = (#)
 306 | 
 307 | export %inline
 308 | SizeOf a => FromPtr (ECArrayIO a) where
 309 |   fromPtr (CP sz ptr) t =
 310 |     (cast (sz `div` sizeof a) ** unsafeWrap ptr) # t
 311 | 
 312 | export
 313 | FromPtr EBuffer where
 314 |   fromPtr (CP sz32 ptr) t =
 315 |     let buf # t := toF1 (prim__newBuf $ cast sz32) t
 316 |         _   # t := toF1 (prim__copy_pb ptr buf sz32) t
 317 |      in (cast sz32 ** unsafeMakeBuffer buf) # t
 318 | 
 319 | export
 320 | FromPtr EMBuffer where
 321 |   fromPtr (CP sz32 ptr) t =
 322 |     let buf # t := toF1 (prim__newBuf $ cast sz32) t
 323 |         _   # t := toF1 (prim__copy_pb ptr buf sz32) t
 324 |      in (cast sz32 ** unsafeMBuffer buf) # t
 325 | 
 326 | export
 327 | FromPtr ByteString where
 328 |   fromPtr cp t =
 329 |     let (n ** ib) # t := fromPtr {a = EBuffer} cp t
 330 |      in BS n (fromIBuffer ib) # t
 331 | 
 332 | export
 333 | FromPtr String where
 334 |   fromPtr cp t =
 335 |     let (n ** ib) # t := fromPtr {a = EBuffer} cp t
 336 |      in toString ib 0 n # t
 337 | 
 338 | export
 339 | Convert t => FromPtr (List t) where
 340 |   fromPtr @{C src conv} cp t =
 341 |     let (n ** arr) # t := fromPtr {a = ECArrayIO src} cp t
 342 |      in values [] arr conv n t
 343 | 
 344 | export
 345 | SizeOf a => Deref a => FromPtr (List a) where
 346 |   fromPtr cp t =
 347 |     let (n ** arr) # t := fromPtr {a = ECArrayIO a} cp t
 348 |      in values [] arr (#) n t
 349 | 
 350 | export
 351 | FromBuf CPtr where
 352 |   fromBuf (B sz buf) t =
 353 |     let p     := prim__malloc sz
 354 |         _ # t := toF1 (prim__copy_bp buf p sz) t
 355 |      in CP sz p # t
 356 | 
 357 | export %inline
 358 | SizeOf a => FromBuf (ECArrayIO a) where
 359 |   fromBuf b t = let cp # t := fromBuf b t in fromPtr cp t
 360 | 
 361 | export
 362 | viaPtrFromBuf : FromPtr r => Buf -> F1 World r
 363 | viaPtrFromBuf b t =
 364 |   let cp # t := fromBuf b t
 365 |       r  # t := fromPtr cp t
 366 |       _  # t := freePtr1 cp t
 367 |    in r # t
 368 | 
 369 | export %inline
 370 | Convert t => FromBuf (List t) where
 371 |   fromBuf = viaPtrFromBuf
 372 |