		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-obj-declor

Pretty-print an object declarator.

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

This requires a bit of care, because we may need to print parentheses for proper grouping. This is similar to the pretty-printing of expressions, but much simpler, so we do can put all the logic into this pretty-printing function, avoiding all the structure needed for expressions (which need that structure due to their greater complexity). The idea is the same, though.

Array declarators bind tighter than pointer declarators. E.g. *x[] is like *(x[]), not like (*x)[]. This is because the concrete syntax *x[] must be organized, according to the C grammar [C:6.7.6], as a pointer and a direct-declarator, the latter consisting of another direct-declarator for just the identifier x and of square brackets with nothing between them.

So, analogously to the treatment of expressions, we need to take the relative precendence of pointer and array declarators when pretty-printing them:

If a declarator is an identifier, we just print it.
If a declarator is a pointer declarator, we recursively pretty-print its sub-declarator, and then we add * in front. We do not add any parentheses in this case. So, if the sub-declarator is a pointer one, the two * will print one after the other, as desired. If instead the sub-declarator is an array one, then as explained above it binds tighter, so it needs no parentheses.
If a declarator is an array one, we recursively pretty-print its sub-declarator. If that sub-declarator is a pointer one, then we need to parenthesize it, because otherwise things would bind in the wrong way. If instead the sub-declarator is an identifier or an array one, then no parentheses are added, as desired.

Definitions and Theorems

Function: pprint-obj-declor

(defun pprint-obj-declor (declor)
  (declare (xargs :guard (obj-declorp declor)))
  (let ((__function__ 'pprint-obj-declor))
    (declare (ignorable __function__))
    (obj-declor-case
         declor :ident (pprint-ident declor.get)
         :pointer
         (msg "*~@0" (pprint-obj-declor declor.decl))
         :array
         (b* ((sub (pprint-obj-declor declor.decl)))
           (if (obj-declor-case declor.decl :pointer)
               (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-declor

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

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

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

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

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