		Search-engine friendly clone of the ACL2 documentation.

Ppr-special-syms

A table to control indentation for pretty-printing

ACL2 output is generally pretty-printed: that is, spacing and indentation are controlled to enhance readability and aesthetics of the output. Indentation may be controlled by using the table, ppr-special-syms as described below. We thank Stephen Westfold for enhancing the pretty-printer with support for ppr-special-syms.

The initial value of the ppr-special-syms table is given by the constant *ppr-special-syms* as follows. It associates each key, a symbol, with a corresponding special-term-num as discussed below.

Definition: *ppr-special-syms*

(defconst *ppr-special-syms*
  '((case . 1)
    (case-match . 1)
    (defabsstobj . 1)
    (defaxiom . 1)
    (defchoose . 3)
    (defcong . 2)
    (defconst . 1)
    (defmacro . 2)
    (defstobj . 1)
    (defthm . 1)
    (defthmd . 1)
    (defun . 2)
    (defun-inline . 2)
    (defun-sk . 2)
    (defund . 2)
    (encapsulate . 1)
    (if . 2)
    (lambda . 1)
    (lambda$ . 1)
    (let . 1)
    (let* . 1)
    (mutual-recursion . 0)
    (mv-let . 2)
    (table . 1)))

The ppr-special-syms table is extended for some common macros in the files where they are defined, for example for define and b*.

For calls of special forms and macros in the ppr-special-syms table, their bodies are indented by 2 rather than in the usual default manner. To support this we allow a special-term-num to be associated with a symbol. Arguments of such symbols in the function position beyond the special-term-num position are indented by 2. Earlier arguments are printed normally. For example, the symbol, let, has a special-term-num of 1, so the first argument is printed normally and subsequent arguments are indented by 2, as follows.

(LET ((A B)
      (C D))
  (F A C))

Since `if' has a special-term-num of 2, the first two arguments are printed normally and the other is indented by 2, for example as follows.

(IF (P A B)
    (F A B)
  (G A B))

Macros often have as their first argument a symbol, so these are treated specially by putting them on the first line and any remaining arguments before the body arguments begin on the same line if there is space. For example, defun has special-term-num 2, which is evident in the following output.

(DEFUN FOO (X Y Z)
  (F X Y Z))

Keyword pairs in macro calls can occur in other places than at the end of an argument list, so keyword pairing is done more aggressively, as in the following output.

(DEFINE FOO ((X P1)
             (Y P2))
  :GUARD (P3 X Y)
  (F X Y Z))