		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-fun-declor

Pretty-print a function declarator.

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

If the parameter list is empty, we pretty-print void for the parameters instead of nothing, which more clearly say that the function takes no parameters [C:6.7.6.3/10] [C:6.7.6.3/14]. If the declarator is part of a function definition, it does not make a difference, but otherwise it makes a difference; see the references given just above.

Definitions and Theorems

Function: pprint-fun-declor

(defun pprint-fun-declor (declor)
 (declare (xargs :guard (fun-declorp declor)))
 (let ((__function__ 'pprint-fun-declor))
  (declare (ignorable __function__))
  (fun-declor-case
   declor
   :base
   (msg
     "~@0(~@1)" (pprint-ident declor.name)
     (if (consp declor.params)
         (pprint-comma-sep (pprint-param-declon-list declor.params))
       "void"))
   :pointer (msg "*~@0"
                 (pprint-fun-declor declor.decl)))))

Theorem: msgp-of-pprint-fun-declor

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

Theorem: pprint-fun-declor-of-fun-declor-fix-declor

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

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

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