Initialize the parser state.
(init-parstate data gcc parstate) → parstate
This is the state when we start parsing a file. Given (the data of) a file to parse, and a flag saying whether GCC extensions should be accepted or not, the initial parsing state consists of the data to parse, no unread characters or tokens, no read characters or tokens, the initial file position, and no checkpoints.
Function:
(defun init-parstate (data gcc parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (byte-listp data) (booleanp gcc)))) (let ((__function__ 'init-parstate)) (declare (ignorable __function__)) (b* ((parstate (update-parstate->bytes data parstate)) (parstate (update-parstate->position (position-init) parstate)) (parstate (update-parstate->chars-read nil parstate)) (parstate (update-parstate->chars-unread nil parstate)) (parstate (update-parstate->tokens-read nil parstate)) (parstate (update-parstate->tokens-read-len 0 parstate)) (parstate (update-parstate->tokens-unread nil parstate)) (parstate (update-parstate->checkpoints nil parstate)) (parstate (update-parstate->gcc gcc parstate)) (parstate (update-parstate->size (len data) parstate))) parstate)))
Theorem:
(defthm parstatep-of-init-parstate (b* ((parstate (init-parstate data gcc parstate))) (parstatep parstate)) :rule-classes :rewrite)
Theorem:
(defthm init-parstate-of-byte-list-fix-data (equal (init-parstate (byte-list-fix data) gcc parstate) (init-parstate data gcc parstate)))
Theorem:
(defthm init-parstate-byte-list-equiv-congruence-on-data (implies (acl2::byte-list-equiv data data-equiv) (equal (init-parstate data gcc parstate) (init-parstate data-equiv gcc parstate))) :rule-classes :congruence)
Theorem:
(defthm init-parstate-of-bool-fix-gcc (equal (init-parstate data (bool-fix gcc) parstate) (init-parstate data gcc parstate)))
Theorem:
(defthm init-parstate-iff-congruence-on-gcc (implies (iff gcc gcc-equiv) (equal (init-parstate data gcc parstate) (init-parstate data gcc-equiv parstate))) :rule-classes :congruence)
Theorem:
(defthm init-parstate-of-parstate-fix-parstate (equal (init-parstate data gcc (parstate-fix parstate)) (init-parstate data gcc parstate)))
Theorem:
(defthm init-parstate-parstate-equiv-congruence-on-parstate (implies (parstate-equiv parstate parstate-equiv) (equal (init-parstate data gcc parstate) (init-parstate data gcc parstate-equiv))) :rule-classes :congruence)