		Search-engine friendly clone of the ACL2 documentation.

Set-evisc-tuple

Control suppression of details when printing

ACL2 output is generally printed in full. However, ACL2 can be directed to abbreviate, or ``eviscerate'', objects before printing them, through 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 of legal sites (see below)

where the value of :iprint is passed to set-iprint, :sites :all abbreviates :sites '(:term :ld :trace :abbrev :gag-mode :brr), 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 set-evisc-tuple that 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 t so that eviscerated terms may be read back in (see set-iprint), as shown here:

ACL2 !>(set-evisc-tuple (evisc-tuple 3   ; print-level
                                     4   ; print-length
                                     nil ; alist
                                     nil ; hiding-cars
                                     )
                        :iprint t
                        :sites :all)

ACL2 Observation in SET-EVISC-TUPLE:  Iprinting has been enabled.
 (:TERM :LD :TRACE :ABBREV . #@1#)
ACL2 !>(without-evisc '(:TERM :LD :TRACE :ABBREV . #@1#))
(:TERM :LD
       :TRACE :ABBREV
       :GAG-MODE :BRR)
ACL2 !>

Indeed, the :iprint argument is required as a reminder to the user to consider that issue, unless iprinting has been enabled at least once. If :sites or a required :iprint argument 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 :EVISC case below), and in response to break-rewrite commands. Users can modify the default behavior by supplying a suitable argument to set-evisc-tuple. The argument may be :default, which 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 six 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 flg is ignored if set-evisc-tuple has been called for :term with value other than :default, and otherwise (hence initially): a flg of nil indicates 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 (abbrev-evisc-tuple state).
:BRR — used for output from brr-commands issued in the break-rewrite loop. When the value is :DEFAULT then the effective value of this evisc-tuple is the :TERM evisc-tuple with flg = t (see above). Also see brr-evisc-tuple.
: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-nil value), 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 (gag-mode-evisc-tuple state).
:LD — used by the ACL2 read-eval-print loop. The accessor is (ld-evisc-tuple state).
:TRACE — used for printing trace output. No accessor is available (though in raw Lisp, (trace-evisc-tuple) returns the trace-evisc-tuple).

Each context 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 (possibly nil).

Subtopics

Set-brr-evisc-tuple: Set the brr-evisc-tuple