Print (the data bytes of) a file.
(print-file tunit) → data
The input is a translation unit in the abstract syntax. We initialize the printing state, we print the translation unit, we extract the data bytes from the final printing state, and we reverse them (see pristate).
We set the indentation size to two spaces for now. In the future, we will make this a top-level parameter. We envision additional top-level parameters to customize various aspects of the printing (e.g. right margin).
Function:
(defun print-file (tunit) (declare (xargs :guard (transunitp tunit))) (let ((__function__ 'print-file)) (declare (ignorable __function__)) (b* ((indent-size 2) (pstate (init-pristate indent-size)) (pstate (print-transunit tunit pstate)) (bytes-rev (pristate->bytes-rev pstate))) (rev bytes-rev))))
Theorem:
(defthm byte-listp-of-print-file (b* ((data (print-file tunit))) (byte-listp data)) :rule-classes :rewrite)
Theorem:
(defthm print-file-of-transunit-fix-tunit (equal (print-file (transunit-fix tunit)) (print-file tunit)))
Theorem:
(defthm print-file-transunit-equiv-congruence-on-tunit (implies (transunit-equiv tunit tunit-equiv) (equal (print-file tunit) (print-file tunit-equiv))) :rule-classes :congruence)