		Search-engine friendly clone of the ACL2 documentation.

Output-files-implementation

Output-files-gen-files

Generate the files.

Signature
(output-files-gen-files code path indent-size paren-nested-conds state) → (mv erp state)
Arguments: code — Guard (code-ensemblep code).; path — Guard (stringp path).; indent-size — Guard (posp indent-size).; paren-nested-conds — Guard (booleanp paren-nested-conds).

Definitions and Theorems

Function: output-files-gen-files-loop

(defun output-files-gen-files-loop (map path state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (filepath-filedata-mapp map)
                             (stringp path))))
 (let ((__function__ 'output-files-gen-files-loop))
  (declare (ignorable __function__))
  (b*
   (((reterr) state)
    ((when (omap::emptyp map))
     (retok state))
    ((mv filepath data) (omap::head map))
    (file-string (filepath->unwrap filepath))
    ((unless (stringp file-string))
     (reterr
      (msg
       "File path must contain a string, ~
                         but it contains ~x0 instead."
       file-string)))
    (path-to-write (str::cat path "/" file-string))
    ((mv erp state)
     (acl2::write-bytes-to-file! (filedata->unwrap data)
                                 path-to-write 'output-files
                                 state))
    ((when erp)
     (reterr (msg "Writing ~x0 failed." path-to-write))))
   (output-files-gen-files-loop (omap::tail map)
                                path state))))

Function: output-files-gen-files

(defun output-files-gen-files
       (code path
             indent-size paren-nested-conds state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (code-ensemblep code)
                             (stringp path)
                             (posp indent-size)
                             (booleanp paren-nested-conds))))
 (declare (xargs :guard (and (code-ensemble-unambp code)
                             (code-ensemble-aidentp code))))
 (let ((__function__ 'output-files-gen-files))
   (declare (ignorable __function__))
   (b*
     (((reterr) state)
      (options (make-priopt :indent-size indent-size
                            :paren-nested-conds paren-nested-conds))
      (tunits (code-ensemble->transunits code))
      (files (print-fileset tunits options
                            (ienv->gcc (code-ensemble->ienv code))))
      ((erp state)
       (output-files-gen-files-loop (fileset->unwrap files)
                                    path state)))
     (retok state))))