		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Pproc-files

Preprocess zero or more files.

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

This is the top-level function of the preprocessor. The files are identified by paths, organized in a list, whose elements are preprocessed in order. For each path, the file is read from the file system and preprocessed. The result of this function is a file set, whose paths are generally a superset of the input ones: the files specified by the input paths may include, directly or indirectly, files whose paths are not in the input list, 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 (paths preprocessed ienv state)
 (declare (xargs :stobjs (state)))
 (declare
      (xargs :guard (and (filepath-listp paths)
                         (filepath-plexeme-list-alistp preprocessed)
                         (ienvp ienv))))
 (b* (((reterr) nil)
      ((when (endp paths))
       (retok (filepath-plexeme-list-alist-fix preprocessed)))
      ((erp preprocessed)
       (pproc-file (car paths)
                   preprocessed ienv state)))
   (pproc-files-loop (cdr paths)
                     preprocessed ienv state)))

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

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

Function: pproc-files

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

Theorem: filesetp-of-pproc-files.fileset

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