Backtrack to the latest checkpoint.
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 (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'backtrack-checkpoint)) (declare (ignorable __function__)) (b* ((checkpoints (parstate->checkpoints pstate)) ((unless (consp checkpoints)) (raise "Internal error: no checkpoints to backtrack.") (parstate-fix pstate)) (checkpoint (car checkpoints)) (new-chechpoints (cdr checkpoints)) (number-tokens-read (parstate->tokens-read-len pstate)) (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 pstate)) (pstate (unread-tokens number-tokens-to-unread pstate)) (new-pstate (change-parstate pstate :checkpoints new-chechpoints))) new-pstate)))
Theorem:
(defthm parstatep-of-backtrack-checkpoint (b* ((new-pstate (backtrack-checkpoint pstate))) (parstatep new-pstate)) :rule-classes :rewrite)