		Search-engine friendly clone of the ACL2 documentation.

Parser

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 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 a boolean flag saying whether certain GCC extensions should be accepted or not. These GCC extensions are limited to the ones currently captured in our grammar and abstract syntax. 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. This parser state component could potentially evolve into a richer set of options for different versions and dialects of C.

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 ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

Definition: raw-parstate->position-p

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

Definition: raw-parstate->chars-p

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

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

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

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

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

Definition: raw-parstate->tokens-p

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

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

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

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

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

Definition: raw-parstate->gcc-p

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

Definition: raw-parstate->size-p

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

Definition: parstatep

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

Definition: create-parstate

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

Definition: raw-parstate->bytes

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

Definition: raw-update-parstate->bytes

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

Definition: raw-parstate->position

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

Definition: raw-update-parstate->position

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

Definition: raw-parstate->chars-length

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

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

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

Definition: raw-parstate->char

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

Definition: raw-update-parstate->char

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

Definition: raw-parstate->chars-read

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

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

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

Definition: raw-parstate->chars-unread

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

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

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

Definition: raw-parstate->tokens-length

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

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

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

Definition: raw-parstate->token

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

Definition: raw-update-parstate->token

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

Definition: raw-parstate->tokens-read

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

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

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

Definition: raw-parstate->tokens-unread

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

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

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

Definition: raw-parstate->gcc

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

Definition: raw-update-parstate->gcc

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

Definition: raw-parstate->size

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

Definition: raw-update-parstate->size

(defstobj parstate
  (bytes :type (satisfies byte-listp)
         :initially nil)
  (position :type (satisfies positionp)
            :initially ((line . 1) (column . 0)))
  (chars :type (array (satisfies char+position-p) (1))
         :initially ((char . 0)
                     (position (line . 1) (column . 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 ((token :ident ((unwrap . :irrelevant)))
                      (span (start (line . 1) (column . 0))
                            (end (line . 1) (column . 0))))
          :resizable t)
  (tokens-read :type (integer 0 *)
               :initially 0)
  (tokens-unread :type (integer 0 *)
                 :initially 0)
  (gcc :type (satisfies booleanp)
       :initially nil)
  (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)
   (gccp raw-parstate->gcc-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)
   (gcc raw-parstate->gcc)
   (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-gcc raw-update-parstate->gcc)
   (update-size raw-update-parstate->size)))

Function: parstate-fix

(defun parstate-fix (parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard t))
  (let ((__function__ 'parstate-fix))
    (declare (ignorable __function__))
    (mbe :logic
         (if (parstatep parstate)
             parstate
           (create-parstate))
         :exec parstate)))

Theorem: parstatep-of-parstate-fix

(defthm parstatep-of-parstate-fix
  (b* ((parstate (parstate-fix 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-of-resize-list

(defthm raw-parstate->chars-p-of-resize-list
  (implies
       (and (raw-parstate->chars-p chars)
            (char+position-p default))
       (raw-parstate->chars-p (resize-list chars length default))))

Theorem: raw-parstate->tokens-p-of-resize-list

(defthm raw-parstate->tokens-p-of-resize-list
 (implies
      (and (raw-parstate->tokens-p tokens)
           (token+span-p default))
      (raw-parstate->tokens-p (resize-list tokens length default))))

Theorem: char+position-p-of-nth-when-raw-parstate->chars-p

(defthm char+position-p-of-nth-when-raw-parstate->chars-p
  (implies (and (raw-parstate->chars-p chars)
                (natp i)
                (< i (len chars)))
           (char+position-p (nth i chars))))

Theorem: token+span-p-of-nth-when-raw-parstate->tokens-p

(defthm token+span-p-of-nth-when-raw-parstate->tokens-p
  (implies (and (raw-parstate->tokens-p tokens)
                (natp i)
                (< i (len tokens)))
           (token+span-p (nth i tokens))))

Theorem: raw-parstate->chars-p-of-update-nth

(defthm raw-parstate->chars-p-of-update-nth
  (implies (raw-parstate->chars-p chars)
           (equal (raw-parstate->chars-p (update-nth i char chars))
                  (and (char+position-p char)
                       (<= (nfix i) (len chars))))))

Theorem: raw-parstate->tokens-p-of-update-nth

(defthm raw-parstate->tokens-p-of-update-nth
  (implies
       (raw-parstate->tokens-p tokens)
       (equal (raw-parstate->tokens-p (update-nth i token tokens))
              (and (token+span-p token)
                   (<= (nfix i) (len tokens))))))

Function: parstate->bytes

(defun parstate->bytes (parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard t))
  (let ((__function__ 'parstate->bytes))
    (declare (ignorable __function__))
    (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 parstate)))
    (byte-listp bytes))
  :rule-classes :rewrite)

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

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

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

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

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

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

Function: parstate->position

(defun parstate->position (parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard t))
  (let ((__function__ 'parstate->position))
    (declare (ignorable __function__))
    (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 parstate)))
    (positionp position))
  :rule-classes :rewrite)

Function: parstate->chars-length

(defun parstate->chars-length (parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard t))
  (let ((__function__ 'parstate->chars-length))
    (declare (ignorable __function__))
    (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 parstate)))
    (natp length))
  :rule-classes :rewrite)

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

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

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

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

Function: parstate->char

(defun parstate->char (i parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard (natp i)))
  (declare (xargs :guard (< i (parstate->chars-length parstate))))
  (let ((__function__ 'parstate->char))
    (declare (ignorable __function__))
    (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 i parstate)))
    (char+position-p char+pos))
  :rule-classes :rewrite)

Function: parstate->chars-read

(defun parstate->chars-read (parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard t))
  (let ((__function__ 'parstate->chars-read))
    (declare (ignorable __function__))
    (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 parstate)))
    (natp chars-read))
  :rule-classes (:rewrite :type-prescription))

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

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

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

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

Function: parstate->chars-unread

(defun parstate->chars-unread (parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard t))
  (let ((__function__ 'parstate->chars-unread))
    (declare (ignorable __function__))
    (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 parstate)))
    (natp chars-unread))
  :rule-classes (:rewrite :type-prescription))

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

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

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

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

Function: parstate->tokens-length

(defun parstate->tokens-length (parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard t))
  (let ((__function__ 'parstate->tokens-length))
    (declare (ignorable __function__))
    (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 parstate)))
    (natp length))
  :rule-classes :rewrite)

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

(defthm parstate->tokens-length-of-parstate-fix-parstate
  (equal (parstate->tokens-length (parstate-fix parstate))
         (parstate->tokens-length parstate)))

Theorem: parstate->tokens-length-parstate-equiv-congruence-on-parstate

(defthm
      parstate->tokens-length-parstate-equiv-congruence-on-parstate
  (implies (parstate-equiv parstate parstate-equiv)
           (equal (parstate->tokens-length parstate)
                  (parstate->tokens-length parstate-equiv)))
  :rule-classes :congruence)

Function: parstate->token

(defun parstate->token (i parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard (natp i)))
  (declare (xargs :guard (< i (parstate->tokens-length parstate))))
  (let ((__function__ 'parstate->token))
    (declare (ignorable __function__))
    (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 i parstate)))
    (token+span-p token+span))
  :rule-classes :rewrite)

Function: parstate->tokens-read

(defun parstate->tokens-read (parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard t))
  (let ((__function__ 'parstate->tokens-read))
    (declare (ignorable __function__))
    (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 parstate)))
    (natp tokens-read))
  :rule-classes (:rewrite :type-prescription))

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

(defthm parstate->tokens-read-of-parstate-fix-parstate
  (equal (parstate->tokens-read (parstate-fix parstate))
         (parstate->tokens-read parstate)))

Theorem: parstate->tokens-read-parstate-equiv-congruence-on-parstate

(defthm parstate->tokens-read-parstate-equiv-congruence-on-parstate
  (implies (parstate-equiv parstate parstate-equiv)
           (equal (parstate->tokens-read parstate)
                  (parstate->tokens-read parstate-equiv)))
  :rule-classes :congruence)

Function: parstate->tokens-unread

(defun parstate->tokens-unread (parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard t))
  (let ((__function__ 'parstate->tokens-unread))
    (declare (ignorable __function__))
    (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 parstate)))
    (natp tokens-unread))
  :rule-classes (:rewrite :type-prescription))

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

(defthm parstate->tokens-unread-of-parstate-fix-parstate
  (equal (parstate->tokens-unread (parstate-fix parstate))
         (parstate->tokens-unread parstate)))

Theorem: parstate->tokens-unread-parstate-equiv-congruence-on-parstate

(defthm
      parstate->tokens-unread-parstate-equiv-congruence-on-parstate
  (implies (parstate-equiv parstate parstate-equiv)
           (equal (parstate->tokens-unread parstate)
                  (parstate->tokens-unread parstate-equiv)))
  :rule-classes :congruence)

Function: parstate->gcc

(defun parstate->gcc (parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard t))
  (let ((__function__ 'parstate->gcc))
    (declare (ignorable __function__))
    (mbe :logic
         (if (parstatep parstate)
             (raw-parstate->gcc parstate)
           nil)
         :exec (raw-parstate->gcc parstate))))

Theorem: booleanp-of-parstate->gcc

(defthm booleanp-of-parstate->gcc
  (b* ((gcc (parstate->gcc parstate)))
    (booleanp gcc))
  :rule-classes :rewrite)

Theorem: parstate->gcc-of-parstate-fix-parstate

(defthm parstate->gcc-of-parstate-fix-parstate
  (equal (parstate->gcc (parstate-fix parstate))
         (parstate->gcc parstate)))

Theorem: parstate->gcc-parstate-equiv-congruence-on-parstate

(defthm parstate->gcc-parstate-equiv-congruence-on-parstate
  (implies (parstate-equiv parstate parstate-equiv)
           (equal (parstate->gcc parstate)
                  (parstate->gcc parstate-equiv)))
  :rule-classes :congruence)

Function: parstate->size

(defun parstate->size (parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard t))
  (let ((__function__ 'parstate->size))
    (declare (ignorable __function__))
    (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 parstate)))
    (natp size))
  :rule-classes (:rewrite :type-prescription))

Theorem: parstate->size-of-parstate-fix-parstate

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

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

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

Function: update-parstate->bytes

(defun update-parstate->bytes (bytes parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard (byte-listp bytes)))
  (let ((__function__ 'update-parstate->bytes))
    (declare (ignorable __function__))
    (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 bytes parstate)))
    (parstatep parstate))
  :rule-classes :rewrite)

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

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

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

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

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

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

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

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

Function: update-parstate->position

(defun update-parstate->position (position parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard (positionp position)))
  (let ((__function__ 'update-parstate->position))
    (declare (ignorable __function__))
    (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 position parstate)))
    (parstatep parstate))
  :rule-classes :rewrite)

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

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

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

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

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

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

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

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

Function: update-parstate->chars-length

(defun update-parstate->chars-length (length parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard (natp length)))
  (let ((__function__ 'update-parstate->chars-length))
    (declare (ignorable __function__))
    (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 length parstate)))
    (parstatep parstate))
  :rule-classes :rewrite)

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

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

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

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

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

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

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

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

Function: update-parstate->char

(defun update-parstate->char (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))))
 (let ((__function__ 'update-parstate->char))
  (declare (ignorable __function__))
  (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 i char+pos parstate)))
    (parstatep parstate))
  :rule-classes :rewrite)

Function: update-parstate->chars-read

(defun update-parstate->chars-read (chars-read parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard (natp chars-read)))
  (let ((__function__ 'update-parstate->chars-read))
    (declare (ignorable __function__))
    (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 chars-read parstate)))
    (parstatep parstate))
  :rule-classes :rewrite)

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

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

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

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

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

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

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

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

Function: update-parstate->chars-unread

(defun update-parstate->chars-unread (chars-unread parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard (natp chars-unread)))
  (let ((__function__ 'update-parstate->chars-unread))
    (declare (ignorable __function__))
    (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 chars-unread parstate)))
  (parstatep parstate))
 :rule-classes :rewrite)

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

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

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

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

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

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

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

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

Function: update-parstate->tokens-length

(defun update-parstate->tokens-length (length parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard (natp length)))
  (let ((__function__ 'update-parstate->tokens-length))
    (declare (ignorable __function__))
    (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 length parstate)))
    (parstatep parstate))
  :rule-classes :rewrite)

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

(defthm update-parstate->tokens-length-of-nfix-length
  (equal (update-parstate->tokens-length (nfix length)
                                         parstate)
         (update-parstate->tokens-length length parstate)))

Theorem: update-parstate->tokens-length-nat-equiv-congruence-on-length

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

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

(defthm update-parstate->tokens-length-of-parstate-fix-parstate
 (equal
     (update-parstate->tokens-length length (parstate-fix parstate))
     (update-parstate->tokens-length length parstate)))

Theorem: update-parstate->tokens-length-parstate-equiv-congruence-on-parstate

(defthm
 update-parstate->tokens-length-parstate-equiv-congruence-on-parstate
 (implies
     (parstate-equiv parstate parstate-equiv)
     (equal (update-parstate->tokens-length length parstate)
            (update-parstate->tokens-length length parstate-equiv)))
 :rule-classes :congruence)

Function: update-parstate->token

(defun update-parstate->token (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))))
 (let ((__function__ 'update-parstate->token))
  (declare (ignorable __function__))
  (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 i token+span parstate)))
    (parstatep parstate))
  :rule-classes :rewrite)

Function: update-parstate->tokens-read

(defun update-parstate->tokens-read (tokens-read parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard (natp tokens-read)))
  (let ((__function__ 'update-parstate->tokens-read))
    (declare (ignorable __function__))
    (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 tokens-read parstate)))
    (parstatep parstate))
  :rule-classes :rewrite)

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

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

Theorem: update-parstate->tokens-read-nat-equiv-congruence-on-tokens-read

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

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

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

Theorem: update-parstate->tokens-read-parstate-equiv-congruence-on-parstate

(defthm
 update-parstate->tokens-read-parstate-equiv-congruence-on-parstate
 (implies
  (parstate-equiv parstate parstate-equiv)
  (equal (update-parstate->tokens-read tokens-read parstate)
         (update-parstate->tokens-read tokens-read parstate-equiv)))
 :rule-classes :congruence)

Function: update-parstate->tokens-unread

(defun update-parstate->tokens-unread (tokens-unread parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard (natp tokens-unread)))
  (let ((__function__ 'update-parstate->tokens-unread))
    (declare (ignorable __function__))
    (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 tokens-unread parstate)))
   (parstatep parstate))
 :rule-classes :rewrite)

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

(defthm update-parstate->tokens-unread-of-nfix-tokens-unread
  (equal (update-parstate->tokens-unread (nfix tokens-unread)
                                         parstate)
         (update-parstate->tokens-unread tokens-unread parstate)))

Theorem: update-parstate->tokens-unread-nat-equiv-congruence-on-tokens-unread

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

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

(defthm update-parstate->tokens-unread-of-parstate-fix-parstate
  (equal (update-parstate->tokens-unread
              tokens-unread (parstate-fix parstate))
         (update-parstate->tokens-unread tokens-unread parstate)))

Theorem: update-parstate->tokens-unread-parstate-equiv-congruence-on-parstate

(defthm
 update-parstate->tokens-unread-parstate-equiv-congruence-on-parstate
 (implies
  (parstate-equiv parstate parstate-equiv)
  (equal
     (update-parstate->tokens-unread tokens-unread parstate)
     (update-parstate->tokens-unread tokens-unread parstate-equiv)))
 :rule-classes :congruence)

Function: update-parstate->gcc

(defun update-parstate->gcc (gcc parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard (booleanp gcc)))
  (let ((__function__ 'update-parstate->gcc))
    (declare (ignorable __function__))
    (b* ((parstate (parstate-fix parstate)))
      (raw-update-parstate->gcc (bool-fix gcc)
                                parstate))))

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

(defthm parstatep-of-update-parstate->gcc
  (b* ((parstate (update-parstate->gcc gcc parstate)))
    (parstatep parstate))
  :rule-classes :rewrite)

Theorem: update-parstate->gcc-of-bool-fix-gcc

(defthm update-parstate->gcc-of-bool-fix-gcc
  (equal (update-parstate->gcc (bool-fix gcc)
                               parstate)
         (update-parstate->gcc gcc parstate)))

Theorem: update-parstate->gcc-iff-congruence-on-gcc

(defthm update-parstate->gcc-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (update-parstate->gcc gcc parstate)
                  (update-parstate->gcc gcc-equiv parstate)))
  :rule-classes :congruence)

Theorem: update-parstate->gcc-of-parstate-fix-parstate

(defthm update-parstate->gcc-of-parstate-fix-parstate
  (equal (update-parstate->gcc gcc (parstate-fix parstate))
         (update-parstate->gcc gcc parstate)))

Theorem: update-parstate->gcc-parstate-equiv-congruence-on-parstate

(defthm update-parstate->gcc-parstate-equiv-congruence-on-parstate
  (implies (parstate-equiv parstate parstate-equiv)
           (equal (update-parstate->gcc gcc parstate)
                  (update-parstate->gcc gcc parstate-equiv)))
  :rule-classes :congruence)

Function: update-parstate->size

(defun update-parstate->size (size parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard (natp size)))
  (let ((__function__ 'update-parstate->size))
    (declare (ignorable __function__))
    (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 size parstate)))
    (parstatep parstate))
  :rule-classes :rewrite)

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

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

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

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

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

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

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

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

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)))