		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

Ppr

Low-level routine to do both passes of pretty-printing.

Signature
(ppr x col config eviscp acc) → new-acc
Arguments: x — Any ACL2 object to be printed.; col — Current column number.
Guard (natp col).; config — Guard (printconfig-p config).; eviscp — Guard (booleanp eviscp).
Returns: new-acc — Type (character-listp new-acc), given (character-listp acc).

If eviscp is nil, then we pretty print x as given. Otherwise, x has been eviscerated and we give special importance to the *evisceration-mark*. NOTE WELL: This function does not eviscerate -- it assumes the evisceration has been done if needed.

Definitions and Theorems

Function: ppr

(defun ppr (x col config eviscp acc)
  (declare (xargs :guard (and (natp col)
                              (printconfig-p config)
                              (booleanp eviscp))))
  (let ((acl2::__function__ 'ppr))
    (declare (ignorable acl2::__function__))
    (b* (((printconfig config) config)
         (col (if (>= col
                      (the unsigned-byte config.hard-right-margin))
                  0
                col))
         (inst (ppr1 x 0 (- config.hard-right-margin col)
                     config eviscp)))
      (print-instruction inst col config eviscp acc))))

Theorem: character-listp-of-ppr

(defthm character-listp-of-ppr
  (implies (character-listp acc)
           (b* ((new-acc (ppr x col config eviscp acc)))
             (character-listp new-acc)))
  :rule-classes :rewrite)