Lex a decimal exponent.
This is called when we expect an exponent.
We try to read a
Function:
(defun lex-dec-expo (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'lex-dec-expo)) (declare (ignorable __function__)) (b* (((reterr) (irr-dec-expo) (irr-position) (irr-parstate)) ((erp char pos pstate) (read-char pstate))) (cond ((not char) (reterr-msg :where (position-to-msg pos) :expected "a character in {e, E}" :found (char-to-msg char))) ((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-last-pos pstate) (lex-sign-if-present pstate)) ((erp digits digits-last-pos digits-next-pos pstate) (lex-*-digit sign-last-pos pstate)) ((unless digits) (reterr-msg :where (position-to-msg digits-next-pos) :expected "one or more digits" :found "none"))) (retok (make-dec-expo :prefix prefix :sign? sign? :digits digits) digits-last-pos pstate))) (t (reterr-msg :where (position-to-msg pos) :expected "a character in {e, E}" :found (char-to-msg char)))))))
Theorem:
(defthm dec-expop-of-lex-dec-expo.expo (b* (((mv acl2::?erp ?expo ?last-pos ?new-pstate) (lex-dec-expo pstate))) (dec-expop expo)) :rule-classes :rewrite)
Theorem:
(defthm positionp-of-lex-dec-expo.last-pos (b* (((mv acl2::?erp ?expo ?last-pos ?new-pstate) (lex-dec-expo pstate))) (positionp last-pos)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-lex-dec-expo.new-pstate (b* (((mv acl2::?erp ?expo ?last-pos ?new-pstate) (lex-dec-expo pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-lex-dec-expo-uncond (b* (((mv acl2::?erp ?expo ?last-pos ?new-pstate) (lex-dec-expo pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-lex-dec-expo-cond (b* (((mv acl2::?erp ?expo ?last-pos ?new-pstate) (lex-dec-expo pstate))) (implies (and (not erp) expo?) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)