Io
Input/output facilities in ACL2
Example:
(mv-let
(channel state)
(open-input-channel "foo.lisp" :object state)
(mv-let (eofp obj state)
(read-object channel state)
(.
.
(let ((state (close-input-channel channel state)))
(mv final-ans state))..)))
Also see std/io and file-reading-example.
For advanced ways to control printing, see print-control.
For a discussion of formatted printing, see fmt.
To control ACL2 abbreviation (``evisceration'') of objects before printing
them, see set-evisc-tuple, see without-evisc, and see set-iprint.
To redirect output to a file, see output-to-file.
ACL2 supports input and output facilities equivalent to a subset of those
found in Common Lisp. ACL2 does not support random access to files (with one
exception: see read-file-into-string) or bidirectional streams. In
Common Lisp, input and output are to or from objects of type stream. In
ACL2, input and output are to or from objects called ``channels,'' which are
actually symbols. Although a channel is a symbol, one may think of it
intuitively as corresponding to a Common Lisp stream. Channels are in one of
two ACL2 packages, "ACL2-INPUT-CHANNEL" and
"ACL2-OUTPUT-CHANNEL". When one ``opens'' a file one gets back a
channel whose symbol-name is the file name passed to ``open,''
postfixed with -n, where n is a counter that is incremented every
time an open or close occurs.
There are three channels which are open from the beginning and which cannot
be closed:
acl2-input-channel::standard-character-input-0
acl2-input-channel::standard-object-input-0
acl2-input-channel::standard-character-output-0
All three of these are really Common Lisp's *standard-input* or
*standard-output*, appropriately.
For convenience, three global variables are bound to these rather tedious
channel names:
*standard-ci*
*standard-oi*
*standard-co*
Common Lisp permits one to open a stream for several different kinds of
io, e.g. character or byte. ACL2 permits an additional type called
``object''. In ACL2 an ``io-type'' is a keyword, either :character,
:byte, or :object. When one opens a file, one specifies a type,
which determines the kind of io operations that can be done on the channel
returned. The types :character and :byte are familiar. Type
:object is an abstraction not found in Common Lisp. An :object file
is a file of Lisp objects. One uses read-object or
read-object-with-case (see below) to read from :object files and
print-object$, its more flexible variant print-object$+, or
print-object$-preserving-case (see below; also, print-object$-fn) to
print to :object files. (The reading and printing are really done with
the Common Lisp read and printing functions. For those familiar with
read, we note that the recursive-p argument is nil.) The
function read-object-suppress is logically the same as read-object
except that read-object-suppress throws away the second returned value,
i.e. the value that would normally be read, simply returning (mv eof
state); under the hood, read-object-suppress avoids errors, for example
those caused by encountering symbols in packages unknown to ACL2.
The functions read-object-with-case is defined logically simply to be
read-object, while the function print-object$-preserving-case and
macro print-object$+ are defined logically simply to be
print-object$. However, these variants generally do I/O
differently (except that when the host Lisp is GCL,
print-object$-preserving-case behaves the same as print-object$).
For read-object-with-case the value that is read is affected by an extra
argument, namely, the second argument: the mode. The mode is one of
the keywords :upcase, :downcase, :preserve, or :invert,
where :upcase gives the same behavior as read-object, and the other
three modes are handled according to the specification for the Common Lisp
function, readtable-case (see for example the
Common Lisp HyperSpec's documentation for ``Examples of Effect of Readtable
Case on the Lisp Reader''). The function
print-object$-preserving-case is somewhat analogous: it is defined
logically to be print-object$ and it has the same behavior, except that
symbols are printed without adding escapes merely because of lowercase
letters; for example, the symbol in the current package with name "abc"
will be printed as abc, not as |abc|. But note that
print-object$-preserving-case may still insert vertical bars, depending
on the host Lisp, because different Lisp implementations choose to escape
symbols differently. Consider the symbol typically printed as |1u|.
Using print-object$-preserving-case, this prints simply as 1u in CCL
and Allegro CL, but it is printed as |1u| in SBCL, LispWorks, and CMUCL
— at least in the implementations that we tested!
File-name arguments are strings (except for the :STRING case
discussed below). ACL2 does not support the Common Lisp type pathname; rather, the underlying host Lisp will interpret the given string as
a pathname. If the string represents a relative pathname, it will be
elaborated to a full pathname using the connected book directory; see cbd. You can do that elaboration yourself with a directory dir using
(extend-pathname dir file-name state); see extend-pathname.
For the file-name argument of the output-related functions listed
below, ACL2 supports a special value, :STRING. For this value, the
channel connects (by way of a Common Lisp output string stream) to a string
rather than to a file: as characters are written to the channel they can be
retrieved by using get-output-stream-string$.
Here are the names, formals and output descriptions of the ACL2 io
functions.
Input Functions:
(open-input-channel (file-name io-type state) (mv channel state))
(open-input-channel-p (channel io-type state) boolean)
(close-input-channel (channel state) state)
(read-char$ (channel state) (mv char/nil state)) ; nil for EOF
(peek-char$ (channel state) char/nil)
(read-byte$ (channel state) (mv byte/nil state)) ; nil for EOF
(read-object (channel state) (mv eof-read-flg obj-read state))
(read-object-with-case (channel mode state) (mv eof-read-flg obj-read state))
(read-object-suppress (channel state) (mv eof-read-flg state))
(read-file-into-string (file-name &key..) string/nil) ; macro (reads state)
Output Functions:
(open-output-channel (file-name io-type state) (mv channel state))
(open-output-channel! (file-name io-type state) (mv channel state))
(open-output-channel-p (channel io-type state) boolean)
(close-output-channel (channel state) state)
(princ$ (obj channel state) state)
(write-byte$ (byte channel state) state)
(print-object$ (obj channel state) state)
(print-object$+ (obj channel &key ...) state)
(print-object$-preserving-case (obj channel state) state)
(print-object$-fn (obj serialize-character channel state) state)
(fms (string alist channel state evisc-tuple) state)
(fms! (string alist channel state evisc-tuple) state)
(fmt (string alist channel state evisc-tuple) (mv col state))
(fmt! (string alist channel state evisc-tuple) (mv col state))
(fmt1 (string alist col channel state evisc-tuple) (mv col state))
(fmt1! (string alist col channel state evisc-tuple) (mv col state))
(cw (string arg0 arg1 ... argn) nil)
(get-output-stream-string$ (channel state
&optional (close-p 't)
(ctx ''get-output-stream-string$))
(mv erp string state))
Note that open-output-channel and open-output-channel! will
attempt to create directories as needed (but this is not the case for
open-input-channel). For example, the following can succeed in writing
to the indicated file by creating subdirectory "dir4" if that directory
does not already exist.
(mv-let
(channel state)
(open-output-channel "dir4/foo4" :object state)
(pprogn (fms "Here: ~x0"
(list (cons #\0 (make-list 10)))
channel state nil)
(close-output-channel channel state)))
The ``formatting'' functions are particularly useful; see fmt and
see cw. In particular, cw prints to a ``comment window'' and
does not involve the ACL2 state, so many may find it easier to use
than fmt and its variants. The functions fms!, fmt!,
and fmt1! are the same as their respective functions without the
``!,'' except that the ``!'' functions are guaranteed to print forms
that can be read back in (at a slight readability cost).
When one enters ACL2 with (lp), input and output are taken from *standard-oi* to *standard-co*. Because these are synonyms for
*standard-input* and *standard-output*, one can drive ACL2 io off of
arbitrary Common Lisp streams, bound to *standard-input* and
*standard-output* before entry to ACL2.
The macro get-output-stream-string$ returns the string accumulated
into the given channel. By default, a call of this macro closes the supplied
output channel. However, a third argument is optional (default t), and
if it evaluates to nil then the channel remains open. The fourth
argument is an optional context, which generally evaluates to a symbol, for
error reporting. The following example illustrates.
ACL2 !>
(mv-let
(channel state)
(open-output-channel :string :object state)
(pprogn (print-object$-fn 17 nil channel state)
(print-object$-fn '(a b (c d)) nil channel state)
(er-let*
((str1 (get-output-stream-string$
channel state
nil))) ; keep the channel open
(pprogn (print-object$-fn 23 nil channel state)
(print-object$-fn '((e f)) nil channel state)
(er-let* ; close the channel
((str2 (get-output-stream-string$ channel state)))
(value (cons str1 str2)))))))
("
17
(A B (C D))" . "
23
((E F))")
ACL2 !>
Also see printing-to-strings for a discussion of formatted printing
functions such as fmt-to-string that do not take a channel or state argument and return a string.
By default, symbols are printed in upper case when vertical bars are not
required, as specified by Common Lisp. See set-print-case for how to
get ACL2 to print symbols in lower case.
By default, numbers are printed in radix 10 (base 10). See set-print-base-radix for how to get ACL2 to print numbers in radix 2, 8, or
16.
To see the guard of an IO function, or indeed any function, see
args or call the function guard; but some built-in functions
(including some IO functions) will print the result using the variable
STATE-STATE. While that is logically correct, if you want to execute the
guard then you should replace that variable by STATE and also replace
each built-in function symbol of the form xxx-p1 by corresponding
function symbol xxx-p. Consider the following example.
ACL2 !>:args princ$
Function PRINC$
Formals: (X CHANNEL STATE-STATE)
Signature: (PRINC$ * * STATE)
=> STATE
Guard: (AND (OR (ACL2-NUMBERP X)
(CHARACTERP X)
(STRINGP X)
(SYMBOLP X))
(STATE-P1 STATE-STATE)
(SYMBOLP CHANNEL)
(OPEN-OUTPUT-CHANNEL-P1 CHANNEL
:CHARACTER STATE-STATE))
Guards Verified: T
Defun-Mode: :logic
Type: (CONSP (PRINC$ X CHANNEL STATE-STATE))
Documentation available via :DOC
PRINC$
ACL2 !>(untranslate (guard 'princ$ nil (w state)) t (w state))
(AND (OR (ACL2-NUMBERP X)
(CHARACTERP X)
(STRINGP X)
(SYMBOLP X))
(STATE-P1 STATE-STATE)
(SYMBOLP CHANNEL)
(OPEN-OUTPUT-CHANNEL-P1 CHANNEL
:CHARACTER STATE-STATE))
ACL2 !>
If you want to execute the guard for princ$, then according to the
suggestion above, you should consider the guard for (princ$ x channel
state) to be as follows.
(AND (OR (ACL2-NUMBERP X)
(CHARACTERP X)
(STRINGP X)
(SYMBOLP X))
(STATE-P STATE)
(SYMBOLP CHANNEL)
(OPEN-OUTPUT-CHANNEL-P CHANNEL :CHARACTER STATE))
For example, we can check the guard for a given value and channel as
follows.
ACL2 !>(let ((x 3) (channel *standard-co*))
(AND (OR (ACL2-NUMBERP X)
(CHARACTERP X)
(STRINGP X)
(SYMBOLP X))
(STATE-P STATE)
(SYMBOLP CHANNEL)
(OPEN-OUTPUT-CHANNEL-P CHANNEL :CHARACTER STATE)))
T
ACL2 !>
Comment for advanced users: Function open-output-channel! is
identical as a function to open-output-channel, except that the former
may be called even during make-event expansion and clause-processor hints, but requires that there is an active trust tag
(see defttag).
Finally, we note that the std/io library contains useful file io
functions whose definitions illustrate some of the features described above,
as does the definition of write-list in community-book
books/misc/file-io.lisp.
Subtopics
- Fmt
- Formatted printing
- Msg
- Construct a ``message'' suitable for the ~@ directive of fmt
- Cw
- Print to the comment window
- Set-evisc-tuple
- Control suppression of details when printing
- Set-iprint
- Control whether abbreviated output can be read back in
- Print-control
- Advanced controls of ACL2 printing
- Read-file-into-string
- The contents of a file (or part of it) as a string
- Std/io
- A library for reasoning about file input/output operations.
- Msgp
- Recognizer for a ``message''
- Printing-to-strings
- Printing to strings instead of files or standard output
- Evisc-tuple
- Control suppression of details when printing
- Output-controls
- Methods for controlling the output produced by the ACL2 prover
- Observation
- Print an observation
- *standard-co*
- The ACL2 analogue of CLTL's *standard-output*
- Ppr-special-syms
- A table to control indentation for pretty-printing
- Standard-oi
- The standard object input ``channel''
- Standard-co
- The character output channel to which ld prints
- Without-evisc
- Print output in full
- Serialize
- Routines for saving ACL2 objects to files, and later restoring them
- Output-to-file
- Redirecting output to a file
- Fmt-to-comment-window
- Print to the comment window
- Princ$
- Print an atom
- Character-encoding
- How bytes are parsed into characters
- Open-output-channel!
- When trust tags are needed to open output channels
- Cw-print-base-radix
- Print to the comment window in a given print-base
- Set-print-case
- Control whether symbols are printed in upper case or in lower case
- Set-print-base
- Control radix in which numbers are printed
- Print-object$
- Print an object to an open object output channel
- Extend-pathname
- Extend a relative pathname to an absolute pathname
- Print-object$+
- Print an object to an open output channel in a specified manner
- Fmx-cw
- (fmx-cw str &rest args) => state
- Set-print-radix
- Control printing of the radix for numbers
- Set-fmt-hard-right-margin
- Set the right margin for formatted output
- File-write-date$
- The write-date of a file as a natural number
- Proofs-co
- The proofs character output channel
- Set-print-base-radix
- Control radix in which numbers are printed and printing of the radix
- Print-base-p
- Recognizer for print bases that are understood by functions such as
explode-nonnegative-integer and explode-atom.
- *standard-oi*
- An ACL2 object-based analogue of CLTL's *standard-input*
- Wof
- Direct standard output and proofs output to a file
- File-length$
- The size of a file in bytes
- Fms!-lst
- Write each object in a list to a character output channel.
- Delete-file$
- Delete a file
- *standard-ci*
- An ACL2 character-based analogue of CLTL's *standard-input*
- Write-list
- Write a list to a file
- Trace-co
- The trace character output channel
- Fmt!
- (fmt! str alist co-channel state evisc) => state
- Fms
- (fms str alist co-channel state evisc) => state
- Cw!
- Print readably to the comment window
- Fmt-to-comment-window!
- Print readably to the comment window
- Fms!
- (fms! str alist co-channel state evisc) => state
- Eviscerate-hide-terms
- To print (hide ...) as <hidden>
- Fmt1!
- (fmt1! str alist col channel state evisc) => (mv col state)
- Fmt-to-comment-window!+
- Print readably and uninhibited to the comment window
- Read-file-into-byte-array-stobj
- Read the bytes from a file into a stobj array.
- Fmt1
- (fmt1 str alist col co-channel state evisc) => (mv col state)
- Fmt-to-comment-window+
- Print uninhibited to the comment window
- Cw-print-base-radix!
- Print to the comment window in a given print-base
- Read-file-into-character-array-stobj
- Read the characters from a file into a stobj array.
- Fmx
- (fmx str &rest args) => state
- Cw!+
- Print readably and uninhibited to the comment window
- Read-objects-from-book
- Read the forms in a book.
- Newline
- Print a newline to a given output channel
- Cw+
- Print uninhibited to the comment window
- Probe-file
- Determine whether a file exists
- Write-objects-to-file!
- Write a list of ACL2 objects to a file, when ttags are needed to write.
- Write-objects-to-file
- Write a list of ACL2 objects to a file.
- Read-objects-from-file
- Read the ACL2 objects from a file.
- Read-object-from-file
- Read an ACL2 object from a file.
- Read-file-into-byte-list
- Read a file into a list of bytes.
- Set-fmt-soft-right-margin
- Set the soft right margin for formatted output
- Read-file-into-character-list
- Read a file into a character-list.
- Io-utilities
- Some utilities for io.
