• 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/osets
    • Std/io
    • 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

• 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))))