Record a checkpoint for possible backtracking.
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 (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'record-checkpoint)) (declare (ignorable __function__)) (b* ((tokens-read-len (parstate->tokens-read-len pstate)) (checkpoints (parstate->checkpoints pstate)) (new-checkpoints (cons tokens-read-len checkpoints)) (new-pstate (change-parstate pstate :checkpoints new-checkpoints))) new-pstate)))
Theorem:
(defthm parstatep-of-record-checkpoint (b* ((new-pstate (record-checkpoint pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-record-checkpoint (b* ((?new-pstate (record-checkpoint pstate))) (equal (parsize new-pstate) (parsize pstate))) :rule-classes (:rewrite :linear))