Lex a decimal exponent, if present.
(lex-dec-expo-if-present parstate) → (mv erp expo? last/next-pos new-parstate)
If an exponent is found,
the
If there is no next character, there is no exponent.
If the next character is not
Function:
(defun lex-dec-expo-if-present (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'lex-dec-expo-if-present)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-position) parstate) ((erp char pos parstate) (read-char parstate))) (cond ((not char) (retok nil pos parstate)) ((or (= char (char-code #\e)) (= char (char-code #\E))) (b* ((prefix (if (= char (char-code #\e)) (dec-expo-prefix-locase-e) (dec-expo-prefix-upcase-e))) ((erp sign? sign-pos parstate) (lex-sign-if-present parstate)) (pos-so-far (if sign? sign-pos pos)) ((erp digits last-pos & parstate) (lex-*-digit pos-so-far parstate)) ((unless digits) (b* ((parstate (if sign? (unread-char parstate) parstate)) (parstate (unread-char parstate))) (retok nil pos parstate)))) (retok (make-dec-expo :prefix prefix :sign? sign? :digits digits) last-pos parstate))) (t (b* ((parstate (unread-char parstate))) (retok nil pos parstate)))))))
Theorem:
(defthm dec-expo-optionp-of-lex-dec-expo-if-present.expo? (b* (((mv acl2::?erp ?expo? ?last/next-pos ?new-parstate) (lex-dec-expo-if-present parstate))) (dec-expo-optionp expo?)) :rule-classes :rewrite)
Theorem:
(defthm positionp-of-lex-dec-expo-if-present.last/next-pos (b* (((mv acl2::?erp ?expo? ?last/next-pos ?new-parstate) (lex-dec-expo-if-present parstate))) (positionp last/next-pos)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-lex-dec-expo-if-present.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expo? ?last/next-pos ?new-parstate) (lex-dec-expo-if-present parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-lex-dec-expo-if-present-uncond (b* (((mv acl2::?erp ?expo? ?last/next-pos ?new-parstate) (lex-dec-expo-if-present parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-lex-dec-expo-if-present-cond (b* (((mv acl2::?erp ?expo? ?last/next-pos ?new-parstate) (lex-dec-expo-if-present parstate))) (implies (and (not erp) expo?) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)