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.
Function:
(defun parsize (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parsize)) (declare (ignorable __function__)) (+ (len (parstate->bytes pstate)) (len (parstate->chars-unread pstate)) (len (parstate->tokens-unread 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)))