0 | module Control.RIO.File

  2 | import public Control.RIO.App

  3 | import public Data.FilePath.File

  4 | import public Data.DPair

  5 | import public Data.List

  6 | import Data.List1

  7 | import Data.IORef

  9 | import System.Directory

 10 | import System.File

 12 | %default total

 18 | public export

 19 | data FileErr : Type where

 20 |   ReadErr       : (path : File t) -> (error : FileError) -> FileErr

 22 |   WriteErr      : (path : File t) -> (error : FileError) -> FileErr

 24 |   DeleteErr     : (path : Path t) -> (error : FileError) -> FileErr

 26 |   LimitExceeded : (path : File t) -> (limit : Bits32) -> FileErr

 28 |   CurDir        : FileErr

 30 |   ChangeDir     : Path t -> FileErr

 32 |   ListDir       : Path t -> FileError -> FileErr

 34 |   MkDir         : Path t -> FileError -> FileErr

 37 | printErr : FileErr -> String

 38 | printErr (ReadErr p err) =

 39 |   "Error when reading from \"\{p}\": \{show err}"

 40 | printErr (WriteErr p err) =

 41 |   "Error when writing to \"\{p}\": \{show err}"

 42 | printErr (DeleteErr p err) =

 43 |   "Error when deleteing \"\{p}\": \{show err}"

 44 | printErr (LimitExceeded p _) =

 45 |   "Error when reading \"\{p}\": File size limit exceeded."

 46 | printErr CurDir = "Failed to get current directory"

 47 | printErr (ChangeDir p) = "Failed to change to directory \"\{p}\""

 48 | printErr (ListDir p err) =

 49 |   "Error when reading directory \"\{p}\": \{show err}."

 50 | printErr (MkDir p err) =

 51 |   "Error when creating directory \"\{p}\": \{show err}."

 59 | public export

 60 | record FS where

 61 |   constructor MkFS

 62 |   ||| Writes the string to the file in question

 63 |   write_  : (0 t : _) -> File t -> String -> IO (Either FileErr ())

 65 |   ||| Appends the string to the file in question

 66 |   append_ : (0 t : _) -> File t -> String -> IO (Either FileErr ())

 68 |   ||| Deletes the given file.

 69 |   removeFile_ : (0 t : _) -> File t -> IO (Either FileErr ())

 71 |   ||| Deletes the given directory.

 72 |   removeDir_ : (0 t : _) -> Path t -> IO (Either FileErr ())

 74 |   ||| Checks if the given file exists in the file system

 75 |   exists_ : (0 t : _) -> Path t -> IO Bool

 77 |   ||| This tries to read a file in whole, so we have to limit

 81 |   read_   : (0 t : _) -> File t -> Bits32 -> IO (Either FileErr String)

 83 |   ||| Prints the current working directory.

 84 |   curDir_ : IO (Either FileErr (Path Abs))

 86 |   ||| Change to the given directory

 87 |   changeDir_ : (0 t : _) -> Path t -> IO (Either FileErr ())

 89 |   ||| List entries in a directory (without `.` and `..`)

 90 |   listDir_ : (0 t : _) -> Path t -> IO (Either FileErr (List Body))

 92 |   ||| Creates the given directory

 93 |   mkDir_ : (0 t : _) -> Path t -> IO (Either FileErr ())

101 | exists : FS => Path t -> RIO x Bool

102 | exists path = liftIO (exists_ %search t path)

105 | export %inline

106 | fileExists : FS => File t -> RIO x Bool

107 | fileExists = exists . toPath

110 | export %inline

111 | missing : FS => Path t -> RIO x Bool

112 | missing = map not . exists

115 | export %inline

116 | fileMissing : FS => File t -> RIO x Bool

117 | fileMissing = missing . toPath

121 | write : FS => Has FileErr xs => File t -> String -> App xs ()

122 | write path str = injectIO (write_ %search t path str)

126 | append : FS => Has FileErr xs => File t -> String -> App xs ()

127 | append path str = injectIO (append_ %search t path str)

132 | read : FS => Has FileErr xs => File t -> Bits32 -> App xs String

133 | read path limit = injectIO (read_ %search t path limit)

137 | removeFile : FS => Has FileErr xs => File t -> App xs ()

138 | removeFile path = injectIO (removeFile_ %search t path)

142 | removeDir : FS => Has FileErr xs => Path t -> App xs ()

143 | removeDir path = injectIO (removeDir_ %search t path)

147 | curDir : FS => Has FileErr xs => App xs (Path Abs)

148 | curDir = injectIO $ curDir_ %search

152 | chgDir : FS => Has FileErr xs => (dir : Path t) -> App xs ()

153 | chgDir dir = injectIO (changeDir_ %search t dir)

158 | inDir :

159 |      {auto _ : FS}

160 |   -> {auto _ : Has FileErr xs}

161 |   -> (dir : Path t)

162 |   -> (act : App xs a)

163 |   -> App xs a

164 | inDir dir act = do

165 |   cur <- curDir

166 |   finally (chgDir cur) (chgDir dir >> act)

170 | listDir : FS => Has FileErr xs => Path t -> App xs (List Body)

171 | listDir dir = injectIO (listDir_ %search t dir)

175 | mkDir : FS => Has FileErr xs => Path t -> App xs ()

176 | mkDir dir = injectIO (mkDir_ %search t dir)

180 | mkDirP : FS => Has FileErr xs => Path t -> App xs ()

181 | mkDirP dir = go (parentDirs dir) >> mkDir dir

183 |   where

184 |     go : List (Path t) -> App xs ()

185 |     go []        = pure ()

186 |     go (x :: xs) = when !(missing x) $ go xs >> mkDir x

189 | export %inline

190 | mkParentDir : FS => Has FileErr xs => File t -> App xs ()

191 | mkParentDir = mkDirP . parent

197 | writeImpl : (0 t : _) -> File t -> String -> IO (Either FileErr ())

198 | writeImpl _ fp s = mapFst (WriteErr fp) <$> writeFile "\{fp}" s

200 | appendImpl : (0 t : _) -> File t -> String -> IO (Either FileErr ())

201 | appendImpl _ fp s = mapFst (WriteErr fp) <$> appendFile "\{fp}" s

203 | removeFileImpl : (0 t : _) -> File t -> IO (Either FileErr ())

204 | removeFileImpl _ fp = mapFst (DeleteErr $ toPath fp) <$> removeFile "\{fp}"

206 | removeDirImpl : (0 t : _) -> Path t -> IO (Either FileErr ())

207 | removeDirImpl _ fp = Right <$> removeDir "\{fp}"

209 | readImpl : (0 t : _) -> File t -> Bits32 -> IO (Either FileErr String)

210 | readImpl _ fp limit = do

211 |   Right s <- withFile "\{fp}" Read pure fileSize

212 |     | Left err => pure (Left $ ReadErr fp err)

213 |   case s <= 0 of

214 |     True => pure (Right "")

215 |     False => case s <= cast limit of

216 |       True  => assert_total $ do

217 |         Left err <- readFile "\{fp}" | Right s => pure (Right s)

218 |         pure (Left $ ReadErr fp err)

220 |       False => pure (Left $ LimitExceeded fp limit)

222 | curDirImpl : IO (Either FileErr (Path Abs))

223 | curDirImpl = do

224 |   Just s <- currentDir | Nothing => pure (Left CurDir)

225 |   case fromString {ty = FilePath} s of

226 |     (FP p@(PAbs {})) => pure (Right p)

227 |     _                => pure (Left CurDir)

229 | changeDirImpl : (0 t : _) -> Path t -> IO (Either FileErr ())

230 | changeDirImpl _ dir = do

231 |   True <- changeDir "\{dir}" | False => pure (Left $ ChangeDir dir)

232 |   pure $ Right ()

234 | listDirImpl : (0 t : _) -> Path t -> IO (Either FileErr $ List Body)

235 | listDirImpl _ dir = bimap (ListDir dir) (mapMaybe parse) <$> listDir "\{dir}"

237 | mkDirImpl : (0 t : _) -> Path t -> IO (Either FileErr ())

238 | mkDirImpl _ dir = mapFst (MkDir dir) <$> createDir "\{dir}"

242 | local : FS

243 | local =

244 |   MkFS

245 |     { write_      = writeImpl

246 |     , append_     = appendImpl

247 |     , removeFile_ = removeFileImpl

248 |     , removeDir_  = removeDirImpl

249 |     , exists_     = \_,fp => exists "\{fp}"

250 |     , read_       = readImpl

251 |     , curDir_     = curDirImpl

252 |     , changeDir_  = changeDirImpl

253 |     , listDir_    = listDirImpl

254 |     , mkDir_      = mkDirImpl

255 |     }