Lex a hexadecimal digit.
(lex-hexadecimal-digit pstate) → (mv erp hexdig pos new-pstate)
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 (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'lex-hexadecimal-digit)) (declare (ignorable __function__)) (b* (((reterr) #\0 (irr-position) (irr-parstate)) ((erp char pos pstate) (read-char pstate)) ((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 pstate))))
Theorem:
(defthm hex-digit-char-p-of-lex-hexadecimal-digit.hexdig (b* (((mv acl2::?erp ?hexdig acl2::?pos ?new-pstate) (lex-hexadecimal-digit pstate))) (hex-digit-char-p hexdig)) :rule-classes :rewrite)
Theorem:
(defthm positionp-of-lex-hexadecimal-digit.pos (b* (((mv acl2::?erp ?hexdig acl2::?pos ?new-pstate) (lex-hexadecimal-digit pstate))) (positionp pos)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-lex-hexadecimal-digit.new-pstate (b* (((mv acl2::?erp ?hexdig acl2::?pos ?new-pstate) (lex-hexadecimal-digit pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-lex-hexadecimal-digit-uncond (b* (((mv acl2::?erp ?hexdig acl2::?pos ?new-pstate) (lex-hexadecimal-digit pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-lex-hexadecimal-digit-cond (b* (((mv acl2::?erp ?hexdig acl2::?pos ?new-pstate) (lex-hexadecimal-digit pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)