Brr-evisc-tuple
Determines partial suppression of output from brr-commands
See evisc-tuple for relevant background on ``evisceration'':
eliding of subexpressions during printing. Also see break-rewrite for
background on the break-rewrite loop.
General Form:
(brr-evisc-tuple state)
The value of this function is used as the evisceration tuple by brr-commands. The value can be changed with set-brr-evisc-tuple or
the more general set-evisc-tuple.
A special value, :default, is legal for this evisc-tuple, and is its
initial value. In that case the actual evisc-tuple used during output from
brr-commands — which we call the effective value of the
brr-evisc-tuple — is the value of the evisc-tuple for terms. See
set-evisc-tuple, in particular, the discussion of the :term site
for setting evisc-tuples.
Think of brr-evisc-tuple as a true global variable, not a locally
bound variable of break-rewrite. In particular, if you set the
brr-evisc-tuple inside a break-rewrite interactive break and eventually
exit that break — either to enter a deeper break or return to a
shallower break or to the ACL2 top-level — the brr-evisc-tuple will
retain its chronologically most recent setting.
The brr-evisc-tuple is used when break-rewrite prints its
banner opening or closing a break on some monitored rune and when certain
brr-commands print their results.
When you're in a break-rewrite break, you're actually dealing with the
read-eval-print loop managed by ld. It prints its results using the
ld-evisc-tuple, while brr-commands use brr-evisc-tuple.
This can cause some confusion.
For example, suppose you have set the brr-evisc-tuple to
(evisc-tuple 2 3 nil nil) so break-rewrite banners and brr-commands only
print to depth 2 and length 3. Suppose the target term is (F (G (H 1)) 2 3
4 5 6 7). Then the following interaction with break-rewrite could
occur:
3 ACL2 >:target
(F (G #) 2 ...)
3 ACL2 >(make-list 10)
(NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL)
You might ask ``Given that the brr-evisc-tuple limits the print length
to 3, which I see when I print :target, how come the make-list
showed all 10 elements?'' The answer is that the brr-command
:target actually printed the target with the brr-evisc-tuple and
returned (value :invisible) which ld's read-eval-print loop doesn't
print. But the make-list returned a list of length ten and the
read-eval-print loop printed it using the ld-evisc-tuple.
Another issue relating brr-evisc-tuple and ld-evisc-tuple is that
while brr-evisc-tuple is a true global, retaining its chronologically
most recently set value at all depths of break-rewrite, ld-evisc-tuple is
locally bound by break-rewrite (actually, by the ld in wormhole) and
so sees its value restored as break-rewrite ascends back toward the top-level
of ACL2.
Subtopics
- Set-brr-evisc-tuple
- Set the brr-evisc-tuple
