Lex a non-octal digit.
This is only called by lex-oct-iconst-/-dec-fconst, for the purpose of returning an informative error message when a sequence of digits is read that are not all octal, but the sequence cannot form a decimal constant. The caller first unreads all those digits, and then calls this function to find the (first) offeding digit. So we expect that a non-octal digit will be found, and it is thus an internal error if it is not found (which should never happen).
Function:
(defun lex-non-octal-digit (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'lex-non-octal-digit)) (declare (ignorable __function__)) (b* (((reterr) 0 (irr-position) parstate) ((erp char pos parstate) (read-char parstate)) ((unless char) (raise "Internal error: no non-octal digit found.") (reterr t)) ((unless (and (<= (char-code #\0) char) (<= char (char-code #\7)))) (retok char pos parstate))) (lex-non-octal-digit parstate))))
Theorem:
(defthm natp-of-lex-non-octal-digit.char (b* (((mv acl2::?erp common-lisp::?char acl2::?pos ?new-parstate) (lex-non-octal-digit parstate))) (natp char)) :rule-classes :rewrite)
Theorem:
(defthm positionp-of-lex-non-octal-digit.pos (b* (((mv acl2::?erp common-lisp::?char acl2::?pos ?new-parstate) (lex-non-octal-digit parstate))) (positionp pos)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-lex-non-octal-digit.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp common-lisp::?char acl2::?pos ?new-parstate) (lex-non-octal-digit parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-lex-non-octal-digit-uncond (b* (((mv acl2::?erp common-lisp::?char acl2::?pos ?new-parstate) (lex-non-octal-digit parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-lex-non-octal-digit-cond (b* (((mv acl2::?erp common-lisp::?char acl2::?pos ?new-parstate) (lex-non-octal-digit parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)