SET-IPRINT

control whether abbreviated output can be read back in 
Major Section:  IO

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

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
            :soft-bound s ; initially  1000
            :hard-bound h ; initially 10000)
where all arguments are optional, but ACL2 queries for action if it is omitted. We defer the explanations of :soft-bound and :hard-bound. The values for action are as follows:

T -- Enable iprinting.

NIL -- Disable iprinting.

: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 -- Make no change to the iprinting state (other than setting the :soft-bound and/or :hard-bound if specified, as explained below).

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. This soft bound can be changed to any positive integer k by calling set-iprint with :soft-bound k, typically (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.

A ``rollover'' is the detection that the soft or hard bound has been exceeded, along with a state update so that the next iprint index will be 1. When a rollover occurs, any index beyond the latest iprint index 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 ***********
Error:  Out-of-bounds index in #@5#.  See :DOC set-iprint.
***********************************************

If you didn't cause an explicit interrupt (Control-C),
then the root cause may be call of a :program mode
function that has the wrong guard specified, or even no
guard specified (i.e., an implicit guard of t).
See :DOC guards.

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, http://www.cs.utexas.edu/users/moore/acl2/workshop-2009/.