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