Control.RIO.File

Reexports

Definitions

data FileErr : Type

Totality: total
Visibility: public export
Constructors:

ReadErr : File t -> FileError -> FileErr

WriteErr : File t -> FileError -> FileErr

DeleteErr : Path t -> FileError -> FileErr

LimitExceeded : File t -> Bits32 -> FileErr

CurDir : FileErr

ChangeDir : Path t -> FileErr

ListDir : Path t -> FileError -> FileErr

MkDir : Path t -> FileError -> FileErr

printErr : FileErr -> String

Totality: total
Visibility: export

record FS : Type

  Record representing a simple file system, where we can
  read from and write to files.

Totality: total
Visibility: public export
Constructor: 

MkFS : ((0 t : PathType) -> File t -> String -> IO (Either FileErr ())) -> ((0 t : PathType) -> File t -> String -> IO (Either FileErr ())) -> ((0 t : PathType) -> File t -> IO (Either FileErr ())) -> ((0 t : PathType) -> Path t -> IO (Either FileErr ())) -> ((0 t : PathType) -> Path t -> IO Bool) -> ((0 t : PathType) -> File t -> Bits32 -> IO (Either FileErr String)) -> IO (Either FileErr (Path Abs)) -> ((0 t : PathType) -> Path t -> IO (Either FileErr ())) -> ((0 t : PathType) -> Path t -> IO (Either FileErr (List Body))) -> ((0 t : PathType) -> Path t -> IO (Either FileErr ())) -> FS

Projections:

.append_ : FS -> (0 t : PathType) -> File t -> String -> IO (Either FileErr ())

  Appends the string to the file in question

.changeDir_ : FS -> (0 t : PathType) -> Path t -> IO (Either FileErr ())

  Change to the given directory

.curDir_ : FS -> IO (Either FileErr (Path Abs))

  Prints the current working directory.

.exists_ : FS -> (0 t : PathType) -> Path t -> IO Bool

  Checks if the given file exists in the file system

.listDir_ : FS -> (0 t : PathType) -> Path t -> IO (Either FileErr (List Body))

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

.mkDir_ : FS -> (0 t : PathType) -> Path t -> IO (Either FileErr ())

  Creates the given directory

.read_ : FS -> (0 t : PathType) -> File t -> Bits32 -> IO (Either FileErr String)

  This tries to read a file in whole, so we have to limit
  the acceptable file size, otherwise this might overflow
  the computer's memory if presented with an infinite stream
  such as `/dev/zero`

.removeDir_ : FS -> (0 t : PathType) -> Path t -> IO (Either FileErr ())

  Deletes the given directory.

.removeFile_ : FS -> (0 t : PathType) -> File t -> IO (Either FileErr ())

  Deletes the given file.

.write_ : FS -> (0 t : PathType) -> File t -> String -> IO (Either FileErr ())

  Writes the string to the file in question

.write_ : FS -> (0 t : PathType) -> File t -> String -> IO (Either FileErr ())

  Writes the string to the file in question

Totality: total
Visibility: public export

write_ : FS -> (0 t : PathType) -> File t -> String -> IO (Either FileErr ())

  Writes the string to the file in question

Totality: total
Visibility: public export

.append_ : FS -> (0 t : PathType) -> File t -> String -> IO (Either FileErr ())

  Appends the string to the file in question

Totality: total
Visibility: public export

append_ : FS -> (0 t : PathType) -> File t -> String -> IO (Either FileErr ())

  Appends the string to the file in question

Totality: total
Visibility: public export

.removeFile_ : FS -> (0 t : PathType) -> File t -> IO (Either FileErr ())

  Deletes the given file.

Totality: total
Visibility: public export

removeFile_ : FS -> (0 t : PathType) -> File t -> IO (Either FileErr ())

  Deletes the given file.

Totality: total
Visibility: public export

.removeDir_ : FS -> (0 t : PathType) -> Path t -> IO (Either FileErr ())

  Deletes the given directory.

Totality: total
Visibility: public export

removeDir_ : FS -> (0 t : PathType) -> Path t -> IO (Either FileErr ())

  Deletes the given directory.

Totality: total
Visibility: public export

.exists_ : FS -> (0 t : PathType) -> Path t -> IO Bool

  Checks if the given file exists in the file system

Totality: total
Visibility: public export

exists_ : FS -> (0 t : PathType) -> Path t -> IO Bool

  Checks if the given file exists in the file system

Totality: total
Visibility: public export

.read_ : FS -> (0 t : PathType) -> File t -> Bits32 -> IO (Either FileErr String)

  This tries to read a file in whole, so we have to limit
  the acceptable file size, otherwise this might overflow
  the computer's memory if presented with an infinite stream
  such as `/dev/zero`

Totality: total
Visibility: public export

read_ : FS -> (0 t : PathType) -> File t -> Bits32 -> IO (Either FileErr String)

  This tries to read a file in whole, so we have to limit
  the acceptable file size, otherwise this might overflow
  the computer's memory if presented with an infinite stream
  such as `/dev/zero`

Totality: total
Visibility: public export

.curDir_ : FS -> IO (Either FileErr (Path Abs))

  Prints the current working directory.

Totality: total
Visibility: public export

curDir_ : FS -> IO (Either FileErr (Path Abs))

  Prints the current working directory.

Totality: total
Visibility: public export

.changeDir_ : FS -> (0 t : PathType) -> Path t -> IO (Either FileErr ())

  Change to the given directory

Totality: total
Visibility: public export

changeDir_ : FS -> (0 t : PathType) -> Path t -> IO (Either FileErr ())

  Change to the given directory

Totality: total
Visibility: public export

.listDir_ : FS -> (0 t : PathType) -> Path t -> IO (Either FileErr (List Body))

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

Totality: total
Visibility: public export

listDir_ : FS -> (0 t : PathType) -> Path t -> IO (Either FileErr (List Body))

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

Totality: total
Visibility: public export

.mkDir_ : FS -> (0 t : PathType) -> Path t -> IO (Either FileErr ())

  Creates the given directory

Totality: total
Visibility: public export

mkDir_ : FS -> (0 t : PathType) -> Path t -> IO (Either FileErr ())

  Creates the given directory

Totality: total
Visibility: public export

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

  True if the given file or directory exists in the file system

Totality: total
Visibility: export

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

  True if the given file exists in the file system

Totality: total
Visibility: export

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

  True if the given file or directory does not exist in the file system

Totality: total
Visibility: export

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

  True if the given file does not exist in the file system

Totality: total
Visibility: export

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

  Writes the given string to a file.

Totality: total
Visibility: export

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

  Writes the given string to a file.

Totality: total
Visibility: export

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

  Reads a string from a file, the size of which must not
  exceed the given number of bytes.

Totality: total
Visibility: export

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

  Delete a file from the file system.

Totality: total
Visibility: export

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

  Delete a file from the file system.

Totality: total
Visibility: export

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

  Returns the current directory's path.

Totality: total
Visibility: export

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

  Changes the working directory

Totality: total
Visibility: export

inDir : FS => Has FileErr xs => Path t -> App xs a -> App xs a

  Runs an action in the given directory, changing back
  to the current directory afterwards.

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export

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

  Creates the given directory

Totality: total
Visibility: export

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

  Creates the given directory (including parent directories)

Totality: total
Visibility: export

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

  Creates the parent directory of the given file

Totality: total
Visibility: export

local : FS

  A computer's local file system

Totality: total
Visibility: export