		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-states

Ppstate

Fixtype of preprocessor states.

This is similar to parstate, but for the preprocessor.

Our preprocessing functions take and return preprocessor states.

The preprocessor state is a stobj, which we turn into a fixtype by adding a fixer along with readers and writers that fix their inputs and unconditionally return typed outputs. The use of a stobj is an optimization for speed: conceptually, the preprocessor state could be defined as a fty::defprod.

Most of the components of the preprocessor state are analogous to the ones of the parser state: see the documentation of parstate first. The only difference in those components is that the processor state contains (preprocessing) lexemes instead of tokens, because our preprocessor preserves comments and white space.

The preprocessor state includes an additional component (not found in the parser state), namely a macro table that consists of all the macros in scope.

Definitions and Theorems

Definition: raw-ppstate->bytes-p

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-ppstate->position-p

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-ppstate->chars-p

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-ppstate->chars-read-p

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-ppstate->chars-unread-p

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-ppstate->lexemes-p

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-ppstate->lexemes-read-p

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-ppstate->lexemes-unread-p

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-ppstate->version-p

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-ppstate->size-p

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-ppstate->macros-p

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: ppstatep

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: create-ppstate

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-ppstate->bytes

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-update-ppstate->bytes

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-ppstate->position

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-update-ppstate->position

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-ppstate->chars-length

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-update-ppstate->chars-length

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-ppstate->char

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-update-ppstate->char

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-ppstate->chars-read

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-update-ppstate->chars-read

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-ppstate->chars-unread

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-update-ppstate->chars-unread

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-ppstate->lexemes-length

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-update-ppstate->lexemes-length

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-ppstate->lexeme

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-update-ppstate->lexeme

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-ppstate->lexemes-read

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-update-ppstate->lexemes-read

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-ppstate->lexemes-unread

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-update-ppstate->lexemes-unread

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-ppstate->version

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-update-ppstate->version

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-ppstate->size

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-update-ppstate->size

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-ppstate->macros

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Definition: raw-update-ppstate->macros

(defstobj ppstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially (1 . 0))
  (chars :type (array (satisfies char+position-p) (1))
         :initially (0 1 . 0)
         :resizable t)
  (chars-read :type (integer 0 *)
              :initially 0)
  (chars-unread :type (integer 0 *)
                :initially 0)
  (lexemes :type (array (satisfies plexeme+span-p) (1))
           :initially ((lexeme :ident (:irrelevant))
                       (span (1 . 0) 1 . 0))
           :resizable t)
  (lexemes-read :type (integer 0 *)
                :initially 0)
  (lexemes-unread :type (integer 0 *)
                  :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  (macros :type (satisfies macro-tablep)
          :initially ((alist)))
  :renaming
  ((bytesp raw-ppstate->bytes-p)
   (positionp raw-ppstate->position-p)
   (charsp raw-ppstate->chars-p)
   (chars-readp raw-ppstate->chars-read-p)
   (chars-unreadp raw-ppstate->chars-unread-p)
   (lexemesp raw-ppstate->lexemes-p)
   (lexemes-readp raw-ppstate->lexemes-read-p)
   (lexemes-unreadp raw-ppstate->lexemes-unread-p)
   (versionp raw-ppstate->version-p)
   (sizep raw-ppstate->size-p)
   (macrosp raw-ppstate->macros-p)
   (bytes raw-ppstate->bytes)
   (position raw-ppstate->position)
   (chars-length raw-ppstate->chars-length)
   (charsi raw-ppstate->char)
   (chars-read raw-ppstate->chars-read)
   (chars-unread raw-ppstate->chars-unread)
   (lexemes-length raw-ppstate->lexemes-length)
   (lexemesi raw-ppstate->lexeme)
   (lexemes-read raw-ppstate->lexemes-read)
   (lexemes-unread raw-ppstate->lexemes-unread)
   (version raw-ppstate->version)
   (size raw-ppstate->size)
   (macros raw-ppstate->macros)
   (update-bytes raw-update-ppstate->bytes)
   (update-position raw-update-ppstate->position)
   (resize-chars raw-update-ppstate->chars-length)
   (update-charsi raw-update-ppstate->char)
   (update-chars-read raw-update-ppstate->chars-read)
   (update-chars-unread raw-update-ppstate->chars-unread)
   (resize-lexemes raw-update-ppstate->lexemes-length)
   (update-lexemesi raw-update-ppstate->lexeme)
   (update-lexemes-read raw-update-ppstate->lexemes-read)
   (update-lexemes-unread raw-update-ppstate->lexemes-unread)
   (update-version raw-update-ppstate->version)
   (update-size raw-update-ppstate->size)
   (update-macros raw-update-ppstate->macros)))

Function: ppstate-fix

(defun ppstate-fix (ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (ppstatep ppstate)
           ppstate
         (non-exec (create-ppstate)))
       :exec ppstate))

Theorem: ppstatep-of-ppstate-fix

(defthm ppstatep-of-ppstate-fix
  (b* ((ppstate (ppstate-fix ppstate)))
    (ppstatep ppstate))
  :rule-classes :rewrite)

Theorem: ppstate-fix-when-ppstatep

(defthm ppstate-fix-when-ppstatep
  (implies (ppstatep ppstate)
           (equal (ppstate-fix ppstate) ppstate)))

Function: ppstate-equiv

(defun ppstate-equiv (acl2::x acl2::y)
  (declare (xargs :non-executable t))
  (prog2$ (acl2::throw-nonexec-error 'ppstate-equiv
                                     (list acl2::x acl2::y))
          (equal (ppstate-fix acl2::x)
                 (ppstate-fix acl2::y))))

Theorem: ppstate-equiv-is-an-equivalence

(defthm ppstate-equiv-is-an-equivalence
  (and (booleanp (ppstate-equiv x y))
       (ppstate-equiv x x)
       (implies (ppstate-equiv x y)
                (ppstate-equiv y x))
       (implies (and (ppstate-equiv x y)
                     (ppstate-equiv y z))
                (ppstate-equiv x z)))
  :rule-classes (:equivalence))

Theorem: ppstate-equiv-implies-equal-ppstate-fix-1

(defthm ppstate-equiv-implies-equal-ppstate-fix-1
  (implies (ppstate-equiv acl2::x x-equiv)
           (equal (ppstate-fix acl2::x)
                  (ppstate-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: ppstate-fix-under-ppstate-equiv

(defthm ppstate-fix-under-ppstate-equiv
  (ppstate-equiv (ppstate-fix acl2::x)
                 acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: raw-ppstate->chars-p-becomes-char+position-listp

(defthm raw-ppstate->chars-p-becomes-char+position-listp
  (equal (raw-ppstate->chars-p x)
         (char+position-listp x)))

Theorem: raw-ppstate->lexemes-p-becomes-plexeme+span-listp

(defthm raw-ppstate->lexemes-p-becomes-plexeme+span-listp
  (equal (raw-ppstate->lexemes-p x)
         (plexeme+span-listp x)))

Function: ppstate->bytes

(defun ppstate->bytes (ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (ppstatep ppstate)
           (raw-ppstate->bytes ppstate)
         nil)
       :exec (raw-ppstate->bytes ppstate)))

Theorem: byte-listp-of-ppstate->bytes

(defthm byte-listp-of-ppstate->bytes
  (b* ((bytes (ppstate->bytes ppstate)))
    (byte-listp bytes))
  :rule-classes :rewrite)

Theorem: true-listp-of-ppstate->bytes

(defthm true-listp-of-ppstate->bytes
  (b* ((bytes (ppstate->bytes ppstate)))
    (true-listp bytes))
  :rule-classes :type-prescription)

Theorem: ppstate->bytes-of-ppstate-fix-ppstate

(defthm ppstate->bytes-of-ppstate-fix-ppstate
  (equal (ppstate->bytes (ppstate-fix ppstate))
         (ppstate->bytes ppstate)))

Theorem: ppstate->bytes-ppstate-equiv-congruence-on-ppstate

(defthm ppstate->bytes-ppstate-equiv-congruence-on-ppstate
  (implies (ppstate-equiv ppstate ppstate-equiv)
           (equal (ppstate->bytes ppstate)
                  (ppstate->bytes ppstate-equiv)))
  :rule-classes :congruence)

Function: ppstate->position

(defun ppstate->position (ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (ppstatep ppstate)
           (raw-ppstate->position ppstate)
         (irr-position))
       :exec (raw-ppstate->position ppstate)))

Theorem: positionp-of-ppstate->position

(defthm positionp-of-ppstate->position
  (b* ((position (ppstate->position ppstate)))
    (positionp position))
  :rule-classes :rewrite)

Function: ppstate->chars-length

(defun ppstate->chars-length (ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (ppstatep ppstate)
           (raw-ppstate->chars-length ppstate)
         1)
       :exec (raw-ppstate->chars-length ppstate)))

Theorem: natp-of-ppstate->chars-length

(defthm natp-of-ppstate->chars-length
  (b* ((length (ppstate->chars-length ppstate)))
    (natp length))
  :rule-classes :rewrite)

Theorem: ppstate->chars-length-of-ppstate-fix-ppstate

(defthm ppstate->chars-length-of-ppstate-fix-ppstate
  (equal (ppstate->chars-length (ppstate-fix ppstate))
         (ppstate->chars-length ppstate)))

Theorem: ppstate->chars-length-ppstate-equiv-congruence-on-ppstate

(defthm ppstate->chars-length-ppstate-equiv-congruence-on-ppstate
  (implies (ppstate-equiv ppstate ppstate-equiv)
           (equal (ppstate->chars-length ppstate)
                  (ppstate->chars-length ppstate-equiv)))
  :rule-classes :congruence)

Function: ppstate->char

(defun ppstate->char (i ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (natp i)))
  (declare (xargs :guard (< i (ppstate->chars-length ppstate))))
  (mbe :logic
       (if (and (ppstatep ppstate)
                (< (nfix i)
                   (ppstate->chars-length ppstate)))
           (raw-ppstate->char (nfix i) ppstate)
         (make-char+position :char 0
                             :position (irr-position)))
       :exec (raw-ppstate->char i ppstate)))

Theorem: char+position-p-of-ppstate->char

(defthm char+position-p-of-ppstate->char
  (b* ((char+pos (ppstate->char i ppstate)))
    (char+position-p char+pos))
  :rule-classes :rewrite)

Function: ppstate->chars-read

(defun ppstate->chars-read (ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (ppstatep ppstate)
           (raw-ppstate->chars-read ppstate)
         0)
       :exec (raw-ppstate->chars-read ppstate)))

Theorem: natp-of-ppstate->chars-read

(defthm natp-of-ppstate->chars-read
  (b* ((chars-read (ppstate->chars-read ppstate)))
    (natp chars-read))
  :rule-classes (:rewrite :type-prescription))

Theorem: ppstate->chars-read-of-ppstate-fix-ppstate

(defthm ppstate->chars-read-of-ppstate-fix-ppstate
  (equal (ppstate->chars-read (ppstate-fix ppstate))
         (ppstate->chars-read ppstate)))

Theorem: ppstate->chars-read-ppstate-equiv-congruence-on-ppstate

(defthm ppstate->chars-read-ppstate-equiv-congruence-on-ppstate
  (implies (ppstate-equiv ppstate ppstate-equiv)
           (equal (ppstate->chars-read ppstate)
                  (ppstate->chars-read ppstate-equiv)))
  :rule-classes :congruence)

Function: ppstate->chars-unread

(defun ppstate->chars-unread (ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (ppstatep ppstate)
           (raw-ppstate->chars-unread ppstate)
         0)
       :exec (raw-ppstate->chars-unread ppstate)))

Theorem: natp-of-ppstate->chars-unread

(defthm natp-of-ppstate->chars-unread
  (b* ((chars-unread (ppstate->chars-unread ppstate)))
    (natp chars-unread))
  :rule-classes (:rewrite :type-prescription))

Theorem: ppstate->chars-unread-of-ppstate-fix-ppstate

(defthm ppstate->chars-unread-of-ppstate-fix-ppstate
  (equal (ppstate->chars-unread (ppstate-fix ppstate))
         (ppstate->chars-unread ppstate)))

Theorem: ppstate->chars-unread-ppstate-equiv-congruence-on-ppstate

(defthm ppstate->chars-unread-ppstate-equiv-congruence-on-ppstate
  (implies (ppstate-equiv ppstate ppstate-equiv)
           (equal (ppstate->chars-unread ppstate)
                  (ppstate->chars-unread ppstate-equiv)))
  :rule-classes :congruence)

Function: ppstate->lexemes-length

(defun ppstate->lexemes-length (ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (ppstatep ppstate)
           (raw-ppstate->lexemes-length ppstate)
         1)
       :exec (raw-ppstate->lexemes-length ppstate)))

Theorem: natp-of-ppstate->lexemes-length

(defthm natp-of-ppstate->lexemes-length
  (b* ((length (ppstate->lexemes-length ppstate)))
    (natp length))
  :rule-classes :rewrite)

Theorem: ppstate->lexemes-length-of-ppstate-fix-ppstate

(defthm ppstate->lexemes-length-of-ppstate-fix-ppstate
  (equal (ppstate->lexemes-length (ppstate-fix ppstate))
         (ppstate->lexemes-length ppstate)))

Theorem: ppstate->lexemes-length-ppstate-equiv-congruence-on-ppstate

(defthm ppstate->lexemes-length-ppstate-equiv-congruence-on-ppstate
  (implies (ppstate-equiv ppstate ppstate-equiv)
           (equal (ppstate->lexemes-length ppstate)
                  (ppstate->lexemes-length ppstate-equiv)))
  :rule-classes :congruence)

Function: ppstate->lexeme

(defun ppstate->lexeme (i ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (natp i)))
  (declare (xargs :guard (< i (ppstate->lexemes-length ppstate))))
  (mbe :logic
       (if (and (ppstatep ppstate)
                (< (nfix i)
                   (ppstate->lexemes-length ppstate)))
           (raw-ppstate->lexeme (nfix i) ppstate)
         (make-plexeme+span :lexeme (irr-plexeme)
                            :span (irr-position)))
       :exec (raw-ppstate->lexeme i ppstate)))

Theorem: plexeme+span-p-of-ppstate->lexeme

(defthm plexeme+span-p-of-ppstate->lexeme
  (b* ((lexeme+span (ppstate->lexeme i ppstate)))
    (plexeme+span-p lexeme+span))
  :rule-classes :rewrite)

Function: ppstate->lexemes-read

(defun ppstate->lexemes-read (ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (ppstatep ppstate)
           (raw-ppstate->lexemes-read ppstate)
         0)
       :exec (raw-ppstate->lexemes-read ppstate)))

Theorem: natp-of-ppstate->lexemes-read

(defthm natp-of-ppstate->lexemes-read
  (b* ((lexemes-read (ppstate->lexemes-read ppstate)))
    (natp lexemes-read))
  :rule-classes (:rewrite :type-prescription))

Theorem: ppstate->lexemes-read-of-ppstate-fix-ppstate

(defthm ppstate->lexemes-read-of-ppstate-fix-ppstate
  (equal (ppstate->lexemes-read (ppstate-fix ppstate))
         (ppstate->lexemes-read ppstate)))

Theorem: ppstate->lexemes-read-ppstate-equiv-congruence-on-ppstate

(defthm ppstate->lexemes-read-ppstate-equiv-congruence-on-ppstate
  (implies (ppstate-equiv ppstate ppstate-equiv)
           (equal (ppstate->lexemes-read ppstate)
                  (ppstate->lexemes-read ppstate-equiv)))
  :rule-classes :congruence)

Function: ppstate->lexemes-unread

(defun ppstate->lexemes-unread (ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (ppstatep ppstate)
           (raw-ppstate->lexemes-unread ppstate)
         0)
       :exec (raw-ppstate->lexemes-unread ppstate)))

Theorem: natp-of-ppstate->lexemes-unread

(defthm natp-of-ppstate->lexemes-unread
  (b* ((lexemes-unread (ppstate->lexemes-unread ppstate)))
    (natp lexemes-unread))
  :rule-classes (:rewrite :type-prescription))

Theorem: ppstate->lexemes-unread-of-ppstate-fix-ppstate

(defthm ppstate->lexemes-unread-of-ppstate-fix-ppstate
  (equal (ppstate->lexemes-unread (ppstate-fix ppstate))
         (ppstate->lexemes-unread ppstate)))

Theorem: ppstate->lexemes-unread-ppstate-equiv-congruence-on-ppstate

(defthm ppstate->lexemes-unread-ppstate-equiv-congruence-on-ppstate
  (implies (ppstate-equiv ppstate ppstate-equiv)
           (equal (ppstate->lexemes-unread ppstate)
                  (ppstate->lexemes-unread ppstate-equiv)))
  :rule-classes :congruence)

Function: ppstate->version

(defun ppstate->version (ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (ppstatep ppstate)
           (raw-ppstate->version ppstate)
         (c::version-c23))
       :exec (raw-ppstate->version ppstate)))

Theorem: versionp-of-ppstate->version

(defthm versionp-of-ppstate->version
  (b* ((version (ppstate->version ppstate)))
    (c::versionp version))
  :rule-classes :rewrite)

Theorem: ppstate->version-of-ppstate-fix-ppstate

(defthm ppstate->version-of-ppstate-fix-ppstate
  (equal (ppstate->version (ppstate-fix ppstate))
         (ppstate->version ppstate)))

Theorem: ppstate->version-ppstate-equiv-congruence-on-ppstate

(defthm ppstate->version-ppstate-equiv-congruence-on-ppstate
  (implies (ppstate-equiv ppstate ppstate-equiv)
           (equal (ppstate->version ppstate)
                  (ppstate->version ppstate-equiv)))
  :rule-classes :congruence)

Function: ppstate->size

(defun ppstate->size (ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (ppstatep ppstate)
           (raw-ppstate->size ppstate)
         0)
       :exec (raw-ppstate->size ppstate)))

Theorem: natp-of-ppstate->size

(defthm natp-of-ppstate->size
  (b* ((size (ppstate->size ppstate)))
    (natp size))
  :rule-classes (:rewrite :type-prescription))

Theorem: ppstate->size-of-ppstate-fix-ppstate

(defthm ppstate->size-of-ppstate-fix-ppstate
  (equal (ppstate->size (ppstate-fix ppstate))
         (ppstate->size ppstate)))

Theorem: ppstate->size-ppstate-equiv-congruence-on-ppstate

(defthm ppstate->size-ppstate-equiv-congruence-on-ppstate
  (implies (ppstate-equiv ppstate ppstate-equiv)
           (equal (ppstate->size ppstate)
                  (ppstate->size ppstate-equiv)))
  :rule-classes :congruence)

Function: ppstate->macros

(defun ppstate->macros (ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (ppstatep ppstate)
           (raw-ppstate->macros ppstate)
         (macro-table-init))
       :exec (raw-ppstate->macros ppstate)))

Theorem: macro-tablep-of-ppstate->macros

(defthm macro-tablep-of-ppstate->macros
  (b* ((macros (ppstate->macros ppstate)))
    (macro-tablep macros))
  :rule-classes :rewrite)

Theorem: ppstate->macros-of-ppstate-fix-ppstate

(defthm ppstate->macros-of-ppstate-fix-ppstate
  (equal (ppstate->macros (ppstate-fix ppstate))
         (ppstate->macros ppstate)))

Theorem: ppstate->macros-ppstate-equiv-congruence-on-ppstate

(defthm ppstate->macros-ppstate-equiv-congruence-on-ppstate
  (implies (ppstate-equiv ppstate ppstate-equiv)
           (equal (ppstate->macros ppstate)
                  (ppstate->macros ppstate-equiv)))
  :rule-classes :congruence)

Function: update-ppstate->bytes

(defun update-ppstate->bytes (bytes ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (byte-listp bytes)))
  (b* ((ppstate (ppstate-fix ppstate)))
    (raw-update-ppstate->bytes (byte-list-fix bytes)
                               ppstate)))

Theorem: ppstatep-of-update-ppstate->bytes

(defthm ppstatep-of-update-ppstate->bytes
  (b* ((ppstate (update-ppstate->bytes bytes ppstate)))
    (ppstatep ppstate))
  :rule-classes :rewrite)

Theorem: update-ppstate->bytes-of-byte-list-fix-bytes

(defthm update-ppstate->bytes-of-byte-list-fix-bytes
  (equal (update-ppstate->bytes (byte-list-fix bytes)
                                ppstate)
         (update-ppstate->bytes bytes ppstate)))

Theorem: update-ppstate->bytes-byte-list-equiv-congruence-on-bytes

(defthm update-ppstate->bytes-byte-list-equiv-congruence-on-bytes
  (implies (acl2::byte-list-equiv bytes bytes-equiv)
           (equal (update-ppstate->bytes bytes ppstate)
                  (update-ppstate->bytes bytes-equiv ppstate)))
  :rule-classes :congruence)

Theorem: update-ppstate->bytes-of-ppstate-fix-ppstate

(defthm update-ppstate->bytes-of-ppstate-fix-ppstate
  (equal (update-ppstate->bytes bytes (ppstate-fix ppstate))
         (update-ppstate->bytes bytes ppstate)))

Theorem: update-ppstate->bytes-ppstate-equiv-congruence-on-ppstate

(defthm update-ppstate->bytes-ppstate-equiv-congruence-on-ppstate
  (implies (ppstate-equiv ppstate ppstate-equiv)
           (equal (update-ppstate->bytes bytes ppstate)
                  (update-ppstate->bytes bytes ppstate-equiv)))
  :rule-classes :congruence)

Function: update-ppstate->position

(defun update-ppstate->position (position ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (positionp position)))
  (b* ((ppstate (ppstate-fix ppstate)))
    (raw-update-ppstate->position (position-fix position)
                                  ppstate)))

Theorem: ppstatep-of-update-ppstate->position

(defthm ppstatep-of-update-ppstate->position
  (b* ((ppstate (update-ppstate->position position ppstate)))
    (ppstatep ppstate))
  :rule-classes :rewrite)

Theorem: update-ppstate->position-of-position-fix-position

(defthm update-ppstate->position-of-position-fix-position
  (equal (update-ppstate->position (position-fix position)
                                   ppstate)
         (update-ppstate->position position ppstate)))

Theorem: update-ppstate->position-position-equiv-congruence-on-position

(defthm
     update-ppstate->position-position-equiv-congruence-on-position
 (implies (position-equiv position position-equiv)
          (equal (update-ppstate->position position ppstate)
                 (update-ppstate->position position-equiv ppstate)))
 :rule-classes :congruence)

Theorem: update-ppstate->position-of-ppstate-fix-ppstate

(defthm update-ppstate->position-of-ppstate-fix-ppstate
  (equal (update-ppstate->position position (ppstate-fix ppstate))
         (update-ppstate->position position ppstate)))

Theorem: update-ppstate->position-ppstate-equiv-congruence-on-ppstate

(defthm update-ppstate->position-ppstate-equiv-congruence-on-ppstate
 (implies (ppstate-equiv ppstate ppstate-equiv)
          (equal (update-ppstate->position position ppstate)
                 (update-ppstate->position position ppstate-equiv)))
 :rule-classes :congruence)

Function: update-ppstate->chars-length

(defun update-ppstate->chars-length (length ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (natp length)))
  (b* ((ppstate (ppstate-fix ppstate)))
    (raw-update-ppstate->chars-length (nfix length)
                                      ppstate)))

Theorem: ppstatep-of-update-ppstate->chars-length

(defthm ppstatep-of-update-ppstate->chars-length
  (b* ((ppstate (update-ppstate->chars-length length ppstate)))
    (ppstatep ppstate))
  :rule-classes :rewrite)

Theorem: update-ppstate->chars-length-of-nfix-length

(defthm update-ppstate->chars-length-of-nfix-length
  (equal (update-ppstate->chars-length (nfix length)
                                       ppstate)
         (update-ppstate->chars-length length ppstate)))

Theorem: update-ppstate->chars-length-nat-equiv-congruence-on-length

(defthm update-ppstate->chars-length-nat-equiv-congruence-on-length
  (implies
       (acl2::nat-equiv length length-equiv)
       (equal (update-ppstate->chars-length length ppstate)
              (update-ppstate->chars-length length-equiv ppstate)))
  :rule-classes :congruence)

Theorem: update-ppstate->chars-length-of-ppstate-fix-ppstate

(defthm update-ppstate->chars-length-of-ppstate-fix-ppstate
  (equal (update-ppstate->chars-length length (ppstate-fix ppstate))
         (update-ppstate->chars-length length ppstate)))

Theorem: update-ppstate->chars-length-ppstate-equiv-congruence-on-ppstate

(defthm
   update-ppstate->chars-length-ppstate-equiv-congruence-on-ppstate
  (implies
       (ppstate-equiv ppstate ppstate-equiv)
       (equal (update-ppstate->chars-length length ppstate)
              (update-ppstate->chars-length length ppstate-equiv)))
  :rule-classes :congruence)

Function: update-ppstate->char

(defun update-ppstate->char (i char+pos ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (and (natp i)
                              (char+position-p char+pos))))
  (declare (xargs :guard (< i (ppstate->chars-length ppstate))))
  (b* ((ppstate (ppstate-fix ppstate)))
    (mbe :logic
         (if (< (nfix i)
                (ppstate->chars-length ppstate))
             (raw-update-ppstate->char (nfix i)
                                       (char+position-fix char+pos)
                                       ppstate)
           ppstate)
         :exec (raw-update-ppstate->char i char+pos ppstate))))

Theorem: ppstatep-of-update-ppstate->char

(defthm ppstatep-of-update-ppstate->char
  (b* ((ppstate (update-ppstate->char i char+pos ppstate)))
    (ppstatep ppstate))
  :rule-classes :rewrite)

Function: update-ppstate->chars-read

(defun update-ppstate->chars-read (chars-read ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (natp chars-read)))
  (b* ((ppstate (ppstate-fix ppstate)))
    (raw-update-ppstate->chars-read (nfix chars-read)
                                    ppstate)))

Theorem: ppstatep-of-update-ppstate->chars-read

(defthm ppstatep-of-update-ppstate->chars-read
  (b* ((ppstate (update-ppstate->chars-read chars-read ppstate)))
    (ppstatep ppstate))
  :rule-classes :rewrite)

Theorem: update-ppstate->chars-read-of-nfix-chars-read

(defthm update-ppstate->chars-read-of-nfix-chars-read
  (equal (update-ppstate->chars-read (nfix chars-read)
                                     ppstate)
         (update-ppstate->chars-read chars-read ppstate)))

Theorem: update-ppstate->chars-read-nat-equiv-congruence-on-chars-read

(defthm
      update-ppstate->chars-read-nat-equiv-congruence-on-chars-read
 (implies
      (acl2::nat-equiv chars-read chars-read-equiv)
      (equal (update-ppstate->chars-read chars-read ppstate)
             (update-ppstate->chars-read chars-read-equiv ppstate)))
 :rule-classes :congruence)

Theorem: update-ppstate->chars-read-of-ppstate-fix-ppstate

(defthm update-ppstate->chars-read-of-ppstate-fix-ppstate
  (equal
       (update-ppstate->chars-read chars-read (ppstate-fix ppstate))
       (update-ppstate->chars-read chars-read ppstate)))

Theorem: update-ppstate->chars-read-ppstate-equiv-congruence-on-ppstate

(defthm
     update-ppstate->chars-read-ppstate-equiv-congruence-on-ppstate
 (implies
      (ppstate-equiv ppstate ppstate-equiv)
      (equal (update-ppstate->chars-read chars-read ppstate)
             (update-ppstate->chars-read chars-read ppstate-equiv)))
 :rule-classes :congruence)

Function: update-ppstate->chars-unread

(defun update-ppstate->chars-unread (chars-unread ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (natp chars-unread)))
  (b* ((ppstate (ppstate-fix ppstate)))
    (raw-update-ppstate->chars-unread (nfix chars-unread)
                                      ppstate)))

Theorem: ppstatep-of-update-ppstate->chars-unread

(defthm ppstatep-of-update-ppstate->chars-unread
 (b* ((ppstate (update-ppstate->chars-unread chars-unread ppstate)))
   (ppstatep ppstate))
 :rule-classes :rewrite)

Theorem: update-ppstate->chars-unread-of-nfix-chars-unread

(defthm update-ppstate->chars-unread-of-nfix-chars-unread
  (equal (update-ppstate->chars-unread (nfix chars-unread)
                                       ppstate)
         (update-ppstate->chars-unread chars-unread ppstate)))

Theorem: update-ppstate->chars-unread-nat-equiv-congruence-on-chars-unread

(defthm
  update-ppstate->chars-unread-nat-equiv-congruence-on-chars-unread
 (implies
  (acl2::nat-equiv chars-unread chars-unread-equiv)
  (equal (update-ppstate->chars-unread chars-unread ppstate)
         (update-ppstate->chars-unread chars-unread-equiv ppstate)))
 :rule-classes :congruence)

Theorem: update-ppstate->chars-unread-of-ppstate-fix-ppstate

(defthm update-ppstate->chars-unread-of-ppstate-fix-ppstate
 (equal
   (update-ppstate->chars-unread chars-unread (ppstate-fix ppstate))
   (update-ppstate->chars-unread chars-unread ppstate)))

Theorem: update-ppstate->chars-unread-ppstate-equiv-congruence-on-ppstate

(defthm
   update-ppstate->chars-unread-ppstate-equiv-congruence-on-ppstate
 (implies
  (ppstate-equiv ppstate ppstate-equiv)
  (equal (update-ppstate->chars-unread chars-unread ppstate)
         (update-ppstate->chars-unread chars-unread ppstate-equiv)))
 :rule-classes :congruence)

Function: update-ppstate->lexemes-length

(defun update-ppstate->lexemes-length (length ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (natp length)))
  (b* ((ppstate (ppstate-fix ppstate)))
    (raw-update-ppstate->lexemes-length (nfix length)
                                        ppstate)))

Theorem: ppstatep-of-update-ppstate->lexemes-length

(defthm ppstatep-of-update-ppstate->lexemes-length
  (b* ((ppstate (update-ppstate->lexemes-length length ppstate)))
    (ppstatep ppstate))
  :rule-classes :rewrite)

Theorem: update-ppstate->lexemes-length-of-nfix-length

(defthm update-ppstate->lexemes-length-of-nfix-length
  (equal (update-ppstate->lexemes-length (nfix length)
                                         ppstate)
         (update-ppstate->lexemes-length length ppstate)))

Theorem: update-ppstate->lexemes-length-nat-equiv-congruence-on-length

(defthm
      update-ppstate->lexemes-length-nat-equiv-congruence-on-length
 (implies
      (acl2::nat-equiv length length-equiv)
      (equal (update-ppstate->lexemes-length length ppstate)
             (update-ppstate->lexemes-length length-equiv ppstate)))
 :rule-classes :congruence)

Theorem: update-ppstate->lexemes-length-of-ppstate-fix-ppstate

(defthm update-ppstate->lexemes-length-of-ppstate-fix-ppstate
  (equal
       (update-ppstate->lexemes-length length (ppstate-fix ppstate))
       (update-ppstate->lexemes-length length ppstate)))

Theorem: update-ppstate->lexemes-length-ppstate-equiv-congruence-on-ppstate

(defthm
 update-ppstate->lexemes-length-ppstate-equiv-congruence-on-ppstate
 (implies
      (ppstate-equiv ppstate ppstate-equiv)
      (equal (update-ppstate->lexemes-length length ppstate)
             (update-ppstate->lexemes-length length ppstate-equiv)))
 :rule-classes :congruence)

Function: update-ppstate->lexeme

(defun update-ppstate->lexeme (i lexeme+span ppstate)
 (declare (xargs :stobjs (ppstate)))
 (declare (xargs :guard (and (natp i)
                             (plexeme+span-p lexeme+span))))
 (declare (xargs :guard (< i (ppstate->lexemes-length ppstate))))
 (b* ((ppstate (ppstate-fix ppstate)))
  (mbe
      :logic
      (if (< (nfix i)
             (ppstate->lexemes-length ppstate))
          (raw-update-ppstate->lexeme (nfix i)
                                      (plexeme+span-fix lexeme+span)
                                      ppstate)
        ppstate)
      :exec (raw-update-ppstate->lexeme i lexeme+span ppstate))))

Theorem: ppstatep-of-update-ppstate->lexeme

(defthm ppstatep-of-update-ppstate->lexeme
  (b* ((ppstate (update-ppstate->lexeme i lexeme+span ppstate)))
    (ppstatep ppstate))
  :rule-classes :rewrite)

Function: update-ppstate->lexemes-read

(defun update-ppstate->lexemes-read (lexemes-read ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (natp lexemes-read)))
  (b* ((ppstate (ppstate-fix ppstate)))
    (raw-update-ppstate->lexemes-read (nfix lexemes-read)
                                      ppstate)))

Theorem: ppstatep-of-update-ppstate->lexemes-read

(defthm ppstatep-of-update-ppstate->lexemes-read
 (b* ((ppstate (update-ppstate->lexemes-read lexemes-read ppstate)))
   (ppstatep ppstate))
 :rule-classes :rewrite)

Theorem: update-ppstate->lexemes-read-of-nfix-lexemes-read

(defthm update-ppstate->lexemes-read-of-nfix-lexemes-read
  (equal (update-ppstate->lexemes-read (nfix lexemes-read)
                                       ppstate)
         (update-ppstate->lexemes-read lexemes-read ppstate)))

Theorem: update-ppstate->lexemes-read-nat-equiv-congruence-on-lexemes-read

(defthm
  update-ppstate->lexemes-read-nat-equiv-congruence-on-lexemes-read
 (implies
  (acl2::nat-equiv lexemes-read lexemes-read-equiv)
  (equal (update-ppstate->lexemes-read lexemes-read ppstate)
         (update-ppstate->lexemes-read lexemes-read-equiv ppstate)))
 :rule-classes :congruence)

Theorem: update-ppstate->lexemes-read-of-ppstate-fix-ppstate

(defthm update-ppstate->lexemes-read-of-ppstate-fix-ppstate
 (equal
   (update-ppstate->lexemes-read lexemes-read (ppstate-fix ppstate))
   (update-ppstate->lexemes-read lexemes-read ppstate)))

Theorem: update-ppstate->lexemes-read-ppstate-equiv-congruence-on-ppstate

(defthm
   update-ppstate->lexemes-read-ppstate-equiv-congruence-on-ppstate
 (implies
  (ppstate-equiv ppstate ppstate-equiv)
  (equal (update-ppstate->lexemes-read lexemes-read ppstate)
         (update-ppstate->lexemes-read lexemes-read ppstate-equiv)))
 :rule-classes :congruence)

Function: update-ppstate->lexemes-unread

(defun update-ppstate->lexemes-unread (lexemes-unread ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (natp lexemes-unread)))
  (b* ((ppstate (ppstate-fix ppstate)))
    (raw-update-ppstate->lexemes-unread (nfix lexemes-unread)
                                        ppstate)))

Theorem: ppstatep-of-update-ppstate->lexemes-unread

(defthm ppstatep-of-update-ppstate->lexemes-unread
 (b* ((ppstate
           (update-ppstate->lexemes-unread lexemes-unread ppstate)))
   (ppstatep ppstate))
 :rule-classes :rewrite)

Theorem: update-ppstate->lexemes-unread-of-nfix-lexemes-unread

(defthm update-ppstate->lexemes-unread-of-nfix-lexemes-unread
  (equal (update-ppstate->lexemes-unread (nfix lexemes-unread)
                                         ppstate)
         (update-ppstate->lexemes-unread lexemes-unread ppstate)))

Theorem: update-ppstate->lexemes-unread-nat-equiv-congruence-on-lexemes-unread

(defthm
 update-ppstate->lexemes-unread-nat-equiv-congruence-on-lexemes-unread
 (implies
  (acl2::nat-equiv lexemes-unread lexemes-unread-equiv)
  (equal
     (update-ppstate->lexemes-unread lexemes-unread ppstate)
     (update-ppstate->lexemes-unread lexemes-unread-equiv ppstate)))
 :rule-classes :congruence)

Theorem: update-ppstate->lexemes-unread-of-ppstate-fix-ppstate

(defthm update-ppstate->lexemes-unread-of-ppstate-fix-ppstate
  (equal (update-ppstate->lexemes-unread
              lexemes-unread (ppstate-fix ppstate))
         (update-ppstate->lexemes-unread lexemes-unread ppstate)))

Theorem: update-ppstate->lexemes-unread-ppstate-equiv-congruence-on-ppstate

(defthm
 update-ppstate->lexemes-unread-ppstate-equiv-congruence-on-ppstate
 (implies
  (ppstate-equiv ppstate ppstate-equiv)
  (equal
     (update-ppstate->lexemes-unread lexemes-unread ppstate)
     (update-ppstate->lexemes-unread lexemes-unread ppstate-equiv)))
 :rule-classes :congruence)

Function: update-ppstate->version

(defun update-ppstate->version (version ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (c::versionp version)))
  (b* ((ppstate (ppstate-fix ppstate)))
    (raw-update-ppstate->version (c::version-fix version)
                                 ppstate)))

Theorem: ppstatep-of-update-ppstate->version

(defthm ppstatep-of-update-ppstate->version
  (b* ((ppstate (update-ppstate->version version ppstate)))
    (ppstatep ppstate))
  :rule-classes :rewrite)

Theorem: update-ppstate->version-of-version-fix-version

(defthm update-ppstate->version-of-version-fix-version
  (equal (update-ppstate->version (c::version-fix version)
                                  ppstate)
         (update-ppstate->version version ppstate)))

Theorem: update-ppstate->version-version-equiv-congruence-on-version

(defthm update-ppstate->version-version-equiv-congruence-on-version
  (implies (c::version-equiv version version-equiv)
           (equal (update-ppstate->version version ppstate)
                  (update-ppstate->version version-equiv ppstate)))
  :rule-classes :congruence)

Theorem: update-ppstate->version-of-ppstate-fix-ppstate

(defthm update-ppstate->version-of-ppstate-fix-ppstate
  (equal (update-ppstate->version version (ppstate-fix ppstate))
         (update-ppstate->version version ppstate)))

Theorem: update-ppstate->version-ppstate-equiv-congruence-on-ppstate

(defthm update-ppstate->version-ppstate-equiv-congruence-on-ppstate
  (implies (ppstate-equiv ppstate ppstate-equiv)
           (equal (update-ppstate->version version ppstate)
                  (update-ppstate->version version ppstate-equiv)))
  :rule-classes :congruence)

Function: update-ppstate->size

(defun update-ppstate->size (size ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (natp size)))
  (b* ((ppstate (ppstate-fix ppstate)))
    (raw-update-ppstate->size (lnfix size)
                              ppstate)))

Theorem: ppstatep-of-update-ppstate->size

(defthm ppstatep-of-update-ppstate->size
  (b* ((ppstate (update-ppstate->size size ppstate)))
    (ppstatep ppstate))
  :rule-classes :rewrite)

Theorem: update-ppstate->size-of-nfix-size

(defthm update-ppstate->size-of-nfix-size
  (equal (update-ppstate->size (nfix size)
                               ppstate)
         (update-ppstate->size size ppstate)))

Theorem: update-ppstate->size-nat-equiv-congruence-on-size

(defthm update-ppstate->size-nat-equiv-congruence-on-size
  (implies (acl2::nat-equiv size size-equiv)
           (equal (update-ppstate->size size ppstate)
                  (update-ppstate->size size-equiv ppstate)))
  :rule-classes :congruence)

Theorem: update-ppstate->size-of-ppstate-fix-ppstate

(defthm update-ppstate->size-of-ppstate-fix-ppstate
  (equal (update-ppstate->size size (ppstate-fix ppstate))
         (update-ppstate->size size ppstate)))

Theorem: update-ppstate->size-ppstate-equiv-congruence-on-ppstate

(defthm update-ppstate->size-ppstate-equiv-congruence-on-ppstate
  (implies (ppstate-equiv ppstate ppstate-equiv)
           (equal (update-ppstate->size size ppstate)
                  (update-ppstate->size size ppstate-equiv)))
  :rule-classes :congruence)

Function: update-ppstate->macros

(defun update-ppstate->macros (macros ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (macro-tablep macros)))
  (b* ((ppstate (ppstate-fix ppstate)))
    (raw-update-ppstate->macros (macro-table-fix macros)
                                ppstate)))

Theorem: ppstatep-of-update-ppstate->macros

(defthm ppstatep-of-update-ppstate->macros
  (b* ((ppstate (update-ppstate->macros macros ppstate)))
    (ppstatep ppstate))
  :rule-classes :rewrite)

Theorem: update-ppstate->macros-of-macro-table-fix-macros

(defthm update-ppstate->macros-of-macro-table-fix-macros
  (equal (update-ppstate->macros (macro-table-fix macros)
                                 ppstate)
         (update-ppstate->macros macros ppstate)))

Theorem: update-ppstate->macros-macro-table-equiv-congruence-on-macros

(defthm
      update-ppstate->macros-macro-table-equiv-congruence-on-macros
  (implies (macro-table-equiv macros macros-equiv)
           (equal (update-ppstate->macros macros ppstate)
                  (update-ppstate->macros macros-equiv ppstate)))
  :rule-classes :congruence)

Theorem: update-ppstate->macros-of-ppstate-fix-ppstate

(defthm update-ppstate->macros-of-ppstate-fix-ppstate
  (equal (update-ppstate->macros macros (ppstate-fix ppstate))
         (update-ppstate->macros macros ppstate)))

Theorem: update-ppstate->macros-ppstate-equiv-congruence-on-ppstate

(defthm update-ppstate->macros-ppstate-equiv-congruence-on-ppstate
  (implies (ppstate-equiv ppstate ppstate-equiv)
           (equal (update-ppstate->macros macros ppstate)
                  (update-ppstate->macros macros ppstate-equiv)))
  :rule-classes :congruence)

Theorem: ppstate->chars-length-of-update-ppstate->bytes

(defthm ppstate->chars-length-of-update-ppstate->bytes
  (equal
       (ppstate->chars-length (update-ppstate->bytes bytes ppstate))
       (ppstate->chars-length ppstate)))

Theorem: ppstate->size-of-update-ppstate->bytes

(defthm ppstate->size-of-update-ppstate->bytes
  (equal (ppstate->size (update-ppstate->bytes bytes ppstate))
         (ppstate->size ppstate)))

Theorem: ppstate->size-of-update-ppstate->position

(defthm ppstate->size-of-update-ppstate->position
  (equal (ppstate->size (update-ppstate->position position ppstate))
         (ppstate->size ppstate)))

Theorem: ppstate->size-of-update-ppstate->chars-read

(defthm ppstate->size-of-update-ppstate->chars-read
 (equal
     (ppstate->size (update-ppstate->chars-read chars-read ppstate))
     (ppstate->size ppstate)))

Theorem: ppstate->size-of-update-ppstate->chars-unread

(defthm ppstate->size-of-update-ppstate->chars-unread
  (equal (ppstate->size
              (update-ppstate->chars-unread chars-unread ppstate))
         (ppstate->size ppstate)))

Theorem: ppstate->size-of-update-ppstate->lexeme

(defthm ppstate->size-of-update-ppstate->lexeme
  (equal (ppstate->size (update-ppstate->lexeme i lexeme ppstate))
         (ppstate->size ppstate)))

Theorem: ppstate->size-of-update-ppstate->lexemes-read

(defthm ppstate->size-of-update-ppstate->lexemes-read
  (equal (ppstate->size
              (update-ppstate->lexemes-read lexemes-read ppstate))
         (ppstate->size ppstate)))

Theorem: ppstate->size-of-update-ppstate->size

(defthm ppstate->size-of-update-ppstate->size
  (equal (ppstate->size (update-ppstate->size size ppstate))
         (lnfix size)))

Theorem: update-ppstate->chars-read-of-ppstate->chars-read

(defthm update-ppstate->chars-read-of-ppstate->chars-read
  (equal (update-ppstate->chars-read (ppstate->chars-read ppstate)
                                     ppstate)
         (ppstate-fix ppstate)))

Theorem: update-ppstate->chars-read-of-ppstate->chars-unread

(defthm update-ppstate->chars-read-of-ppstate->chars-unread
  (equal
       (update-ppstate->chars-unread (ppstate->chars-unread ppstate)
                                     ppstate)
       (ppstate-fix ppstate)))