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