This is called after the initial
We read all the digits that follow the initial
If there is a dot or an
If there is any other character just after the digits, there are two cases. If all the digits read are octal, we may well have an octal constant, so long as the subsequent characters are not part of the preprocessing number, except for possibly an integer suffix. If not all the digits are octal, then it cannot be an octal constant, but it cannot be a decimal constant either, because in the latter case the digits would have to be followed by a dot or an exponent; so it is an error in that case.
Function:
(defun oct-iconst-leading-zeros (octdigs) (declare (xargs :guard (oct-digit-char-listp octdigs))) (let ((__function__ 'oct-iconst-leading-zeros)) (declare (ignorable __function__)) (b* (((when (endp octdigs)) 0) (octdig (car octdigs))) (if (eql octdig #\0) (1+ (oct-iconst-leading-zeros (cdr octdigs))) 0))))
Theorem:
(defthm natp-of-oct-iconst-leading-zeros (b* ((count (oct-iconst-leading-zeros octdigs))) (natp count)) :rule-classes :rewrite)
Function:
(defun lex-oct-iconst-/-dec-fconst (zero-pos pstate) (declare (xargs :guard (and (positionp zero-pos) (parstatep pstate)))) (let ((__function__ 'lex-oct-iconst-/-dec-fconst)) (declare (ignorable __function__)) (b* (((reterr) (irr-const) (irr-position) (irr-parstate)) ((erp digits digits-last-pos & pstate) (lex-*-digit zero-pos pstate)) ((erp char pos pstate) (read-char pstate))) (cond ((not char) (cond ((oct-digit-char-listp digits) (retok (const-int (make-iconst :dec/oct/hex (make-dec/oct/hex-const-oct :leading-zeros (1+ (oct-iconst-leading-zeros digits)) :value (str::oct-digit-chars-value digits)) :suffix? nil)) (cond (digits digits-last-pos) (t (position-fix zero-pos))) pstate)) (t (b* ((pstate (unread-chars (len digits) pstate)) ((erp nonoctdig pos pstate) (lex-non-octal-digit pstate))) (reterr-msg :where (position-to-msg pos) :expected "octal digit" :found (char-to-msg nonoctdig)))))) ((= char (char-code #\.)) (b* (((erp digits2 digits2-last-pos & pstate) (lex-*-digit pos pstate)) ((erp expo? expo-last/next-pos pstate) (lex-dec-expo-if-present pstate)) ((erp fsuffix? suffix-last/next-pos pstate) (lex-fsuffix-if-present pstate)) ((erp pstate) (check-full-ppnumber nil pstate)) (core (cond (digits2 (cond (expo? (make-dec-core-fconst-frac :significand (make-dec-frac-const :before (cons #\0 digits) :after digits2) :expo? expo?)) (t (make-dec-core-fconst-frac :significand (make-dec-frac-const :before (cons #\0 digits) :after digits2) :expo? nil)))) (t (cond (expo? (make-dec-core-fconst-frac :significand (make-dec-frac-const :before (cons #\0 digits) :after nil) :expo? expo?)) (t (make-dec-core-fconst-frac :significand (make-dec-frac-const :before (cons #\0 digits) :after nil) :expo? nil))))))) (retok (const-float (make-fconst-dec :core core :suffix? fsuffix?)) (cond (fsuffix? suffix-last/next-pos) (expo? expo-last/next-pos) (digits2 digits2-last-pos) (t pos)) pstate))) ((or (= char (char-code #\e)) (= char (char-code #\E))) (b* ((pstate (unread-char pstate)) ((erp expo expo-last-pos pstate) (lex-dec-expo pstate)) ((erp fsuffix? suffix-last/next-pos pstate) (lex-fsuffix-if-present pstate)) ((erp pstate) (check-full-ppnumber nil pstate))) (retok (const-float (make-fconst-dec :core (make-dec-core-fconst-int :significand (cons #\0 digits) :expo expo) :suffix? fsuffix?)) (cond (fsuffix? suffix-last/next-pos) (t expo-last-pos)) pstate))) (t (cond ((oct-digit-char-listp digits) (b* ((pstate (unread-char pstate)) ((erp isuffix? suffix-last/next-pos pstate) (lex-isuffix-if-present pstate)) ((erp pstate) (check-full-ppnumber nil pstate))) (retok (const-int (make-iconst :dec/oct/hex (make-dec/oct/hex-const-oct :leading-zeros (1+ (oct-iconst-leading-zeros digits)) :value (str::oct-digit-chars-value digits)) :suffix? isuffix?)) (cond (isuffix? suffix-last/next-pos) (digits digits-last-pos) (t (position-fix zero-pos))) pstate))) (t (b* ((pstate (unread-chars (len digits) pstate)) ((erp nonoctdig pos pstate) (lex-non-octal-digit pstate))) (reterr-msg :where (position-to-msg pos) :expected "octal digit" :found (char-to-msg nonoctdig))))))))))
Theorem:
(defthm constp-of-lex-oct-iconst-/-dec-fconst.const (b* (((mv acl2::?erp ?const ?last-pos ?new-pstate) (lex-oct-iconst-/-dec-fconst zero-pos pstate))) (constp const)) :rule-classes :rewrite)
Theorem:
(defthm positionp-of-lex-oct-iconst-/-dec-fconst.last-pos (b* (((mv acl2::?erp ?const ?last-pos ?new-pstate) (lex-oct-iconst-/-dec-fconst zero-pos pstate))) (positionp last-pos)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-lex-oct-iconst-/-dec-fconst.new-pstate (b* (((mv acl2::?erp ?const ?last-pos ?new-pstate) (lex-oct-iconst-/-dec-fconst zero-pos pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-lex-oct-iconst-/-dec-fconst-uncond (b* (((mv acl2::?erp ?const ?last-pos ?new-pstate) (lex-oct-iconst-/-dec-fconst zero-pos pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)