Print a file set.
(print-fileset tunits) → fileset
The input is a translation unit ensemble in the abstract syntax. We go through each translation unit in the ensemble and print it, obtaining a file for each. We return a file set that corresponds to the translation unit ensemble. The file paths are the same for the translation unit ensemble and for the file set (they are the keys of the maps).
Function:
(defun print-fileset-loop (tunitmap) (declare (xargs :guard (filepath-transunit-mapp tunitmap))) (let ((__function__ 'print-fileset-loop)) (declare (ignorable __function__)) (b* (((when (omap::emptyp tunitmap)) nil) ((mv filepath tunit) (omap::head tunitmap)) (data (print-file tunit)) (filemap (print-fileset-loop (omap::tail tunitmap)))) (omap::update (filepath-fix filepath) (filedata data) filemap))))
Theorem:
(defthm filepath-filedata-mapp-of-print-fileset-loop (b* ((filemap (print-fileset-loop tunitmap))) (filepath-filedata-mapp filemap)) :rule-classes :rewrite)
Theorem:
(defthm keys-of-print-fileset-loop (implies (filepath-transunit-mapp tunitmap) (b* ((?filemap (print-fileset-loop tunitmap))) (equal (omap::keys filemap) (omap::keys tunitmap)))))
Function:
(defun print-fileset (tunits) (declare (xargs :guard (transunit-ensemblep tunits))) (let ((__function__ 'print-fileset)) (declare (ignorable __function__)) (fileset (print-fileset-loop (transunit-ensemble->unwrap tunits)))))
Theorem:
(defthm filesetp-of-print-fileset (b* ((fileset (print-fileset tunits))) (filesetp fileset)) :rule-classes :rewrite)
Theorem:
(defthm keys-of-print-fileset (b* ((?fileset (print-fileset tunits))) (equal (omap::keys (fileset->unwrap fileset)) (omap::keys (transunit-ensemble->unwrap tunits)))))
Theorem:
(defthm print-fileset-of-transunit-ensemble-fix-tunits (equal (print-fileset (transunit-ensemble-fix tunits)) (print-fileset tunits)))
Theorem:
(defthm print-fileset-transunit-ensemble-equiv-congruence-on-tunits (implies (transunit-ensemble-equiv tunits tunits-equiv) (equal (print-fileset tunits) (print-fileset tunits-equiv))) :rule-classes :congruence)