
   0 | module System.Posix.File
   1 | 
   2 | import Data.Bits
   3 | import System.Posix.File.Prim as P
   4 | 
   5 | import public Control.Monad.Resource
   6 | import public Data.Buffer
   7 | import public Data.Buffer.Core
   8 | import public Data.ByteString
   9 | import public Data.ByteVect
  10 | 
  11 | import public Data.C.Ptr
  12 | 
  13 | import public System.Posix.Errno
  14 | import public System.Posix.File.FileDesc
  15 | import public System.Posix.File.Flags
  16 | import public System.Posix.File.ReadRes
  17 | import public System.Posix.File.Whence
  18 | 
  19 | %default total
  20 | 
  21 | --------------------------------------------------------------------------------
  22 | -- File Operations
  23 | --------------------------------------------------------------------------------
  24 | 
  25 | ||| Tries to open a file with the given flags and mode.
  26 | export %inline
  27 | openFile : Has Errno es => EIO1 f => String -> Flags -> Mode -> f es Fd
  28 | openFile p f m = elift1 (P.openFile p f m)
  29 | 
  30 | ||| Convenience version of `close` that fails silently.
  31 | export %inline
  32 | close' : FileDesc a => HasIO io => (fd : a) -> io ()
  33 | close' fd = primIO (P.close' fd)
  34 | 
  35 | export %inline
  36 | ELift1 World f => FileDesc a => Resource f a where
  37 |   cleanup fd = lift1 {s = World} $ ffi (P.close' fd)
  38 | 
  39 | parameters {auto fid : FileDesc a}
  40 |            (fd       : a)
  41 |            {auto has : Has Errno es}
  42 |            {auto eoi : EIO1 f}
  43 | 
  44 |   ||| Closes a file descriptor.
  45 |   export %inline
  46 |   close : f es ()
  47 |   close = elift1 (P.close fd)
  48 | 
  49 |   ||| Reads at most `n` bytes from a file into a pre-allocated pointer.
  50 |   export %inline
  51 |   readPtr : (0 r : Type) -> FromPtr r => CPtr -> f es r
  52 |   readPtr r p = elift1 (P.readPtr fd r p)
  53 | 
  54 |   ||| Reads at most `n` bytes from a file into a pre-allocated pointer.
  55 |   export %inline
  56 |   readPtrRes : (0 r : Type) -> FromPtr r => CPtr -> f es (ReadRes r)
  57 |   readPtrRes r p = elift1 (P.readPtrRes fd r p)
  58 | 
  59 |   ||| Reads at most `n` bytes from a file into a bytestring.
  60 |   export %inline
  61 |   read : (0 r : Type) -> FromBuf r => (n : Bits32) -> f es r
  62 |   read r n = elift1 (P.read fd r n)
  63 | 
  64 |   ||| Reads data from a file into a preallocated buffer
  65 |   export %inline
  66 |   readRaw : Buf -> f es EMBuffer
  67 |   readRaw buf = elift1 (P.readRaw fd buf)
  68 | 
  69 |   ||| Reads at most `n` bytes from a file into a bytestring.
  70 |   |||
  71 |   ||| This is a more convenient version of `read` that gives detailed
  72 |   ||| information about why a read might fail. It is especially useful
  73 |   ||| when reading from - possibly non-blocking - pipes or sockets.
  74 |   export %inline
  75 |   readres : (0 r : Type) -> FromBuf r => (n : Bits32) -> f es (ReadRes r)
  76 |   readres r n = elift1 (P.readres fd r n)
  77 | 
  78 |   ||| Atomically reads up to `n` bytes from the given file at
  79 |   ||| the given file offset.
  80 |   |||
  81 |   ||| Notes: This will only work with seekable files but not with
  82 |   |||        arbitrary data streams such as pipes or sockets.
  83 |   |||        Also, it will not change the position of the open file description.
  84 |   export %inline
  85 |   pread : (0 r : Type) -> FromBuf r => (n : Bits32) -> OffT -> f es r
  86 |   pread r n o = elift1 (P.pread fd r n o)
  87 | 
  88 |   ||| Writes up to the number of bytes in the bytestring
  89 |   ||| to the given file.
  90 |   |||
  91 |   ||| Note: This is an atomic operation if `fd` is a regular file that
  92 |   |||       was opened in "append" mode (with the `O_APPEND` flag).
  93 |   export %inline
  94 |   write : ToBuf r => r -> f es Bits32
  95 |   write v = elift1 (P.write fd v)
  96 | 
  97 |   ||| Iteratively writes a value to a file descriptor making sure
  98 |   ||| that the whole value is written. Use this, if a single call to
  99 |   ||| `write` might not write the complete data (for instance, when
 100 |   ||| writing to a pipe or socket).
 101 |   export %inline
 102 |   fwrite : ToBuf r => r -> f es ()
 103 |   fwrite v = elift1 (P.fwrite fd v)
 104 | 
 105 |   ||| Atomically writes up to the number of bytes in the bytestring
 106 |   ||| to the given file at the given file offset.
 107 |   |||
 108 |   ||| Notes: This will only work with seekable files but not with
 109 |   |||        arbitrary data streams such as pipes or sockets.
 110 |   |||        Also, it will not change the position of the open file description.
 111 |   export
 112 |   pwrite : ToBuf r => r -> OffT -> f es Bits32
 113 |   pwrite bs o = elift1 (P.pwrite fd bs o)
 114 | 
 115 | 
 116 | --------------------------------------------------------------------------------
 117 | -- File seeking
 118 | --------------------------------------------------------------------------------
 119 | 
 120 | ||| Moves the file pointer to the given offset relative to the
 121 | ||| `Whence` value.
 122 | export %inline
 123 | lseek : FileDesc a => HasIO io => (fd : a) -> OffT -> Whence -> io OffT
 124 | lseek fd offset whence = primIO (P.lseek fd offset whence)
 125 | 
 126 | --------------------------------------------------------------------------------
 127 | -- Duplicating file descriptors
 128 | --------------------------------------------------------------------------------
 129 | 
 130 | parameters {auto fid : FileDesc a}
 131 |            (fd       : a)
 132 |            {auto has : Has Errno es}
 133 |            {auto eoi : EIO1 f}
 134 | 
 135 |   ||| Duplicates the given open file descriptor.
 136 |   |||
 137 |   ||| The duplicate is guaranteed to be given the smallest available
 138 |   ||| file descriptor.
 139 |   export %inline
 140 |   dup : f es Fd
 141 |   dup = elift1 (P.dup fd)
 142 | 
 143 |   ||| Duplicates the given open file descriptor.
 144 |   |||
 145 |   ||| The new file descriptor vill have the integer value of `fd2`.
 146 |   ||| This is an atomic operation that will close `fd2` if it is still open.
 147 |   export %inline
 148 |   dup2 : FileDesc b => (fd2 : b) -> f es Fd
 149 |   dup2 fd2 = elift1 (P.dup2 fd fd2)
 150 | 
 151 |   ||| Duplicates the given open file descriptor.
 152 |   |||
 153 |   ||| The new file descriptor vill have the integer value of `fd2`.
 154 |   ||| This is an atomic operation that will close `fd2` if it is still open.
 155 |   export %inline
 156 |   dupfd : (start : Bits32) -> f es Fd
 157 |   dupfd start = elift1 (P.dupfd fd start)
 158 | 
 159 | --------------------------------------------------------------------------------
 160 | -- Setting and getting file flags
 161 | --------------------------------------------------------------------------------
 162 | 
 163 |   ||| Gets the flags set at an open file descriptor.
 164 |   export
 165 |   getFlags : f es Flags
 166 |   getFlags = elift1 (P.getFlags fd)
 167 | 
 168 |   ||| Sets the flags of an open file descriptor.
 169 |   |||
 170 |   ||| Note: This replaces the currently set flags. See also `addFlags`.
 171 |   export %inline
 172 |   setFlags : Flags -> f es ()
 173 |   setFlags fs = elift1 (P.setFlags fd fs)
 174 | 
 175 |   ||| Adds the given flags to the flags set for an open
 176 |   ||| file descriptor by ORing them with the currently set flags.
 177 |   export
 178 |   addFlags : Flags -> f es ()
 179 |   addFlags fs = elift1 (P.addFlags fd fs)
 180 | 
 181 |   ||| Truncates a file to the given length.
 182 |   export %inline
 183 |   ftruncate : OffT -> f es ()
 184 |   ftruncate o = elift1 (P.ftruncate fd o)
 185 | 
 186 | ||| Truncates a file to the given length.
 187 | export %inline
 188 | truncate : Has Errno es => EIO1 f => String -> OffT -> f es ()
 189 | truncate s o = elift1 (P.truncate s o)
 190 | 
 191 | ||| Atomically creates and opens a temporary, unique file.
 192 | export
 193 | mkstemp : Has Errno es => EIO1 f => String -> f es (Fd, String)
 194 | mkstemp s = elift1 (P.mkstemp s)
 195 | 
 196 | --------------------------------------------------------------------------------
 197 | -- Links
 198 | --------------------------------------------------------------------------------
 199 | 
 200 | ||| Creates a (hard) link to a file.
 201 | export %inline
 202 | link : Has Errno es => EIO1 f => (file, link : String) -> f es ()
 203 | link f l = elift1 (P.link f l)
 204 | 
 205 | ||| Creates a (hard) link to a file.
 206 | export %inline
 207 | symlink : Has Errno es => EIO1 f => (file, link : String) -> f es ()
 208 | symlink f l = elift1 (P.symlink f l)
 209 | 
 210 | ||| Deletes a (hard) link to a file.
 211 | |||
 212 | ||| If this is the last link to the file, the file is removed.
 213 | |||
 214 | ||| Note: Files with open file descriptors will only be deleted after the last
 215 | |||       open file descriptor is closed, but the file name will already
 216 | |||       disapper from the file system before that.
 217 | export %inline
 218 | unlink : Has Errno es => EIO1 f => (file : String) -> f es ()
 219 | unlink file = elift1 (P.unlink file)
 220 | 
 221 | ||| Removes a file or (empty) directory calling `unlink` or `rmdir`
 222 | ||| internally.
 223 | export %inline
 224 | remove : Has Errno es => EIO1 f => (file : String) -> f es ()
 225 | remove file = elift1 (P.remove file)
 226 | 
 227 | ||| Renames a file within a file system.
 228 | |||
 229 | ||| Note: This will fail if the two paths point to different file systems.
 230 | |||       In that case, the file needs to be copied from one FS to the other.
 231 | export %inline
 232 | rename : Has Errno es => EIO1 f => (file, link : String) -> f es ()
 233 | rename f l = elift1 (P.rename f l)
 234 | 
 235 | ||| Returns the path of a file a symbolic link points to
 236 | |||
 237 | ||| This allocates a buffer of 4096 bytes for the byte array holding
 238 | ||| the result.
 239 | export %inline
 240 | readlink : Has Errno es => EIO1 f => (file : String) -> f es ByteString
 241 | readlink file = elift1 (P.readlink file)
 242 | 
 243 | --------------------------------------------------------------------------------
 244 | -- Standard input and output
 245 | --------------------------------------------------------------------------------
 246 | 
 247 | parameters {auto hio : HasIO io}
 248 | 
 249 |   export %inline
 250 |   stdout : String -> io ()
 251 |   stdout = primIO . P.stdout
 252 | 
 253 |   export %inline
 254 |   stdoutLn : String -> io ()
 255 |   stdoutLn = primIO . P.stdoutLn
 256 | 
 257 |   export %inline
 258 |   prnt : Show a => a -> io ()
 259 |   prnt = primIO . P.prnt
 260 | 
 261 |   export %inline
 262 |   prntLn : Show a => a -> io ()
 263 |   prntLn = primIO . P.prntLn
 264 | 
 265 |   export %inline
 266 |   stderr : String -> io ()
 267 |   stderr = primIO . P.stderr
 268 | 
 269 |   export %inline
 270 |   stderrLn : String -> io ()
 271 |   stderrLn = primIO . P.stderrLn
 272 |