
   0 | module System.Posix.File.Prim
   1 | 
   2 | import Data.Bits
   3 | 
   4 | import public Data.Buffer
   5 | import public Data.Buffer.Core
   6 | import public Data.ByteString
   7 | import public Data.ByteVect
   8 | 
   9 | import public Data.C.Ptr
  10 | 
  11 | import public System.Posix.Errno
  12 | import public System.Posix.File.FileDesc
  13 | import public System.Posix.File.Flags
  14 | import public System.Posix.File.ReadRes
  15 | import public System.Posix.File.Whence
  16 | 
  17 | %default total
  18 | 
  19 | --------------------------------------------------------------------------------
  20 | -- FFI
  21 | --------------------------------------------------------------------------------
  22 | 
  23 | %foreign "C:li_open, posix-idris"
  24 | prim__open : String -> Bits32 -> ModeT -> PrimIO CInt
  25 | 
  26 | %foreign "C:li_close, posix-idris"
  27 | prim__close : Bits32 -> PrimIO CInt
  28 | 
  29 | %foreign "C__collect_safe:li_read, posix-idris"
  30 | prim__readptr : (file : Bits32) -> AnyPtr -> (max : Bits32) -> PrimIO SsizeT
  31 | 
  32 | %foreign "C:li_read, posix-idris"
  33 | prim__read : (file : Bits32) -> Buffer -> (max : Bits32) -> PrimIO SsizeT
  34 | 
  35 | %foreign "C:li_pread, posix-idris"
  36 | prim__pread : (file : Bits32) -> Buffer -> (max : Bits32) -> OffT -> PrimIO SsizeT
  37 | 
  38 | %foreign "C:li_write, posix-idris"
  39 | prim__write : (file : Bits32) -> Buffer -> (off,max : Bits32) -> PrimIO SsizeT
  40 | 
  41 | %foreign "C__collect_safe:li_write, posix-idris"
  42 | prim__writeptr : (file : Bits32) -> AnyPtr -> (off,max : Bits32) -> PrimIO SsizeT
  43 | 
  44 | %foreign "C:li_pwrite, posix-idris"
  45 | prim__pwrite : (file : Bits32) -> Buffer -> (off,max : Bits32) -> OffT -> PrimIO SsizeT
  46 | 
  47 | %foreign "C__collect_safe:li_pwrite, posix-idris"
  48 | prim__pwriteptr : (file : Bits32) -> AnyPtr -> (off,max : Bits32) -> OffT -> PrimIO SsizeT
  49 | 
  50 | %foreign "C:lseek, posix-idris"
  51 | prim__lseek : (file : Bits32) -> (off : OffT) -> (whence : CInt) -> PrimIO OffT
  52 | 
  53 | %foreign "C:li_set_flags, posix-idris"
  54 | prim__setFlags : (file : Bits32) -> (flags : Bits32) -> PrimIO CInt
  55 | 
  56 | %foreign "C:li_get_flags, posix-idris"
  57 | prim__getFlags : (file : Bits32) -> PrimIO CInt
  58 | 
  59 | %foreign "C:li_dup, posix-idris"
  60 | prim__dup : (file : Bits32) -> PrimIO CInt
  61 | 
  62 | %foreign "C:li_dup2, posix-idris"
  63 | prim__dup2 : (file, dst : Bits32) -> PrimIO CInt
  64 | 
  65 | %foreign "C:li_dupfd, posix-idris"
  66 | prim__dupfd : (file, startfd : Bits32) -> PrimIO CInt
  67 | 
  68 | %foreign "C:li_ftruncate, posix-idris"
  69 | prim__ftruncate : (file : Bits32) -> (len : OffT) -> PrimIO CInt
  70 | 
  71 | %foreign "C:li_truncate, posix-idris"
  72 | prim__truncate : (file : String) -> (len : OffT) -> PrimIO CInt
  73 | 
  74 | %foreign "C:li_mkstemp, posix-idris"
  75 | prim__mkstemp : Buffer -> PrimIO CInt
  76 | 
  77 | %foreign "C:li_link, posix-idris"
  78 | prim__link : String -> String -> PrimIO CInt
  79 | 
  80 | %foreign "C:li_symlink, posix-idris"
  81 | prim__symlink : String -> String -> PrimIO CInt
  82 | 
  83 | %foreign "C:li_rename, posix-idris"
  84 | prim__rename : String -> String -> PrimIO CInt
  85 | 
  86 | %foreign "C:li_unlink, posix-idris"
  87 | prim__unlink : String -> PrimIO CInt
  88 | 
  89 | %foreign "C:li_remove, posix-idris"
  90 | prim__remove : String -> PrimIO CInt
  91 | 
  92 | %foreign "C:li_readlink, posix-idris"
  93 | prim__readlink : (file : String) -> Buffer -> (max : Bits32) -> PrimIO SsizeT
  94 | 
  95 | --------------------------------------------------------------------------------
  96 | -- Utilities
  97 | --------------------------------------------------------------------------------
  98 | 
  99 | ||| Converts a number of bytes read into a buffer to a suitable result.
 100 | export %inline
 101 | allocRead : FromBuf a => Bits32 -> (Buffer -> Bits32 -> PrimIO SsizeT) -> EPrim a
 102 | allocRead n act t =
 103 |   let buf # t := toF1 (prim__newBuf $ cast n) t
 104 |       rd  # t := toF1 (act buf n) t
 105 |    in if rd < 0
 106 |          then E (inject $ fromNeg rd) t
 107 |          else let r # t := fromBuf (B (cast rd) buf) t in R r t
 108 | 
 109 | ||| Like `allocRead` but treats certain errors as valid results.
 110 | export %inline
 111 | toRes :
 112 |      {auto fb : FromBuf a}
 113 |   -> Bits32
 114 |   -> (Buffer -> Bits32 -> PrimIO SsizeT)
 115 |   -> EPrim (ReadRes a)
 116 | toRes n act t =
 117 |   let buf # t := toF1 (prim__newBuf $ cast n) t
 118 |       rd  # t := toF1 (act buf n) t
 119 |    in if      rd < 0  then fromErr (fromNeg rd) t
 120 |       else if rd == 0 then R EOI t
 121 |       else let r # t := fromBuf (B (cast rd) buf) t in R (Res r) t
 122 | 
 123 | 
 124 | ||| Converts a number of bytes read into a C-ptr to a suitable result.
 125 | export %inline
 126 | ptrRead : FromPtr a => AnyPtr -> PrimIO SsizeT -> EPrim a
 127 | ptrRead ptr act t =
 128 |   let rd  # t := toF1 act t
 129 |    in if rd < 0
 130 |          then E (inject $ fromNeg rd) t
 131 |          else let res # t := fromPtr (CP (cast rd) ptr) t in R res t
 132 | 
 133 | ||| Like `ptrRead` but treats certain errors as valid results.
 134 | export %inline
 135 | ptrToRes : FromPtr a => AnyPtr -> PrimIO SsizeT -> EPrim (ReadRes a)
 136 | ptrToRes ptr act t =
 137 |   let rd  # t := toF1 act t
 138 |    in if      rd < 0  then fromErr (fromNeg rd) t
 139 |       else if rd == 0 then R EOI t
 140 |       else let res # t := fromPtr (CP (cast rd) ptr) t  in R (Res res) t
 141 | 
 142 | export %inline
 143 | toFD : PrimIO CInt -> EPrim Fd
 144 | toFD = toVal (MkFd . cast)
 145 | 
 146 | --------------------------------------------------------------------------------
 147 | -- File Operations
 148 | --------------------------------------------------------------------------------
 149 | 
 150 | ||| Tries to open a file with the given flags and mode.
 151 | export %inline
 152 | openFile : String -> Flags -> Mode -> EPrim Fd
 153 | openFile p (F f) (M m) = toFD (prim__open p f m)
 154 | 
 155 | parameters {auto fid : FileDesc a}
 156 |            (fd       : a)
 157 | 
 158 |   ||| Closes a file descriptor.
 159 |   export %inline
 160 |   close : EPrim ()
 161 |   close = toUnit (prim__close $ fileDesc fd)
 162 | 
 163 |   ||| Convenience version of `close` that fails silently.
 164 |   export %inline
 165 |   close' : PrimIO ()
 166 |   close' w =
 167 |     let MkIORes _ w := prim__close (fileDesc fd) w
 168 |      in MkIORes () w
 169 | 
 170 |   ||| Reads at most `n` bytes from a file into a pre-allocated pointer.
 171 |   export %inline
 172 |   readPtr : (0 r : Type) -> FromPtr r => CPtr -> EPrim r
 173 |   readPtr r (CP sz p) = ptrRead p $ prim__readptr (fileDesc fd) p sz
 174 | 
 175 |   ||| Reads at most `n` bytes from a file into a pre-allocated pointer.
 176 |   |||
 177 |   ||| This is similar to `readres`, but it allows us to efficiently stream
 178 |   ||| data into a large pointer, even in case the chunks of data are much smaller.
 179 |   export %inline
 180 |   readPtrRes : (0 r : Type) -> FromPtr r => CPtr -> EPrim (ReadRes r)
 181 |   readPtrRes r (CP sz p) = ptrToRes p $ prim__readptr (fileDesc fd) p sz
 182 | 
 183 |   ||| Reads at most `n` bytes from a file into a suitable result type.
 184 |   export
 185 |   read : (0 r : Type) -> FromBuf r => (n : Bits32) -> EPrim r
 186 |   read r n = allocRead n $  prim__read (fileDesc fd)
 187 | 
 188 |   ||| Reads data from a file into a preallocated buffer
 189 |   export
 190 |   readRaw : Buf -> EPrim EMBuffer
 191 |   readRaw (B sz buf) t =
 192 |    let rd # t := toF1 (prim__read (fileDesc fd) buf sz) t
 193 |     in if rd < 0
 194 |          then E (inject $ fromNeg rd) t
 195 |          else R (cast rd ** unsafeMBuffer buf) t
 196 | 
 197 |   ||| Reads at most `n` bytes from a file into a suitable result type.
 198 |   |||
 199 |   ||| This is a more convenient version of `read` that gives detailed
 200 |   ||| information about why a read might fail. It is especially useful
 201 |   ||| when reading from - possibly non-blocking - pipes or sockets.
 202 |   export
 203 |   readres : (0 r : Type) -> FromBuf r => (n : Bits32) -> EPrim (ReadRes r)
 204 |   readres r n = toRes n $  prim__read (fileDesc fd)
 205 | 
 206 |   ||| Atomically reads up to `n` bytes from the given file at
 207 |   ||| the given file offset.
 208 |   |||
 209 |   ||| Notes: This will only work with seekable files but not with
 210 |   |||        arbitrary data streams such as pipes or sockets.
 211 |   |||        Also, it will not change the position of the open file description.
 212 |   export
 213 |   pread : (0 r : Type) -> FromBuf r => (n : Bits32) -> OffT -> EPrim r
 214 |   pread r n off = allocRead n $ \b,x => prim__pread (fileDesc fd) b x off
 215 | 
 216 |   ||| Writes up to the number of bytes in the bytestring
 217 |   ||| to the given file.
 218 |   |||
 219 |   ||| Note: This is an atomic operation if `fd` is a regular file that
 220 |   |||       was opened in "append" mode (with the `O_APPEND` flag).
 221 |   export
 222 |   write : ToBuf r => r -> EPrim Bits32
 223 |   write v =
 224 |     case unsafeToBuf v of
 225 |       Left (CP sz ptr)        =>
 226 |         toSize $ prim__writeptr (fileDesc fd) ptr 0 sz
 227 |       Right (BS n $ BV b o _) =>
 228 |         toSize $ prim__write (fileDesc fd) (unsafeGetBuffer b) (cast o) (cast n)
 229 | 
 230 |   ||| Iteratively writes a value to a file descriptor making sure
 231 |   ||| that the whole value is written. Use this, if a single call to
 232 |   ||| `write` might not write the complete data (for instance, when
 233 |   ||| writing to a pipe or socket).
 234 |   export
 235 |   fwrite : ToBuf r => r -> EPrim ()
 236 |   fwrite v =
 237 |     case (unsafeToBuf v) of
 238 |       Left  (CP sz p) => goPtr p sz
 239 |       Right bs        => go bs
 240 | 
 241 |     where
 242 |       goPtr : AnyPtr -> Bits32 -> EPrim ()
 243 |       goPtr p 0  t = R () t
 244 |       goPtr p sz t =
 245 |         let R m t := write (CP sz p) t | E x t => E x t
 246 |          in goPtr (prim__inc_ptr p m 1) (assert_smaller sz $ sz - m) t
 247 | 
 248 |       go : ByteString -> EPrim ()
 249 |       go (BS 0 _) t = R () t
 250 |       go bs       t =
 251 |         let R m t := write bs t | E x t => E x t
 252 |          in go (assert_smaller bs $ drop (cast m) bs) t
 253 | 
 254 |   ||| Atomically writes up to the number of bytes in the bytestring
 255 |   ||| to the given file at the given file offset.
 256 |   |||
 257 |   ||| Notes: This will only work with seekable files but not with
 258 |   |||        arbitrary data streams such as pipes or sockets.
 259 |   |||        Also, it will not change the position of the open file description.
 260 |   export
 261 |   pwrite : ToBuf r => r -> OffT -> EPrim Bits32
 262 |   pwrite v off =
 263 |     case unsafeToBuf v of
 264 |       Left (CP sz ptr)        =>
 265 |         toSize $ prim__pwriteptr (fileDesc fd) ptr 0 sz off
 266 |       Right (BS n $ BV b o _) =>
 267 |         toSize $ prim__pwrite (fileDesc fd) (unsafeGetBuffer b) (cast o) (cast n) off
 268 | 
 269 | --------------------------------------------------------------------------------
 270 | -- File seeking
 271 | --------------------------------------------------------------------------------
 272 | 
 273 |   ||| Moves the file pointer to the given offset relative to the
 274 |   ||| `Whence` value.
 275 |   export %inline
 276 |   lseek : OffT -> Whence -> PrimIO OffT
 277 |   lseek offset whence =
 278 |     prim__lseek (fileDesc fd) offset (cast $ whenceCode whence)
 279 | 
 280 | --------------------------------------------------------------------------------
 281 | -- Duplicating file descriptors
 282 | --------------------------------------------------------------------------------
 283 | 
 284 |   ||| Duplicates the given open file descriptor.
 285 |   |||
 286 |   ||| The duplicate is guaranteed to be given the smallest available
 287 |   ||| file descriptor.
 288 |   export %inline
 289 |   dup : EPrim Fd
 290 |   dup = toFD $ prim__dup (fileDesc fd)
 291 | 
 292 |   ||| Duplicates the given open file descriptor.
 293 |   |||
 294 |   ||| The new file descriptor vill have the integer value of `fd2`.
 295 |   ||| This is an atomic operation that will close `fd2` if it is still open.
 296 |   export %inline
 297 |   dup2 : FileDesc b => (fd2 : b) -> EPrim Fd
 298 |   dup2 fd2 = toFD $ prim__dup2 (fileDesc fd) (fileDesc fd2)
 299 | 
 300 |   ||| Duplicates the given open file descriptor.
 301 |   |||
 302 |   ||| The new file descriptor vill have the integer value of `fd2`.
 303 |   ||| This is an atomic operation that will close `fd2` if it is still open.
 304 |   export %inline
 305 |   dupfd : (start : Bits32) -> EPrim Fd
 306 |   dupfd fd2 = toFD $ prim__dupfd (fileDesc fd) fd2
 307 | 
 308 | --------------------------------------------------------------------------------
 309 | -- Setting and getting file flags
 310 | --------------------------------------------------------------------------------
 311 | 
 312 |   ||| Gets the flags set at an open file descriptor.
 313 |   export
 314 |   getFlags : EPrim Flags
 315 |   getFlags t =
 316 |    let r # t := toF1 (prim__getFlags (fileDesc fd)) t
 317 |     in if r < 0 then E (inject $ fromNeg r) t else R (F $ cast r) t
 318 | 
 319 |   ||| Sets the flags of an open file descriptor.
 320 |   |||
 321 |   ||| Note: This replaces the currently set flags. See also `addFlags`.
 322 |   export %inline
 323 |   setFlags : Flags -> EPrim ()
 324 |   setFlags (F fs) = toUnit $ prim__setFlags (fileDesc fd) fs
 325 | 
 326 |   ||| Adds the given flags to the flags set for an open
 327 |   ||| file descriptor by ORing them with the currently set flags.
 328 |   export
 329 |   addFlags : Flags -> EPrim ()
 330 |   addFlags fs w =
 331 |     let R x w := getFlags w | E x w => E x w
 332 |      in setFlags (x <+> fs) w
 333 | 
 334 |   ||| Truncates a file to the given length.
 335 |   export %inline
 336 |   ftruncate : OffT -> EPrim ()
 337 |   ftruncate len = toUnit $ prim__ftruncate (fileDesc fd) len
 338 | 
 339 | ||| Truncates a file to the given length.
 340 | export %inline
 341 | truncate : String -> OffT -> EPrim ()
 342 | truncate f len = toUnit $ prim__truncate f len
 343 | 
 344 | ||| Atomically creates and opens a temporary, unique file.
 345 | export
 346 | mkstemp : String -> EPrim (Fd, String)
 347 | mkstemp f t =
 348 |   let pat     := "\{f}XXXXXX"
 349 |       len     := cast {to = Bits32} $ stringByteLength pat
 350 |       buf # t := toF1 (prim__newBuf $ cast len) t
 351 |       _   # t := ioToF1 (setString buf 0 pat) t
 352 |       R fd  t := toFD (prim__mkstemp buf) t | E x t => E x t
 353 |       nm  # t := fromBuf (B len buf) t
 354 |    in R (fd, nm) t
 355 | 
 356 | --------------------------------------------------------------------------------
 357 | -- Links
 358 | --------------------------------------------------------------------------------
 359 | 
 360 | ||| Creates a (hard) link to a file.
 361 | export %inline
 362 | link : (file, link : String) -> EPrim ()
 363 | link f l = toUnit $ prim__link f l
 364 | 
 365 | ||| Creates a (hard) link to a file.
 366 | export %inline
 367 | symlink : (file, link : String) -> EPrim ()
 368 | symlink f l = toUnit $ prim__symlink f l
 369 | 
 370 | ||| Deletes a (hard) link to a file.
 371 | |||
 372 | ||| If this is the last link to the file, the file is removed.
 373 | |||
 374 | ||| Note: Files with open file descriptors will only be deleted after the last
 375 | |||       open file descriptor is closed, but the file name will already
 376 | |||       disapper from the file system before that.
 377 | export %inline
 378 | unlink : (file : String) -> EPrim ()
 379 | unlink f = toUnit $ prim__unlink f
 380 | 
 381 | ||| Removes a file or (empty) directory calling `unlink` or `rmdir`
 382 | ||| internally.
 383 | export %inline
 384 | remove : (file : String) -> EPrim ()
 385 | remove f = toUnit $ prim__remove f
 386 | 
 387 | ||| Renames a file within a file system.
 388 | |||
 389 | ||| Note: This will fail if the two paths point to different file systems.
 390 | |||       In that case, the file needs to be copied from one FS to the other.
 391 | export %inline
 392 | rename : (file, link : String) -> EPrim ()
 393 | rename f l = toUnit $ prim__rename f l
 394 | 
 395 | ||| Returns the path of a file a symbolic link points to
 396 | |||
 397 | ||| This allocates a buffer of 4096 bytes for the byte array holding
 398 | ||| the result.
 399 | export %inline
 400 | readlink : FromBuf a => (file : String) -> EPrim a
 401 | readlink f = allocRead 4096 $ prim__readlink f
 402 | 
 403 | --------------------------------------------------------------------------------
 404 | -- Standard input and output
 405 | --------------------------------------------------------------------------------
 406 | 
 407 | export %inline
 408 | stdout : String -> PrimIO ()
 409 | stdout s = Errno.ignore $ fwrite {es = [Errno]} Stdout s
 410 | 
 411 | export %inline
 412 | stdoutLn : String -> PrimIO ()
 413 | stdoutLn = stdout . (++ "\n")
 414 | 
 415 | export %inline
 416 | prnt : Show a => a -> PrimIO ()
 417 | prnt = stdout . show
 418 | 
 419 | export %inline
 420 | prntLn : Show a => a -> PrimIO ()
 421 | prntLn = stdoutLn . show
 422 | 
 423 | export %inline
 424 | stderr : String -> PrimIO ()
 425 | stderr s = ignore $ fwrite {es = [Errno]} Stderr s
 426 | 
 427 | export %inline
 428 | stderrLn : String -> PrimIO ()
 429 | stderrLn = stderr . (++ "\n")
 430 |