std.filesystem

For files by path: reading one, writing one, listing a directory, removing one, making one read-only, copying one, moving one, putting one in place of another; what a path is, its status and its mode; a temporary directory or file. A file open, read and written a piece at a time, is std.file’s.

import co
import exception
import std.filesystem
import std.path

-- | a file's text, with a line added
appended : {e : HFunctor}
         -> {{disk : filesystem <: e}}
         -> {{ex : exception FileError <: e}}
         -> Path
         -> String
         -> Co e Unit
appended path line = do
  text <- readFile path
  writeFile path (text ^ line ^ "\n")

-- | the files under a directory, and under those in it
filesUnder : {e : HFunctor}
           -> {{disk : filesystem <: e}}
           -> {{ex : exception FileError <: e}}
           -> Path
           -> Co e (List Path)
filesUnder dir = do
  lists <- for p in (<- readDirectory dir) do
    if <- isDirectory p then filesUnder p else pure [p]
  pure (List.concatMap (\ps -> ps) lists)

A path is std.path’s Path; a string is taken as one where one is expected (readFile "notes.txt", where std.path is imported), read as the system the program runs on writes a path. The system is given it, and a path it gives back (realPath, temporaryDirectory) is read, in its own style, std.path’s native.

An open file, a File, is the host’s own thing: std.file opens it, reads and writes it, and closes it, by this module’s effect.

An operation on a path that fails throws why, a FileError, over the exception effect: the system’s errno, its name, what the system says of it, and the path it was said of. Whether something is at a path (exists, isFile, isDirectory, kindAt) is asked without a throw.

File

data File

A file open, the host’s own (a foreign value; no value of the program has it): std.file’s open gives one.

FileError

type FileError =
  { code : Int
  , name : String
  , message : String
  , path : String
  , other : Maybe String = Nothing
  }

Why an operation failed: the system’s errno, its name (ENOENT, EACCES; the same on every system, where the number is not), what the system says of it, and the path the failing call was given, as the program wrote it — in a tree (copy, remove, readOnly), the one inside it that failed; an open file’s, the path it was opened by (<stdin>, <stdout>, <stderr>, a standard stream’s). Where the call took two paths (move and replace’s rename), the errno says not which is at fault: path is the first, other the second; else other is Nothing.

Kind

data Kind = Regular | Directory | Link | Other

What a path is: a regular file, a directory, a link (where links are not followed), or something else — a pipe, a device, a socket.

Status

type Status = { kind : Kind, size : Int, modified : Int, mode : Int }

What the system says of a file: its kind, its size in bytes, when it was last modified (nanoseconds since the epoch, as precise as the system keeps it), and its mode (its permission bits, 0o755 for rwxr-xr-x; on Windows, 0o555 read-only or 0o666 not).

FilesystemF

data FilesystemF (m : Type -> Type) x
  = ReadFile String (Either FileError String -> x)
  | WriteFile String String (Either FileError Unit -> x)
  | MakeDirectory String (Either FileError Unit -> x)
  | ReadDirectory String (Either FileError (List String) -> x)
  | Remove String (Either FileError Unit -> x)
  | ReadOnly String (Either FileError Unit -> x)
  | Copy String String (Either FileError Unit -> x)
  | Move String String (Either FileError Unit -> x)
  | Replace String String (Either FileError Unit -> x)
  | Writable String (Either FileError Unit -> x)
  | PathStatus String Bool (Either FileError Status -> x)
  | SetMode String Int (Either FileError Unit -> x)
  | RealPath String (Either FileError String -> x)
  | ReadLink String (Either FileError String -> x)
  | TemporaryDirectory String (Either FileError String -> x)
  | TemporaryFile String (Either FileError String -> x)
  | OpenPath String Int Bool Bool Bool Int (Either FileError File -> x)
  | Standard Int (File -> x)
  | StandardPort Int (File -> x)
  | ReadChunk File Int (Either FileError Bytes -> x)
  | ReadLine File (Either FileError (Maybe String) -> x)
  | WriteBytes File Bytes (Either FileError Unit -> x)
  | WriteString File String (Either FileError Unit -> x)
  | Seek File Int Int (Either FileError Int -> x)
  | FileStatus File (Either FileError Status -> x)
  | CloseFile File (Either FileError Unit -> x)

filesystem

filesystem : HFunctor

For files and directories by path: whole files read and written, directories listed and made, paths removed, copied, moved, their status and mode, temporary files; and the operations std.file’s open files are read and written by.

readFile

readFile : {e : HFunctor}
         -> {{ev : filesystem <: e}}
         -> {{ex : exception FileError <: e}}
         -> Path
         -> Co e String

A file’s text: in any effect the files are in, by the evidence; where it cannot be read, why is thrown.

readBytes

readBytes : {e : HFunctor}
          -> {{ev : filesystem <: e}}
          -> {{ex : exception FileError <: e}}
          -> Path
          -> Co e Bytes

A file’s bytes, as they are (readFile’s text, as Bytes): where it cannot be read, why is thrown.

writeFile

writeFile : {e : HFunctor}
          -> {{ev : filesystem <: e}}
          -> {{ex : exception FileError <: e}}
          -> Path
          -> String
          -> Co e Unit

Write a file (a new one, or over what it had).

makeDirectory

makeDirectory : {e : HFunctor}
              -> {{ev : filesystem <: e}}
              -> {{ex : exception FileError <: e}}
              -> Path
              -> Co e Unit

Make a directory, and the ones above it, where there is none (a file there is none: EEXIST).

readDirectory

readDirectory : {e : HFunctor}
              -> {{ev : filesystem <: e}}
              -> {{ex : exception FileError <: e}}
              -> Path
              -> Co e (List Path)

What a directory holds, each in it (path / name), sorted by name.

remove

remove : {e : HFunctor}
       -> {{ev : filesystem <: e}}
       -> {{ex : exception FileError <: e}}
       -> Path
       -> Co e Unit

Remove a file, or a directory and all it holds (read-only or not): where nothing is, nothing is done.

readOnly

readOnly : {e : HFunctor}
         -> {{ev : filesystem <: e}}
         -> {{ex : exception FileError <: e}}
         -> Path
         -> Co e Unit

Make a file, or a directory and all it holds, read-only.

writable

writable : {e : HFunctor}
         -> {{ev : filesystem <: e}}
         -> {{ex : exception FileError <: e}}
         -> Path
         -> Co e Unit

Make a file, or a directory and all it holds, writable by its owner again (readOnly undone).

copy

copy : {e : HFunctor}
     -> {{ev : filesystem <: e}}
     -> {{ex : exception FileError <: e}}
     -> Path
     -> Path
     -> Co e Unit

Copy a file, or a directory and all it holds, to to, where nothing is (links followed, modes kept; something there: EEXIST).

move

move : {e : HFunctor}
     -> {{ev : filesystem <: e}}
     -> {{ex : exception FileError <: e}}
     -> Path
     -> Path
     -> Co e Unit

Move a file, or a directory, to to, on the same disk, where nothing is (something there: EEXIST).

replace

replace : {e : HFunctor}
        -> {{ev : filesystem <: e}}
        -> {{ex : exception FileError <: e}}
        -> Path
        -> Path
        -> Co e Unit

Move a file to to, on the same disk, in place of the file there if there is one, at once: what opens to meanwhile opens the one or the other, never neither nor a part of either, and what had the one open keeps it (on Windows, not in place of a program running).

pathStatus

pathStatus : {e : HFunctor}
           -> {{ev : filesystem <: e}}
           -> {{ex : exception FileError <: e}}
           -> Path
           -> Co e Status

What the system says of the file at a path, links followed.

linkStatus

linkStatus : {e : HFunctor}
           -> {{ev : filesystem <: e}}
           -> {{ex : exception FileError <: e}}
           -> Path
           -> Co e Status

What the system says of the file at a path, a link itself where there is one (its kind Link), not what it links to.

kindAt

kindAt : {e : HFunctor} -> {{ev : filesystem <: e}} -> Path -> Co e (Maybe Kind)

What is at a path, links followed: Nothing where nothing is (or a link to nothing).

isRegular

isRegular : Kind -> Bool

isDirectoryKind

isDirectoryKind : Kind -> Bool

exists

exists : {e : HFunctor} -> {{ev : filesystem <: e}} -> Path -> Co e Bool

Whether something is at a path, links followed.

isFile

isFile : {e : HFunctor} -> {{ev : filesystem <: e}} -> Path -> Co e Bool

Whether a regular file is at a path, links followed.

isDirectory

isDirectory : {e : HFunctor} -> {{ev : filesystem <: e}} -> Path -> Co e Bool

Whether a directory is at a path, links followed.

setMode

setMode : {e : HFunctor}
        -> {{ev : filesystem <: e}}
        -> {{ex : exception FileError <: e}}
        -> Path
        -> Int
        -> Co e Unit

The mode of the file at a path set (chmod): its permission bits, 0o755 for rwxr-xr-x (on Windows, only whether the owner may write it is kept).

makeExecutable

makeExecutable : {e : HFunctor}
               -> {{ev : filesystem <: e}}
               -> {{ex : exception FileError <: e}}
               -> Path
               -> Co e Unit

A file made executable by whoever may read it (chmod +x, as the umask has it: rw-r--r-- becomes rwxr-xr-x).

realPath

realPath : {e : HFunctor}
         -> {{ev : filesystem <: e}}
         -> {{ex : exception FileError <: e}}
         -> Path
         -> Co e Path

A path with its links resolved, and . and .. gone: absolute, of something that is there.

readLink

readLink : {e : HFunctor}
         -> {{ev : filesystem <: e}}
         -> {{ex : exception FileError <: e}}
         -> Path
         -> Co e Path

What the link at a path says, as it was written: where it points, perhaps from the directory it is in, perhaps to nothing (a path that is no link: EINVAL).

temporaryDirectory

temporaryDirectory : {e : HFunctor}
                   -> {{ev : filesystem <: e}}
                   -> {{ex : exception FileError <: e}}
                   -> String
                   -> Co e Path

A directory of its own, new and empty, where the system keeps temporary ones (TMPDIR, else /tmp; on Windows GetTempPath), its name prefix and six letters: its path. It is the program’s to remove.

temporaryFile

temporaryFile : {e : HFunctor}
              -> {{ev : filesystem <: e}}
              -> {{ex : exception FileError <: e}}
              -> String
              -> Co e Path

A file of its own, new and empty, where the system keeps temporary ones, its name prefix and six letters: its path, to be opened by std.file’s open. It is the program’s to remove.

Visit

data Visit = Descend | SkipDirectory | Stop

What a walk does after a path is visited: go into it (a directory; for any other, go on), not go into it (a directory; for any other, skip what is left of the directory it is in), or end.

walk

walk : {e : HFunctor}
     -> {{ev : filesystem <: e}}
     -> {{ex : exception FileError <: e}}
     -> Path
     -> (Path -> Kind -> Co e Visit)
     -> Co e Unit

Each path from root down, root first, given to visit with its kind, as Go’s WalkDir gives them: depth first, a directory’s entries in the order readDirectory sorts them, and links not followed — a link is visited, its kind Link, and not gone into, root too. What visit answers says what is next: Descend, go into a directory (for any other, go on); SkipDirectory, not go into a directory (for any other, as Go’s SkipDir on a file, skip what is left of the directory it is in); Stop, end the walk. A path that cannot be read (root not there, a directory not to be opened) is thrown.

findFiles

findFiles : {e : HFunctor}
          -> {{ev : filesystem <: e}}
          -> {{ex : exception FileError <: e}}
          -> Path
          -> (Path -> Kind -> Bool)
          -> Co e (List Path)

Every path from root down, root too, of which holds holds (given the path and its kind, as walk gives them), in the order walk visits them (Racket’s find-files).

instanceShowFileError

instance instanceShowFileError : Show FileError

As a system’s tools say it: the path, the errno’s name, and what it is.

>>> show ({ code = 2, name = "ENOENT", message = "No such file or directory", path = "notes.txt" } : FileError)
"notes.txt: ENOENT: No such file or directory"
>>> show ({ code = 18, name = "EXDEV", message = "Cross-device link", path = "a", other = Just "b" } : FileError)
"a -> b: EXDEV: Cross-device link"