		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

Maybe-merge-flat

Basic merging of flat singleton objects into rows.

Signature
(maybe-merge-flat x rows width config) → new-rows
Arguments: x — Instruction for the car of the list.
Guard (pinst-p x).; rows — Instructions for the cdr of the list.
Guard (pinstlist-p rows).; width — Width we're trying to stay within.
Guard (natp width).; config — Guard (printconfig-p config).
Returns: new-rows — Type (pinstlist-p new-rows).

Definitions and Theorems

Function: maybe-merge-flat

(defun maybe-merge-flat (x rows width config)
 (declare (xargs :guard (and (pinst-p x)
                             (pinstlist-p rows)
                             (natp width)
                             (printconfig-p config))))
 (declare
   (xargs
        :guard (and (eq (pinst-kind x) :flat)
                    (let ((what (pflat->what (pinst-flat->guts x))))
                      (and (consp what) (not (cdr what))))
                    (consp rows))))
 (let ((acl2::__function__ 'maybe-merge-flat))
   (declare (ignorable acl2::__function__))
   (b*
     ((x (pinst-fix x))
      (rows (pinstlist-fix rows))
      (row1 (car rows))
      ((unless (eq (pinst-kind row1) :flat))
       (cons x rows))
      (x.guts (pinst-flat->guts x))
      (row1.guts (pinst-flat->guts row1))
      ((the unsigned-byte row1.width)
       (pflat->width row1.guts))
      ((the unsigned-byte x.width)
       (pflat->width x.guts))
      ((the unsigned-byte merged-width)
       (+ 1
          (the unsigned-byte (+ x.width row1.width))))
      ((the unsigned-byte flat-right-margin)
       (printconfig->flat-right-margin config))
      ((unless (and (<= merged-width flat-right-margin)
                    (<= merged-width width)))
       (cons x rows))
      (x.what (pflat->what x.guts))
      (row1.what (pflat->what row1.guts))
      (merged-guts (make-pflat :width merged-width
                               :what (cons (car x.what) row1.what)))
      (merged-inst (make-pinst-flat :guts merged-guts)))
     (cons merged-inst (rest rows)))))

Theorem: pinstlist-p-of-maybe-merge-flat

(defthm pinstlist-p-of-maybe-merge-flat
  (b* ((new-rows (maybe-merge-flat x rows width config)))
    (pinstlist-p new-rows))
  :rule-classes :rewrite)