A fast, state-free, logic-mode re-implementation of
much of ACL2's built-in pretty-printing capabilities.
This is a two pass, linear time, "exact" pretty printer for ACL2 objects.
My implementation is substantially based on the pretty-printing algorithm from
ACL2 6.4, and offers many similar features.
Why not just use ACL2's built-in pretty-printer? As of ACL2 6.4, the
built-in pretty-printer is a program-mode function that makes heavy use of
state; it gets its configuration settings (margins, arithmetic base,
etc.) out of state globals and does its printing via functions like princ$ which write to an output channel. This can be inconvenient:
- You can't use ACL2's pretty-printer from logic-mode functions.
- You need state available any time you want to create a string using
the printing functions.
- The printing routines are generally not thread-safe.
- Functions like fmt-to-string aren't usable outside of the ACL2
My new pretty-printer has none of these problems. Instead of incrementally
printing to an output stream, it builds up a character list in reverse order,
then reverses it with rchars-to-string. This uses more memory than
ACL2's pretty printer, but the overhead is linear in the size of the output.
Moreover, it appears to perform well---I measured it at about 5.5x
faster than ACL2's pretty printer on one possibly realistic
benchmark; see std/strings/pretty-tests.lisp for details.
The most convenient, high-level functions to use are:
- pretty - convert any ACL2 object into a string.
- revappend-pretty - pretty print onto an accumulator, in reverse
order, which is useful for building strings as described in revappend-chars.
There are many available settings that you can tune to customize the way
that objects are printed; see printconfig-p for details. The defaults
are sensible and are mostly compatible with the way that ACL2 normally prints
We also implement our own eviscerate, which is more limited than
ACL2's and does not, for instance, support ACL2::iprinting.
I do not reimplement the format-string style functions such as fmt
and cw, although something like this is available as part of the vl::printer. Instead, my focus here is on ACL2's ppr functionality that
is at the heart of ACL2's s-expression printing. In other words, this is an
implementation of something like the ~x fmt directive.
Even with respect to ppr, there is some missing-functionality.
I don't implement ACL2::iprinting or include any infix printing support.
(Note added June 2023 by ACL2 implementors: infix printing is now completely
removed for ACL2.) Various complex and unhelpful printer-control variables are
More details about the algorithm and implementation can be found in pretty-printing-implementation.
- Implementation details of our pretty-printing support.
- Elide portions of a term, for use with pretty.
- Pretty-print any ACL2 object into a string.
- Pretty-print any ACL2 object, in reverse order, onto a reverse-order
- Pretty-print a list of ACL2 objects, creating a list of strings.