Read and preprocess a file set from a given set of paths.
(read-files-read-and-preprocess paths preprocessor state) → (mv erp fileset state)
This is just a thin wrapper around preprocess-files,
added just so that, in case of error,
the
We tell the preprocessing tool not to save any files.
Function:
(defun read-files-read-and-preprocess (paths preprocessor state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (filepath-setp paths) (stringp preprocessor)))) (let ((__function__ 'read-files-read-and-preprocess)) (declare (ignorable __function__)) (b* (((reterr) (fileset nil) state) ((mv erp fileset state) (preprocess-files paths :preprocessor preprocessor)) ((when erp) (reterr (msg "Preprocessing of ~x0 failed." paths)))) (retok fileset state))))
Theorem:
(defthm filesetp-of-read-files-read-and-preprocess.fileset (b* (((mv acl2::?erp ?fileset acl2::?state) (read-files-read-and-preprocess paths preprocessor state))) (filesetp fileset)) :rule-classes :rewrite)