		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-messages

Pchar-to-msg

Represent an optional character as a message, in the preprocessor.

Signature
(pchar-to-msg char) → msg
Arguments: char — Guard (nat-optionp char).
Returns: msg — Type (msgp msg).

This is almost identical to char-to-msg (see its documentation first) with the difference that we consider LF and CR separately. This matches the fact that pread-char, unlike read-char, does not normalize the three possible kinds of new lines to LF.

Definitions and Theorems

Function: pchar-to-msg

(defun pchar-to-msg (char)
  (declare (xargs :guard (nat-optionp char)))
  (cond ((not char) "end of file")
        ((< char 32)
         (msg "the ~s0 character (ASCII code ~x1)"
              (nth char
                   *pchar-to-msg-ascii-control-char-names*)
              char))
        ((utf8-= char 32)
         "the SP (space) character (ASCII code 32)")
        ((and (utf8-<= 33 char)
              (utf8-<= char 126))
         (msg "the ~s0 character (ASCII code ~x1)"
              (acl2::implode (list (code-char char)))
              char))
        ((utf8-= char 127)
         "the DEL (delete) character (ASCII code 127)")
        (t (msg "the non-ASCII Unicode character with code ~x0"
                char))))

Theorem: msgp-of-pchar-to-msg

(defthm msgp-of-pchar-to-msg
  (b* ((msg (pchar-to-msg char)))
    (msgp msg))
  :rule-classes :rewrite)