		Search-engine friendly clone of the ACL2 documentation.

Std/strings

Pretty-printing

A fast, state-free, logic-mode re-implementation of much of ACL2's built-in pretty-printing capabilities.

Introduction

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 read-eval-print loop.

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.

Quick Start

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 things.

We also implement our own eviscerate, which is more limited than ACL2's and does not, for instance, support ACL2::iprinting.

Limitations

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 also omitted.

Implementation Details

More details about the algorithm and implementation can be found in pretty-printing-implementation.

Subtopics

Pretty-printing-implementation: Implementation details of our pretty-printing support.
Eviscerate: Elide portions of a term, for use with pretty.
Pretty: Pretty-print any ACL2 object into a string.
Revappend-pretty: Pretty-print any ACL2 object, in reverse order, onto a reverse-order character list.
Pretty-list: Pretty-print a list of ACL2 objects, creating a list of strings.