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 description below of the parser state treats the parser state as if it were defined via fty::defprod, not as a stobj; at the end, we explain how the stobj represents that parser state.
The primary component of a parser state
is the input sequence
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, the
To avoid putting back the wrong character by mistake,
i.e. a character that was not actually read,
we use the
+----------+ read +--------+-------+ | chars | <----- | chars | bytes | | read | | unread | | | reversed | -----> | | | +----------+ unread +--------+-------+
The reading of a character moves the character from right to left,
from the
When a character is unread, it is moved from left to right,
i.e. from the reversed
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 lists
are not characters but tokens.
The parser state has lists
+----------+----------+ read +--------+-------+ | tokens | chars | <----- | chars | bytes | | read | read | | unread | | | reversed | reversed | -----> | | | +----------+----------+ unread +--------+-------+ +----------+ read +--------+--------+-------+ | tokens | <----- | tokens | chars | bytes | | read | | unread | unread | | | reversed | -----> | | | | +----------+ unread +--------+--------+-------+
When a token is successfully read,
it is moved left to the reversed
Characters are read only as a subroutine of reading tokens.
If a token is unread, it is unread just after having been read,
with the
While
For reporting errors, it is useful to keep track of
where in a file the constructs being parsed occur.
To this end, the
To support backtracking,
we also keep track of zero or more checkpoints,
which indicate positions in the
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 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.
Also for speed, we cache the number of the tokens read so far. The checkpointing and backtracking mechanism described above calculates that length in order to record it as a checkpoint. When there is a significant number of read token, that can take time, as revealed by some profiling.
The stobj for the parser state consists of the components described above, but in a stobj instead of a fty::defprod. This is a ``shallow'' stobj, because several of the components are still lists that are updated in a non-destructive way. We plan to ``deepen'' the stobj by using arrays and indices to simulate those lists in a more efficient way.
The definition of the stobj itself is straightforward, but we use a make-event so we can use position-init instead of a term for its value that exposes the internal representation of positions.
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
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. The generated ones are enabled, but we do not both 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.
By making the parser state a stobj instead of a fty::defprod,
we cannot use the
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Definition:
(defstobj parstate (bytes :type (satisfies byte-listp) :initially nil) (position :type (satisfies positionp) :initially ((line . 1) (column . 0))) (chars-read :type (satisfies char+position-listp) :initially nil) (chars-unread :type (satisfies char+position-listp) :initially nil) (tokens-read :type (satisfies token+span-listp) :initially nil) (tokens-read-len :type (integer 0 *) :initially 0) (tokens-unread :type (satisfies token+span-listp) :initially nil) (checkpoints :type (satisfies nat-listp) :initially nil) (gcc :type (satisfies booleanp) :initially nil) (size :type (integer 0 *) :initially 0) :renaming ((bytesp raw-parstate->bytes-p) (positionp raw-parstate->position-p) (chars-readp raw-parstate->chars-read-p) (chars-unreadp raw-parstate->chars-unread-p) (tokens-readp raw-parstate->tokens-read-p) (tokens-read-lenp raw-parstate->tokens-read-len-p) (tokens-unreadp raw-parstate->tokens-unread-p) (checkpointsp raw-parstate->checkpoints-p) (gccp raw-parstate->gcc-p) (sizep raw-parstate->size-p) (bytes raw-parstate->bytes) (position raw-parstate->position) (chars-read raw-parstate->chars-read) (chars-unread raw-parstate->chars-unread) (tokens-read raw-parstate->tokens-read) (tokens-read-len raw-parstate->tokens-read-len) (tokens-unread raw-parstate->tokens-unread) (checkpoints raw-parstate->checkpoints) (gcc raw-parstate->gcc) (size raw-parstate->size) (update-bytes raw-update-parstate->bytes) (update-position raw-update-parstate->position) (update-chars-read raw-update-parstate->chars-read) (update-chars-unread raw-update-parstate->chars-unread) (update-tokens-read raw-update-parstate->tokens-read) (update-tokens-read-len raw-update-parstate->tokens-read-len) (update-tokens-unread raw-update-parstate->tokens-unread) (update-checkpoints raw-update-parstate->checkpoints) (update-gcc raw-update-parstate->gcc) (update-size raw-update-parstate->size)))
Function:
(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:
(defthm parstatep-of-parstate-fix (b* ((parstate (parstate-fix parstate))) (parstatep parstate)) :rule-classes :rewrite)
Theorem:
(defthm parstate-fix-when-parstatep (implies (parstatep parstate) (equal (parstate-fix parstate) parstate)))
Function:
(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:
(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:
(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:
(defthm parstate-fix-under-parstate-equiv (parstate-equiv (parstate-fix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))
Function:
(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:
(defthm byte-listp-of-parstate->bytes (b* ((bytes (parstate->bytes parstate))) (byte-listp bytes)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-parstate->bytes (b* ((bytes (parstate->bytes parstate))) (true-listp bytes)) :rule-classes :type-prescription)
Theorem:
(defthm parstate->bytes-of-parstate-fix-parstate (equal (parstate->bytes (parstate-fix parstate)) (parstate->bytes parstate)))
Theorem:
(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:
(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) (position-init)) :exec (raw-parstate->position parstate))))
Theorem:
(defthm positionp-of-parstate->position (b* ((position (parstate->position parstate))) (positionp position)) :rule-classes :rewrite)
Theorem:
(defthm parstate->position-of-parstate-fix-parstate (equal (parstate->position (parstate-fix parstate)) (parstate->position parstate)))
Theorem:
(defthm parstate->position-parstate-equiv-congruence-on-parstate (implies (parstate-equiv parstate parstate-equiv) (equal (parstate->position parstate) (parstate->position parstate-equiv))) :rule-classes :congruence)
Function:
(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) nil) :exec (raw-parstate->chars-read parstate))))
Theorem:
(defthm char+position-listp-of-parstate->chars-read (b* ((chars-read (parstate->chars-read parstate))) (char+position-listp chars-read)) :rule-classes :rewrite)
Theorem:
(defthm parstate->chars-read-of-parstate-fix-parstate (equal (parstate->chars-read (parstate-fix parstate)) (parstate->chars-read parstate)))
Theorem:
(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:
(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) nil) :exec (raw-parstate->chars-unread parstate))))
Theorem:
(defthm char+position-listp-of-parstate->chars-unread (b* ((chars-unread (parstate->chars-unread parstate))) (char+position-listp chars-unread)) :rule-classes :rewrite)
Theorem:
(defthm parstate->chars-unread-of-parstate-fix-parstate (equal (parstate->chars-unread (parstate-fix parstate)) (parstate->chars-unread parstate)))
Theorem:
(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:
(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) nil) :exec (raw-parstate->tokens-read parstate))))
Theorem:
(defthm token+span-listp-of-parstate->tokens-read (b* ((tokens-read (parstate->tokens-read parstate))) (token+span-listp tokens-read)) :rule-classes :rewrite)
Theorem:
(defthm parstate->tokens-read-of-parstate-fix-parstate (equal (parstate->tokens-read (parstate-fix parstate)) (parstate->tokens-read parstate)))
Theorem:
(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:
(defun parstate->tokens-read-len (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard t)) (let ((__function__ 'parstate->tokens-read-len)) (declare (ignorable __function__)) (mbe :logic (if (parstatep parstate) (raw-parstate->tokens-read-len parstate) 0) :exec (raw-parstate->tokens-read-len parstate))))
Theorem:
(defthm natp-of-parstate->tokens-read-len (b* ((tokens-read-len (parstate->tokens-read-len parstate))) (natp tokens-read-len)) :rule-classes (:rewrite :type-prescription))
Theorem:
(defthm parstate->tokens-read-len-of-parstate-fix-parstate (equal (parstate->tokens-read-len (parstate-fix parstate)) (parstate->tokens-read-len parstate)))
Theorem:
(defthm parstate->tokens-read-len-parstate-equiv-congruence-on-parstate (implies (parstate-equiv parstate parstate-equiv) (equal (parstate->tokens-read-len parstate) (parstate->tokens-read-len parstate-equiv))) :rule-classes :congruence)
Function:
(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) nil) :exec (raw-parstate->tokens-unread parstate))))
Theorem:
(defthm token+span-listp-of-parstate->tokens-unread (b* ((tokens-unread (parstate->tokens-unread parstate))) (token+span-listp tokens-unread)) :rule-classes :rewrite)
Theorem:
(defthm parstate->tokens-unread-of-parstate-fix-parstate (equal (parstate->tokens-unread (parstate-fix parstate)) (parstate->tokens-unread parstate)))
Theorem:
(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:
(defun parstate->checkpoints (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard t)) (let ((__function__ 'parstate->checkpoints)) (declare (ignorable __function__)) (mbe :logic (if (parstatep parstate) (raw-parstate->checkpoints parstate) nil) :exec (raw-parstate->checkpoints parstate))))
Theorem:
(defthm nat-listp-of-parstate->checkpoints (b* ((checkpoints (parstate->checkpoints parstate))) (nat-listp checkpoints)) :rule-classes :rewrite)
Theorem:
(defthm parstate->checkpoints-of-parstate-fix-parstate (equal (parstate->checkpoints (parstate-fix parstate)) (parstate->checkpoints parstate)))
Theorem:
(defthm parstate->checkpoints-parstate-equiv-congruence-on-parstate (implies (parstate-equiv parstate parstate-equiv) (equal (parstate->checkpoints parstate) (parstate->checkpoints parstate-equiv))) :rule-classes :congruence)
Function:
(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:
(defthm booleanp-of-parstate->gcc (b* ((gcc (parstate->gcc parstate))) (booleanp gcc)) :rule-classes :rewrite)
Theorem:
(defthm parstate->gcc-of-parstate-fix-parstate (equal (parstate->gcc (parstate-fix parstate)) (parstate->gcc parstate)))
Theorem:
(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:
(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:
(defthm natp-of-parstate->size (b* ((size (parstate->size parstate))) (natp size)) :rule-classes (:rewrite :type-prescription))
Theorem:
(defthm parstate->size-of-parstate-fix-parstate (equal (parstate->size (parstate-fix parstate)) (parstate->size parstate)))
Theorem:
(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:
(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:
(defthm parstatep-of-update-parstate->bytes (b* ((parstate (update-parstate->bytes bytes parstate))) (parstatep parstate)) :rule-classes :rewrite)
Theorem:
(defthm update-parstate->bytes-of-byte-list-fix-bytes (equal (update-parstate->bytes (byte-list-fix bytes) parstate) (update-parstate->bytes bytes parstate)))
Theorem:
(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:
(defthm update-parstate->bytes-of-parstate-fix-parstate (equal (update-parstate->bytes bytes (parstate-fix parstate)) (update-parstate->bytes bytes parstate)))
Theorem:
(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:
(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:
(defthm parstatep-of-update-parstate->position (b* ((parstate (update-parstate->position position parstate))) (parstatep parstate)) :rule-classes :rewrite)
Theorem:
(defthm update-parstate->position-of-position-fix-position (equal (update-parstate->position (position-fix position) parstate) (update-parstate->position position parstate)))
Theorem:
(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:
(defthm update-parstate->position-of-parstate-fix-parstate (equal (update-parstate->position position (parstate-fix parstate)) (update-parstate->position position parstate)))
Theorem:
(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:
(defun update-parstate->chars-read (chars-read parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (char+position-listp chars-read))) (let ((__function__ 'update-parstate->chars-read)) (declare (ignorable __function__)) (b* ((parstate (parstate-fix parstate))) (raw-update-parstate->chars-read (char+position-list-fix chars-read) parstate))))
Theorem:
(defthm parstatep-of-update-parstate->chars-read (b* ((parstate (update-parstate->chars-read chars-read parstate))) (parstatep parstate)) :rule-classes :rewrite)
Theorem:
(defthm update-parstate->chars-read-of-char+position-list-fix-chars-read (equal (update-parstate->chars-read (char+position-list-fix chars-read) parstate) (update-parstate->chars-read chars-read parstate)))
Theorem:
(defthm update-parstate->chars-read-char+position-list-equiv-congruence-on-chars-read (implies (char+position-list-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:
(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:
(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:
(defun update-parstate->chars-unread (chars-unread parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (char+position-listp chars-unread))) (let ((__function__ 'update-parstate->chars-unread)) (declare (ignorable __function__)) (b* ((parstate (parstate-fix parstate))) (raw-update-parstate->chars-unread (char+position-list-fix chars-unread) parstate))))
Theorem:
(defthm parstatep-of-update-parstate->chars-unread (b* ((parstate (update-parstate->chars-unread chars-unread parstate))) (parstatep parstate)) :rule-classes :rewrite)
Theorem:
(defthm update-parstate->chars-unread-of-char+position-list-fix-chars-unread (equal (update-parstate->chars-unread (char+position-list-fix chars-unread) parstate) (update-parstate->chars-unread chars-unread parstate)))
Theorem:
(defthm update-parstate->chars-unread-char+position-list-equiv-congruence-on-chars-unread (implies (char+position-list-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:
(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:
(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:
(defun update-parstate->tokens-read (tokens-read parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (token+span-listp tokens-read))) (let ((__function__ 'update-parstate->tokens-read)) (declare (ignorable __function__)) (b* ((parstate (parstate-fix parstate))) (raw-update-parstate->tokens-read (token+span-list-fix tokens-read) parstate))))
Theorem:
(defthm parstatep-of-update-parstate->tokens-read (b* ((parstate (update-parstate->tokens-read tokens-read parstate))) (parstatep parstate)) :rule-classes :rewrite)
Theorem:
(defthm update-parstate->tokens-read-of-token+span-list-fix-tokens-read (equal (update-parstate->tokens-read (token+span-list-fix tokens-read) parstate) (update-parstate->tokens-read tokens-read parstate)))
Theorem:
(defthm update-parstate->tokens-read-token+span-list-equiv-congruence-on-tokens-read (implies (token+span-list-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:
(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:
(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:
(defun update-parstate->tokens-read-len (tokens-read-len parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (natp tokens-read-len))) (let ((__function__ 'update-parstate->tokens-read-len)) (declare (ignorable __function__)) (b* ((parstate (parstate-fix parstate))) (raw-update-parstate->tokens-read-len (lnfix tokens-read-len) parstate))))
Theorem:
(defthm parstatep-of-update-parstate->tokens-read-len (b* ((parstate (update-parstate->tokens-read-len tokens-read-len parstate))) (parstatep parstate)) :rule-classes :rewrite)
Theorem:
(defthm update-parstate->tokens-read-len-of-nfix-tokens-read-len (equal (update-parstate->tokens-read-len (nfix tokens-read-len) parstate) (update-parstate->tokens-read-len tokens-read-len parstate)))
Theorem:
(defthm update-parstate->tokens-read-len-nat-equiv-congruence-on-tokens-read-len (implies (acl2::nat-equiv tokens-read-len tokens-read-len-equiv) (equal (update-parstate->tokens-read-len tokens-read-len parstate) (update-parstate->tokens-read-len tokens-read-len-equiv parstate))) :rule-classes :congruence)
Theorem:
(defthm update-parstate->tokens-read-len-of-parstate-fix-parstate (equal (update-parstate->tokens-read-len tokens-read-len (parstate-fix parstate)) (update-parstate->tokens-read-len tokens-read-len parstate)))
Theorem:
(defthm update-parstate->tokens-read-len-parstate-equiv-congruence-on-parstate (implies (parstate-equiv parstate parstate-equiv) (equal (update-parstate->tokens-read-len tokens-read-len parstate) (update-parstate->tokens-read-len tokens-read-len parstate-equiv))) :rule-classes :congruence)
Function:
(defun update-parstate->tokens-unread (tokens-unread parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (token+span-listp tokens-unread))) (let ((__function__ 'update-parstate->tokens-unread)) (declare (ignorable __function__)) (b* ((parstate (parstate-fix parstate))) (raw-update-parstate->tokens-unread (token+span-list-fix tokens-unread) parstate))))
Theorem:
(defthm parstatep-of-update-parstate->tokens-unread (b* ((parstate (update-parstate->tokens-unread tokens-unread parstate))) (parstatep parstate)) :rule-classes :rewrite)
Theorem:
(defthm update-parstate->tokens-unread-of-token+span-list-fix-tokens-unread (equal (update-parstate->tokens-unread (token+span-list-fix tokens-unread) parstate) (update-parstate->tokens-unread tokens-unread parstate)))
Theorem:
(defthm update-parstate->tokens-unread-token+span-list-equiv-congruence-on-tokens-unread (implies (token+span-list-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:
(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:
(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:
(defun update-parstate->checkpoints (checkpoints parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (nat-listp checkpoints))) (let ((__function__ 'update-parstate->checkpoints)) (declare (ignorable __function__)) (b* ((parstate (parstate-fix parstate))) (raw-update-parstate->checkpoints (nat-list-fix checkpoints) parstate))))
Theorem:
(defthm parstatep-of-update-parstate->checkpoints (b* ((parstate (update-parstate->checkpoints checkpoints parstate))) (parstatep parstate)) :rule-classes :rewrite)
Theorem:
(defthm update-parstate->checkpoints-of-nat-list-fix-checkpoints (equal (update-parstate->checkpoints (nat-list-fix checkpoints) parstate) (update-parstate->checkpoints checkpoints parstate)))
Theorem:
(defthm update-parstate->checkpoints-nat-list-equiv-congruence-on-checkpoints (implies (acl2::nat-list-equiv checkpoints checkpoints-equiv) (equal (update-parstate->checkpoints checkpoints parstate) (update-parstate->checkpoints checkpoints-equiv parstate))) :rule-classes :congruence)
Theorem:
(defthm update-parstate->checkpoints-of-parstate-fix-parstate (equal (update-parstate->checkpoints checkpoints (parstate-fix parstate)) (update-parstate->checkpoints checkpoints parstate)))
Theorem:
(defthm update-parstate->checkpoints-parstate-equiv-congruence-on-parstate (implies (parstate-equiv parstate parstate-equiv) (equal (update-parstate->checkpoints checkpoints parstate) (update-parstate->checkpoints checkpoints parstate-equiv))) :rule-classes :congruence)
Function:
(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:
(defthm parstatep-of-update-parstate->gcc (b* ((parstate (update-parstate->gcc gcc parstate))) (parstatep parstate)) :rule-classes :rewrite)
Theorem:
(defthm update-parstate->gcc-of-bool-fix-gcc (equal (update-parstate->gcc (bool-fix gcc) parstate) (update-parstate->gcc gcc parstate)))
Theorem:
(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:
(defthm update-parstate->gcc-of-parstate-fix-parstate (equal (update-parstate->gcc gcc (parstate-fix parstate)) (update-parstate->gcc gcc parstate)))
Theorem:
(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:
(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:
(defthm parstatep-of-update-parstate->size (b* ((parstate (update-parstate->size size parstate))) (parstatep parstate)) :rule-classes :rewrite)
Theorem:
(defthm update-parstate->size-of-nfix-size (equal (update-parstate->size (nfix size) parstate) (update-parstate->size size parstate)))
Theorem:
(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:
(defthm update-parstate->size-of-parstate-fix-parstate (equal (update-parstate->size size (parstate-fix parstate)) (update-parstate->size size parstate)))
Theorem:
(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:
(defthm parstate->size-of-update-parstate->tokens-read (equal (parstate->size (update-parstate->tokens-read tokens-read parstate)) (parstate->size parstate)))
Theorem:
(defthm parstate->size-of-update-parstate->tokens-read-len (equal (parstate->size (update-parstate->tokens-read-len tokens-read-len parstate)) (parstate->size parstate)))
Theorem:
(defthm parstate->size-of-update-parstate->checkpoints (equal (parstate->size (update-parstate->checkpoints checkpoints parstate)) (parstate->size parstate)))
Theorem:
(defthm parstate->size-of-update-parstate->size (equal (parstate->size (update-parstate->size size parstate)) (lnfix size)))