Generate the files and (if any) the events.
(output-files-gen-files+events tunits/files process const-files indent-size paren-nested-conds 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 indent-size paren-nested-conds state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (tunitens/fileset-p tunits/files) (output-files-process-inputp process) (symbolp const-files) (posp indent-size) (booleanp paren-nested-conds)))) (declare (xargs :guard (and (implies (equal process :write) (filesetp tunits/files)) (implies (equal process :print) (and (transunit-ensemblep tunits/files) (transunit-ensemble-unambp tunits/files)))))) (let ((__function__ 'output-files-gen-files+events)) (declare (ignorable __function__)) (b* (((reterr) nil state) (events nil) (files (if (eq process :print) (b* ((options (make-priopt :indent-size indent-size :paren-nested-conds paren-nested-conds))) (print-fileset tunits/files options)) 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 indent-size paren-nested-conds state))) (pseudo-event-form-listp events)) :rule-classes :rewrite)