control suppression of details when printing
Major Section:  IO

ACL2 output is generally printed in full. However, ACL2 can be directed to abbreviate, or ``eviscerate'', objects before printing them. To ``eviscerate'' an object we replace certain substructures within it by strings that are printed in their stead. Such replacement is made relative to a so-called ``evisc-tuple'', which has four components: (evisc-tuple print-level print-length alist hiding-cars) is the same as the value of (list alist print-level print-length hiding-cars), and the components are used as follows (with priority order as discussed below). The alist component is used to replace any substructure occurring as a key by the corresponding string. The print-level and print-length are analogous to Common Lisp variables *print-level* and *print-length*, respectively, and cause replacement of substructures deeper than print-level by `#' and those longer than print-length by `...'. Finally, any consp x that starts with one of the symbols in hiding-cars is printed as <hidden>.

The following example illustrates the use of an evisc-tuple that limits the print-level to 3 -- only three descents into list structures are permitted before replacing a subexpression by `#' -- and limits the print-length to 4 -- only the first four elements of any list structure will be printed before replacing its tail by `...'.

ACL2 !>(fms "~x0~%"
            (list (cons #\0 '((a b ((c d)) e f g) u v w x y)))
            (evisc-tuple 3 4 nil nil))

((A B (#) E ...) U V W ...)
ACL2 !>
Notice that it is impossible to read the printed value back into ACL2, since there is no way for the ACL2 reader to interpret `#' or `...'. To solve this problem, see set-iprint.

In the above example we pass an evisc-tuple explicitly to a printing function, in this case, fms (see fmt). But ACL2 also does its own printing, for example during a proof attempt. There are global evisc-tuples that control ACL2's printing; see set-evisc-tuple and see without-evisc.