		Search-engine friendly clone of the ACL2 documentation.

Events

Evisc-table

Support for abbreviated output

The evisc-table is an ACL2 table (see table) whose purpose is to modify the print representations of specified non-nil objects. When a key (some object) is associated with a string value, then that string is printed instead of that key (as an abbreviation). For example, the following log shows how to abbreviate the key (a b c) with the token <my-abc-list>.

ACL2 !>(table evisc-table '(a b c) "<my-abc-list>")

Summary
Form:  ( TABLE EVISC-TABLE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 EVISC-TABLE
ACL2 !>'(a b c)
<my-abc-list>
ACL2 !>'(4 5 a b c)
(4 5 . <my-abc-list>)
ACL2 !>

Every value in this table must be either a string or nil, where nil eliminates any association of the key with an abbreviation. Continuing with the log above:

ACL2 !>(table evisc-table '(a b c) nil)

Summary
Form:  ( TABLE EVISC-TABLE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 EVISC-TABLE
ACL2 !>'(a b c)
(A B C)
ACL2 !>'(4 5 a b c)
(4 5 A B C)
ACL2 !>

It can be particularly helpful to use this table to abbreviate a constant introduced by defconst by prefixing the constant name with "#.", as we now describe. Consider first the following example.

(defconst *abc* '(1 2 3 4 5 6 7 8))
(table evisc-table *abc*
  (concatenate 'string "#." (symbol-name '*abc*)))

Then the constant *abc* is printed as follows — very helpful if its associated structure is significantly larger than the 8-element list of numbers shown above!

ACL2 !>*abc*
#.*ABC*
ACL2 !>

What's more, the ACL2 reader will replace #.*C*, where *C* is defined by defconst, by its value, regardless of evisc-table; see sharp-dot-reader. Continuing with the example above, we have:

ACL2 !>(cdr (quote #.*ABC*))
(2 3 4 5 6 7 8)
ACL2 !>

Of course, more care needs to be taken if packages are involved (see defpkg), as we now illustrate.

ACL2 !>(defpkg "FOO" nil)

Summary
Form:  ( DEFPKG "FOO" ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 "FOO"
ACL2 !>(defconst foo::*a* '(1 2 3))

Summary
Form:  ( DEFCONST FOO::*A* ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 FOO::*A*
ACL2 !>(table evisc-table foo::*a* "#.foo::*a*")

Summary
Form:  ( TABLE EVISC-TABLE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 EVISC-TABLE
ACL2 !>foo::*a*
#.foo::*a*
ACL2 !>'#.foo::*a*
#.foo::*a*
ACL2 !>(cdr '#.foo::*a*)
(2 3)
ACL2 !>

We conclude by an example showing some extra care that may be important to consider taking. We start with:

(defconst |*BaR*| '(3 4))

Then the following works just fine; but try it without the extra code for the may-need-slashes case and you'll see that the sharp-dot printing is missing. First:

(table evisc-table
       |*BaR*|
       (let ((x (symbol-name '|*BaR*|)))
         (if (may-need-slashes x)
             (concatenate 'string "#.|" x "|")
           (concatenate 'string "#." x))))

Then:

ACL2 !>|*BaR*|
#.|*BaR*|
ACL2 !>

The examples above illulstrate how the evisc-table is used when printing evaluation results. More generally, that table is used when fmt (or a related function such as fms) prints an object using ~x ~X, ~y, ~Y, ~f, or ~F.