		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 nontoknls toknl span ppstate)
        (pread-token/newline nil ppstate)))
    (cond ((not toknl)
           (reterr-msg :where (position-to-msg (span->start span))
                       :expected "a token or new line"
                       :found (plexeme-to-msg toknl)))
          ((or (plexeme-case toknl :newline)
               (plexeme-case toknl :line-comment))
           (retok (cons toknl
                        (revappend nontoknls
                                   (plexeme-list-fix rev-lexemes)))
                  ppstate
                  (string-plexeme-list-alist-fix preprocessed)
                  state))
          ((plexeme-hashp toknl)
           (pproc-directive path file preprocessed preprocessing
                            rev-lexemes ppstate state))
          (t (b* ((ppstate (punread-token ppstate)))
               (pproc-text-line nontoknls
                                path file preprocessed preprocessing
                                rev-lexemes ppstate state)))))))

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*)))
 (let ((__function__ 'pproc-directive))
  (declare (ignorable __function__))
  (b* (((reterr) nil ppstate nil state)
       ((unless (mbt (<= (len preprocessed)
                         *pproc-files-max*)))
        (reterr :impossible))
       ((erp & toknl span ppstate)
        (pread-token/newline nil ppstate)))
   (cond
    ((not toknl)
     (reterr-msg :where (position-to-msg (span->start span))
                 :expected "a token or new line"
                 :found (plexeme-to-msg toknl)))
    ((or (plexeme-case toknl :newline)
         (plexeme-case toknl :line-comment))
     (b*
      ((newline
        (if (plexeme-case toknl :newline)
            toknl
          (plexeme-newline (plexeme-line-comment->newline toknl)))))
      (retok (cons newline (plexeme-list-fix rev-lexemes))
             ppstate
             (string-plexeme-list-alist-fix preprocessed)
             state)))
    ((plexeme-case toknl :ident)
     (b* ((dirname (ident->unwrap (plexeme-ident->ident toknl))))
      (cond
       ((equal dirname "if") (reterr :todo))
       ((equal dirname "ifdef") (reterr :todo))
       ((equal dirname "ifndef")
        (reterr :todo))
       ((equal dirname "include")
        (pproc-include-directive
             path file preprocessed preprocessing
             rev-lexemes ppstate state))
       ((equal dirname "define")
        (reterr :todo))
       ((equal dirname "undef") (reterr :todo))
       ((equal dirname "line") (reterr :todo))
       ((equal dirname "error") (reterr :todo))
       ((equal dirname "pragma")
        (reterr :todo))
       (t
        (reterr-msg
         :where (span->start span)
         :expected
         "a directive name among ~
                                   'if', ~
                                   'ifdef', ~
                                   'ifndef', ~
                                   'include', ~
                                   'define', ~
                                   'undef', ~
                                   'line', ~
                                   'error', and ~
                                   'pragma'"
         :found (plexeme-to-msg toknl))))))
    (t
     (reterr-msg
      :where (span->start span)
      :expected
      "a directive name among ~
                               'if', ~
                               'ifdef', ~
                               'ifndef', ~
                               'include', ~
                               'define', ~
                               'undef', ~
                               'line', ~
                               'error', and ~
                               'pragma'"
      :found (plexeme-to-msg toknl)))))))

Function: pproc-include-directive

(defun pproc-include-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 (ignore path file preprocessing rev-lexemes))
 (declare (xargs :guard (<= (len preprocessed)
                            *pproc-files-max*)))
 (let ((__function__ 'pproc-include-directive))
  (declare (ignorable __function__))
  (b* (((reterr) nil ppstate nil state)
       ((unless (mbt (<= (len preprocessed)
                         *pproc-files-max*)))
        (reterr :impossible))
       ((erp & toknl span ppstate)
        (pread-token/newline t ppstate)))
   (cond
     ((not toknl)
      (reterr-msg :where (position-to-msg (span->start span))
                  :expected "a token"
                  :found (plexeme-to-msg toknl)))
     ((or (plexeme-case toknl :newline)
          (plexeme-case toknl :line-comment))
      (reterr-msg :where (position-to-msg (span->start span))
                  :expected "a token"
                  :found (plexeme-to-msg toknl)))
     ((plexeme-case toknl :header)
      (reterr :todo))
     (t (reterr (msg "Non-direct #include not yet supported.")))))))

Function: pproc-text-line

(defun pproc-text-line
       (nontoknls path file preprocessed
                  preprocessing rev-lexemes ppstate state)
  (declare (xargs :stobjs (ppstate state)))
  (declare
       (xargs :guard (and (plexeme-listp nontoknls)
                          (stringp path)
                          (stringp file)
                          (string-plexeme-list-alistp preprocessed)
                          (string-listp preprocessing)
                          (plexeme-listp rev-lexemes)
                          (ppstatep ppstate))))
  (declare (ignore nontoknls))
  (declare (xargs :guard (<= (len preprocessed)
                             *pproc-files-max*)))
  (b* (((reterr) nil ppstate nil state)
       ((unless (mbt (<= (len preprocessed)
                         *pproc-files-max*)))
        (reterr :impossible)))
    (reterr (list :todo
                  path file preprocessing rev-lexemes))))

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: return-type-of-pproc-include-directive.new-rev-lexemes

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

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

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

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

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

Theorem: return-type-of-pproc-text-line.new-rev-lexemes

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

Theorem: return-type-of-pproc-text-line.new-ppstate

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

Theorem: return-type-of-pproc-text-line.new-preprocessed

(defthm return-type-of-pproc-text-line.new-preprocessed
  (b* (((mv acl2::?erp ?new-rev-lexemes ?new-ppstate
            ?new-preprocessed acl2::?state)
        (pproc-text-line nontoknls
                         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-include-directive-upper-bound

(defthm
     len-of-new-preprocessed-of-pproc-include-directive-upper-bound
 (b* (((mv acl2::?erp ?new-rev-lexemes ?new-ppstate
           ?new-preprocessed acl2::?state)
       (pproc-include-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-text-line-upper-bound

(defthm len-of-new-preprocessed-of-pproc-text-line-upper-bound
  (b* (((mv acl2::?erp ?new-rev-lexemes ?new-ppstate
            ?new-preprocessed acl2::?state)
        (pproc-text-line nontoknls
                         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: len-of-new-preprocessed-of-pproc-include-directive-lower-bound

(defthm
     len-of-new-preprocessed-of-pproc-include-directive-lower-bound
 (implies
   (string-plexeme-list-alistp preprocessed)
   (b*
     (((mv acl2::?erp ?new-rev-lexemes ?new-ppstate
           ?new-preprocessed acl2::?state)
       (pproc-include-directive 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-text-line-lower-bound

(defthm len-of-new-preprocessed-of-pproc-text-line-lower-bound
  (implies
       (string-plexeme-list-alistp preprocessed)
       (b* (((mv acl2::?erp ?new-rev-lexemes ?new-ppstate
                 ?new-preprocessed acl2::?state)
             (pproc-text-line nontoknls
                              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-include-directive-uncond

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

Theorem: ppstate->size-of-pproc-text-line-uncond

(defthm ppstate->size-of-pproc-text-line-uncond
  (b* (((mv acl2::?erp ?new-rev-lexemes ?new-ppstate
            ?new-preprocessed acl2::?state)
        (pproc-text-line nontoknls
                         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)

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

(defthm ppstate->size-of-pproc-include-directive-cond
 (b* (((mv acl2::?erp ?new-rev-lexemes ?new-ppstate
           ?new-preprocessed acl2::?state)
       (pproc-include-directive 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-text-line-cond

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

Subtopics

Pproc-directive: Preprocess a directive.
Pproc-group-part: Preprocess a group part.
Pproc-file: Preprocess a file.
Pproc-include-directive: Preprocess a #include directive.
Pproc-text-line: Preprocess a (non-empty) text line.
Pproc-*-group-part: Preprocess zero or more group parts.