A tree structure for building up a block of text from components.

A printtree is simply either a printable object or else a cons of printtree objects. It represents a block of text formed by concatenating together all its leaves in reverse order, i.e. from rightmost to leftmost.

It might seem like an odd choice to standardize on right-to-left. We do so because usually we build up a block of text by adding text to the end, and usually we expect trees of conses to be longer on the right than on the left, like lists. Some Lisps might be especially optimized for such constructs and not so much for the other kind.

A printtree object can be turned into a string using the function

In case there's any reason to accumulate a printtree left to right instead,
it can be turned into a string in reverse order using

**Function: **

(defun printtree-p (x) (declare (xargs :guard t)) (if (atom x) (printable-p x) (and (printtree-p (car x)) (printtree-p (cdr x)))))

**Theorem: **

(defthm printtree-p-when-printable-p (implies (printable-p x) (printtree-p x)))

**Theorem: **

(defthm printtree-p-of-cons (equal (printtree-p (cons x y)) (and (printtree-p x) (printtree-p y))))

**Theorem: **

(defthm printtree-p-when-consp (implies (and (consp x) (printtree-p (car x)) (printtree-p (cdr x))) (printtree-p x)) :rule-classes ((:rewrite :backchain-limit-lst (0 nil nil))))

**Function: **

(defun printtree-fix$ (x) (declare (xargs :guard t)) (if (atom x) (printable-fix$ x) (cons (printtree-fix$ (car x)) (printtree-fix$ (cdr x)))))

**Function: **

(defun printtree-fix (x) (declare (xargs :guard (printtree-p x))) (mbe :logic (if (atom x) (printable-fix x) (cons (printtree-fix (car x)) (printtree-fix (cdr x)))) :exec x))

**Theorem: **

(defthm printtree-p-of-printtree-fix (printtree-p (printtree-fix x)))

**Theorem: **

(defthm printtree-fix-when-printtree-p (implies (printtree-p x) (equal (printtree-fix x) x)))

**Theorem: **

(defthm printtree-fix-of-cons (equal (printtree-fix (cons a b)) (cons (printtree-fix a) (printtree-fix b))))

**Function: **

(defun printtree->strlist-aux (x acc) (declare (xargs :guard (printtree-p x))) (if (atom x) (if (printable-fix x) (cons (printable->str x) acc) acc) (printtree->strlist-aux (cdr x) (printtree->strlist-aux (car x) acc))))

**Function: **

(defun printtree->strlist (x) (declare (xargs :guard (printtree-p x))) (mbe :logic (if (atom x) (and (printable-fix x) (list (printable->str x))) (append (printtree->strlist (cdr x)) (printtree->strlist (car x)))) :exec (printtree->strlist-aux x nil)))

**Theorem: **

(defthm printtree->strlist-aux-elim (equal (printtree->strlist-aux x acc) (append (printtree->strlist x) acc)))

**Theorem: **

(defthm string-listp-of-printtree->strlist (string-listp (printtree->strlist x)))

**Function: **

(defun revappend-printtree (x acc) (declare (xargs :guard (printtree-p x))) (if (atom x) (revappend-printable x acc) (revappend-printtree (car x) (revappend-printtree (cdr x) acc))))

**Theorem: **

(defthm revappend-printtree-elim (equal (revappend-printtree x acc) (revappend-chars (string-append-lst (printtree->strlist x)) acc)))

**Function: **

(defun printtree->str1 (x) (declare (xargs :guard (printtree-p x))) (rchars-to-string (revappend-printtree x nil)))

**Function: **

(defun printtree->str (x) (declare (xargs :guard (printtree-p x))) (mbe :logic (if (atom x) (printable->str x) (concatenate 'string (printtree->str (cdr x)) (printtree->str (car x)))) :exec (if (atom x) (printable->str x) (printtree->str1 x))))

**Theorem: **

(defthm printtree->str-of-cons (equal (printtree->str (cons a b)) (string-append (printtree->str b) (printtree->str a))))

**Theorem: **

(defthm string-append-lst-of-printtree->strlist (equal (string-append-lst (printtree->strlist x)) (printtree->str x)))

**Function: **

(defun printtree->str-left2right (x) (declare (xargs :guard (printtree-p x))) (fast-string-append-lst (reverse (printtree->strlist x))))

- Printable
- A printable element: a string, a character, or NIL, which we take as equivalent to the empty string.