Backtrack to the latest checkpoint.
(backtrack-checkpoint parstate) → new-parstate
This is called when the parser needs to backtrack. We calculate the number of tokens to unread and we unread them. We also remove the checkpoint from the list of checkpoints, since it no longer serves a purpose (we have backtracked to it).
It is an internal error if this is called when the list of checkpoints is empty. If this happens, there is a bug in the parser.
Function:
(defun backtrack-checkpoint (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'backtrack-checkpoint)) (declare (ignorable __function__)) (b* ((checkpoints (parstate->checkpoints parstate)) ((unless (consp checkpoints)) (raise "Internal error: no checkpoints to backtrack.") (parstate-fix parstate)) (checkpoint (car checkpoints)) (new-chechpoints (cdr checkpoints)) (number-tokens-read (parstate->tokens-read-len parstate)) (number-tokens-to-unread (- number-tokens-read checkpoint)) ((unless (> number-tokens-to-unread 0)) (raise "Internal error: ~ the checkpoint ~x0 is not less than ~ the number ~x1 of tokens read so far." checkpoint number-tokens-read) (parstate-fix parstate)) (parstate (unread-tokens number-tokens-to-unread parstate)) (parstate (update-parstate->checkpoints new-chechpoints parstate))) parstate)))
Theorem:
(defthm parstatep-of-backtrack-checkpoint (implies (parstatep parstate) (b* ((new-parstate (backtrack-checkpoint parstate))) (parstatep new-parstate))) :rule-classes :rewrite)