• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
      • Pretty-printing
      • Printtree
        • Printable
      • Base64
      • Charset-p
      • Strtok!
      • Cases
      • Concatenation
      • Html-encoding
      • Character-kinds
      • Substrings
      • Strtok
      • Equivalences
      • Url-encoding
      • Lines
      • Explode-implode-equalities
      • Ordering
      • Numbers
      • Pad-trim
      • Coercion
      • Std/strings/digit-to-char
      • Substitution
      • Symbols
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Std/strings

Printtree

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 printtree->str.

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 printtree->str-left2right.

pcat is a convenient macro for composing printtree objects together; think of it as string concatenation for printtree objects. (pcat a b c d) simply macroexpands to (list* d c b a), so that (printtree->str (pcat a b c d)) equals (concatenate 'string (printtree->str a) ... (printtree->str d)).

Definitions and Theorems

Function: printtree-p

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

Theorem: printtree-p-when-printable-p

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

Theorem: printtree-p-of-cons

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

Theorem: printtree-p-when-consp

(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: printtree-fix$

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

Function: printtree-fix

(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: printtree-p-of-printtree-fix

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

Theorem: printtree-fix-when-printtree-p

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

Theorem: printtree-fix-of-cons

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

Function: printtree->strlist-aux

(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: printtree->strlist

(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: printtree->strlist-aux-elim

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

Theorem: string-listp-of-printtree->strlist

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

Function: revappend-printtree

(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: revappend-printtree-elim

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

Function: printtree->str1

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

Function: printtree->str

(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: printtree->str-of-cons

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

Theorem: string-append-lst-of-printtree->strlist

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

Function: printtree->str-left2right

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

Subtopics

Printable

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