Skip to content
heff

std.file

Files open, read and written a piece at a time: a file opened by open and closed by close, or held by a with that closes it when its body ends (with f := File.open path do ...); read a chunk or a line at a time, written, sought in; what the system says of it (stat); and the standard streams, as open files. Use it by a name, import std.file as File, as its names are short.

import co
import exception
import std.file as File
import std.filesystem
import std.io
import std.path


-- | the words of the standard input, read a line at a time
wordsIn : {e : HFunctor}
        -> {{disk : filesystem <: e}}
        -> {{ex : exception FileError <: e}}
        -> Co e Int
wordsIn = File.foldStdinLines 0 (\n line -> pure (n + List.length (words line)))


-- | a file's first line, the file opened and closed again
firstLine : {e : HFunctor}
          -> {{disk : filesystem <: e}}
          -> {{ex : exception FileError <: e}}
          -> Path
          -> Co e (Maybe String)
firstLine path = do
  f <- File.open path
  line <- File.readLine f
  File.close f
  pure line


-- | a file's lines, printed one at a time as they are read: the file
-- | held a chunk at a time, closed when the `with` ends
printed : {e : HFunctor}
        -> {{io : stdio <: e}}
        -> {{disk : filesystem <: e}}
        -> {{ex : exception FileError <: e}}
        -> Path
        -> Co e Unit
printed path = do
  with f := File.open path do
    File.foldLines f () (\u l -> print l)


-- | a file's lines, in order: gathered the other way round as they
-- | are read, then turned
linesOf : {e : HFunctor}
        -> {{disk : filesystem <: e}}
        -> {{ex : exception FileError <: e}}
        -> Path
        -> Co e (List String)
linesOf path = do
  with f := File.open path do
    ls <- File.foldLines f Nil (\ls l -> pure (l :: ls))
    pure (List.reverse ls)


-- | a line added to the end of a file
logged : {e : HFunctor}
       -> {{disk : filesystem <: e}}
       -> {{ex : exception FileError <: e}}
       -> Path
       -> String
       -> Co e Unit
logged path line = do
  with f := File.open (access := Write { exists = Append }) path do
    File.writeString f (line ^ "\n")

An open file is the host’s own thing, a File (std.filesystem’s, as its effect’s operations take it). open opens one, and close closes it. A file is closed once: an operation on it after is EBADF, never one on a file opened since, and a second close does nothing. A file not closed is closed where the program drops its last reference to it: at once, in C, as it is counted.

with f := File.open path do ... is open and close around its body. The standard streams are had the same way (withStdin, withStdout, withStderr), by the shared held, as they are always there, and left open when their body ends, so that a program reads its input a line at a time (foldLines), in as little memory as a chunk and a line take.

A file is opened, read and written by std.filesystem’s effect, filesystem. An operation that fails — a file that does not open, a write the disk did not take, a read of a closed file — throws why, a FileError, over the exception effect, as std.filesystem’s operations on a path do.

A regular file is read and written there and then: the system has it ready at once, as far as poll can tell, so even where green threads are scheduled by std.reactor, a read of a file waits for the disk, the other threads with it. A pipe, a terminal or a socket — the standard streams, most often — waits in std.reactor’s reactor, as std.net’s sockets do: the other threads go on while it waits.

Exists

data Exists
  = Error
  | Truncate
  | MustTruncate
  | Replace
  | TruncateOrReplace
  | Update
  | CanUpdate
  | Append

What opening a file to write does, as Racket’s #:exists says, with a file there, and where there is none:

  • Error: one there is EEXIST; else it is made.
  • Truncate: one there is emptied; else it is made.
  • MustTruncate: one there is emptied; else ENOENT.
  • Replace: one there is removed, and a new one made in its place (not a directory: there, EEXIST); else it is made.
  • TruncateOrReplace: one there is emptied, or, where it cannot be (its permissions), replaced; else it is made.
  • Update: one there is kept as it is; else ENOENT.
  • CanUpdate: one there is kept as it is; else it is made.
  • Append: one there is kept, each write at its end; else it is made.

WriteOpts

type WriteOpts = { exists : Exists = Error, permissions : Int = 438 }

How a file is opened to write: what is done with one there (exists, unless said Error: it must be new), and the permissions of one it makes (0o666, rw-rw-rw-, unless said, less the umask).

Access

data Access = Read | Write WriteOpts | ReadWrite WriteOpts

What a file is opened for: reading (it must be there, and is had as it is), writing, or both, as the WriteOpts says (Write {}, a new file; Write { exists = Truncate }, emptied, as C’s fopen does).

From

data From = FromStart | FromCurrent | FromEnd

Where a seek counts from.

open

open : {e : HFunctor}
     -> {{ev : filesystem <: e}}
     -> {{ex : exception FileError <: e}}
     -> {access : Access := Read}
     -> Path
     -> Co e File

path opened for access, reading unless said (open (access := Write {}) p): the file, the host’s own; where it does not open, why is thrown.

close

close : {e : HFunctor}
      -> {{ev : filesystem <: e}}
      -> {{ex : exception FileError <: e}}
      -> File
      -> Co e Unit

The file closed; where it does not close — a write the disk did not take — why is thrown. A standard stream is left open.

withStdin

withStdin : {e : HFunctor}
          -> {a : Type}
          -> {{ev : filesystem <: e}}
          -> {{cu : custodian <: e}}
          -> (File -> Co e a)
          -> Co e a

The standard input, as a port of its own held by body: read it so, a line at a time, or by std.io’s readStdin, not both (what one has read ahead the other does not see). The port is closed as the block is left, the stream itself left open, what was read ahead kept for the next withStdin.

withStdout

withStdout : {e : HFunctor}
           -> {a : Type}
           -> {{ev : filesystem <: e}}
           -> {{cu : custodian <: e}}
           -> (File -> Co e a)
           -> Co e a

The standard output, as a port of its own held by body (what std.io wrote before is written out first), closed as the block is left: std.io’s print and the stream itself go on as before.

withStderr

withStderr : {e : HFunctor}
           -> {a : Type}
           -> {{ev : filesystem <: e}}
           -> {{cu : custodian <: e}}
           -> (File -> Co e a)
           -> Co e a

The standard error, as a port of its own held by body, closed as the block is left.

readChunk

readChunk : {e : HFunctor}
          -> {{ev : filesystem <: e}}
          -> {{ex : exception FileError <: e}}
          -> File
          -> Int
          -> Co e Bytes

Up to n bytes of the file, from where it is: as many as there are, waiting for one at least (from a pipe or a terminal, as many as have come); none at its end. At most 16 mebibytes at a time. After the file is closed, EBADF is thrown, as by each operation below.

readLine

readLine : {e : HFunctor}
         -> {{ev : filesystem <: e}}
         -> {{ex : exception FileError <: e}}
         -> File
         -> Co e (Maybe String)

The next line of the file, without its \n (or \r\n); the last one too where no \n ends it; Nothing at its end. Its bytes as they are, UTF-8 or not.

writeBytes

writeBytes : {e : HFunctor}
           -> {{ev : filesystem <: e}}
           -> {{ex : exception FileError <: e}}
           -> File
           -> Bytes
           -> Co e Unit

All the bytes written, where the file is (at its end, appending), waiting until the system has taken them.

writeString

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

A string’s bytes written, as they are.

seek

seek : {e : HFunctor}
     -> {{ev : filesystem <: e}}
     -> {{ex : exception FileError <: e}}
     -> File
     -> From
     -> Int
     -> Co e Int

Where the file is read and written next, moved by n bytes from its start, from where it is, or from its end: where it is now, from its start. (A pipe or a terminal cannot be sought in: ESPIPE.)

tell

tell : {e : HFunctor}
     -> {{ev : filesystem <: e}}
     -> {{ex : exception FileError <: e}}
     -> File
     -> Co e Int

Where the file is read and written next, from its start.

stat

stat : {e : HFunctor}
     -> {{ev : filesystem <: e}}
     -> {{ex : exception FileError <: e}}
     -> File
     -> Co e Status

What the system says of the file.

foldLinesBy

foldLinesBy : {e : HFunctor}
            -> {{ev : filesystem <: e}}
            -> {{ex : exception FileError <: e}}
            -> {a : Type}
            -> Int
            -> File
            -> a
            -> (a -> String -> Co e a)
            -> Co e a

foldLines, the file read n bytes at a time (as readChunk reads them): however few, each line is given whole.

foldLines

foldLines : {e : HFunctor}
          -> {{ev : filesystem <: e}}
          -> {{ex : exception FileError <: e}}
          -> {a : Type}
          -> File
          -> a
          -> (a -> String -> Co e a)
          -> Co e a

Each line of the file, from where it is to its end, given to step with what the lines before it came to: what they all come to. A line is as readLine gives it: without its \n (or \r\n), the last one too where no \n ends it. The file is read 64 kibibytes at a time (from a pipe or a terminal, as much as has come), so that a chunk and a line are held, however long the file; should the fold be left before its end, what it read past the line it was at is not read again.

foldStdinLines

foldStdinLines : {e : HFunctor}
               -> {{ev : filesystem <: e}}
               -> {{ex : exception FileError <: e}}
               -> {a : Type}
               -> {{cu : custodian <: e}}
               -> a
               -> (a -> String -> Co e a)
               -> Co e a

Each line of the standard input given to step, as foldLines gives them: what they all come to.

copyOpen

copyOpen : {e : HFunctor}
         -> {{ev : filesystem <: e}}
         -> {{ex : exception FileError <: e}}
         -> File
         -> File
         -> Co e Int

What is left of one open file written to another, a chunk at a time: how many bytes.

instanceBinderOpen

instance instanceBinderOpen : {e : HFunctor} -> Binder (Co e File)

A with of a file open opens, with f := File.open path do ...: its name the file open, and the with comes to what its body came to.

instanceHolderOpen

instance instanceHolderOpen : {e : HFunctor}
                            -> {{ev : filesystem <: e}}
                            -> {{ex : exception FileError <: e}}
                            -> {{cu : custodian <: e}}
                            -> Holder
                              e
                              (Co e File)
                              (\s -> File)
                              (\x -> x)
                              (\r -> r)

A file open opens, held by a with: opened, the body run with it, and closed when the body ends. A file that does not open is thrown (a FileError), the body not run; one that does not close — a write the disk did not take — is thrown once the body has ended. Should the body be left otherwise — a throw heard outside it, a handler between that drops the continuation — the file is closed where the program drops its last reference to it.