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