		Search-engine friendly clone of the ACL2 documentation.

Parser

Char-to-msg

Represent an optional character as a message.

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

As mentioned in parstate, we represent characters as natural numbers, meant to be Unicode code points (more precisely, Unicode scalar values), including ASCII codes as a subset. When an unexpected character is encountered during lexing, we return user-oriented error messages that include a description of the unexpected character. This ACL2 function constructs that description.

We use read-char (defined later) to read characters. That function recognizes three new-line delimiters: line feed, carriage return, and carriage return followed by line feed. That function turns all these three into just a line feed. Thus, when this function is called to convert to a message a character coming from read-char, that character has never code 13 (for carriage return), and if it has code 10 (line feed) it is not necessarily a line feed in the file, but it could be a carriage return possibly followed by line feed. For this reason, we treat the case of code 10 a bit differently, and our *ascii-control-char-names* table has an internal-error-signaling entry for codes 10 and 13, because we do not access that table for those two codes.

We also allow the character to be absent, i.e. to be nil. This happens when we reach the end of the file: attempting to read a character returns nil, instead of a natural number (see read-char). For error messages, it is convenient to treat this case similarly to the case of an actual character. So, for nil, this function returns a description of `end of file'.

Definitions and Theorems

Function: char-to-msg

(defun char-to-msg (char)
  (declare (xargs :guard (nat-optionp char)))
  (let ((__function__ 'char-to-msg))
    (declare (ignorable __function__))
    (cond ((not char) "end of file")
          ((= char 10)
           (msg "the new-line character (LF, CR, or CR LF)"))
          ((< char 32)
           (msg "the ~s0 character (ASCII code ~x1)"
                (nth char *ascii-control-char-names*)
                char))
          ((= char 32)
           "the SP (space) character (ASCII code 32)")
          ((and (<= 33 char) (<= char 126))
           (msg "the ~s0 character (ASCII code ~x1)"
                (acl2::implode (list (code-char char)))
                char))
          ((= char 127)
           "the DEL (delete) character (ASCII code 127)")
          (t (msg "the non-ASCII Unicode character with code ~x0"
                  char)))))

Theorem: msgp-of-char-to-msg

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