Lex an integer suffix, if present.
(lex-isuffix-if-present pstate) → (mv erp isuffix? last/next-pos new-pstate)
If a suffix is found,
the
We read the next character. If there is no next character, there is no integer suffix.
If the next character is
If the next character is
This code turned out to be verbose.
We could shorten it by merging the treatment of
lowercase
Function:
(defun lex-isuffix-if-present (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'lex-isuffix-if-present)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-position) (irr-parstate)) ((erp char pos pstate) (read-char pstate))) (cond ((not char) (retok nil pos pstate)) ((= char (char-code #\l)) (b* (((erp char2 pos2 pstate) (read-char pstate))) (cond ((not char2) (retok (isuffix-l (lsuffix-locase-l)) pos pstate)) ((= char2 (char-code #\l)) (b* (((erp char3 pos3 pstate) (read-char pstate))) (cond ((not char3) (retok (isuffix-l (lsuffix-locase-ll)) pos2 pstate)) ((= char3 (char-code #\u)) (retok (make-isuffix-lu :length (lsuffix-locase-ll) :unsigned (usuffix-locase-u)) pos3 pstate)) ((= char3 (char-code #\U)) (retok (make-isuffix-lu :length (lsuffix-locase-ll) :unsigned (usuffix-upcase-u)) pos3 pstate)) (t (b* ((pstate (unread-char pstate))) (retok (isuffix-l (lsuffix-locase-ll)) pos2 pstate)))))) ((= char2 (char-code #\u)) (retok (make-isuffix-lu :length (lsuffix-locase-l) :unsigned (usuffix-locase-u)) pos2 pstate)) ((= char2 (char-code #\U)) (retok (make-isuffix-lu :length (lsuffix-locase-l) :unsigned (usuffix-upcase-u)) pos2 pstate)) (t (b* ((pstate (unread-char pstate))) (retok (isuffix-l (lsuffix-locase-l)) pos pstate)))))) ((= char (char-code #\L)) (b* (((erp char2 pos2 pstate) (read-char pstate))) (cond ((not char2) (retok (isuffix-l (lsuffix-upcase-l)) pos pstate)) ((= char2 (char-code #\L)) (b* (((erp char3 pos3 pstate) (read-char pstate))) (cond ((not char3) (retok (isuffix-l (lsuffix-upcase-ll)) pos2 pstate)) ((= char3 (char-code #\u)) (retok (make-isuffix-lu :length (lsuffix-upcase-ll) :unsigned (usuffix-locase-u)) pos3 pstate)) ((= char3 (char-code #\U)) (retok (make-isuffix-lu :length (lsuffix-upcase-ll) :unsigned (usuffix-upcase-u)) pos3 pstate)) (t (b* ((pstate (unread-char pstate))) (retok (isuffix-l (lsuffix-upcase-ll)) pos2 pstate)))))) ((= char2 (char-code #\u)) (retok (make-isuffix-lu :length (lsuffix-upcase-l) :unsigned (usuffix-locase-u)) pos2 pstate)) ((= char2 (char-code #\U)) (retok (make-isuffix-lu :length (lsuffix-upcase-l) :unsigned (usuffix-upcase-u)) pos2 pstate)) (t (b* ((pstate (unread-char pstate))) (retok (isuffix-l (lsuffix-upcase-l)) pos pstate)))))) ((= char (char-code #\u)) (b* (((erp char2 pos2 pstate) (read-char pstate))) (cond ((not char2) (retok (isuffix-u (usuffix-locase-u)) pos pstate)) ((= char2 (char-code #\l)) (b* (((erp char3 pos3 pstate) (read-char pstate))) (cond ((not char3) (retok (make-isuffix-ul :unsigned (usuffix-locase-u) :length (lsuffix-locase-l)) pos2 pstate)) ((= char3 (char-code #\l)) (retok (make-isuffix-ul :unsigned (usuffix-locase-u) :length (lsuffix-locase-ll)) pos3 pstate)) (t (b* ((pstate (unread-char pstate))) (retok (make-isuffix-ul :unsigned (usuffix-locase-u) :length (lsuffix-locase-l)) pos2 pstate)))))) ((= char2 (char-code #\L)) (b* (((erp char3 pos3 pstate) (read-char pstate))) (cond ((not char3) (retok (make-isuffix-ul :unsigned (usuffix-locase-u) :length (lsuffix-upcase-l)) pos2 pstate)) ((= char3 (char-code #\L)) (retok (make-isuffix-ul :unsigned (usuffix-locase-u) :length (lsuffix-upcase-ll)) pos3 pstate)) (t (b* ((pstate (unread-char pstate))) (retok (make-isuffix-ul :unsigned (usuffix-locase-u) :length (lsuffix-upcase-l)) pos2 pstate)))))) (t (b* ((pstate (unread-char pstate))) (retok (isuffix-u (usuffix-locase-u)) pos pstate)))))) ((= char (char-code #\U)) (b* (((erp char2 pos2 pstate) (read-char pstate))) (cond ((not char2) (retok (isuffix-u (usuffix-upcase-u)) pos pstate)) ((= char2 (char-code #\l)) (b* (((erp char3 pos3 pstate) (read-char pstate))) (cond ((not char3) (retok (make-isuffix-ul :unsigned (usuffix-upcase-u) :length (lsuffix-locase-l)) pos2 pstate)) ((= char3 (char-code #\l)) (retok (make-isuffix-ul :unsigned (usuffix-upcase-u) :length (lsuffix-locase-ll)) pos3 pstate)) (t (b* ((pstate (unread-char pstate))) (retok (make-isuffix-ul :unsigned (usuffix-upcase-u) :length (lsuffix-locase-l)) pos2 pstate)))))) ((= char2 (char-code #\L)) (b* (((erp char3 pos3 pstate) (read-char pstate))) (cond ((not char3) (retok (make-isuffix-ul :unsigned (usuffix-upcase-u) :length (lsuffix-upcase-l)) pos2 pstate)) ((= char3 (char-code #\L)) (retok (make-isuffix-ul :unsigned (usuffix-upcase-u) :length (lsuffix-upcase-ll)) pos3 pstate)) (t (b* ((pstate (unread-char pstate))) (retok (make-isuffix-ul :unsigned (usuffix-upcase-u) :length (lsuffix-upcase-l)) pos2 pstate)))))) (t (b* ((pstate (unread-char pstate))) (retok (isuffix-u (usuffix-upcase-u)) pos pstate)))))) (t (b* ((pstate (unread-char pstate))) (retok nil pos pstate)))))))
Theorem:
(defthm isuffix-optionp-of-lex-isuffix-if-present.isuffix? (b* (((mv acl2::?erp ?isuffix? ?last/next-pos ?new-pstate) (lex-isuffix-if-present pstate))) (isuffix-optionp isuffix?)) :rule-classes :rewrite)
Theorem:
(defthm positionp-of-lex-isuffix-if-present.last/next-pos (b* (((mv acl2::?erp ?isuffix? ?last/next-pos ?new-pstate) (lex-isuffix-if-present pstate))) (positionp last/next-pos)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-lex-isuffix-if-present.new-pstate (b* (((mv acl2::?erp ?isuffix? ?last/next-pos ?new-pstate) (lex-isuffix-if-present pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-lex-isuffix-if-present-uncond (b* (((mv acl2::?erp ?isuffix? ?last/next-pos ?new-pstate) (lex-isuffix-if-present pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-lex-isuffix-if-present-cond (b* (((mv acl2::?erp ?isuffix? ?last/next-pos ?new-pstate) (lex-isuffix-if-present pstate))) (implies (and (not erp) isuffix?) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)