		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-file

Print (the data bytes of) a file.

Signature
(print-file tunit options) → data
Arguments: tunit — Guard (transunitp tunit).; options — Guard (prioptp options).
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)
  (declare (xargs :guard (and (transunitp tunit)
                              (prioptp options))))
  (declare (xargs :guard (transunit-unambp tunit)))
  (let ((__function__ 'print-file))
    (declare (ignorable __function__))
    (b* ((pstate (init-pristate options))
         (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)))
    (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)
         (print-file tunit options)))

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)
                  (print-file tunit-equiv options)))
  :rule-classes :congruence)

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

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

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)
                  (print-file tunit options-equiv)))
  :rule-classes :congruence)