Write a file set to the file system.
(write-files-gen-files fileset state) → (mv erp state)
We go through the file set, and write the data of each value in the map to the path of the associated key in the map.
Function:
(defun write-files-gen-files-loop (map state) (declare (xargs :stobjs (state))) (declare (xargs :guard (filepath-filedata-mapp map))) (let ((__function__ '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 'write-files state)) ((when erp) (reterr (msg "Writing ~x0 failed." path-string)))) (write-files-gen-files-loop (omap::tail map) state))))
Function:
(defun write-files-gen-files (fileset state) (declare (xargs :stobjs (state))) (declare (xargs :guard (filesetp fileset))) (let ((__function__ 'write-files-gen-files)) (declare (ignorable __function__)) (write-files-gen-files-loop (fileset->unwrap fileset) state)))