Major Section: IO
ACL2 output is generally printed in full. However, ACL2 can be directed to
abbreviate, or ``eviscerate'', objects before printing them, though the use
of a so-called ``evisc-tuple''. See evisc-tuple for a discussion of
evisc-tuples. The utility
set-evisc-tuple modifies certain global
evisc-tuples, as explained below, to affect the extent to which ACL2
eviscerates objects during printing, for example during proof output or when
printing top-level evaluation results.
General Form: (set-evisc-tuple evisc-tuple ; a legal evisc-tuple, or :DEFAULT :iprint val ; one of *iprint-actions* :sites sites ; either :ALL, or an element or a subset of the ; list (:TERM :LD :TRACE :ABBREV)where the value of
:iprintis passed to
:sites '(:TERM :LD :TRACE :ABBREV), and other documentation is provided below. Note that all arguments are evaluated.
See without-evisc for how to avoid evisceration for ACL2 output.
The following example illustrates an invocation of
limits the print-level to 3 -- only three descents into list structures are
permitted before eviscerating a subterm -- and limits the print-length to 4
-- only the first four elements of any list structure will be printed.
ACL2 !>(set-evisc-tuple (evisc-tuple 3 ; print-level 4 ; print-length nil ; alist nil ; hiding-cars ) :iprint :same ; better yet, T :sites :all) (:TERM :LD :TRACE :ABBREV) ACL2 !>'((a b ((c d)) e f g) u v w x y) ((A B (#) E ...) U V W ...) ACL2 !>We recommend however using
:iprint tso that eviscerated terms may be read back in; see set-iprint. Indeed, the
:iprintargument is required as a reminder to the user to consider that issue, unless iprinting has been enabled at least once. If
:sitesor a required
:iprintargument is omitted, however, ACL2 will query the user for the missing arguments rather than causing an error.
ACL2 eviscerates by default only in a few cases, primarily in informational
messages for errors, warnings, and queries (i.e., in the
below). Users can modify the default behavior by supplying a suitable
set-evisc-tuple. The argument may be
denotes the evisceration provided when ACL2 starts up. Otherwise that
argument is an evisc-tuple, which is either
nil (no evisceration) or as
described above. Moreover, there are four evisc-tuple ``evisceration
contexts'', each with its own evisceration control. The value returned by
set-evisc-tuple indicates the evisceration contexts whose evisc-tuple has
been set. The evisceration contexts are as follows, all of which use a
default value of
nil for the hiding-cars. Accessors are also shown for
retrieving the corresponding evisc-tuple.
:TERM-- used for printing terms. The accessor is
(term-evisc-tuple flg state), where
flgis ignored if
set-evisc-tuplehas been called for
:termwith value other than
:default, and otherwise (hence initially): a
nilindicates an evisc-tuple of
nil, and otherwise the term-evisc-tuple has a print-level of 3 and print-length of 4.
:ABBREV-- used for printing informational messages for errors, warnings, and queries. Initially, the alist abbreviates the ACL2
world, print-level is 5, and print-level is 7. The accessor is
:GAG-MODE-- used for printing induction schemes (and perhaps, in the future, for other printing) when gag-mode is on. If gag-mode is off, the value used for this evisc-tuple is
(term-evisc-tuple nil state). But if gag-mode is on (i.e.,
(gag-mode)evaluates to a non-
nilvalue), then with one exception, the value is an evisc-tuple or
nil, to be used in gag-mode for printing of induction schemes and, during proofs, the ``The non-trivial part of the guard conjecture''. The exceptional value is
t, which indicates that in gag-mode, no printing of induction schemes should be and the guard conjecture should be printed using
(term-evisc-tuple t state). The accessor is
:LD-- used by the ACL2 read-eval-print loop. The accessor is
:TRACE-- used for printing trace output. No accessor is available (though in raw Lisp,
(trace-evisc-tuple)returns the trace-evisc-tuple).
ectx also has an updater,
(set-ectx-evisc-tuple val state), where
val is a legal value for
set-evisc-tuple as described above:
:default or an evisc-tuple
Note that the break-rewrite commands and the proof-checker generally do their printing using the term-evisc-tuple.