		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-file

Print (the data bytes of) a file.

Signature
(print-file tunit options gcc) → data
Arguments: tunit — Guard (transunitp tunit).; options — Guard (prioptp options).; gcc — Guard (booleanp gcc).
Returns: data — Type (byte-listp data).

The input is a translation unit in the abstract syntax. We initialize the printing state, with the printing options passed as input. We print the translation unit, we extract the data bytes from the final printing state, and we reverse them (see pristate).

Definitions and Theorems

Function: print-file

(defun print-file (tunit options gcc)
  (declare (xargs :guard (and (transunitp tunit)
                              (prioptp options)
                              (booleanp gcc))))
  (declare (xargs :guard (transunit-unambp tunit)))
  (let ((__function__ 'print-file))
    (declare (ignorable __function__))
    (b* ((pstate (init-pristate options gcc))
         (pstate (print-transunit tunit pstate))
         (bytes-rev (pristate->bytes-rev pstate)))
      (rev bytes-rev))))

Theorem: byte-listp-of-print-file

(defthm byte-listp-of-print-file
  (b* ((data (print-file tunit options gcc)))
    (byte-listp data))
  :rule-classes :rewrite)

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

(defthm print-file-of-transunit-fix-tunit
  (equal (print-file (transunit-fix tunit)
                     options gcc)
         (print-file tunit options gcc)))

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

(defthm print-file-transunit-equiv-congruence-on-tunit
  (implies (transunit-equiv tunit tunit-equiv)
           (equal (print-file tunit options gcc)
                  (print-file tunit-equiv options gcc)))
  :rule-classes :congruence)

Theorem: print-file-of-priopt-fix-options

(defthm print-file-of-priopt-fix-options
  (equal (print-file tunit (priopt-fix options)
                     gcc)
         (print-file tunit options gcc)))

Theorem: print-file-priopt-equiv-congruence-on-options

(defthm print-file-priopt-equiv-congruence-on-options
  (implies (priopt-equiv options options-equiv)
           (equal (print-file tunit options gcc)
                  (print-file tunit options-equiv gcc)))
  :rule-classes :congruence)

Theorem: print-file-of-bool-fix-gcc

(defthm print-file-of-bool-fix-gcc
  (equal (print-file tunit options (bool-fix gcc))
         (print-file tunit options gcc)))

Theorem: print-file-iff-congruence-on-gcc

(defthm print-file-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (print-file tunit options gcc)
                  (print-file tunit options gcc-equiv)))
  :rule-classes :congruence)