0 | ||| Directory access and handling.
  1 | module System.Directory
  2 |
  3 | import System.Errno
  4 | import public System.File
  5 | import System.FFI
  6 |
  7 | %default total
  8 |
  9 | public export
 10 | DirPtr : Type
 11 | DirPtr = AnyPtr
 12 |
 13 | ||| Shorthand for referring to the C support library
 14 | |||
 15 | ||| @ fn the function name to refer to in the C support library
 16 | supportC : (fn : String) -> String
 17 | supportC fn = "C:\{fn}, libidris2_support, idris_directory.h"
 18 |
 19 | ||| Shorthand for referring to the Node system support library
 20 | |||
 21 | ||| @ fn the function name to refer to in the js/system_support.js file
 22 | supportNode : (fn : String) -> String
 23 | supportNode fn = "node:support:\{fn},support_system_directory"
 24 |
 25 | ok : HasIO io => a -> io (Either FileError a)
 26 | ok x = pure (Right x)
 27 |
 28 | %foreign supportC "idris2_currentDirectory"
 29 |          "node:lambda:()=>process.cwd()"
 30 | prim__currentDir : PrimIO (Ptr String)
 31 |
 32 | %foreign supportC "idris2_changeDir"
 33 |          supportNode "changeDir"
 34 | prim__changeDir : String -> PrimIO Int
 35 |
 36 | %foreign supportC "idris2_createDir"
 37 |          supportNode "createDir"
 38 | prim__createDir : String -> PrimIO Int
 39 |
 40 | %foreign supportC "idris2_openDir"
 41 |          supportNode "openDir"
 42 | prim__openDir : String -> PrimIO DirPtr
 43 |
 44 | %foreign supportC "idris2_closeDir"
 45 |          supportNode "closeDir"
 46 | prim__closeDir : DirPtr -> PrimIO ()
 47 |
 48 | %foreign supportC "idris2_removeDir"
 49 |          supportNode "removeDir"
 50 | prim__removeDir : String -> PrimIO ()
 51 |
 52 | %foreign supportC "idris2_nextDirEntry"
 53 |          supportNode "dirEntry"
 54 | prim__dirEntry : DirPtr -> PrimIO (Ptr String)
 55 |
 56 | ||| Data structure for managing the pointer to a directory.
 57 | export
 58 | data Directory : Type where
 59 |      MkDir : DirPtr -> Directory
 60 |
 61 | ||| Try to create a directory at the specified path.
 62 | export
 63 | createDir : HasIO io => String -> io (Either FileError ())
 64 | createDir dir
 65 |     = do res <- primIO (prim__createDir dir)
 66 |          if res == 0
 67 |             then ok ()
 68 |             else returnError
 69 |
 70 | ||| Change the current working directory to the specified path. Returns whether
 71 | ||| the operation succeeded.
 72 | export
 73 | changeDir : HasIO io => String -> io Bool
 74 | changeDir dir
 75 |     = do ok <- primIO (prim__changeDir dir)
 76 |          pure (ok == 0)
 77 |
 78 | ||| Get the absolute path of the current working directory. Returns `Nothing` if
 79 | ||| an error occurred.
 80 | export
 81 | currentDir : HasIO io => io (Maybe String)
 82 | currentDir
 83 |     = do res <- primIO prim__currentDir
 84 |          if prim__nullPtr res /= 0
 85 |             then pure Nothing
 86 |             else do let s = prim__getString res
 87 |                     free $ prim__forgetPtr res
 88 |                     pure (Just s)
 89 |
 90 | ||| Try to open the directory at the specified path.
 91 | export
 92 | openDir : HasIO io => String -> io (Either FileError Directory)
 93 | openDir d
 94 |     = do res <- primIO (prim__openDir d)
 95 |          if prim__nullAnyPtr res /= 0
 96 |             then returnError
 97 |             else ok (MkDir res)
 98 |
 99 | ||| Close the given `Directory`.
100 | export
101 | closeDir : HasIO io => Directory -> io ()
102 | closeDir (MkDir d) = primIO (prim__closeDir d)
103 |
104 | ||| Remove the directory at the specified path.
105 | ||| If the directory is not empty, this operation fails.
106 | export
107 | removeDir : HasIO io => String -> io ()
108 | removeDir dirName = primIO (prim__removeDir dirName)
109 |
110 | ||| Get the next entry in the `Directory`, omitting the '.' and '..' entries.
111 | export
112 | nextDirEntry : HasIO io => Directory -> io (Either FileError (Maybe String))
113 | nextDirEntry (MkDir d)
114 |     = do res <- primIO (prim__dirEntry d)
115 |          if prim__nullPtr res /= 0
116 |             then if !(getErrno) /= 0
117 |                     then returnError
118 |                     else pure $ Right Nothing
119 |             else do let n = prim__getString res
120 |                     if n == "." || n == ".."
121 |                        then assert_total $ nextDirEntry (MkDir d)
122 |                        else pure $ Right (Just n)
123 |
124 | ||| Get a list of all the entries in the `Directory`, excluding the '.' and '..'
125 | ||| entries.
126 | collectDir : HasIO io => Directory -> io (Either FileError (List String))
127 | collectDir d
128 |     = liftIO $ do let (>>=) : (IO . Either e) a -> (a -> (IO . Either e) b) -> (IO . Either e) b
129 |                       (>>=) = Prelude.(>>=) @{Monad.Compose {m = IO} {t = Either e}}
130 |                   Just n <- nextDirEntry d
131 |                     | Nothing => pure $ Right []
132 |                   ns <- assert_total $ collectDir d
133 |                   pure $ Right (n :: ns)
134 |
135 | ||| Get a list of all the entries in the directory at the specified path,
136 | ||| excluding the '.' and '..' entries.
137 | |||
138 | ||| @ name the directory to list
139 | export
140 | listDir : HasIO io => (name : String) -> io (Either FileError (List String))
141 | listDir name = do Right d <- openDir name
142 |                     | Left e => pure $ Left e
143 |                   ns <- collectDir d
144 |                   ignore <- closeDir d
145 |                   pure $ ns
146 |