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 (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'lex-non-octal-digit)) (declare (ignorable __function__)) (b* (((reterr) 0 (irr-position) (irr-parstate)) ((erp char pos pstate) (read-char pstate)) ((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 pstate))) (lex-non-octal-digit pstate))))
Theorem:
(defthm natp-of-lex-non-octal-digit.char (b* (((mv acl2::?erp common-lisp::?char acl2::?pos ?new-pstate) (lex-non-octal-digit pstate))) (natp char)) :rule-classes :rewrite)
Theorem:
(defthm positionp-of-lex-non-octal-digit.pos (b* (((mv acl2::?erp common-lisp::?char acl2::?pos ?new-pstate) (lex-non-octal-digit pstate))) (positionp pos)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-lex-non-octal-digit.new-pstate (b* (((mv acl2::?erp common-lisp::?char acl2::?pos ?new-pstate) (lex-non-octal-digit pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-lex-non-octal-digit-uncond (b* (((mv acl2::?erp common-lisp::?char acl2::?pos ?new-pstate) (lex-non-octal-digit pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-lex-non-octal-digit-cond (b* (((mv acl2::?erp common-lisp::?char acl2::?pos ?new-pstate) (lex-non-octal-digit pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)