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:
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.
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
Even with respect to
More details about the algorithm and implementation can be found in pretty-printing-implementation.