		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Pproc

Preprocess files.

All these functions are mutually recursive because, as we preprocess a file, we may need to recursively preprocess files that it includes.

The top-level function of the clique is pproc-file, which is called by pproc-files outside the clique. But it is also called when encoutering files to be included, which is why it is mutually recursive with the other functions.

All the functions take and return state, since they (indirectly) read files.

All the functions take as inputs the path prefix path and the path rest file of the file being preprocessed. These are needed to recursively find and read included files.

All the functions take and return the preprocessed alist, which is extended not only with the file indicated in pproc-file, but also possibly with other files included along the way. See pproc-file and pproc-files.

All the functions also take the preprocessing list, to detect and avoid circularities; see pproc-file and pproc-files.

The top-level function pproc-file takes an implementation environment, from which it constructs a local preprocessing state stobj ppstate, which is passed to and returned from all the other functions. There is one such stobj for each file being preprocessed.

All the functions except the top-level pproc-file take and return the list of lexemes resulting from preprocessing, in reverse order for efficiency. They are reversed into the right order by pproc-file.

Definitions and Theorems

Function: pproc-file

(defun pproc-file (path file
                        preprocessed preprocessing ienv state)
 (declare (xargs :stobjs (state)))
 (declare
      (xargs :guard (and (stringp path)
                         (stringp file)
                         (string-plexeme-list-alistp preprocessed)
                         (string-listp preprocessing)
                         (ienvp ienv))))
 (declare (xargs :guard (<= (len preprocessed)
                            *pproc-files-max*)))
 (b*
  (((reterr) nil state)
   ((unless (mbt (<= (len preprocessed)
                     *pproc-files-max*)))
    (reterr :impossible))
   (file (str-fix file))
   (preprocessing (string-list-fix preprocessing))
   ((when (member-equal file preprocessing))
    (reterr (msg "Circular file dependencies involving ~&0."
                 preprocessing)))
   (file+lexemes
        (assoc-equal file
                     (string-plexeme-list-alist-fix preprocessed)))
   ((when file+lexemes)
    (retok (string-plexeme-list-alist-fix preprocessed)
           state))
   ((erp bytes state)
    (read-input-file-to-preproc path file state))
   (preprocessing (cons file (string-list-fix preprocessing)))
   ((erp rev-lexemes preprocessed state)
    (with-local-stobj
     ppstate
     (mv-let (erp lexemes ppstate preprocessed state)
             (b* ((ppstate (init-ppstate bytes (ienv->version ienv)
                                         ppstate)))
               (pproc-*-group-part path file preprocessed
                                   preprocessing nil ppstate state))
       (mv erp lexemes preprocessed state))))
   (lexemes (rev rev-lexemes))
   ((when (= (len preprocessed)
             *pproc-files-max*))
    (reterr (msg "Exceeded ~x0 file limit."
                 *pproc-files-max*)))
   (preprocessed (acons file lexemes preprocessed)))
  (retok preprocessed state)))

Function: pproc-*-group-part

(defun pproc-*-group-part
       (path file preprocessed
             preprocessing rev-lexemes ppstate state)
  (declare (xargs :stobjs (ppstate state)))
  (declare
       (xargs :guard (and (stringp path)
                          (stringp file)
                          (string-plexeme-list-alistp preprocessed)
                          (string-listp preprocessing)
                          (plexeme-listp rev-lexemes)
                          (ppstatep ppstate))))
  (declare (xargs :guard (<= (len preprocessed)
                             *pproc-files-max*)))
  (b* (((reterr) nil ppstate nil state)
       ((unless (mbt (<= (len preprocessed)
                         *pproc-files-max*)))
        (reterr :impossible))
       ((when (= (ppstate->size ppstate) 0))
        (retok (plexeme-list-fix rev-lexemes)
               ppstate
               (string-plexeme-list-alist-fix preprocessed)
               state))
       (psize (ppstate->size ppstate))
       (plen (len preprocessed))
       ((erp rev-lexemes ppstate preprocessed state)
        (pproc-group-part path file preprocessed preprocessing
                          rev-lexemes ppstate state))
       ((unless (mbt (<= (ppstate->size ppstate)
                         (1- psize))))
        (reterr :impossible))
       ((unless (mbt (>= (len preprocessed) plen)))
        (reterr :impossible)))
    (pproc-*-group-part path file preprocessed preprocessing
                        rev-lexemes ppstate state)))

Function: pproc-group-part

(defun pproc-group-part
       (path file preprocessed
             preprocessing rev-lexemes ppstate state)
 (declare (xargs :stobjs (ppstate state)))
 (declare
      (xargs :guard (and (stringp path)
                         (stringp file)
                         (string-plexeme-list-alistp preprocessed)
                         (string-listp preprocessing)
                         (plexeme-listp rev-lexemes)
                         (ppstatep ppstate))))
 (declare (xargs :guard (<= (len preprocessed)
                            *pproc-files-max*)))
 (let ((__function__ 'pproc-group-part))
   (declare (ignorable __function__))
   (b* (((reterr) nil ppstate nil state)
        ((unless (mbt (<= (len preprocessed)
                          *pproc-files-max*)))
         (reterr :impossible))
        ((erp nontokens-nonnewlines
              token/newline span ppstate)
         (pread-token/newline nil ppstate)))
     (cond ((not token/newline)
            (reterr-msg :where (position-to-msg (span->start span))
                        :expected "a token or newline"
                        :found token/newline))
           ((plexeme-case token/newline :newline)
            (retok (cons token/newline
                         (revappend nontokens-nonnewlines
                                    (plexeme-list-fix rev-lexemes)))
                   ppstate
                   (string-plexeme-list-alist-fix preprocessed)
                   state))
           ((plexeme-hashp token/newline)
            (pproc-directive path file preprocessed preprocessing
                             rev-lexemes ppstate state))
           (t (reterr (list :todo path file preprocessing)))))))

Function: pproc-directive

(defun pproc-directive
       (path file preprocessed
             preprocessing rev-lexemes ppstate state)
  (declare (xargs :stobjs (ppstate state)))
  (declare
       (xargs :guard (and (stringp path)
                          (stringp file)
                          (string-plexeme-list-alistp preprocessed)
                          (string-listp preprocessing)
                          (plexeme-listp rev-lexemes)
                          (ppstatep ppstate))))
  (declare (xargs :guard (<= (len preprocessed)
                             *pproc-files-max*)))
  (b* (((reterr) nil ppstate nil state)
       ((unless (mbt (<= (len preprocessed)
                         *pproc-files-max*)))
        (reterr :impossible))
       ((erp nontokens-nonnewlines
             token/newline span ppstate)
        (pread-token/newline nil ppstate)))
    (cond (t (reterr (list :todo path file preprocessing
                           rev-lexemes nontokens-nonnewlines
                           token/newline span))))))

Theorem: return-type-of-pproc-file.new-preprocessed

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

Theorem: return-type-of-pproc-*-group-part.new-rev-lexemes

(defthm return-type-of-pproc-*-group-part.new-rev-lexemes
  (b* (((mv acl2::?erp ?new-rev-lexemes ?new-ppstate
            ?new-preprocessed acl2::?state)
        (pproc-*-group-part path file preprocessed preprocessing
                            rev-lexemes ppstate state)))
    (plexeme-listp new-rev-lexemes))
  :rule-classes :rewrite)

Theorem: return-type-of-pproc-*-group-part.new-ppstate

(defthm return-type-of-pproc-*-group-part.new-ppstate
 (implies
      (ppstatep ppstate)
      (b* (((mv acl2::?erp ?new-rev-lexemes ?new-ppstate
                ?new-preprocessed acl2::?state)
            (pproc-*-group-part path file preprocessed preprocessing
                                rev-lexemes ppstate state)))
        (ppstatep new-ppstate)))
 :rule-classes :rewrite)

Theorem: return-type-of-pproc-*-group-part.new-preprocessed

(defthm return-type-of-pproc-*-group-part.new-preprocessed
  (b* (((mv acl2::?erp ?new-rev-lexemes ?new-ppstate
            ?new-preprocessed acl2::?state)
        (pproc-*-group-part path file preprocessed preprocessing
                            rev-lexemes ppstate state)))
    (string-plexeme-list-alistp new-preprocessed))
  :rule-classes :rewrite)

Theorem: return-type-of-pproc-group-part.new-rev-lexemes

(defthm return-type-of-pproc-group-part.new-rev-lexemes
  (b* (((mv acl2::?erp ?new-rev-lexemes ?new-ppstate
            ?new-preprocessed acl2::?state)
        (pproc-group-part path file preprocessed preprocessing
                          rev-lexemes ppstate state)))
    (plexeme-listp new-rev-lexemes))
  :rule-classes :rewrite)

Theorem: return-type-of-pproc-group-part.new-ppstate

(defthm return-type-of-pproc-group-part.new-ppstate
  (implies
       (ppstatep ppstate)
       (b* (((mv acl2::?erp ?new-rev-lexemes ?new-ppstate
                 ?new-preprocessed acl2::?state)
             (pproc-group-part path file preprocessed preprocessing
                               rev-lexemes ppstate state)))
         (ppstatep new-ppstate)))
  :rule-classes :rewrite)

Theorem: return-type-of-pproc-group-part.new-preprocessed

(defthm return-type-of-pproc-group-part.new-preprocessed
  (b* (((mv acl2::?erp ?new-rev-lexemes ?new-ppstate
            ?new-preprocessed acl2::?state)
        (pproc-group-part path file preprocessed preprocessing
                          rev-lexemes ppstate state)))
    (string-plexeme-list-alistp new-preprocessed))
  :rule-classes :rewrite)

Theorem: return-type-of-pproc-directive.new-rev-lexemes

(defthm return-type-of-pproc-directive.new-rev-lexemes
  (b* (((mv acl2::?erp ?new-rev-lexemes ?new-ppstate
            ?new-preprocessed acl2::?state)
        (pproc-directive path file preprocessed preprocessing
                         rev-lexemes ppstate state)))
    (plexeme-listp new-rev-lexemes))
  :rule-classes :rewrite)

Theorem: return-type-of-pproc-directive.new-ppstate

(defthm return-type-of-pproc-directive.new-ppstate
  (implies
       (ppstatep ppstate)
       (b* (((mv acl2::?erp ?new-rev-lexemes ?new-ppstate
                 ?new-preprocessed acl2::?state)
             (pproc-directive path file preprocessed preprocessing
                              rev-lexemes ppstate state)))
         (ppstatep new-ppstate)))
  :rule-classes :rewrite)

Theorem: return-type-of-pproc-directive.new-preprocessed

(defthm return-type-of-pproc-directive.new-preprocessed
  (b* (((mv acl2::?erp ?new-rev-lexemes ?new-ppstate
            ?new-preprocessed acl2::?state)
        (pproc-directive path file preprocessed preprocessing
                         rev-lexemes ppstate state)))
    (string-plexeme-list-alistp new-preprocessed))
  :rule-classes :rewrite)

Theorem: len-of-new-preprocessed-of-pproc-file-upper-bound

(defthm len-of-new-preprocessed-of-pproc-file-upper-bound
  (b* (((mv acl2::?erp
            ?new-preprocessed acl2::?state)
        (pproc-file path file
                    preprocessed preprocessing ienv state)))
    (<= (len new-preprocessed)
        *pproc-files-max*))
  :rule-classes :linear)

Theorem: len-of-new-preprocessed-of-pproc-*-group-part-upper-bound

(defthm len-of-new-preprocessed-of-pproc-*-group-part-upper-bound
  (b* (((mv acl2::?erp ?new-rev-lexemes ?new-ppstate
            ?new-preprocessed acl2::?state)
        (pproc-*-group-part path file preprocessed preprocessing
                            rev-lexemes ppstate state)))
    (<= (len new-preprocessed)
        *pproc-files-max*))
  :rule-classes :linear)

Theorem: len-of-new-preprocessed-of-pproc-group-part-upper-bound

(defthm len-of-new-preprocessed-of-pproc-group-part-upper-bound
  (b* (((mv acl2::?erp ?new-rev-lexemes ?new-ppstate
            ?new-preprocessed acl2::?state)
        (pproc-group-part path file preprocessed preprocessing
                          rev-lexemes ppstate state)))
    (<= (len new-preprocessed)
        *pproc-files-max*))
  :rule-classes :linear)

Theorem: len-of-new-preprocessed-of-pproc-directive-upper-bound

(defthm len-of-new-preprocessed-of-pproc-directive-upper-bound
  (b* (((mv acl2::?erp ?new-rev-lexemes ?new-ppstate
            ?new-preprocessed acl2::?state)
        (pproc-directive path file preprocessed preprocessing
                         rev-lexemes ppstate state)))
    (<= (len new-preprocessed)
        *pproc-files-max*))
  :rule-classes :linear)

Theorem: len-of-new-preprocessed-of-pproc-file-lower-bound

(defthm len-of-new-preprocessed-of-pproc-file-lower-bound
 (implies (string-plexeme-list-alistp preprocessed)
          (b* (((mv acl2::?erp
                    ?new-preprocessed acl2::?state)
                (pproc-file path file
                            preprocessed preprocessing ienv state)))
            (implies (not erp)
                     (>= (len new-preprocessed)
                         (len preprocessed)))))
 :rule-classes :linear)

Theorem: len-of-new-preprocessed-of-pproc-*-group-part-lower-bound

(defthm len-of-new-preprocessed-of-pproc-*-group-part-lower-bound
 (implies
      (string-plexeme-list-alistp preprocessed)
      (b* (((mv acl2::?erp ?new-rev-lexemes ?new-ppstate
                ?new-preprocessed acl2::?state)
            (pproc-*-group-part path file preprocessed preprocessing
                                rev-lexemes ppstate state)))
        (implies (not erp)
                 (>= (len new-preprocessed)
                     (len preprocessed)))))
 :rule-classes :linear)

Theorem: len-of-new-preprocessed-of-pproc-group-part-lower-bound

(defthm len-of-new-preprocessed-of-pproc-group-part-lower-bound
  (implies
       (string-plexeme-list-alistp preprocessed)
       (b* (((mv acl2::?erp ?new-rev-lexemes ?new-ppstate
                 ?new-preprocessed acl2::?state)
             (pproc-group-part path file preprocessed preprocessing
                               rev-lexemes ppstate state)))
         (implies (not erp)
                  (>= (len new-preprocessed)
                      (len preprocessed)))))
  :rule-classes :linear)

Theorem: len-of-new-preprocessed-of-pproc-directive-lower-bound

(defthm len-of-new-preprocessed-of-pproc-directive-lower-bound
  (implies
       (string-plexeme-list-alistp preprocessed)
       (b* (((mv acl2::?erp ?new-rev-lexemes ?new-ppstate
                 ?new-preprocessed acl2::?state)
             (pproc-directive path file preprocessed preprocessing
                              rev-lexemes ppstate state)))
         (implies (not erp)
                  (>= (len new-preprocessed)
                      (len preprocessed)))))
  :rule-classes :linear)

Theorem: ppstate->size-of-pproc-file-uncond

(defthm ppstate->size-of-pproc-file-uncond
  (b* nil t)
  :rule-classes nil)

Theorem: ppstate->size-of-pproc-*-group-part-uncond

(defthm ppstate->size-of-pproc-*-group-part-uncond
  (b* (((mv acl2::?erp ?new-rev-lexemes ?new-ppstate
            ?new-preprocessed acl2::?state)
        (pproc-*-group-part path file preprocessed preprocessing
                            rev-lexemes ppstate state)))
    (<= (ppstate->size new-ppstate)
        (ppstate->size ppstate)))
  :rule-classes :linear)

Theorem: ppstate->size-of-pproc-group-part-uncond

(defthm ppstate->size-of-pproc-group-part-uncond
  (b* (((mv acl2::?erp ?new-rev-lexemes ?new-ppstate
            ?new-preprocessed acl2::?state)
        (pproc-group-part path file preprocessed preprocessing
                          rev-lexemes ppstate state)))
    (<= (ppstate->size new-ppstate)
        (ppstate->size ppstate)))
  :rule-classes :linear)

Theorem: ppstate->size-of-pproc-directive-uncond

(defthm ppstate->size-of-pproc-directive-uncond
  (b* (((mv acl2::?erp ?new-rev-lexemes ?new-ppstate
            ?new-preprocessed acl2::?state)
        (pproc-directive path file preprocessed preprocessing
                         rev-lexemes ppstate state)))
    (<= (ppstate->size new-ppstate)
        (ppstate->size ppstate)))
  :rule-classes :linear)

Theorem: ppstate->size-of-pproc-file-cond

(defthm ppstate->size-of-pproc-file-cond
  (b* nil t)
  :rule-classes nil)

Theorem: ppstate->size-of-pproc-*-group-part-cond

(defthm ppstate->size-of-pproc-*-group-part-cond
  (b* nil t)
  :rule-classes nil)

Theorem: ppstate->size-of-pproc-group-part-cond

(defthm ppstate->size-of-pproc-group-part-cond
  (b* (((mv acl2::?erp ?new-rev-lexemes ?new-ppstate
            ?new-preprocessed acl2::?state)
        (pproc-group-part path file preprocessed preprocessing
                          rev-lexemes ppstate state)))
    (implies (not erp)
             (<= (ppstate->size new-ppstate)
                 (1- (ppstate->size ppstate)))))
  :rule-classes :linear)

Theorem: ppstate->size-of-pproc-directive-cond

(defthm ppstate->size-of-pproc-directive-cond
  (b* (((mv acl2::?erp ?new-rev-lexemes ?new-ppstate
            ?new-preprocessed acl2::?state)
        (pproc-directive path file preprocessed preprocessing
                         rev-lexemes ppstate state)))
    (implies (not erp)
             (<= (ppstate->size new-ppstate)
                 (1- (ppstate->size ppstate)))))
  :rule-classes :linear)

Subtopics

Pproc-file: Preprocess a file.
Pproc-group-part: Preprocess a group part.
Pproc-*-group-part: Preprocess zero or more group parts.
Pproc-directive: Preprocess a directive.