Record a checkpoint for possible backtracking.
(record-checkpoint parstate) → new-parstate
As explained in parstate, we add (by consing) to the list of checkpoints the current length of the list of tokens read so far.
Function:
(defun record-checkpoint (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'record-checkpoint)) (declare (ignorable __function__)) (b* ((tokens-read-len (parstate->tokens-read-len parstate)) (checkpoints (parstate->checkpoints parstate)) (new-checkpoints (cons tokens-read-len checkpoints)) (parstate (update-parstate->checkpoints new-checkpoints parstate))) parstate)))
Theorem:
(defthm parstatep-of-record-checkpoint (implies (parstatep parstate) (b* ((new-parstate (record-checkpoint parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-record-checkpoint (b* ((?new-parstate (record-checkpoint parstate))) (equal (parsize new-parstate) (parsize parstate))) :rule-classes (:rewrite :linear))