		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

Print-escaped-charlist

Print a character list, escaping backslashes and some other character.

Signature
(print-escaped-charlist x slash-char acc) → new-acc
Arguments: x — Characters in the name to be printed.
Guard (character-listp x).; slash-char — Extra character to escape. When printing escaped strings this is typically the " character; for printing symbol names it would typically be the | character.
Guard (characterp slash-char).
Returns: new-acc — Type (character-listp new-acc), given (and (character-listp acc) (character-listp x)).

This is a logically nice definition for print-escaped-str.

Definitions and Theorems

Function: print-escaped-charlist

(defun print-escaped-charlist (x slash-char acc)
  (declare (xargs :guard (and (character-listp x)
                              (characterp slash-char))))
  (let ((acl2::__function__ 'print-escaped-charlist))
    (declare (ignorable acl2::__function__))
    (if (atom x)
        acc
      (print-escaped-charlist (cdr x)
                              slash-char
                              (if (or (eql (car x) #\\)
                                      (eql (car x) slash-char))
                                  (list* (car x) #\\ acc)
                                (cons (car x) acc))))))

Theorem: character-listp-of-print-escaped-charlist

(defthm character-listp-of-print-escaped-charlist
  (implies (and (character-listp acc)
                (character-listp x))
           (b* ((new-acc (print-escaped-charlist x slash-char acc)))
             (character-listp new-acc)))
  :rule-classes :rewrite)

Theorem: print-escaped-charlist-when-atom

(defthm print-escaped-charlist-when-atom
  (implies (atom x)
           (equal (print-escaped-charlist x slash-char acc)
                  acc)))

Theorem: len-of-print-escaped-charlist-weak

(defthm len-of-print-escaped-charlist-weak
  (<= (len acc)
      (len (print-escaped-charlist x slash-char acc)))
  :rule-classes ((:rewrite) (:linear)))

Theorem: len-of-print-escaped-charlist-strong

(defthm len-of-print-escaped-charlist-strong
  (implies (consp x)
           (< (len acc)
              (len (print-escaped-charlist x slash-char acc))))
  :rule-classes ((:rewrite) (:linear)))

Theorem: equal-with-print-escaped-charlist

(defthm equal-with-print-escaped-charlist
  (equal (equal (print-escaped-charlist x slash-char acc)
                acc)
         (atom x)))