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