		Search-engine friendly clone of the ACL2 documentation.

Parser-states

Parstate

Fixtype of parser states.

Our parsing functions take and return parser states.

The parser 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 parser state could be defined as a fty::defprod, and in fact it was defined like that in previous versions of the parser.

The first component of the parser state is the input sequence bytes of bytes remaining, which initially comes from a file (see files). Bytes are read and removed from this component, and turned into characters.

Given the need for look-ahead during lexing, we use the common technique of ``unreading'' characters sometimes, i.e. putting them back into the parser state. But since we have already turned bytes into characters, we do not want to put back the bytes: thus, we keep, as part of the parser state (the exact representation is explained later), a sequence of unread characters, i.e. characters that have been read and then put back (i.e. unread), in character form; the form is natural numbers, i.e. Unicode code points. The sequence is initially empty. When non-empty, it can be thought of as preceding the bytes byte list. If the sequence of unread characters is not empty, the next character will be read directly from that list, not from the byte list.

To avoid putting back the wrong character by mistake, i.e. a character that was not actually read, the parser state also includes a sequence of all the characters read so far and that have not been unread (the exact representation is explained later), to keep track of which characters have been read and could be unread. Thus, every time we read a character, we add it to the sequence of read characters, which can be visualized to the left of the sequence of unread characters and the bytes list:

+----------+    read    +--------+-------+
| chars    |   <-----   | chars  | bytes |
| read     |   ----->   | unread |       |
+----------+   unread   +--------+-------+

The reading of a character moves the character from right to left, from the sequence of unread characters to the sequence of read characters if the sequence of unread characters is not empty, or from the bytes list to the sequence of read characters where one or more bytes are UTF-8-decoded into the character.

When a character is unread, it is moved from left to right, i.e. from the sequence of read characters to the sequence of unread characters. If the sequence of read characters is empty, it is an internal error: if the parser code is correct, this must never happen.

The reading and unreading of characters happens at the lexing level. A similar look-ahead happens at the proper parsing level, where the elements of the read and unread sequences are not characters but tokens. The parser state includes a sequence of read tokens and a sequence of unread tokens (the exact representation is explained later), whose handling is similar to the ones for characters. The sequence can be visualized as follows, similarly to characters:

+----------+    read    +--------+
| tokens   |   <-----   | tokens |
| read     |   ----->   | unread |
+----------+   unread   +--------+

When characters are read to form a token, the token is added to the sequence of read tokens. If the token is unread (i.e. put back), it is moved right to the sequence of unread tokens. When a token is read, if the sequence of unread tokens is not empty, the token is moved from right to left; if instead the sequence of unread tokens is empty, the token is read by reading characters and forming the token.

At the end of the parsing, the sequence of read characters contains all the characters read, and the sequence of read tokens contains all the tokens read. That is, the sequences are never cleared. For tokens, this lets us do some backtracking when needed, but without saving and copying the whole parser state: we just need to keep track of how many tokens must be put back for backtracking. For characters, in principle we could clear the sequence of read characters once a token is formed, but due to the representation of the sequence in the stobj, it is more time-efficient to never clear the sequence, at the cost of some space inefficiency, but we believe the latter not to be significant.

For reporting errors, it is useful to keep track of where in a file the constructs being parsed occur. To this end, the position component of the parser state is the position, in the file, of the next character to be read from the bytes component; if this component is empty, the position is just one past the last character in the file. For read and unread characters, since we have already found their position and have moved past it, we store their positions in the sequences of read and unread characters; so those sequences contain not just characters, but char+position pairs. Similarly, for tokens, we also store their spans in the sequences.

The sequences of read and unread characters are represented by three stobj components. The chars component consists of the concatenation of the two sequences, read characters then unread characters (as shown in the diagrams above), with additional elements to the right to extend the sequences. The chars-read component is the numbers of characters read, which are in the positions 0 (inclusive) to chars-read (exclusive). When chars-read is 0, there are no read characters, which happens at the beginning. The chars-unread component is the number of characters unread, which are in the positions chars-read (inclusive) to chars-read + chars-unread (exclusive). When chars-unread is 0, there are no unread characters, which happens at the beginning, and every time all the unread characters are read again. This organization lets us move characters between the two sequences just by changing char-read and char-unread, but leaving all the characters stored in the stobj array. The position from chars-read + chars-unread (inclusive) to the end of the array are not part of the sequences, but they are used when extending the sequence of read characters when there are no more unread characters: in this situation, chars-unread is 0, and the next character read from the bytes is stored into position chars-read, which is the same as chars-read + chars-unread since chars-unread is 0.

The sequence of read and unread tokens are represented similarly to read and unread characters, via the three stobj components tokens, tokens-read, and tokens-unread.

We include the C version. This parser state component is set at the beginning and never changes, but it is useful to have it as part of the parser state to avoid passing an additional parameter.

For speed, we cache the value returned by the function parsize defined later. Some profiling revealed that significant time was spent there, due to the need to save the parser state size before certain mbt tests. Ideally we should obtain this optimization using apt::isodata, but that transformation currently does not quite handle all of the parser's functions.

The definition of the stobj itself is straightforward, but we use a make-event so we can use richer terms for initial values. The initial chars and tokens arrays have length 1, which seems convenient for some fixing theorems, but it is irrelevant because it is resized at the very beginning of parsing.

The defstobj generates an enabled recognizer, which we disable after introducing the readers and writers. We define a fixer for that recognizer, using mbe to avoid the stobj restriction of having to return the stobj on all paths. Then we define a fixtype with the same name as the stobj, which causes no issue because fixtypes and stobjs are in different name spaces. In defining the fixtype, we set the equivalence relation to be non-executable, because otherwise we run into stobj restrictions.

The defstobj also generates recognizers for the fields, for which we have no use. But we rename them to less ambiguous names, by incorporating parstate into them, to avoid polluting the name space. These recognizers are enabled, but we do not bother disabling them, because we are not going to use them anywhere anyhow.

The defstobj also generates readers and writers for the fields, but they neither fix their inputs nor return outputs with unconditional types. So we define our own readers and writers that do both things, which we define in terms of the generated ones (actually, a few readers and writers do not fix their inputs yet, because we need to tweak the definition of the fixer for that, which we plan to do soon). The generated ones are enabled, but we do not bother disabling them, because we are not going to use them anywhere anyhow. We also prove some theorems about how readers and writers interact, as needed.

We locally enable length in order for the proofs generated by defstobj to go through. This is also useful for proofs about our readers and writers; for those, we also locally enable the fixer, and we prove some local theorems that are used there.

By making the parser state a stobj instead of a fty::defprod, we cannot use the :require feature of fty::defprod to enforce invariants, such as the fact that the size component is derived from others. But we can probably use defabsstobj for that, which may be also overall a better way to ``turn'' a stobj into a fty::defprod-like fixtype; we will look into that in the future.

Definitions and Theorems

Definition: raw-parstate->bytes-p

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-parstate->position-p

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-parstate->chars-p

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

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

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

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

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-parstate->tokens-p

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-parstate->tokens-read-p

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-parstate->tokens-unread-p

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-parstate->version-p

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-parstate->size-p

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: parstatep

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: create-parstate

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-parstate->bytes

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-update-parstate->bytes

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-parstate->position

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-update-parstate->position

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-parstate->chars-length

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

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

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-parstate->char

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-update-parstate->char

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-parstate->chars-read

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

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

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-parstate->chars-unread

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

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

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-parstate->tokens-length

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-update-parstate->tokens-length

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-parstate->token

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-update-parstate->token

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-parstate->tokens-read

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-update-parstate->tokens-read

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-parstate->tokens-unread

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-update-parstate->tokens-unread

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-parstate->version

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-update-parstate->version

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-parstate->size

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Definition: raw-update-parstate->size

(defstobj parstate
  (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)
  (tokens :type (array (satisfies token+span-p) (1))
          :initially ((:ident :irrelevant) (1 . 0) 1 . 0)
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (version :type (satisfies c::versionp)
           :initially (:c23))
  (size :type (integer 0 *) :initially 0)
  :renaming
  ((bytesp raw-parstate->bytes-p)
   (positionp raw-parstate->position-p)
   (charsp raw-parstate->chars-p)
   (chars-readp raw-parstate->chars-read-p)
   (chars-unreadp raw-parstate->chars-unread-p)
   (tokensp raw-parstate->tokens-p)
   (tokens-readp raw-parstate->tokens-read-p)
   (tokens-unreadp raw-parstate->tokens-unread-p)
   (versionp raw-parstate->version-p)
   (sizep raw-parstate->size-p)
   (bytes raw-parstate->bytes)
   (position raw-parstate->position)
   (chars-length raw-parstate->chars-length)
   (charsi raw-parstate->char)
   (chars-read raw-parstate->chars-read)
   (chars-unread raw-parstate->chars-unread)
   (tokens-length raw-parstate->tokens-length)
   (tokensi raw-parstate->token)
   (tokens-read raw-parstate->tokens-read)
   (tokens-unread raw-parstate->tokens-unread)
   (version raw-parstate->version)
   (size raw-parstate->size)
   (update-bytes raw-update-parstate->bytes)
   (update-position raw-update-parstate->position)
   (resize-chars raw-update-parstate->chars-length)
   (update-charsi raw-update-parstate->char)
   (update-chars-read raw-update-parstate->chars-read)
   (update-chars-unread raw-update-parstate->chars-unread)
   (resize-tokens raw-update-parstate->tokens-length)
   (update-tokensi raw-update-parstate->token)
   (update-tokens-read raw-update-parstate->tokens-read)
   (update-tokens-unread raw-update-parstate->tokens-unread)
   (update-version raw-update-parstate->version)
   (update-size raw-update-parstate->size))
  :inline t)

Function: parstate-fix$inline

(defun parstate-fix$inline (parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (parstatep parstate)
           parstate
         (non-exec (create-parstate)))
       :exec parstate))

Theorem: parstatep-of-parstate-fix

(defthm parstatep-of-parstate-fix
  (b* ((parstate (parstate-fix$inline parstate)))
    (parstatep parstate))
  :rule-classes :rewrite)

Theorem: parstate-fix-when-parstatep

(defthm parstate-fix-when-parstatep
  (implies (parstatep parstate)
           (equal (parstate-fix parstate)
                  parstate)))

Function: parstate-equiv

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

Theorem: parstate-equiv-is-an-equivalence

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

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

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

Theorem: parstate-fix-under-parstate-equiv

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

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

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

Theorem: raw-parstate->tokens-p-becomes-token+span-listp

(defthm raw-parstate->tokens-p-becomes-token+span-listp
  (equal (raw-parstate->tokens-p x)
         (token+span-listp x)))

Function: parstate->bytes$inline

(defun parstate->bytes$inline (parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (parstatep parstate)
           (raw-parstate->bytes parstate)
         nil)
       :exec (raw-parstate->bytes parstate)))

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

(defthm byte-listp-of-parstate->bytes
  (b* ((bytes (parstate->bytes$inline parstate)))
    (byte-listp bytes))
  :rule-classes :rewrite)

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

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

Theorem: parstate->bytes$inline-of-parstate-fix-parstate

(defthm parstate->bytes$inline-of-parstate-fix-parstate
  (equal (parstate->bytes$inline (parstate-fix parstate))
         (parstate->bytes$inline parstate)))

Theorem: parstate->bytes$inline-parstate-equiv-congruence-on-parstate

(defthm parstate->bytes$inline-parstate-equiv-congruence-on-parstate
  (implies (parstate-equiv parstate parstate-equiv)
           (equal (parstate->bytes$inline parstate)
                  (parstate->bytes$inline parstate-equiv)))
  :rule-classes :congruence)

Function: parstate->position$inline

(defun parstate->position$inline (parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (parstatep parstate)
           (raw-parstate->position parstate)
         (irr-position))
       :exec (raw-parstate->position parstate)))

Theorem: positionp-of-parstate->position

(defthm positionp-of-parstate->position
  (b* ((position (parstate->position$inline parstate)))
    (positionp position))
  :rule-classes :rewrite)

Function: parstate->chars-length$inline

(defun parstate->chars-length$inline (parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (parstatep parstate)
           (raw-parstate->chars-length parstate)
         1)
       :exec (raw-parstate->chars-length parstate)))

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

(defthm natp-of-parstate->chars-length
  (b* ((length (parstate->chars-length$inline parstate)))
    (natp length))
  :rule-classes :rewrite)

Theorem: parstate->chars-length$inline-of-parstate-fix-parstate

(defthm parstate->chars-length$inline-of-parstate-fix-parstate
  (equal (parstate->chars-length$inline (parstate-fix parstate))
         (parstate->chars-length$inline parstate)))

Theorem: parstate->chars-length$inline-parstate-equiv-congruence-on-parstate

(defthm
 parstate->chars-length$inline-parstate-equiv-congruence-on-parstate
 (implies (parstate-equiv parstate parstate-equiv)
          (equal (parstate->chars-length$inline parstate)
                 (parstate->chars-length$inline parstate-equiv)))
 :rule-classes :congruence)

Function: parstate->char$inline

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

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

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

Function: parstate->chars-read$inline

(defun parstate->chars-read$inline (parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (parstatep parstate)
           (raw-parstate->chars-read parstate)
         0)
       :exec (raw-parstate->chars-read parstate)))

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

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

Function: parstate->chars-unread$inline

(defun parstate->chars-unread$inline (parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (parstatep parstate)
           (raw-parstate->chars-unread parstate)
         0)
       :exec (raw-parstate->chars-unread parstate)))

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

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

Function: parstate->tokens-length$inline

(defun parstate->tokens-length$inline (parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (parstatep parstate)
           (raw-parstate->tokens-length parstate)
         1)
       :exec (raw-parstate->tokens-length parstate)))

Theorem: natp-of-parstate->tokens-length

(defthm natp-of-parstate->tokens-length
  (b* ((length (parstate->tokens-length$inline parstate)))
    (natp length))
  :rule-classes :rewrite)

Function: parstate->token$inline

(defun parstate->token$inline (i parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard (natp i)))
  (declare (xargs :guard (< i (parstate->tokens-length parstate))))
  (mbe :logic
       (if (and (parstatep parstate)
                (< (nfix i)
                   (parstate->tokens-length parstate)))
           (raw-parstate->token (nfix i) parstate)
         (make-token+span :token (irr-token)
                          :span (irr-position)))
       :exec (raw-parstate->token i parstate)))

Theorem: token+span-p-of-parstate->token

(defthm token+span-p-of-parstate->token
  (b* ((token+span (parstate->token$inline i parstate)))
    (token+span-p token+span))
  :rule-classes :rewrite)

Function: parstate->tokens-read$inline

(defun parstate->tokens-read$inline (parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (parstatep parstate)
           (raw-parstate->tokens-read parstate)
         0)
       :exec (raw-parstate->tokens-read parstate)))

Theorem: natp-of-parstate->tokens-read

(defthm natp-of-parstate->tokens-read
  (b* ((tokens-read (parstate->tokens-read$inline parstate)))
    (natp tokens-read))
  :rule-classes (:rewrite :type-prescription))

Function: parstate->tokens-unread$inline

(defun parstate->tokens-unread$inline (parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (parstatep parstate)
           (raw-parstate->tokens-unread parstate)
         0)
       :exec (raw-parstate->tokens-unread parstate)))

Theorem: natp-of-parstate->tokens-unread

(defthm natp-of-parstate->tokens-unread
  (b* ((tokens-unread (parstate->tokens-unread$inline parstate)))
    (natp tokens-unread))
  :rule-classes (:rewrite :type-prescription))

Function: parstate->version$inline

(defun parstate->version$inline (parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (parstatep parstate)
           (raw-parstate->version parstate)
         (c::version-c23))
       :exec (raw-parstate->version parstate)))

Theorem: versionp-of-parstate->version

(defthm versionp-of-parstate->version
  (b* ((version (parstate->version$inline parstate)))
    (c::versionp version))
  :rule-classes :rewrite)

Function: parstate->size$inline

(defun parstate->size$inline (parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (parstatep parstate)
           (raw-parstate->size parstate)
         0)
       :exec (raw-parstate->size parstate)))

Theorem: natp-of-parstate->size

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

Function: update-parstate->bytes$inline

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

Theorem: parstatep-of-update-parstate->bytes

(defthm parstatep-of-update-parstate->bytes
  (b* ((parstate (update-parstate->bytes$inline bytes parstate)))
    (parstatep parstate))
  :rule-classes :rewrite)

Function: update-parstate->position$inline

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

Theorem: parstatep-of-update-parstate->position

(defthm parstatep-of-update-parstate->position
  (b*
   ((parstate (update-parstate->position$inline position parstate)))
   (parstatep parstate))
  :rule-classes :rewrite)

Function: update-parstate->chars-length$inline

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

Theorem: parstatep-of-update-parstate->chars-length

(defthm parstatep-of-update-parstate->chars-length
  (b* ((parstate
            (update-parstate->chars-length$inline length parstate)))
    (parstatep parstate))
  :rule-classes :rewrite)

Function: update-parstate->char$inline

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

Theorem: parstatep-of-update-parstate->char

(defthm parstatep-of-update-parstate->char
 (b* ((parstate (update-parstate->char$inline i char+pos parstate)))
   (parstatep parstate))
 :rule-classes :rewrite)

Function: update-parstate->chars-read$inline

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

Theorem: parstatep-of-update-parstate->chars-read

(defthm parstatep-of-update-parstate->chars-read
  (b*
    ((parstate
          (update-parstate->chars-read$inline chars-read parstate)))
    (parstatep parstate))
  :rule-classes :rewrite)

Function: update-parstate->chars-unread$inline

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

Theorem: parstatep-of-update-parstate->chars-unread

(defthm parstatep-of-update-parstate->chars-unread
 (b*
  ((parstate
      (update-parstate->chars-unread$inline chars-unread parstate)))
  (parstatep parstate))
 :rule-classes :rewrite)

Function: update-parstate->tokens-length$inline

(defun update-parstate->tokens-length$inline (length parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard (natp length)))
  (b* ((parstate (parstate-fix parstate)))
    (raw-update-parstate->tokens-length (nfix length)
                                        parstate)))

Theorem: parstatep-of-update-parstate->tokens-length

(defthm parstatep-of-update-parstate->tokens-length
 (b* ((parstate
           (update-parstate->tokens-length$inline length parstate)))
   (parstatep parstate))
 :rule-classes :rewrite)

Function: update-parstate->token$inline

(defun update-parstate->token$inline (i token+span parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard (and (natp i)
                              (token+span-p token+span))))
  (declare (xargs :guard (< i (parstate->tokens-length parstate))))
  (b* ((parstate (parstate-fix parstate)))
    (mbe :logic
         (if (< (nfix i)
                (parstate->tokens-length parstate))
             (raw-update-parstate->token (nfix i)
                                         (token+span-fix token+span)
                                         parstate)
           parstate)
         :exec (raw-update-parstate->token i token+span parstate))))

Theorem: parstatep-of-update-parstate->token

(defthm parstatep-of-update-parstate->token
 (b*
  ((parstate (update-parstate->token$inline i token+span parstate)))
  (parstatep parstate))
 :rule-classes :rewrite)

Function: update-parstate->tokens-read$inline

(defun update-parstate->tokens-read$inline (tokens-read parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard (natp tokens-read)))
  (b* ((parstate (parstate-fix parstate)))
    (raw-update-parstate->tokens-read (nfix tokens-read)
                                      parstate)))

Theorem: parstatep-of-update-parstate->tokens-read

(defthm parstatep-of-update-parstate->tokens-read
 (b*
  ((parstate
        (update-parstate->tokens-read$inline tokens-read parstate)))
  (parstatep parstate))
 :rule-classes :rewrite)

Function: update-parstate->tokens-unread$inline

(defun update-parstate->tokens-unread$inline
       (tokens-unread parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard (natp tokens-unread)))
  (b* ((parstate (parstate-fix parstate)))
    (raw-update-parstate->tokens-unread (nfix tokens-unread)
                                        parstate)))

Theorem: parstatep-of-update-parstate->tokens-unread

(defthm parstatep-of-update-parstate->tokens-unread
 (b*
  ((parstate
    (update-parstate->tokens-unread$inline tokens-unread parstate)))
  (parstatep parstate))
 :rule-classes :rewrite)

Function: update-parstate->version$inline

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

Theorem: parstatep-of-update-parstate->version

(defthm parstatep-of-update-parstate->version
 (b* ((parstate (update-parstate->version$inline version parstate)))
   (parstatep parstate))
 :rule-classes :rewrite)

Function: update-parstate->size$inline

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

Theorem: parstatep-of-update-parstate->size

(defthm parstatep-of-update-parstate->size
  (b* ((parstate (update-parstate->size$inline size parstate)))
    (parstatep parstate))
  :rule-classes :rewrite)

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

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

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

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

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

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

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

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

Theorem: parstate->size-of-update-parstate->token

(defthm parstate->size-of-update-parstate->token
  (equal (parstate->size (update-parstate->token i token parstate))
         (parstate->size parstate)))

Theorem: parstate->size-of-update-parstate->tokens-read

(defthm parstate->size-of-update-parstate->tokens-read
  (equal (parstate->size
              (update-parstate->tokens-read tokens-read parstate))
         (parstate->size parstate)))

Theorem: parstate->size-of-update-parstate->size

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

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

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

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

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