Lex a hexadecimal digit.
(lex-hexadecimal-digit parstate) → (mv erp hexdig pos new-parstate)
This is called when we expect a hexadecimal digit: if the character is not a hexadecimal digit, it is an error. If the next character is present and is a hexadecimal digit, we return the corresponding ACL2 character, along with its position in the file.
Function:
(defun lex-hexadecimal-digit (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'lex-hexadecimal-digit)) (declare (ignorable __function__)) (b* (((reterr) #\0 (irr-position) parstate) ((erp char pos parstate) (read-char parstate)) ((when (not char)) (reterr-msg :where (position-to-msg pos) :expected "a hexadecimal digit" :found (char-to-msg char))) ((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))))) (reterr-msg :where (position-to-msg pos) :expected "a hexadecimal digit" :found (char-to-msg char)))) (retok (code-char char) pos parstate))))
Theorem:
(defthm hex-digit-char-p-of-lex-hexadecimal-digit.hexdig (b* (((mv acl2::?erp ?hexdig acl2::?pos ?new-parstate) (lex-hexadecimal-digit parstate))) (hex-digit-char-p hexdig)) :rule-classes :rewrite)
Theorem:
(defthm positionp-of-lex-hexadecimal-digit.pos (b* (((mv acl2::?erp ?hexdig acl2::?pos ?new-parstate) (lex-hexadecimal-digit parstate))) (positionp pos)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-lex-hexadecimal-digit.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?hexdig acl2::?pos ?new-parstate) (lex-hexadecimal-digit parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-lex-hexadecimal-digit-uncond (b* (((mv acl2::?erp ?hexdig acl2::?pos ?new-parstate) (lex-hexadecimal-digit parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-lex-hexadecimal-digit-cond (b* (((mv acl2::?erp ?hexdig acl2::?pos ?new-parstate) (lex-hexadecimal-digit parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)