		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-char

Pretty-print a character.

Signature
(pprint-char char) → part
Arguments: char — Guard (charp char).
Returns: part — Type (msgp part).

If the Leo character is ASCII, there are two cases: if the code is between 32 and 126 (i.e. it is printable), we print the character as the corresponding ACL2 character; otherwise (i.e. the code is between 0 and 31, or is 127), we print it as an ASCII escape. If the Leo character is not ASCII, we print is as a Unicode escape.

Definitions and Theorems

Function: pprint-char

(defun pprint-char (char)
 (declare (xargs :guard (charp char)))
 (let ((__function__ 'pprint-char))
  (declare (ignorable __function__))
  (b* ((code (char->codepoint char)))
   (cond
    ((and (<= 32 code) (<= code 126))
     (acl2::implode (list (code-char code))))
    ((<= code 127)
     (msg "\\x~s0~s1"
          (acl2::implode
               (list (str::octal-digit-to-char (truncate code 16))))
          (acl2::implode
               (list (str::hex-digit-to-char (rem code 16))))))
    (t (msg "\\u{~s0}"
            (str::nat-to-hex-string code)))))))

Theorem: msgp-of-pprint-char

(defthm msgp-of-pprint-char
  (b* ((part (pprint-char char)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: pprint-char-of-char-fix-char

(defthm pprint-char-of-char-fix-char
  (equal (pprint-char (char-fix char))
         (pprint-char char)))

Theorem: pprint-char-char-equiv-congruence-on-char

(defthm pprint-char-char-equiv-congruence-on-char
  (implies (char-equiv char char-equiv)
           (equal (pprint-char char)
                  (pprint-char char-equiv)))
  :rule-classes :congruence)