		Search-engine friendly clone of the ACL2 documentation.

Parser

Token-to-msg

Represent a token as a message.

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

This is used in parser error messages, so it does not have to provide a complete description of the token for all possible tokens. We only give a complete description of keyword and punctuator tokens, because those are the kinds that may be a mismatch (e.g. expecing a :, found a ; instead). For the other kinds, we give a more generic description.

It is convenient to treat uniformly tokens and nil, which happens when the end of the file is reached. This is why this function takes an optional token as input.

Definitions and Theorems

Function: token-to-msg

(defun token-to-msg (token)
 (declare (xargs :guard (token-optionp token)))
 (let ((__function__ 'token-to-msg))
   (declare (ignorable __function__))
   (if token
    (token-case token
                :keyword (msg "the keyword ~x0" token.unwrap)
                :ident "an identifier"
                :const "a constant"
                :string "a string literal"
                :punctuator (msg "the punctuator ~x0" token.unwrap))
    "end of file")))

Theorem: msgp-of-token-to-msg

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