		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Pproc-file

Preprocess a file.

Signature
(pproc-file path preprocessed ienv state) → (mv erp new-preprocessed)
Arguments: path — Guard (filepathp path).; preprocessed — Guard (filepath-plexeme-list-alistp preprocessed).; ienv — Guard (ienvp ienv).
Returns: new-preprocessed — Type (filepath-plexeme-list-alistp new-preprocessed).

The file is specified by the path. If the path is found in the alist of already preprocessed files, the alist is returned unchanged. Otherwise, we read the file from the file system and preprocess it, which may involve the recursive preprocessing of more files. This code needs to be fleshed out.

Definitions and Theorems

Function: pproc-file

(defun pproc-file (path preprocessed ienv state)
 (declare (xargs :stobjs (state)))
 (declare
      (xargs :guard (and (filepathp path)
                         (filepath-plexeme-list-alistp preprocessed)
                         (ienvp ienv))))
 (declare (ignore ienv state))
 (b* (((reterr) nil)
      (preprocessed (filepath-plexeme-list-alist-fix preprocessed))
      (filepath+lexemes (assoc-equal (filepath-fix path)
                                     preprocessed))
      ((when filepath+lexemes)
       (retok preprocessed)))
   (reterr :todo)))

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

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