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