Clear the latest checkpoint.
(clear-checkpoint parstate) → new-parstate
This is called when the parser resolves that there is no longer a need to backtrack to the latest checkpoint. This simply removes the latest checkpoint.
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 clear-checkpoint (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'clear-checkpoint)) (declare (ignorable __function__)) (b* ((checkpoints (parstate->checkpoints parstate)) ((unless (consp checkpoints)) (raise "Internal error: no checkpoint to clear.") (parstate-fix parstate)) (new-checkpoints (cdr checkpoints)) (parstate (update-parstate->checkpoints new-checkpoints parstate))) parstate)))
Theorem:
(defthm parstatep-of-clear-checkpoint (implies (parstatep parstate) (b* ((new-parstate (clear-checkpoint parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-clear-checkpoint (b* ((?new-parstate (clear-checkpoint parstate))) (equal (parsize new-parstate) (parsize parstate))) :rule-classes (:rewrite :linear))