		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

Cons-ppr1

Signature
(cons-ppr1 x rows width pair-keywords-p config eviscp) → new-rows
Arguments: x — A single printer instruction, representing either a DOT or a single object. Intuitively this is the instruction for the car of the list we're trying to print.
Guard (pinst-p x).; rows — A list of printer instructions that will be printed as a column. Intuitively these are the instructions for the cdr of the list we're trying to print.
Guard (pinstlist-p rows).; width — Guard (posp width).; config — Guard (printconfig-p config).; eviscp — Guard (booleanp eviscp).
Returns: new-rows — Type (pinstlist-p new-rows).

The goal here is to add x to rows by either merging it with the first row or—if that won't work because it's too wide—by putting it into a new row. For instance, x might be (FLAT 3 ABC) and rows could be ((FLAT 7 DEF GHI) ...). In this case we need to decide to either:

add a new row                   merge with the first row
ABC                    -or-     ABC DEF GHI
DEF GHI                         ...
...

The default behavior is always to add a new row, i.e., to just cons x onto rows. But if the first row is flat, and we can fit x onto it without using up too many characters, then we should extend the first row.

It is also here that we deal specially with keywords. If x is (FLAT 3 :ABC) and column is ((...) (...)) then we have the choice:

add a new row                   merge with the first row
:ABC                   -or-     :ABC (...)
(...)                           (...)
(...)

Definitions and Theorems

Function: cons-ppr1

(defun cons-ppr1 (x rows
                    width pair-keywords-p config eviscp)
 (declare (xargs :guard (and (pinst-p x)
                             (pinstlist-p rows)
                             (posp width)
                             (printconfig-p config)
                             (booleanp eviscp))))
 (declare
    (xargs :guard
           (case (pinst-kind x)
             (:flat (let ((what (pflat->what (pinst-flat->guts x))))
                      (and (consp what) (not (cdr what)))))
             (otherwise t))))
 (let ((acl2::__function__ 'cons-ppr1))
  (declare (ignorable acl2::__function__))
  (b*
   ((x (pinst-fix x))
    (rows (pinstlist-fix rows))
    ((when (atom rows)) (cons x rows))
    (xkind (pinst-kind x))
    ((when (eq xkind :flat))
     (b* ((x.guts (pinst-flat->guts x))
          (x.what (pflat->what x.guts))
          (x.obj (first x.what))
          ((unless (or (atom x.obj)
                       (and eviscp (evisceratedp x.obj))))
           (cons x rows))
          (row1 (first rows))
          ((unless (and (keywordp x.obj)
                        (keyword-param-valuep row1 eviscp)))
           (maybe-merge-flat x rows width config))
          ((unless (or pair-keywords-p (atom (rest rows))
                       (eq (pinst-kind (second rows)) :keypair)
                       (eq (pinst-kind (second rows))
                           :keyline)))
           (maybe-merge-flat x rows width config))
          ((the unsigned-byte x.width)
           (pflat->width x.guts))
          ((the unsigned-byte row1.width)
           (pinst->width row1))
          (keypair-width (+ 1 x.width row1.width))
          ((when (<= keypair-width width))
           (cons (make-pinst-keypair :width keypair-width
                                     :kwd x.guts
                                     :value row1)
                 (cdr rows))))
       (cons (make-pinst-keyline :guts x.guts)
             rows)))
    ((when (eq xkind :dot))
     (b*
      ((row1 (first rows))
       ((unless (eq (pinst-kind row1) :flat))
        (cons x rows))
       (row1.guts (pinst-flat->guts row1))
       (row1.width (pflat->width row1.guts))
       (merged-width (+ 2 row1.width))
       (flat-right-margin (printconfig->flat-right-margin config))
       ((unless (and (<= merged-width flat-right-margin)
                     (<= merged-width width)))
        (cons x rows))
       (new-guts
        (make-pflat :width merged-width
                    :what (ec-call (car (pflat->what row1.guts))))))
      (cons (make-pinst-flat :guts new-guts)
            (cdr rows)))))
   (cons x rows))))

Theorem: pinstlist-p-of-cons-ppr1

(defthm pinstlist-p-of-cons-ppr1
  (b* ((new-rows (cons-ppr1 x rows
                            width pair-keywords-p config eviscp)))
    (pinstlist-p new-rows))
  :rule-classes :rewrite)