EVISC-TABLE

support for abbreviated output 
Major Section:  EVENTS

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 !>