Lex zero or more decimal digits, as many as available.
(lex-dec-digits pos-so-far pstate) → (mv erp decdigs last-pos next-pos new-pstate)
The
We read the next character.
If it does not exist, we return.
If it exists but is not a decimal digit,
we put the character back and return.
Otherwise, we recursively read zero or more,
and we put the one just read in front.
We always return the position of the last decimal character,
or the input
Function:
(defun lex-dec-digits (pos-so-far pstate) (declare (xargs :guard (and (positionp pos-so-far) (parstatep pstate)))) (let ((__function__ 'lex-dec-digits)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-position) (irr-position) (irr-parstate)) ((erp char pos pstate) (read-char pstate)) ((when (not char)) (retok nil (position-fix pos-so-far) pos pstate)) ((unless (and (<= (char-code #\0) char) (<= char (char-code #\9)))) (b* ((pstate (unread-char pstate))) (retok nil (position-fix pos-so-far) pos pstate))) (decdig (code-char char)) ((erp decdigs last-pos next-pos pstate) (lex-dec-digits pos pstate))) (retok (cons decdig decdigs) last-pos next-pos pstate))))
Theorem:
(defthm dec-digit-char-listp-of-lex-dec-digits.decdigs (b* (((mv acl2::?erp ?decdigs ?last-pos ?next-pos ?new-pstate) (lex-dec-digits pos-so-far pstate))) (dec-digit-char-listp decdigs)) :rule-classes :rewrite)
Theorem:
(defthm positionp-of-lex-dec-digits.last-pos (b* (((mv acl2::?erp ?decdigs ?last-pos ?next-pos ?new-pstate) (lex-dec-digits pos-so-far pstate))) (positionp last-pos)) :rule-classes :rewrite)
Theorem:
(defthm positionp-of-lex-dec-digits.next-pos (b* (((mv acl2::?erp ?decdigs ?last-pos ?next-pos ?new-pstate) (lex-dec-digits pos-so-far pstate))) (positionp next-pos)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-lex-dec-digits.new-pstate (b* (((mv acl2::?erp ?decdigs ?last-pos ?next-pos ?new-pstate) (lex-dec-digits pos-so-far pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-lex-dec-digits.decdigs (b* (((mv acl2::?erp ?decdigs ?last-pos ?next-pos ?new-pstate) (lex-dec-digits pos-so-far pstate))) (true-listp decdigs)) :rule-classes :type-prescription)
Theorem:
(defthm parsize-of-lex-dec-digits-uncond (b* (((mv acl2::?erp ?decdigs ?last-pos ?next-pos ?new-pstate) (lex-dec-digits pos-so-far pstate))) (<= (parsize new-pstate) (- (parsize pstate) (len decdigs)))) :rule-classes :linear)