Lex a floating suffix, if present.
(lex-fsuffix-if-present pstate) → (mv erp fsuffix? last/next-pos new-pstate)
If a suffix is found, the
If there is no next character, there is no suffix. Otherwise, there are four possibilities for suffixes. If the next character is not part of any suffix, we unread the character and return no suffix.
Function:
(defun lex-fsuffix-if-present (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'lex-fsuffix-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 #\f)) (retok (fsuffix-locase-f) pos pstate)) ((= char (char-code #\F)) (retok (fsuffix-upcase-f) pos pstate)) ((= char (char-code #\l)) (retok (fsuffix-locase-l) pos pstate)) ((= char (char-code #\L)) (retok (fsuffix-upcase-l) pos pstate)) (t (b* ((pstate (unread-char pstate))) (retok nil pos pstate)))))))
Theorem:
(defthm fsuffix-optionp-of-lex-fsuffix-if-present.fsuffix? (b* (((mv acl2::?erp ?fsuffix? ?last/next-pos ?new-pstate) (lex-fsuffix-if-present pstate))) (fsuffix-optionp fsuffix?)) :rule-classes :rewrite)
Theorem:
(defthm positionp-of-lex-fsuffix-if-present.last/next-pos (b* (((mv acl2::?erp ?fsuffix? ?last/next-pos ?new-pstate) (lex-fsuffix-if-present pstate))) (positionp last/next-pos)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-lex-fsuffix-if-present.new-pstate (b* (((mv acl2::?erp ?fsuffix? ?last/next-pos ?new-pstate) (lex-fsuffix-if-present pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-lex-fsuffix-if-present-uncond (b* (((mv acl2::?erp ?fsuffix? ?last/next-pos ?new-pstate) (lex-fsuffix-if-present pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-lex-fsuffix-if-present-cond (b* (((mv acl2::?erp ?fsuffix? ?last/next-pos ?new-pstate) (lex-fsuffix-if-present pstate))) (implies (and (not erp) fsuffix?) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)