advanced controls of ACL2 printing
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.)