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