Major Section: IO
When ACL2 pretty-prints large expressions using formatted printing
(see fmt), it may save time and space by printing tokens `
...' 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= 1,2,3,... -- all in base 10. ACL2 can read back in such `
#@i#' because under the hood,
iis 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 ``
iprinting'', to suggest the printing of token `
#@i#'. We call
ithe ``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-countexample just above, but so that you can see it. The macro
without-evisceliminates 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
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
actionif it is omitted. We defer the explanations of
:hard-bound. The values for
actionare as follows:
T-- Enable iprinting.
NIL-- Disable iprinting.
:RESET-- Reset iprinting to its initial disabled state, so that when enabled, the first index
ifor 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
:hard-boundif 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
: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
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
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/sandip/acl2-09/.