Std/io
A library for reasoning about file input/output operations.
Introduction
The std/io library provides:
- Basic lemmas about low-level, built-in ACL2 io operations like open-input-channel, read-byte$, close-output-channel, and so
on. (These are especially useful for guard proofs about IO functions.)
- A file-measure for proving the termination of functions that read
from files.
- Extended low-level file input operations such as read-bytes$, which
lets you efficiently read 16-, 32-, and 64-bits from a file at once.
- High-level operations for reading whole files, such as read-file-bytes, read-file-characters, and read-file-objects.
Some basic information about low-level i/o facilities in ACL2 can be found
in io, and for some and also logical-story-of-io.
Loading the Library
If you just want to load the whole IO library, you can include the top
book, e.g.,
(include-book "std/io/top" :dir :system)
But this may be more than you need. The library is split up into sensible
books that can generally be loaded individually.
Subtopics
- Open-channel-lemmas
- Lemmas about when various state-modifying functions
do and don't affect the list of open channels.
- Std/io/read-char$
- Read one character from an open :character stream.
- Std/io/read-object
- Read one object from an open :object stream.
- Std/io/open-output-channel
- Open a file for writing.
- Unsound-read
- A faster alternative to serialize-read, which is unsound in
general, but may be fine in many common cases.
- Read-string
- Parse a string into s-expressions, by using Common Lisp's read
under the hood. (requires a ttag)
- Read-bytes$
- Flexible macro for reading and combining 1, 2, 4, or 8 bytes from an
open :byte input stream into a single value.
- File-measure
- A measure for admitting functions that read from files.
- Read-bytes$-n
- Flexible macro for reading whole lists of n 1-, 2-, 4-, or
8-byte values from an open :byte input stream.
- Std/io/read-byte$
- Read one byte from an open :byte stream.
- Std/io/open-input-channel
- Open an file for reading.
- Read-file-lines-no-newlines
- Read an entire file into a list of lines (strings), omitting
newline characters from the resuting strings
- Print-compressed
- Wrapper for print-object$ that ensures serialize
compression is enabled (if supported).
- Nthcdr-bytes
- Skip past some number of bytes in an open file.
- Read-file-lines
- Read an entire file into a list of lines (strings).
- Std/io/close-output-channel
- Close an output channel.
- Read-file-characters
- Read an entire file into a character-listp.
- Read-file-bytes
- Read an entire file into a list of (unsigned) bytes.
- Print-legibly
- Wrapper for print-object$ that ensures serialize
compression is disabled.
- Std/io/close-input-channel
- Close an input channel.
- Read-file-objects
- Read an entire file into a list of ACL2 objects.
- Logical-story-of-io
- How file reading operations are modeled in the ACL2 logic.
- Take-bytes
- Read the first n bytes from an open file.
- Std/io/peek-char$
- Inspect the next character that will be read from an open
:character input stream.
- Read-file-characters-rev
- Read an entire file into a character-listp, but in reverse
order!
- Read-file-as-string
- Std/io/write-byte$
- Write one byte to an open :byte output stream.
- Std/io/set-serialize-character
- Control the use of serialize in print-object$.
- Std/io/print-object$
- Print a Lisp object to an :object output stream.
- Std/io/princ$
- Print an atom to a :character output stream.
- Std/io/read-file-into-string
- *file-types*
- Different ways to open files for reading and writing.
