		Search-engine friendly clone of the ACL2 documentation.

Set-iprint

Control whether abbreviated output can be read back in

The following log may be sufficient for you to see how to use set-iprint; more explanation is below. The example is taken from a session that used the break-rewrite utility, but familiarity with that utility is not necessary in order to understand this example. What it shows is that the form (set-iprint t) allows you to recover, using without-evisc, output that had been hidden. (See break-rewrite for more about the interaction of break-rewrite with iprinting.)

ACL2 !>(thm (p y))

(1 Breaking (:REWRITE AX) on (P Y):
1 ACL2 >:eval

1x (:REWRITE AX) failed because :HYP 1 rewrote to
(EQUAL Y '(NIL NIL NIL NIL ...)).

1 ACL2 >:a!
Abort to ACL2 top-level
Here is the current pstack [see :DOC pstack]:
(REWRITE-ATM SIMPLIFY-CLAUSE WATERFALL)

*** Note: No checkpoints to print. ***

ACL2 Version 6.4.  Level 1.  Cbd "u/smith/".
System books directory "/u/smith/acl2/v6-4/books/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !>(set-iprint t)

ACL2 Observation in SET-IPRINT:  Iprinting has been enabled.
ACL2 !>(thm (p y))

(1 Breaking (:REWRITE AX) on (P Y):
1 ACL2 >:eval

1x (:REWRITE AX) failed because :HYP 1 rewrote to
(EQUAL Y '(NIL NIL NIL NIL . #@2#)).

1 ACL2 >(without-evisc '(EQUAL Y '(NIL NIL NIL NIL . #@2#)))
(EQUAL Y
       '(NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL
             NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL
             NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL
             NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL
             NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL
             NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL
             NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL
             NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL
             NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL
             NIL NIL NIL NIL NIL NIL NIL NIL NIL))
1 ACL2 >

This concludes the introductory example.

When ACL2 pretty-prints large expressions using formatted printing (see fmt), it may save time and space by printing tokens `#' or `...' in place of certain subexpressions. By default this only happens for a few settings such as error and warning messages; see set-evisc-tuple for controlling such elision in general. The full expression is unavailable to the user when `#' or `...' is printed, but that is easily solved by evaluating the form

(set-iprint t)

to enable a mode called ``iprinting''. Then, instead of printing `#' or `...', ACL2 prints `#@i#' for i = 1,2,3,... — all in base 10. ACL2 can read back in such `#@i#' because under the hood, i is associated with its corresponding elided form. Thus the term ``iprint'' can be viewed as suggesting ``interactive print'' or ``index print''. We also think of ``iprint'' as suggesting ``i printing'', to suggest the printing of token `#@i#'. We call i the ``iprint index'' of that token.

The following example should suffice to illustrate how to recover elided subexpressions. (Below this example we provide details that may be of interest only to advanced users.) Here we cause an error by defining a macro of one argument and then calling it with two arguments. By default, error messages abbreviate subexpressions deeper than level 5 with `#' and past the 7th element of a list with `...'. We see this behavior below.

ACL2 !>(defmacro foo (x) x)

Summary
Form:  ( DEFMACRO FOO ...)
Rules: NIL
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
 FOO
ACL2 !>(foo arg1 (a (b (c (d (e (f (g)))))) h i j k l m n))

ACL2 Error in macro expansion:  Wrong number of args in macro expansion
of (FOO ARG1 (A (B (C (D #))) H I J K L ...)).  (See :DOC set-iprint
to be able to see elided values in this message.)

ACL2 !>(set-iprint t)

ACL2 Observation in SET-IPRINT:  Iprinting has been enabled.
ACL2 !>(foo arg1 (a (b (c (d (e (f (g)))))) h i j k l m n))

ACL2 Error in macro expansion:  Wrong number of args in macro expansion
of (FOO ARG1 (A (B (C (D #@1#))) H I J K L . #@2#)).

ACL2 !>(acl2-count '(FOO ARG1 (A (B (C (D #@1#))) H I J K L . #@2#)))
23
ACL2 !>

Sometimes you may want to supply the abbreviated form not to compute with it, as in the ACL2-count example just above, but so that you can see it. The macro without-evisc eliminates elision during printing. Below we show two ways to use this utility: first, we use it to print the elided form, and then, we use it instead on the original input form to print the entire error message.

ACL2 !>(without-evisc '(FOO ARG1 (A (B (C (D #@1#))) H I J K L . #@2#)))
(FOO ARG1
     (A (B (C (D (E (F (G))))))
        H I J K L M N))
ACL2 !>(without-evisc (foo arg1 (a (b (c (d (e (f (g)))))) h i j k l m n)))

ACL2 Error in macro expansion:  Wrong number of args in macro expansion
of (FOO ARG1 (A (B (C (D (E (F (G)))))) H I J K L M N)).

ACL2 !>

If you wish to know which elided expressions are equal, you may call set-iprint with non-nil value for keyword argument :share. That will turn on iprint sharing, which causes behavior as shown below: the value printed shows the iprint index 2 being used twice for the list (C D E F).

ACL2 !>'((a b c d e f) (a b c d e f) (a b c d e f))
((A B . #@2#) (A B . #@2#) . #@3#)
ACL2 !>

We use the log displayed below to explain iprint sharing a bit more. The Warning below is pointing out that previous iprint indices are no longer valid; we are starting over. The first Observation points out that iprint sharing is on, and gives the name :IPRINT-FAL to look for in (fast-alist-summary) in case you want information on the fast-alist that associates values with corresponding iprint indices. To see the relevance of a fast-alist, note that the two elided occurrences of the list (C D E F) were originally not the identical list in memory; to make them identical, hons-copy is applied to each to get the same list in memory, which is the one associated with iprint index 2 in a fast-alist named :IPRINT-FAL.

ACL2 !>(set-iprint t :share t)

ACL2 Warning [Iprint] in SET-IPRINT:  Converting SET-IPRINT action
from T to :RESET-ENABLE, as required by use of keyword :SHARE or :HARD-
BOUND.  See :DOC set-iprint.


ACL2 Observation in SET-IPRINT:  Iprinting is enabled with sharing,
with a fast-alist whose name is :IPRINT-FAL.

ACL2 Observation in SET-IPRINT:  Iprinting has been reset and enabled.
ACL2 !>(set-evisc-tuple (evisc-tuple 2 2 nil nil) :sites :all)
 (:TERM :LD . #@1#)
ACL2 !>'((a b c d e f) (a b c d e f) (a b c d e f))
((A B . #@2#) (A B . #@2#) . #@3#)
ACL2 !>'(b c d e f)
(B C . #@4#)
ACL2 !>

One might have expected the last form printed above to take advantage of the fact that the tail (C D E F) of the input's value is already associated with iprint index 2. If you want that sort of behavior — that is, where we use an existing iprint index even when we have not yet reached the print-level or print-depth specified by our most recent call of set-evisc-tuple — then we can use the special value :eager for keyword :share, which gives us eager iprinting:

(set-iprint t :share :eager)

If we use that call of set-iprint instead of our earlier one above (that is, with :share t), then the first of the two last results from the log above is unchanged, but in the second result, the tail (C D E F) is indeed abbreviated using iprint index 2.

ACL2 !>'((a b c d e f) (a b c d e f) (a b c d e f))
((A B . #@2#) (A B . #@2#) . #@3#)
ACL2 !>'(b c d e f)
(B . #@2#)
ACL2 !>

The documentation above probably suffices for most users. For those who want more details, below we detail all the ways to use the set-iprint utility.

Example Forms:
(set-iprint t)   ; enable iprinting (elision with #@i@)
(set-iprint nil) ; disable iprinting

General Form:
(set-iprint action          ; t, nil, :reset, :reset-enable, or :same
            :share      sym ; initially nil
            :soft-bound s   ; initially  1000
            :hard-bound h   ; initially 10000)

where all arguments are optional, but ACL2 queries for action if it is omitted. All arguments are evaluated. When a keyword argument is omitted, there is no change in the behavior that it controls. For now we defer further explanations of the keyword arguments. The values for action are as follows.

t — Enable iprinting. If either keyword :share or :hard-bound is supplied, then t is converted to :reset-enable.

nil — Disable iprinting. If either keyword :share or :hard-bound is supplied, then nil is converted to :reset. Otherwise, if the next call of set-iprint is with a first argument of t, then iprint indices will start at the next available value rather than going back to 1.

:reset — Reset iprinting to its initial disabled state, so that when enabled, the first index i for which `#@i# is printed will be 1. Note that all stored information for existing iprint indices will be erased.

:reset-enable — Reset iprinting as with :reset, and then enable iprinting.

:same — If either keyword :share or :hard-bound is supplied, then :same is converted to :reset or :reset-enable according to whether iprinting is currently disabled or enabled, respectively. Otherwise, make no change to the iprinting state other than setting the soft-bound if specified, as explained below.

The value of :share must be a symbol, with default nil. If the value is nil, then an elided value will be printed using the next available iprint index. The value :same is treated as though :share had not been supplied. Otherwise, iprint sharing is on, which provides the following behavior. Suppose that a value V is to be elided that would be assigned the next available iprint index, N. If an iprint index I < N is already associated with a value equal to V, then ACL2 will print #@I for V instead of #@N. Thus, N will remain the next available iprint index. This behavior is implemented using a fast-alist that associates values with indices; in our example, the hons-copy of V is associated with I. If the value of :share is t then the name of this fast-alist — that is, its initial value — is :iprint-fal; otherwise, the value of :share (other than nil or :same) is its name. This name is useful when viewing the output of fast-alist-summary. Finally, a special case, called ``eager sharing'', is installed if the value of :share is :eager. In that case, the behavior described above — where #@I is printed for V — will occur even if the value V would otherwise not be elided, provided the most recent call of set-evisc-tuple specified a non-nil print-level or print-length.

Immediately after a top-level form is read, hence before it is evaluated, a check is made for whether the latest iprint index exceeds a certain bound, (iprint-soft-bound state) — 1000, by default. If so, then the (iprint-last-index state) is set back to 0 so that the next iprint index that is generated will be 1. This soft bound can be changed to any positive integer k by calling set-iprint with :soft-bound k, for example: (set-iprint :same :soft-bound k)].

The above ``soft bound'' is applied once for each top-level form, but you may want finer control by applying a bound after the pretty-printing of each individual form (since many forms may be pretty-printed between successive evaluations of top-level forms). That bound is (iprint-hard-bound state), and can be set with the :hard-bound argument in analogy to how :soft-bound is set, as described above, but with the effect of resetting iprinting, with (iprint-last-index state) set back to 0.

A ``rollover'' is the detection that the soft or hard bound has been exceeded, along with a state update setting (iprint-last-index state) to 0 so that the next iprint index will be 1. Immediately before a rollover, any index beyond the last iprint index used (which must be from before an earlier rollover) is no longer available for reading. At the top level of the ACL2 read-eval-print loop, this works as follows: ACL2 reads the next top-level form according to the current iprint state, then handles a rollover if the latest iprint index exceeded the current soft bound. The following log illustrates a rollover, which follows the description above.

ACL2 !>(set-iprint t :soft-bound 3)

ACL2 Observation in SET-IPRINT:  The soft-bound for iprinting has been
set to 3.

ACL2 Observation in SET-IPRINT:  Iprinting has been enabled.
ACL2 !>(set-evisc-tuple (evisc-tuple 2 3 nil nil) :sites :ld)
 (:LD)
ACL2 !>'((a b c d e f g) (a b c d e f g) (a b c d e f g))
((A B C . #@1#) (A B C . #@2#) (A B C . #@3#))
ACL2 !>'((a b c d e f g) (a b c d e f g) (a b c d e f g))
((A B C . #@4#) (A B C . #@5#) (A B C . #@6#))
ACL2 !>(without-evisc '((A B C . #@4#) (A B C . #@5#) (A B C . #@6#)))
((A B C D E F G)
 (A B C D E F G)
 (A B C D E F G))
ACL2 !>'(1 2 3 4 5)
(1 2 3 . #@1#)
ACL2 !>'((a b c d e f g) (a b c d e f g) (a b c d e f g))
((A B C . #@2#) (A B C . #@3#) (A B C . #@4#))
ACL2 !>(without-evisc '((A B C . #@4#) (A B C . #@5#) (A B C . #@6#)))
((A B C D E F G)
 (A B C D E F G)
 (A B C D E F G))
ACL2 !>(without-evisc '((A B C . #@4#) (A B C . #@5#) (A B C . #@6#)))

***********************************************
************ ABORTING from raw Lisp ***********
********** (see :DOC raw-lisp-error) **********
Error:  Out-of-bounds index in #@5#.  See :DOC set-iprint.
***********************************************

The message above might explain the error.  If not, and
if you didn't cause an explicit interrupt (Control-C),
then it may help to see :DOC raw-lisp-error.

To enable breaks into the debugger (also see :DOC acl2-customization):
(SET-DEBUGGER-ENABLE T)
ACL2 !>

Rollover has the following additional effect when iprint sharing is on: it is illegal to read a form that has both an index from before the rollover and an index from after the rollover. The following log illustrates this requirement. Note that if the last input form below were read without error, the result would likely be highly confusing, since iprint index 1 no longer refers to the value it was originally given at the time the other iprint indices in the input (2, 3, and 4) were given their values.

ACL2 !>(set-iprint t :soft-bound 3 :share t)

ACL2 Warning [Iprint] in SET-IPRINT:  Converting SET-IPRINT action
from T to :RESET-ENABLE, as required by use of keyword :SHARE or :HARD-
BOUND.  See :DOC set-iprint.


ACL2 Observation in SET-IPRINT:  The soft-bound for iprinting has been
set to 3.

ACL2 Observation in SET-IPRINT:  Iprinting is enabled with sharing,
with a fast-alist whose name is :IPRINT-FAL.

ACL2 Observation in SET-IPRINT:  Iprinting has been reset and enabled.
ACL2 !>(set-evisc-tuple (evisc-tuple 2 3 nil nil) :sites :ld)
 (:LD)
ACL2 !>'((a b c d) (x y z w))
((A B C . #@1#) (X Y Z . #@2#))
ACL2 !>'((e f g h) (k l m n))
((E F G . #@3#) (K L M . #@4#))
ACL2 !>'(#@1# #@2# #@3# #@4#) ; OK, since rollover occurs after the read
((D) (W) (H) . #@1#)
ACL2 !>'(#@1# #@2# #@3# #@4#)

***********************************************
************ ABORTING from raw Lisp ***********
********** (see :DOC raw-lisp-error) **********
Error:  Attempt to read a form containing both an index
created before the most recent rollover (#@2#) and
an index created after that rollover (#@1#).  See :DOC set-iprint.
***********************************************

The message above might explain the error.  If not, and
if you didn't cause an explicit interrupt (Control-C),
then it may help to see :DOC raw-lisp-error.

To enable breaks into the debugger (also see :DOC acl2-customization):
(SET-DEBUGGER-ENABLE T)
ACL2 !>

We conclude by mentioning two cases where iprinting and evisc-tuples are ignored. (1) This is typically the case when printing results in raw Lisp outside the ACL2 loop. To use iprinting and evisc-tuples in raw Lisp, use raw-mode; see set-raw-mode. In raw-mode, results that are ACL2 objects will be printed in the same way that ACL2 would print those results if not in raw-mode. (2) Iprinting and evisc-tuples are ignored by print-object$, which however is sensitive to many settings that do not affect formatted (fmt etc.) printing; see print-control.

The reader interested in design and implementation issues considered during the addition of iprinting to ACL2 is invited to read the paper ``Abbreviated Output for Input in ACL2: An Implementation Case Study''; see the proceedings of ACL2 Workshop 2009.