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:
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
The most convenient, high-level functions to use are:
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 things.
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
Even with respect to
More details about the algorithm and implementation can be found in pretty-printing-implementation.