0 | module System.File.Handle
 1 |
 2 | import public System.File.Error
 3 | import public System.File.Mode
 4 | import System.File.Support
 5 | import public System.File.Types
 6 |
 7 | %default total
 8 |
 9 | %foreign supportC "idris2_openFile"
10 |          supportNode "openFile"
11 | prim__open : String -> String -> PrimIO FilePtr
12 |
13 | %foreign supportC "idris2_closeFile"
14 |          "node:lambda:(fp) => require('fs').closeSync(fp.fd)"
15 | prim__close : FilePtr -> PrimIO ()
16 |
17 | ||| Open the given file name with the specified mode.
18 | |||
19 | ||| @ f the file name to open
20 | ||| @ m the mode to open the file with
21 | export
22 | openFile : HasIO io => (f : String) -> (m : Mode) -> io (Either FileError File)
23 | openFile f m
24 |     = do res <- primIO (prim__open f (modeStr m))
25 |          if prim__nullAnyPtr res /= 0
26 |             then returnError
27 |             else ok (FHandle res)
28 |
29 | ||| Close the given file handle.
30 | |||
31 | ||| @ fh the file handle to close
32 | export
33 | closeFile : HasIO io => (fh : File) -> io ()
34 | closeFile (FHandle f) = primIO (prim__close f)
35 |
36 | ||| Perform a given operation on successful file open
37 | ||| and ensure the file is closed afterwards or perform
38 | ||| a different operation if the file fails to open.
39 | export
40 | withFile : HasIO io => (filename : String) ->
41 |                        Mode ->
42 |                        (onError : FileError -> io a) ->
43 |                        (onOpen  : File -> io (Either a b)) ->
44 |                        io (Either a b)
45 | withFile filename mode onError onOpen =
46 |   do Right h <- openFile filename mode
47 |        | Left err => Left <$> onError err
48 |      res <- onOpen h
49 |      closeFile h
50 |      pure res
51 |