Major Section: IO
See IO for a summary of printing in ACL2. Here we document some advanced ways to control what is printed by ACL2's primary printing routines.
See set-print-base and see set-print-case for discussions of the most common
ways to control what is printed. Indeed, these are the only ways to control
the behavior of princ$ and prin1$.
The rest of this topic is for advanced users of ACL2. We refer to Common Lisp behavior, as described in any good Common Lisp documentation.
Print-control variables. Set-print-base and set-print-case
assign to corresponding so-called ``state global variables''
'print-base and 'print-case, which can be accessed using the
expressions (@ print-base) and (@ print-case, respectively;
see assign. Here is a table showing all print-control variables, their
setters, and their defaults.
print-base set-print-base 10 print-case set-print-case :upcase print-circle set-print-circle nil print-escape set-print-escape t print-length set-print-length nil print-level set-print-level nil print-lines set-print-lines nil print-pretty set-print-pretty nil print-radix set-print-radix nil print-readably set-print-readably nil print-right-margin set-print-right-margin nil
Each ACL2 print-control variable print-xxx can correspond in function to
Common Lisp variable *PRINT-XXX*. Specifically, the evaluation of forms
(set-print-base t) and (set-print-case t) affects ACL2 printing
functions in much the same way that setting to t Common Lisp variables
*PRINT-BASE* and *PRINT-CASE*, respectively, affects Common Lisp
printing. The same is true for print-escape, except that this does not
affect princ$ or prin1$, which correspond to Common Lisp functions
princ and prin1: princ treats *PRINT-ESCAPE* as nil while
prin1 treats *PRINT-ESCAPE* as t. Moreover, all print-control
variables not mentioned in this paragraph are set to their defaults in
princ$ and prin1$, as indicated by ACL2 constant
*print-control-defaults*, except that print-readably is set to
nil in princ$.
Fmt and its related functions are sensitive to state globals
'print-base, 'print-case, 'print-escape, and 'print-readably,
in analogy with Common Lisp functions that don't fix *PRINT-ESCAPE* or
*PRINT-READABLY*. But the fmt functions do not respect settings of
other print-control variables; for example, they act as though
'print-circle is nil. Since ACL2 output is produced using the same
underlying print routines as the fmt functions, it also is insensitive
to all print-control variables except for the four above. To control the
print-level and print-length used for producing ACL2 output,
see set-evisc-tuple.
Print-object$ is sensitive to all of the print-control variables.
(REMARK: ACL2 binds 'print-circle to t before writing
certificate files, and before writing auxiliary files that are compiled
when make-event forms are present in a book. This binding allows for
structure sharing that can keep these files from growing large.)
Evaluate (reset-print-control) to restore all print-control variables to
their original settings, as stored in constant *print-control-defaults*.
(Remark for those using ACL2 built on Gnu Common Lisp (GCL) versions that are
non-ANSI, which as of October 2008 is all GCL versions recommended for ACL2:
Note that Common Lisp variables *PRINT-LINES*, *PRINT-MISER-WIDTH*,
*PRINT-READABLY*, *PRINT-PPRINT-DISPATCH*, and
*PRINT-RIGHT-MARGIN* do not have any effect for such GCL versions.)