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
