Lex an integer or floating constant.
(lex-iconst/fconst first-digit first-pos pstate) → (mv erp const last-pos new-pstate)
This is called when we expect an integer or floating constant, after reading the first (decimal) digit of the constant. The first digit and its position are passed to this function.
If the first digit is a
If instead the first digit is
Function:
(defun lex-iconst/fconst (first-digit first-pos pstate) (declare (xargs :guard (and (dec-digit-char-p first-digit) (positionp first-pos) (parstatep pstate)))) (let ((__function__ 'lex-iconst/fconst)) (declare (ignorable __function__)) (b* (((reterr) (irr-const) (irr-position) (irr-parstate))) (cond ((eql first-digit #\0) (b* (((erp char pos pstate) (read-char pstate))) (cond ((not char) (retok (const-int (make-iconst :core (make-dec/oct/hex-const-oct :leading-zeros 1 :value 0) :suffix? nil)) (position-fix first-pos) pstate)) ((or (= char (char-code #\x)) (= char (char-code #\X))) (b* ((hprefix (if (= char (char-code #\x)) (hprefix-locase-0x) (hprefix-upcase-0x)))) (lex-hex-iconst/fconst hprefix pos pstate))) (t (b* ((pstate (unread-char pstate))) (lex-oct-iconst-/-dec-fconst first-pos pstate)))))) (t (lex-dec-iconst/fconst first-digit first-pos pstate))))))
Theorem:
(defthm constp-of-lex-iconst/fconst.const (b* (((mv acl2::?erp ?const ?last-pos ?new-pstate) (lex-iconst/fconst first-digit first-pos pstate))) (constp const)) :rule-classes :rewrite)
Theorem:
(defthm positionp-of-lex-iconst/fconst.last-pos (b* (((mv acl2::?erp ?const ?last-pos ?new-pstate) (lex-iconst/fconst first-digit first-pos pstate))) (positionp last-pos)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-lex-iconst/fconst.new-pstate (b* (((mv acl2::?erp ?const ?last-pos ?new-pstate) (lex-iconst/fconst first-digit first-pos pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-lex-iconst/fconst-uncond (b* (((mv acl2::?erp ?const ?last-pos ?new-pstate) (lex-iconst/fconst first-digit first-pos pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)