		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-obj-adeclor

Pretty-print an abstract object declarator.

Signature
(pprint-obj-adeclor declor) → part
Arguments: declor — Guard (obj-adeclorp declor).
Returns: part — Type (msgp part).

This is analogous to pprint-obj-declor.

We print the empty string when there is no declarator, but this case never happens when this pretty-printing function is called from pprint-tyname.

Definitions and Theorems

Function: pprint-obj-adeclor

(defun pprint-obj-adeclor (declor)
  (declare (xargs :guard (obj-adeclorp declor)))
  (let ((__function__ 'pprint-obj-adeclor))
    (declare (ignorable __function__))
    (obj-adeclor-case
         declor :none "" :pointer
         (msg "*~@0" (pprint-obj-adeclor declor.decl))
         :array
         (b* ((sub (pprint-obj-adeclor declor.decl)))
           (if (obj-adeclor-case declor.decl :array)
               (msg "(~@0)[~@1]" sub
                    (if declor.size (pprint-iconst declor.size)
                      ""))
             (msg "~@0[~@1]" sub
                  (if declor.size (pprint-iconst declor.size)
                    "")))))))

Theorem: msgp-of-pprint-obj-adeclor

(defthm msgp-of-pprint-obj-adeclor
  (b* ((part (pprint-obj-adeclor declor)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: pprint-obj-adeclor-of-obj-adeclor-fix-declor

(defthm pprint-obj-adeclor-of-obj-adeclor-fix-declor
  (equal (pprint-obj-adeclor (obj-adeclor-fix declor))
         (pprint-obj-adeclor declor)))

Theorem: pprint-obj-adeclor-obj-adeclor-equiv-congruence-on-declor

(defthm pprint-obj-adeclor-obj-adeclor-equiv-congruence-on-declor
  (implies (obj-adeclor-equiv declor declor-equiv)
           (equal (pprint-obj-adeclor declor)
                  (pprint-obj-adeclor declor-equiv)))
  :rule-classes :congruence)