		Search-engine friendly clone of the ACL2 documentation.

Printer

Ps

The printer state stobj.

Our printer's state is a represented as the stobj ps, whose definition is as follows.

Definition: ps

(defstobj ps
  (rchars :type (satisfies str::printtree-p))
  (col :initially 0 :type unsigned-byte)
  (autowrap-col :initially 80
                :type unsigned-byte)
  (autowrap-ind :initially 5
                :type unsigned-byte)
  (htmlp :type (satisfies booleanp)
         :initially nil)
  (tabsize :initially 8
           :type (integer 1 *))
  (pkg :initially a-symbol-that-is-not-imported
       :type symbol)
  (base :initially 10
        :type (satisfies print-base-p))
  (misc :initially nil
        :type (satisfies alistp))
  (eviscconfig :type (satisfies str::eviscconfig-p)
               :initially (:eviscconfig (5 . 15) nil))
  :inline t
  :renaming ((psp vl-ps-p)
             (rchars vl-ps->rchars-raw)
             (col vl-ps->col-raw)
             (autowrap-col vl-ps->autowrap-col-raw)
             (autowrap-ind vl-ps->autowrap-ind-raw)
             (htmlp vl-ps->htmlp-raw)
             (tabsize vl-ps->tabsize-raw)
             (pkg vl-ps->package-raw)
             (base vl-ps->base-raw)
             (misc vl-ps->misc-raw)
             (eviscconfig vl-ps->eviscconfig-raw)
             (update-rchars vl-ps-update-rchars-fn)
             (update-col vl-ps-update-col-fn)
             (update-autowrap-col vl-ps-update-autowrap-col-fn)
             (update-autowrap-ind vl-ps-update-autowrap-ind-fn)
             (update-htmlp vl-ps-update-htmlp-fn)
             (update-tabsize vl-ps-update-tabsize-fn)
             (update-pkg vl-ps-update-package-fn)
             (update-base vl-ps-update-base-fn)
             (update-misc vl-ps-update-misc-fn)
             (update-eviscconfig vl-ps-update-eviscconfig-fn))
  :non-memoizable t)

The main fields are:

rchars -- holds the printed elements (characters and strings) in reverse order. The is badly named because originally it only held characters, but we later extended it to strings to make string-printing more efficient.
col -- records the current column number.

These fields are typically altered by every printing function.

The printer also includes some configuration fields which allow you to influence the behavior of certain printing functions. These fields are typically not changed by printing functions. They can also be easily loaded and saved into a vl-psconfig-p object.

autowrap-col, a column number for autowrapping,
autowrap-ind, number of spaces to indent after autowrapping,
htmlp, a flag indicating whether we are printing html,
tabsize, the tab size to use for   expansion in html mode,
package, a symbol which specifies the "home" package for printing symbols (e.g., ACL2::foo vs. VL::foo.
base, a print-base-p for base 10, 16, etc.
eviscconfig, an str::eviscconfig for ~x directives.

Finally, the printer includes a misc field which must be an alist, and which can be used to pass along any custom parameters that your own printing functions would like to inspect.

I once considered changing the way ps works, so that we would use an array of characters and write into the array, instead of consing characters. This is appealing because we might be able to avoid consing during printing at the cost of having to allocate a buffer at the beginning. But, preliminary tests suggested that there is not much of a speed improvement, and while it might have some nice memory characteristics, the current solution is particularly nice in that it makes with-local-ps very cheap, etc.

We generally hide the existence of ps by introducing ps-free wrapper ps-macros. We ask that you not use the primitive stobj functions directly, but instead use these wrappers.

Subtopics

Ps-macros: Low-level interface to ps.