SET-EVISC-TUPLE

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, 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 :iprint is passed to set-iprint, :sites :all abbreviates :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 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. 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). 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 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.

o :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.

o :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).

o :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).

o :LD -- used by the ACL2 read-eval-print loop. The accessor is (ld-evisc-tuple state).

o :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).

Note that the break-rewrite commands and the proof-checker generally do their printing using the term-evisc-tuple.