0 | module IO.Async.File
 1 |
 2 | import public System.Posix.File
 3 | import public IO.Async.Posix
 4 | import System
 5 | import System.File.Error
 6 |
 7 | %default total
 8 |
 9 | ||| Opaque flag indicating that stdin has been set to
10 | ||| raw input mode.
11 | export
12 | data RawMode = RM
13 |
14 | export
15 | ELift1 World f => Resource f RawMode where
16 |   cleanup rm = lift1 (ioToF1 resetRawMode)
17 |
18 | ||| Converts a `System.File.Error.FileError` to a POSIX error code
19 | export
20 | toErrno : FileError -> Errno
21 | toErrno (GenericFileError i) = EN (cast i)
22 | toErrno FileReadError        = EPERM
23 | toErrno FileWriteError       = EPERM
24 | toErrno FileNotFound         = ENOENT
25 | toErrno PermissionDenied     = EACCES
26 | toErrno FileExists           = EEXIST
27 |
28 | parameters {auto has : Has Errno es}
29 |
30 |   ||| Wraps an `IO` action from `System.File` in base by converting
31 |   ||| file errors to POSIX error codes.
32 |   export
33 |   fileIO : IO (Either FileError a) -> Async e es a
34 |   fileIO io =
35 |     liftIO io >>= \case
36 |       Left x => throw (toErrno x)
37 |       Right v => pure v
38 |
39 |   ||| Enables raw (unbuffered) input mode for stdin.
40 |   |||
41 |   ||| To make sure this is properly reset when the application ends,
42 |   ||| wrap this in a call to `use` or `use1`:
43 |   |||
44 |   ||| ```idris
45 |   ||| use1 rawMode $ \_ => your_code
46 |   ||| ```
47 |   export
48 |   rawMode : Async e es RawMode
49 |   rawMode = fileIO enableRawMode $> RM
50 |
51 |   export %inline
52 |   withFile : String -> Flags -> Mode -> (Fd -> Async e es a) -> Async e es a
53 |   withFile pth fs m = use1 (openFile pth fs m)
54 |
55 |   ||| Reads up to the given number of bytes from a file.
56 |   export
57 |   readFile : (0 r : Type) -> FromBuf r => String -> Bits32 -> Async e es r
58 |   readFile r pth buf = withFile pth O_RDONLY 0 $ \fd => read fd r buf
59 |
60 |   ||| Writes a value to an existing file.
61 |   export
62 |   writeFile : ToBuf r => String -> r -> Async e es ()
63 |   writeFile pth v = withFile pth O_WRONLY 0 $ \fd => fwrite fd v
64 |
65 |   ||| Writes a value to a file, creating it, if it does not yet exist.
66 |   export
67 |   createFile : ToBuf r => String -> Mode -> r -> Async e es ()
68 |   createFile pth m v = withFile pth create m $ \fd => fwrite fd v
69 |
70 |   ||| Appends a value to a file.
71 |   |||
72 |   ||| The file is created if it does not yet exist.
73 |   export
74 |   appendFile : ToBuf r => String -> Mode -> r -> Async e es ()
75 |   appendFile pth m v = withFile pth append m $ \fd => fwrite fd v
76 |