		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-fundef

Print a function definition.

Signature
(print-fundef fundef pstate) → new-pstate
Arguments: fundef — Guard (fundefp fundef).; pstate — Guard (pristatep pstate).
Returns: new-pstate — Type (pristatep new-pstate).

We ensure that there is at least one declaration specifier.

We ensure that the body is a compound statement.

Function definitions are always at the top level, so there is never any indentation to print.

If there is no declaration list, we print the open curly brace just after the declarator, separated by a space. Otherwise, we print a new line after the declarator, then the declarations at the left margin one per line, and finally the body with the curly brace starting at the left margin.

Definitions and Theorems

Function: print-fundef

(defun print-fundef (fundef pstate)
 (declare (xargs :guard (and (fundefp fundef)
                             (pristatep pstate))))
 (declare (xargs :guard (fundef-unambp fundef)))
 (let ((__function__ 'print-fundef))
  (declare (ignorable __function__))
  (b*
   (((fundef fundef) fundef)
    (pstate
        (if fundef.extension (print-astring "__extension__ " pstate)
          (pristate-fix pstate)))
    ((unless fundef.spec)
     (raise "Misusage error: no declaration specifiers.")
     pstate)
    (pstate (print-decl-spec-list fundef.spec pstate))
    (pstate (print-astring " " pstate))
    (pstate (print-declor fundef.declor pstate))
    (pstate
         (if fundef.asm?
             (b* ((pstate (print-astring " " pstate))
                  (pstate (print-asm-name-spec fundef.asm? pstate)))
               pstate)
           pstate))
    (pstate
      (if
       (consp fundef.attribs)
       (b* ((pstate (print-astring " " pstate))
            (pstate (print-attrib-spec-list fundef.attribs pstate)))
         pstate)
       pstate))
    (pstate (if fundef.decls
                (b* ((pstate (print-new-line pstate))
                     (pstate (print-decl-list fundef.decls pstate)))
                  pstate)
              (print-astring " " pstate)))
    ((unless (stmt-case fundef.body :compound))
     (raise
       "Misusage error: function body is not a compound statement.")
     (pristate-fix pstate))
    (pstate (print-block (stmt-compound->items fundef.body)
                         pstate))
    (pstate (print-new-line pstate)))
   pstate)))

Theorem: pristatep-of-print-fundef

(defthm pristatep-of-print-fundef
  (b* ((new-pstate (print-fundef fundef pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: print-fundef-of-fundef-fix-fundef

(defthm print-fundef-of-fundef-fix-fundef
  (equal (print-fundef (fundef-fix fundef)
                       pstate)
         (print-fundef fundef pstate)))

Theorem: print-fundef-fundef-equiv-congruence-on-fundef

(defthm print-fundef-fundef-equiv-congruence-on-fundef
  (implies (fundef-equiv fundef fundef-equiv)
           (equal (print-fundef fundef pstate)
                  (print-fundef fundef-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-fundef-of-pristate-fix-pstate

(defthm print-fundef-of-pristate-fix-pstate
  (equal (print-fundef fundef (pristate-fix pstate))
         (print-fundef fundef pstate)))

Theorem: print-fundef-pristate-equiv-congruence-on-pstate

(defthm print-fundef-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-fundef fundef pstate)
                  (print-fundef fundef pstate-equiv)))
  :rule-classes :congruence)