Clear the latest checkpoint.
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 (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'clear-checkpoint)) (declare (ignorable __function__)) (b* ((checkpoints (parstate->checkpoints pstate)) ((unless checkpoints) (raise "Internal error: no checkpoint to clear.") (parstate-fix pstate)) (new-checkpoints (cdr checkpoints)) (new-pstate (change-parstate pstate :checkpoints new-checkpoints))) new-pstate)))
Theorem:
(defthm parstatep-of-clear-checkpoint (b* ((new-pstate (clear-checkpoint pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-clear-checkpoint (b* ((?new-pstate (clear-checkpoint pstate))) (equal (parsize new-pstate) (parsize pstate))) :rule-classes (:rewrite :linear))