Lex a decimal integer or floating constant.
(lex-dec-iconst/fconst first-digit first-pos pstate) → (mv erp const last-pos new-pstate)
This is called when we expect a decimal constant,
after reading the first digit, when that digit is not
First we read as many additional decimal digits as possible, of which there may be none. Then we attempt to read the next character, and we do different things based on that.
If there is no character after the digits, we have an integer decimal constant.
If the next character is a dot, then this must be a decimal floating constant. We read as many digits as possible after the dot; there may no other digits. Then we attempt to read a decimal exponent, if any. Then a floating suffix, if any. Finally, if check-full-ppnumber succeeds (see the documentation of that function for details), we return the appropriate constant.
If the next character is
Otherwise, this must be a decimal integer constant, if it is a valid constant at all. We put back the character and read an integer suffix if present. If check-full-ppnumber passes, we return the appropriate integer constant.
Function:
(defun lex-dec-iconst/fconst (first-digit first-pos pstate) (declare (xargs :guard (and (dec-digit-char-p first-digit) (positionp first-pos) (parstatep pstate)))) (declare (xargs :guard (not (equal first-digit #\0)))) (let ((__function__ 'lex-dec-iconst/fconst)) (declare (ignorable __function__)) (b* (((reterr) (irr-const) (irr-position) (irr-parstate)) ((erp decdigs decdigs-last-pos & pstate) (lex-*-digit first-pos pstate)) ((erp char pos pstate) (read-char pstate))) (cond ((not char) (retok (const-int (make-iconst :core (make-dec/oct/hex-const-dec :value (str::dec-digit-chars-value (cons first-digit decdigs))) :suffix? nil)) (cond (decdigs decdigs-last-pos) (t (position-fix first-pos))) pstate)) ((= char (char-code #\.)) (b* (((erp decdigs2 decdigs2-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 (if decdigs2 (if expo? (make-dec-core-fconst-frac :significand (make-dec-frac-const :before (cons first-digit decdigs) :after decdigs2) :expo? expo?) (make-dec-core-fconst-frac :significand (make-dec-frac-const :before (cons first-digit decdigs) :after decdigs2) :expo? nil)) (if expo? (make-dec-core-fconst-frac :significand (make-dec-frac-const :before (cons first-digit decdigs) :after nil) :expo? expo?) (make-dec-core-fconst-frac :significand (make-dec-frac-const :before (cons first-digit decdigs) :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) (decdigs2 decdigs2-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 first-digit decdigs) :expo expo) :suffix? fsuffix?)) (cond (fsuffix? suffix-last/next-pos) (t expo-last-pos)) pstate))) (t (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 :core (make-dec/oct/hex-const-dec :value (str::dec-digit-chars-value (cons first-digit decdigs))) :suffix? isuffix?)) (cond (isuffix? suffix-last/next-pos) (decdigs decdigs-last-pos) (t (position-fix first-pos))) pstate)))))))
Theorem:
(defthm constp-of-lex-dec-iconst/fconst.const (b* (((mv acl2::?erp ?const ?last-pos ?new-pstate) (lex-dec-iconst/fconst first-digit first-pos pstate))) (constp const)) :rule-classes :rewrite)
Theorem:
(defthm positionp-of-lex-dec-iconst/fconst.last-pos (b* (((mv acl2::?erp ?const ?last-pos ?new-pstate) (lex-dec-iconst/fconst first-digit first-pos pstate))) (positionp last-pos)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-lex-dec-iconst/fconst.new-pstate (b* (((mv acl2::?erp ?const ?last-pos ?new-pstate) (lex-dec-iconst/fconst first-digit first-pos pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-lex-dec-iconst/fconst-uncond (b* (((mv acl2::?erp ?const ?last-pos ?new-pstate) (lex-dec-iconst/fconst first-digit first-pos pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)