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)))
*standard-co*
state
(evisc-tuple 3 4 nil nil))
((A B (#) E ...) U V W ...)
<state>
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.
