Pretty-printing-implementation
Implementation details of our pretty-printing support.
My implementation is very much based on ACL2's pretty printer. The
pretty printer operates in two linear passes: the first pass builds a data
structure that tells the second pass how to print. The basic algorithm dates
from about 1971 and was used in the earliest Edinburgh Pure Lisp Theorem
Prover. It is described in:
Robert S. Boyer. Pretty-Print. Memo
number 64. Department of Computational Logic, School of Artificial
Intelligence, University of Edinburgh. 1973.
Some general principles of pretty-printer are:
- Print flat whenever possible, unless argument lists of length over (say)
40; since they become hard to parse.
- Atoms and eviscerated things (which print like atoms, e.g., <world>)
may be printed on a single line.
- Parenthesized expressions should not be printed on a line with any other
argument (unless the whole form fits on the line).
For instance:
'GOOD' 'BAD'
(foo (bar a) b c d) | (foo (bar a) b |
c d) |
(foo a b |
c d) | ^^ we think it's too easy to
miss 'b' when reading this
(foo (bar a) |
b c d) |Subtopics
- Missing-functionality
- Notes about some ACL2 pretty-printer settings that are not
implemented in our printconfig-p objects.
- Printconfig
- Options that govern various aspects of pretty-printing, e.g., the
margins, numeric base, home package for printing symbols, etc.
- Cons-ppr1
- Print-escaped-charlist
- Print a character list, escaping backslashes and some other character.
- Atom-size
- How many characters are required to print an atom? (BOZO: roughly)
- Print-escaped-str
- Print a string, escaping backslashes and some other character.
- Obj-size
- How many characters are required to print an object. (bounded)
- Maybe-merge-flat
- Basic merging of flat singleton objects into rows.
- Ppr
- Low-level routine to do both passes of pretty-printing.
- Printer-instructions
- Internal "instruction" data structure used by our pretty-printing
algorithm.
- Keyword-param-valuep
- Does a pretty-printer instruction represent a single object, which
could plausibly be the value of a keyword parameter?
- Print-flat-objs
- We print the elements of x, separated by spaces. If x is a
non-nil atom, we print a dot and then x.
- Radix-print-int
- Print an integer in a particular print base, with radix.
- Print-escaped-atom
- Print any arbitrary atom with suitable escaping, obeying the print-base,
print-radix, print-lowercase, and home package settings.
- Print-atom
- Print any arbitrary atom with no escaping, but obeying print-base,
print-radix, and (for symbols) print-lowercase.
- Print-escaped-symbol
- Radix-print-complex
- Print a complex rational in a particular print base, with radix.
- Basic-print-complex
- Print a complex rational in a particular print base, no radix.
- Radix-print-rat
- Print a (non-integer) rational in a particular print base, with radix.
- Spaces1
- Basic-print-rat
- Print a (non-integer) rational in a particular print base, no radix.
- Basic-print-nat
- Print a natural number in a particular print base, no radix.
- Basic-print-int
- Print an integer in a particular print base, no radix.
- Spaces
- My-needs-slashes
- Pinstlist->max-width
- Nat-size
- How many characters are required to represent a natural number?
- Special-term-num
- Print-column
- Print a list of instructions in a column.
- Print-base-fix
- Int-size
- How many characters are required to represent an integer?
- Keyword-fix
- Print-instruction
- Print as directed by a printing instruction.
- Pinst->width
- In-home-package-p
- Eviscerated->guts
- Evisceratedp
- Pprdot
