(lex-oct-iconst-/-dec-fconst zero-pos parstate) → (mv erp const last-pos new-parstate)
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 parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (positionp zero-pos) (parstatep parstate)))) (let ((__function__ 'lex-oct-iconst-/-dec-fconst)) (declare (ignorable __function__)) (b* (((reterr) (irr-const) (irr-position) parstate) ((erp digits digits-last-pos & parstate) (lex-*-digit zero-pos parstate)) ((erp char pos parstate) (read-char parstate))) (cond ((not char) (cond ((oct-digit-char-listp digits) (retok (const-int (make-iconst :core (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))) parstate)) (t (b* ((parstate (unread-chars (len digits) parstate)) ((erp nonoctdig pos parstate) (lex-non-octal-digit parstate))) (reterr-msg :where (position-to-msg pos) :expected "octal digit" :found (char-to-msg nonoctdig)))))) ((= char (char-code #\.)) (b* (((erp digits2 digits2-last-pos & parstate) (lex-*-digit pos parstate)) ((erp expo? expo-last/next-pos parstate) (lex-dec-expo-if-present parstate)) ((erp fsuffix? suffix-last/next-pos parstate) (lex-fsuffix-if-present parstate)) ((erp parstate) (check-full-ppnumber nil parstate)) (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)) parstate))) ((or (= char (char-code #\e)) (= char (char-code #\E))) (b* ((parstate (unread-char parstate)) ((erp expo expo-last-pos parstate) (lex-dec-expo parstate)) ((erp fsuffix? suffix-last/next-pos parstate) (lex-fsuffix-if-present parstate)) ((erp parstate) (check-full-ppnumber nil parstate))) (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)) parstate))) (t (cond ((oct-digit-char-listp digits) (b* ((parstate (unread-char parstate)) ((erp isuffix? suffix-last/next-pos parstate) (lex-isuffix-if-present parstate)) ((erp parstate) (check-full-ppnumber nil parstate))) (retok (const-int (make-iconst :core (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))) parstate))) (t (b* ((parstate (unread-chars (len digits) parstate)) ((erp nonoctdig pos parstate) (lex-non-octal-digit parstate))) (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-parstate) (lex-oct-iconst-/-dec-fconst zero-pos parstate))) (constp const)) :rule-classes :rewrite)
Theorem:
(defthm positionp-of-lex-oct-iconst-/-dec-fconst.last-pos (b* (((mv acl2::?erp ?const ?last-pos ?new-parstate) (lex-oct-iconst-/-dec-fconst zero-pos parstate))) (positionp last-pos)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-lex-oct-iconst-/-dec-fconst.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?const ?last-pos ?new-parstate) (lex-oct-iconst-/-dec-fconst zero-pos parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-lex-oct-iconst-/-dec-fconst-uncond (b* (((mv acl2::?erp ?const ?last-pos ?new-parstate) (lex-oct-iconst-/-dec-fconst zero-pos parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)