		Search-engine friendly clone of the ACL2 documentation.

Input-files-implementation

Input-files-read-files

Read a file set from a given set of paths.

Signature
(input-files-read-files files path state) → (mv erp fileset state)
Arguments: files — Guard (string-listp files).; path — Guard (stringp path).
Returns: fileset — Type (filesetp fileset).

We go through each file, we prepend the path, and we attempt to read the file at each resulting path, constructing the file set along the way. Recall that path never ends with / (unless it is just /), because input processing removes the ending slash.

Definitions and Theorems

Function: input-files-read-files

(defun input-files-read-files (files path state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (string-listp files)
                              (stringp path))))
  (let ((__function__ 'input-files-read-files))
    (declare (ignorable __function__))
    (b* (((reterr) (irr-fileset) state)
         ((when (endp files))
          (retok (fileset nil) state))
         (file (car files))
         (path-to-read (str::cat path "/" file))
         ((mv erp bytes state)
          (acl2::read-file-into-byte-list path-to-read state))
         ((when erp)
          (reterr (msg "Reading ~x0 failed." path-to-read)))
         (data (filedata bytes))
         ((erp fileset state)
          (input-files-read-files (cdr files)
                                  path state)))
      (retok (fileset (omap::update (filepath file)
                                    data (fileset->unwrap fileset)))
             state))))

Theorem: filesetp-of-input-files-read-files.fileset

(defthm filesetp-of-input-files-read-files.fileset
  (b* (((mv acl2::?erp ?fileset acl2::?state)
        (input-files-read-files files path state)))
    (filesetp fileset))
  :rule-classes :rewrite)