Preprocess a single file.
(preprocess-file file &key (out 'nil) (save ':auto) (read 't) (preprocessor '"cpp") (extra-args ''("-P")) (state 'state)) → (mv erp pair state)
This function preprocesses a filepathp using the system's C preprocessor. See preprocess-files for a simlilar utility which handles a set of files.
By default, we pass the
Function:
(defun preprocess-file-fn (file out save read preprocessor extra-args state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (filepathp file) (or (not out) (stringp out)) (stringp preprocessor) (string-listp extra-args)))) (let ((__function__ 'preprocess-file)) (declare (ignorable __function__)) (macrolet ((iferr nil '(cons "" (filepath nil)))) (b* ((filename (filepath->unwrap file)) ((unless (stringp filename)) (er-soft-with (iferr) "Filepath is not a string: ~x0" filename)) (canonical-filename (canonical-pathname filename nil state)) ((unless (stringp canonical-filename)) (er-soft-with (iferr) "Filepath does not exist: ~x0" filename)) (filename canonical-filename) (- (acl2::tshell-ensure)) (save (if (eq :auto save) (and out t) save)) ((er out :iferr (iferr)) (if out (value (mbe :exec out :logic (if (stringp out) out ""))) (b* (((mv temp state) (oslib::tempfile filename))) (if temp (value temp) (er-soft-with (iferr) "Could not create temporary file for ~x0" filename))))) ((er out-dirname :iferr (iferr)) (oslib::dirname out)) ((er -) (b* (((mv success state) (oslib::mkdir out-dirname))) (if success (value nil) (er-soft-with (iferr) "Could not make directory: ~x0" out-dirname)))) (preprocess-cmd (str::join (append (list* preprocessor "-E" extra-args) (list filename ">" out)) " ")) ((mv exit-status - state) (acl2::tshell-call preprocess-cmd :print nil :save nil)) ((unless (int= 0 exit-status)) (er-soft-with (iferr) "Preprocessing command ~x0 failed with nonzero exit status: ~x1" preprocess-cmd exit-status)) ((er bytes :iferr (iferr)) (if read (acl2::read-file-into-byte-list out state) (value nil))) ((when (stringp bytes)) (er-soft-with (iferr) "Error reading output file ~x0: ~x1" out bytes)) ((er - :iferr (iferr)) (if save (value nil) (b* (((mv success state) (oslib::rmtree out))) (if success (value nil) (er-soft-with (iferr) "Could not remove output file: ~x0" out)))))) (value (cons (and save out) (and read (filedata bytes))))))))
Theorem:
(defthm consp-of-mv-nth-1-of-preprocess-file (consp (mv-nth 1 (preprocess-file-fn filename save out read preprocessor extra-args state))) :rule-classes ((:rewrite) (:type-prescription)))
Theorem:
(defthm stringp-of-car-of-mv-nth-1-of-preprocess-file (implies (and out save) (stringp (car (mv-nth 1 (preprocess-file-fn filename save out read preprocessor extra-args state))))) :rule-classes ((:rewrite) (:type-prescription)))
Theorem:
(defthm filedatap-of-cdr-of-mv-nth-1-of-preprocess-file (implies read (filedatap (cdr (mv-nth 1 (preprocess-file-fn filename save out read preprocessor extra-args state))))))