Size of the parsing state.
This is used as the measure for termination of the parsing functions. The size is measured as the sum of the lists of bytes, characters, and tokens that can be read.
As explained in parstate, this is cached for efficiency. We use an mbe to just return the value in execution.
Function:
(defun parsize (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parsize)) (declare (ignorable __function__)) (mbe :logic (+ (len (parstate->bytes pstate)) (len (parstate->chars-unread pstate)) (len (parstate->tokens-unread pstate))) :exec (parstate->size pstate))))
Theorem:
(defthm natp-of-parsize (b* ((size (parsize pstate))) (natp size)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parstate-fix (equal (parsize (parstate-fix pstate)) (parsize pstate)))