Read a file set from a given set of paths.
(read-files-read paths state) → (mv erp fileset state)
We go through each path, and we attempt to read the file at each path, constructing the file set along the way.
Function:
(defun read-files-read (paths state) (declare (xargs :stobjs (state))) (declare (xargs :guard (filepath-setp paths))) (let ((__function__ 'read-files-read)) (declare (ignorable __function__)) (b* (((reterr) (fileset nil) state) ((when (emptyp paths)) (retok (fileset nil) state)) (path (head paths)) (path-string (filepath->unwrap path)) ((unless (stringp path-string)) (raise "Internal error: file path ~x0 is not a string." path-string) (reterr t)) ((mv erp bytes state) (acl2::read-file-into-byte-list (filepath->unwrap path) state)) ((when erp) (reterr (msg "Reading ~x0 failed." (filepath->unwrap path)))) (data (filedata bytes)) ((erp fileset state) (read-files-read (tail paths) state))) (retok (fileset (omap::update path data (fileset->unwrap fileset))) state))))
Theorem:
(defthm filesetp-of-read-files-read.fileset (b* (((mv acl2::?erp ?fileset acl2::?state) (read-files-read paths state))) (filesetp fileset)) :rule-classes :rewrite)