		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-messages

Plexeme-to-msg

Represent a preprocessing lexeme as a message.

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

This is used in preprocessor error messages. It is similar to token-to-msg for the parser.

Definitions and Theorems

Function: plexeme-to-msg

(defun plexeme-to-msg (lexeme)
  (declare (xargs :guard (plexeme-optionp lexeme)))
  (if lexeme (plexeme-case lexeme
                           :header "a header name"
                           :ident (msg "the identifier ~x0"
                                       (ident->unwrap lexeme.ident))
                           :number "a preprocessing number"
                           :char "a character constant"
                           :string "a string literal"
                           :punctuator "a punctuator"
                           :other "some other character"
                           :block-comment "a block comment"
                           :line-comment "a line comment"
                           :newline "a new line"
                           :spaces "one ore more spaces"
                           :horizontal-tab "a horizontal tab"
                           :vertical-tab "a vertical tab"
                           :form-feed "a form feed")
    "end of file"))

Theorem: msgp-of-plexeme-to-msg

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

Theorem: plexeme-to-msg-of-plexeme-option-fix-lexeme

(defthm plexeme-to-msg-of-plexeme-option-fix-lexeme
  (equal (plexeme-to-msg (plexeme-option-fix lexeme))
         (plexeme-to-msg lexeme)))

Theorem: plexeme-to-msg-plexeme-option-equiv-congruence-on-lexeme

(defthm plexeme-to-msg-plexeme-option-equiv-congruence-on-lexeme
  (implies (plexeme-option-equiv lexeme lexeme-equiv)
           (equal (plexeme-to-msg lexeme)
                  (plexeme-to-msg lexeme-equiv)))
  :rule-classes :congruence)