		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-literal

Pretty-print a literal.

Signature
(pprint-literal lit) → part
Arguments: lit — Guard (literalp lit).
Returns: part — Type (msgp part).

Definitions and Theorems

Function: pprint-literal

(defun pprint-literal (lit)
  (declare (xargs :guard (literalp lit)))
  (let ((__function__ 'pprint-literal))
    (declare (ignorable __function__))
    (literal-case
         lit
         :bool (pprint-boolean lit.val)
         :unsigned (msg "~@0~@1" (pprint-natural lit.val)
                        (pprint-bitsize-to-utype lit.size))
         :signed (msg "~@0~@1" (pprint-natural lit.val)
                      (pprint-bitsize-to-itype lit.size))
         :string (msg "\"~@0\"" (pprint-char-list lit.get))
         :address (pprint-address lit.get)
         :field (msg "~@0field" (pprint-natural lit.val))
         :group (pprint-group-literal lit.get)
         :scalar (msg "~@0scalar" (pprint-natural lit.val)))))

Theorem: msgp-of-pprint-literal

(defthm msgp-of-pprint-literal
  (b* ((part (pprint-literal lit)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: pprint-literal-of-literal-fix-lit

(defthm pprint-literal-of-literal-fix-lit
  (equal (pprint-literal (literal-fix lit))
         (pprint-literal lit)))

Theorem: pprint-literal-literal-equiv-congruence-on-lit

(defthm pprint-literal-literal-equiv-congruence-on-lit
  (implies (literal-equiv lit lit-equiv)
           (equal (pprint-literal lit)
                  (pprint-literal lit-equiv)))
  :rule-classes :congruence)