		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-jchar

Pretty-print a character.

Signature
(print-jchar char) → part
Arguments: char — Guard (characterp char).
Returns: part — Type (msgp part).

This turns an ACL2 character, viewed as a Java character, into a form that can be correctly pretty-printed when the character is part of a Java character or string literal. This takes into account not only Java's character and string literal syntax [JLS14:3.10], but also the fact that the pretty-printer uses ACL2's formatted printing, where the tilde has a special meaning.

A single quote or double quote or backslash is preceded by a backslash. Double quotes do not need a preceding backslash in a character literal, and single quotes do not need a preceding backslash in a string literal, but for now for simplicity we escape both single and double quotes in both character and string literals.

The other characters with codes between 32 and 125 are left unchanged.

For backspace, horizontal tab, line feed, form feed, and carriage return we use the escape sequences b, t, n, f, and r.

All the other characters, including tilde, are turned into their octal escapes. This is needed for tilde, which otherwise would cause errors or misinterpretations in ACL2's formatted printing.

Definitions and Theorems

Function: print-jchar

(defun print-jchar (char)
  (declare (xargs :guard (characterp char)))
  (let ((__function__ 'print-jchar))
    (declare (ignorable __function__))
    (b* (((when (member char '(#\' #\" #\\)))
          (implode (list #\\ char)))
         (code (char-code char))
         ((when (and (<= 32 code) (<= code 125)))
          (implode (list char)))
         ((when (= code 8)) "\\b")
         ((when (= code 9)) "\\t")
         ((when (= code 10)) "\\n")
         ((when (= code 12)) "\\f")
         ((when (= code 13)) "\\r"))
      (implode (cons #\\ (str::nat-to-oct-chars code))))))

Theorem: msgp-of-print-jchar

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