Lex zero or more hexadecimal digits, as many as available.
(lex-*-hexadecimal-digit pos-so-far parstate) → (mv erp hexdigs 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 hexadecimal 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 hexadecimal character,
or the input
Function:
(defun lex-*-hexadecimal-digit (pos-so-far parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (positionp pos-so-far) (parstatep parstate)))) (let ((__function__ 'lex-*-hexadecimal-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 (or (and (<= (char-code #\0) char) (<= char (char-code #\9))) (and (<= (char-code #\A) char) (<= char (char-code #\F))) (and (<= (char-code #\a) char) (<= char (char-code #\f))))) (b* ((parstate (unread-char parstate))) (retok nil (position-fix pos-so-far) pos parstate))) (hexdig (code-char char)) ((erp hexdigs last-pos next-pos parstate) (lex-*-hexadecimal-digit pos parstate))) (retok (cons hexdig hexdigs) last-pos next-pos parstate))))
Theorem:
(defthm hex-digit-char-listp-of-lex-*-hexadecimal-digit.hexdigs (b* (((mv acl2::?erp ?hexdigs ?last-pos ?next-pos ?new-parstate) (lex-*-hexadecimal-digit pos-so-far parstate))) (hex-digit-char-listp hexdigs)) :rule-classes :rewrite)
Theorem:
(defthm positionp-of-lex-*-hexadecimal-digit.last-pos (b* (((mv acl2::?erp ?hexdigs ?last-pos ?next-pos ?new-parstate) (lex-*-hexadecimal-digit pos-so-far parstate))) (positionp last-pos)) :rule-classes :rewrite)
Theorem:
(defthm positionp-of-lex-*-hexadecimal-digit.next-pos (b* (((mv acl2::?erp ?hexdigs ?last-pos ?next-pos ?new-parstate) (lex-*-hexadecimal-digit pos-so-far parstate))) (positionp next-pos)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-lex-*-hexadecimal-digit.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?hexdigs ?last-pos ?next-pos ?new-parstate) (lex-*-hexadecimal-digit pos-so-far parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-lex-*-hexadecimal-digit.hexdigs (b* (((mv acl2::?erp ?hexdigs ?last-pos ?next-pos ?new-parstate) (lex-*-hexadecimal-digit pos-so-far parstate))) (true-listp hexdigs)) :rule-classes :type-prescription)
Theorem:
(defthm parsize-of-lex-*-hexadecimal-digit-uncond (b* (((mv acl2::?erp ?hexdigs ?last-pos ?next-pos ?new-parstate) (lex-*-hexadecimal-digit pos-so-far parstate))) (<= (parsize new-parstate) (- (parsize parstate) (len hexdigs)))) :rule-classes :linear)