Unread a token.
(unread-token parstate) → new-parstate
We pop the token from the
It is an internal error if the
Function:
(defun unread-token (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'unread-token)) (declare (ignorable __function__)) (b* ((parstate.tokens-read (parstate->tokens-read parstate)) (parstate.tokens-read-len (parstate->tokens-read-len parstate)) (parstate.tokens-unread (parstate->tokens-unread parstate)) (parstate.size (parstate->size parstate)) ((unless (and (consp parstate.tokens-read) (> parstate.tokens-read-len 0))) (raise "Internal error: no token to unread.") (b* ((parstate (update-parstate->tokens-unread (cons (make-token+span :token (irr-token) :span (irr-span)) parstate.tokens-unread) parstate)) (parstate (update-parstate->size (1+ parstate.size) parstate))) parstate)) (token+span (car parstate.tokens-read)) (parstate (update-parstate->tokens-unread (cons token+span parstate.tokens-unread) parstate)) (parstate (update-parstate->tokens-read (cdr parstate.tokens-read) parstate)) (parstate (update-parstate->tokens-read-len (1- parstate.tokens-read-len) parstate)) (parstate (update-parstate->size (1+ parstate.size) parstate))) parstate)))
Theorem:
(defthm parstatep-of-unread-token (implies (parstatep parstate) (b* ((new-parstate (unread-token parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-unread-token (b* ((?new-parstate (unread-token parstate))) (equal (parsize new-parstate) (1+ (parsize parstate)))))