		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-printer

Pprint-ident

Print an identifier after preprocessing.

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

Definitions and Theorems

Function: pprint-ident

(defun pprint-ident (ident bytes)
  (declare (xargs :guard (and (identp ident)
                              (byte-listp bytes))))
  (let ((__function__ 'pprint-ident))
    (declare (ignorable __function__))
    (b* ((string (ident->unwrap ident))
         ((unless (stringp string))
          (raise "Internal error: bad identifier non-string ~x0."
                 string))
         (chars (acl2::string=>nats string))
         ((unless (grammar-character-listp chars))
          (raise "Internal error: bad identifier characters ~x0."
                 chars)))
      (pprint-chars chars bytes))))

Theorem: byte-listp-of-pprint-ident

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