		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Pproc-files

Preprocess zero or more files.

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

This is the top-level function of the preprocessor. The files are identified by the files strings, which must be all paths relative to the path string (as in input-files). The elements of files are preprocessed in order. Each file is read from the file system and preprocessed. We keep track of the files under preprocessing in a list (initially empty), to detect and avoid circularities. The result of this function is a file set, whose paths are generally a superset of the input ones: the files specified by files may include, directly or indirectly, files whose paths are not in files, e.g. files from the C library. The resulting file set is ``closed'' with respect to #include.

Definitions and Theorems

Function: pproc-files-loop

(defun pproc-files-loop (path files
                              preprocessed preprocessing ienv state)
  (declare (xargs :stobjs (state)))
  (declare
       (xargs :guard (and (stringp path)
                          (string-listp files)
                          (string-plexeme-list-alistp preprocessed)
                          (string-listp preprocessing)
                          (ienvp ienv))))
  (declare (xargs :guard (<= (len preprocessed)
                             *pproc-files-max*)))
  (b* (((reterr) nil state)
       ((when (endp files))
        (retok (string-plexeme-list-alist-fix preprocessed)
               state))
       ((erp preprocessed state)
        (pproc-file path (car files)
                    preprocessed preprocessing ienv state)))
    (pproc-files-loop path (cdr files)
                      preprocessed preprocessing ienv state)))

Theorem: string-plexeme-list-alistp-of-pproc-files-loop.new-preprocessed

(defthm
    string-plexeme-list-alistp-of-pproc-files-loop.new-preprocessed
  (b* (((mv acl2::?erp
            ?new-preprocessed acl2::?state)
        (pproc-files-loop path files
                          preprocessed preprocessing ienv state)))
    (string-plexeme-list-alistp new-preprocessed))
  :rule-classes :rewrite)

Function: pproc-files

(defun pproc-files (path files ienv state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (stringp path)
                              (string-listp files)
                              (ienvp ienv))))
  (b* (((reterr) (irr-fileset) state)
       ((erp preprocessed state)
        (pproc-files-loop path files nil nil ienv state)))
    (retok (fileset (string-plexeme-list-alist-to-filepath-filedata-map
                         preprocessed))
           state)))

Theorem: filesetp-of-pproc-files.fileset

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