Write a translation unit ensemble to the file system.
(print-and-write-files-gen-files tunits state) → (mv erp state)
We go through the file set obtained by printing the translation unit ensemble, and write the data of each value in the map to the path of the associated key in the map.
Function:
(defun print-and-write-files-gen-files-loop (map state) (declare (xargs :stobjs (state))) (declare (xargs :guard (filepath-filedata-mapp map))) (let ((__function__ 'print-and-write-files-gen-files-loop)) (declare (ignorable __function__)) (b* (((reterr) state) ((when (omap::emptyp map)) (retok state)) ((mv path data) (omap::head map)) (path-string (filepath->unwrap path)) ((unless (stringp path-string)) (reterr (msg "File path must contain a string, ~ but it contains ~x0 instead." path-string))) ((mv erp state) (acl2::write-bytes-to-file! (filedata->unwrap data) path-string 'print-and-write-files state)) ((when erp) (reterr (msg "Writing ~x0 failed." path-string)))) (print-and-write-files-gen-files-loop (omap::tail map) state))))
Function:
(defun print-and-write-files-gen-files (tunits state) (declare (xargs :stobjs (state))) (declare (xargs :guard (transunit-ensemblep tunits))) (let ((__function__ 'print-and-write-files-gen-files)) (declare (ignorable __function__)) (b* ((fileset (print-fileset tunits))) (print-and-write-files-gen-files-loop (fileset->unwrap fileset) state))))