		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-transunit

Print a translation unit.

Signature
(print-transunit tunit pstate) → new-pstate
Arguments: tunit — Guard (transunitp tunit).; pstate — Guard (pristatep pstate).
Returns: new-pstate — Type (pristatep new-pstate).

If there is a line comment, we print it in one line, followed by a blank line if there are external declarations.

Definitions and Theorems

Function: print-transunit

(defun print-transunit (tunit pstate)
 (declare (xargs :guard (and (transunitp tunit)
                             (pristatep pstate))))
 (declare
  (xargs
     :guard (and (transunit-unambp tunit)
                 (transunit-aidentp tunit (pristate->gcc pstate)))))
 (let ((__function__ 'print-transunit))
  (declare (ignorable __function__))
  (b*
   (((transunit tunit) tunit)
    (pstate
     (if tunit.comment
      (if (grammar-character-listp tunit.comment)
          (b* ((pstate (print-astring "// " pstate))
               (pstate (print-chars tunit.comment pstate))
               (pstate (print-new-line pstate))
               (pstate (if tunit.declons (print-new-line pstate)
                         pstate)))
            pstate)
       (prog2$
        (raise
         "Internal error: ~
                       non-grammatical line comment ~x0."
         tunit.comment)
        pstate))
      pstate)))
   (print-ext-declon-list tunit.declons pstate))))

Theorem: pristatep-of-print-transunit

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

Theorem: pristate->gcc-of-print-transunit

(defthm pristate->gcc-of-print-transunit
  (b* ((?new-pstate (print-transunit tunit pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: print-transunit-of-transunit-fix-tunit

(defthm print-transunit-of-transunit-fix-tunit
  (equal (print-transunit (transunit-fix tunit)
                          pstate)
         (print-transunit tunit pstate)))

Theorem: print-transunit-transunit-equiv-congruence-on-tunit

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

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

(defthm print-transunit-of-pristate-fix-pstate
  (equal (print-transunit tunit (pristate-fix pstate))
         (print-transunit tunit pstate)))

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

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