Lex zero or more (decimal) digits, as many as available.
(lex-*-digit pos-so-far pstate) → (mv erp decdigs last-pos next-pos new-pstate)
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 pstate) (declare (xargs :guard (and (positionp pos-so-far) (parstatep pstate)))) (let ((__function__ 'lex-*-digit)) (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-*-digit pos pstate))) (retok (cons decdig decdigs) last-pos next-pos pstate))))
Theorem:
(defthm dec-digit-char-listp-of-lex-*-digit.decdigs (b* (((mv acl2::?erp ?decdigs ?last-pos ?next-pos ?new-pstate) (lex-*-digit pos-so-far pstate))) (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-pstate) (lex-*-digit pos-so-far pstate))) (positionp last-pos)) :rule-classes :rewrite)
Theorem:
(defthm positionp-of-lex-*-digit.next-pos (b* (((mv acl2::?erp ?decdigs ?last-pos ?next-pos ?new-pstate) (lex-*-digit pos-so-far pstate))) (positionp next-pos)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-lex-*-digit.new-pstate (b* (((mv acl2::?erp ?decdigs ?last-pos ?next-pos ?new-pstate) (lex-*-digit pos-so-far pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-lex-*-digit.decdigs (b* (((mv acl2::?erp ?decdigs ?last-pos ?next-pos ?new-pstate) (lex-*-digit pos-so-far pstate))) (true-listp decdigs)) :rule-classes :type-prescription)
Theorem:
(defthm parsize-of-lex-*-digit-uncond (b* (((mv acl2::?erp ?decdigs ?last-pos ?next-pos ?new-pstate) (lex-*-digit pos-so-far pstate))) (<= (parsize new-pstate) (- (parsize pstate) (len decdigs)))) :rule-classes :linear)