		Search-engine friendly clone of the ACL2 documentation.

Printtree

Printable

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

The main operation on a printable element is printable->str, which turns it into a string. Printable objects are the leaves of printtree objects.

Definitions and Theorems

Function: printable-p

(defun printable-p (x)
  (declare (xargs :guard t))
  (or (stringp x)
      (characterp x)
      (eq x nil)))

Theorem: printable-p-compound-recognizer

(defthm printable-p-compound-recognizer
  (iff (printable-p x)
       (or (stringp x)
           (characterp x)
           (eq x nil)))
  :rule-classes :compound-recognizer)

Theorem: printable-p-when-stringp

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

Theorem: printable-p-when-characterp

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

Function: printable-fix$

(defun printable-fix$ (x)
  (declare (xargs :guard t))
  (and (printable-p x) x))

Function: printable-fix

(defun printable-fix (x)
  (declare (xargs :guard (printable-p x)))
  (mbe :logic (and (printable-p x) x)
       :exec x))

Theorem: printable-p-of-printable-fix

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

Theorem: printable-fix-when-printable-p

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

Theorem: printable-fix$-is-printable-fix

(defthm printable-fix$-is-printable-fix
  (equal (printable-fix$ x)
         (printable-fix x)))

Function: printable->str

(defun printable->str (x)
  (declare (xargs :guard (printable-p x)))
  (cond ((stringp x) x)
        ((characterp x)
         (coerce (list x) 'string))
        (t "")))

Function: revappend-printable

(defun revappend-printable (x acc)
  (declare (xargs :guard (printable-p x)))
  (mbe :logic (revappend-chars (printable->str x) acc)
       :exec (cond ((stringp x) (revappend-chars x acc))
                   ((characterp x) (cons x acc))
                   (t acc))))