Generate the files and (if any) the events.
(output-files-gen-files+events tunits/files process const-files state) → (mv erp events state)
If required, we print the translation unit ensemble to a file set; if required, we also generate the constant for the file set. Then 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 output-files-gen-files (map state) (declare (xargs :stobjs (state))) (declare (xargs :guard (filepath-filedata-mapp map))) (let ((__function__ 'output-files-gen-files)) (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 'output-files state)) ((when erp) (reterr (msg "Writing ~x0 failed." path-string)))) (output-files-gen-files (omap::tail map) state))))
Function:
(defun output-files-gen-files+events (tunits/files process const-files state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (tunitens/fileset-p tunits/files) (output-files-process-inputp process) (symbolp const-files)))) (declare (xargs :guard (and (implies (equal process nil) (filesetp tunits/files)) (implies (equal process :print) (transunit-ensemblep tunits/files))))) (let ((__function__ 'output-files-gen-files+events)) (declare (ignorable __function__)) (b* (((reterr) nil state) (events nil) (files (if (eq process :print) (print-fileset tunits/files) tunits/files)) (events (if const-files (cons (cons 'defconst (cons const-files (cons (cons 'quote (cons files 'nil)) 'nil))) events) events)) ((erp state) (output-files-gen-files (fileset->unwrap files) state))) (retok events state))))
Theorem:
(defthm pseudo-event-form-listp-of-output-files-gen-files+events.events (b* (((mv acl2::?erp ?events acl2::?state) (output-files-gen-files+events tunits/files process const-files state))) (pseudo-event-form-listp events)) :rule-classes :rewrite)