Without-evisc
Print output in full
General Form:
(without-evisc form)
where form is any expression to evaluate. The effect is to evaluate
form as though the without-evisc wrapper were absent, except that
expressions are printed in full for the ensuing output, regardless of the
current evisc-tuples (see set-evisc-tuple). See set-iprint for
an example.
More precisely, without-evisc binds each of the term-evisc-tuple,
ld-evisc-tuple, abbrev-evisc-tuple and gag-mode-evisc-tuple to nil (see
set-evisc-tuple). It does not modify the trace or brr evisc-tuples, so
trace and brr output are not modified by without-evisc. Also note that
calls of printing functions such as fmt that include explicit
evisc-tuples will not have those evisc-tuples overridden. The following
example illustrates this point.
ACL2 !>(without-evisc
(fms "~x0~%"
(list (cons #0 '((a b ((c d)) e f g) u v w x y)))
*standard-co*
state
(evisc-tuple 2 3 nil nil)))
((A B # ...) U V ...)
<state>
ACL2 !>
We conclude with two remarks. (1) A call of without-evisc on
expression exp actually invokes a specialized call of ld on a
one-element list containing exp, which prints the value returned by
evaluation of exp. It actually returns the useless value (mv nil
:invisible state), except that if an error is detected then it generally
returns (mv t nil state), indicating an error; see error-triple.
So do not use without-evisc in programs if you want the value of the
computation to be returned, rather than merely printed. (2) Even when using
without-evisc, if the ACL2 logical world is part of the value returned,
it will be printed in abbreviated form because the ACL2 read-eval-print loop
always arranges for this to be the case, regardless of the ld-evisc-tuple.
For example:
ACL2 !>(without-evisc (w state))
<world>
ACL2 !>
An alternative to the use of without-evisc is to explore large objects
using the ACL2 function (walkabout object state); see walkabout.
