Re-read tokens up to a specified index.
(reread-to-token token-index parstate) → new-parstate
We set
Function:
(defun reread-to-token (token-index parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (natp token-index) (parstatep parstate)))) (let ((__function__ 'reread-to-token)) (declare (ignorable __function__)) (b* ((token-index (nfix token-index)) (tokens-read (parstate->tokens-read parstate)) (tokens-unread (parstate->tokens-unread parstate)) ((unless (>= token-index tokens-read)) (raise "Internal error: ~ attempting to re-read tokens up to index ~x0 ~ but the currently read tokens are ~x1." token-index tokens-read) (parstate-fix parstate)) ((unless (<= token-index (+ tokens-read tokens-unread))) (raise "Internal error: ~ attempting to re-read tokens up to index ~x0 ~ but the currently available tokens (read and unread) are ~x1." token-index (+ tokens-read tokens-unread)) (parstate-fix parstate)) (parstate (update-parstate->tokens-read token-index parstate)) (tokens-diff (- token-index tokens-read)) (parstate (update-parstate->tokens-unread (- tokens-unread tokens-diff) parstate)) ((unless (>= (parstate->size parstate) tokens-diff)) (raise "Internal error: ~ size ~x0 is less than decrement ~x1." (parstate->size parstate) tokens-diff) (parstate-fix parstate)) (parstate (update-parstate->size (- (parstate->size parstate) tokens-diff) parstate))) parstate)))
Theorem:
(defthm parstatep-of-reread-to-token (implies (parstatep parstate) (b* ((new-parstate (reread-to-token token-index parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm reread-to-token-of-nfix-token-index (equal (reread-to-token (nfix token-index) parstate) (reread-to-token token-index parstate)))
Theorem:
(defthm reread-to-token-nat-equiv-congruence-on-token-index (implies (acl2::nat-equiv token-index token-index-equiv) (equal (reread-to-token token-index parstate) (reread-to-token token-index-equiv parstate))) :rule-classes :congruence)
Theorem:
(defthm reread-to-token-of-parstate-fix-parstate (equal (reread-to-token token-index (parstate-fix parstate)) (reread-to-token token-index parstate)))
Theorem:
(defthm reread-to-token-parstate-equiv-congruence-on-parstate (implies (parstate-equiv parstate parstate-equiv) (equal (reread-to-token token-index parstate) (reread-to-token token-index parstate-equiv))) :rule-classes :congruence)