		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-printer

Pprint-lexeme

Print a lexeme after preprocessing.

Signature
(pprint-lexeme lexeme bytes) → new-bytes
Arguments: lexeme — Guard (plexemep lexeme).; bytes — Guard (byte-listp bytes).
Returns: new-bytes — Type (byte-listp new-bytes).

Definitions and Theorems

Function: pprint-lexeme

(defun pprint-lexeme (lexeme bytes)
  (declare (xargs :guard (and (plexemep lexeme)
                              (byte-listp bytes))))
  (plexeme-case
       lexeme
       :header (pprint-header-name lexeme.name bytes)
       :ident (pprint-ident lexeme.ident bytes)
       :number (pprint-pnumber lexeme.number bytes)
       :char (pprint-cconst lexeme.const bytes)
       :string (pprint-stringlit lexeme.literal bytes)
       :punctuator (pprint-punctuator lexeme.punctuator bytes)
       :other (pprint-other lexeme.char bytes)
       :block-comment (pprint-block-comment lexeme.content bytes)
       :line-comment (pprint-line-comment lexeme.content bytes)
       :newline (pprint-newline lexeme.chars bytes)
       :spaces (pprint-spaces lexeme.count bytes)
       :horizontal-tab (pprint-horizontal-tab bytes)
       :vertical-tab (pprint-vertical-tab bytes)
       :form-feed (pprint-form-feed bytes)))

Theorem: byte-listp-of-pprint-lexeme

(defthm byte-listp-of-pprint-lexeme
  (b* ((new-bytes (pprint-lexeme lexeme bytes)))
    (byte-listp new-bytes))
  :rule-classes :rewrite)