Lex a sign, if present.
(lex-sign-if-present pstate) → (mv erp sign? last/next-pos new-pstate)
If a sign is found, the
If there is no next character, there is no sign. Otherwise, we read the next character, and return a sign if appropriate, otherwise no sign and we put back the character.
Function:
(defun lex-sign-if-present (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'lex-sign-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 #\+)) (retok (sign-plus) pos pstate)) ((= char (char-code #\-)) (retok (sign-minus) pos pstate)) (t (b* ((pstate (unread-char pstate))) (retok nil pos pstate)))))))
Theorem:
(defthm sign-optionp-of-lex-sign-if-present.sign? (b* (((mv acl2::?erp ?sign? ?last/next-pos ?new-pstate) (lex-sign-if-present pstate))) (sign-optionp sign?)) :rule-classes :rewrite)
Theorem:
(defthm positionp-of-lex-sign-if-present.last/next-pos (b* (((mv acl2::?erp ?sign? ?last/next-pos ?new-pstate) (lex-sign-if-present pstate))) (positionp last/next-pos)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-lex-sign-if-present.new-pstate (b* (((mv acl2::?erp ?sign? ?last/next-pos ?new-pstate) (lex-sign-if-present pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-lex-sign-if-present-ucond (b* (((mv acl2::?erp ?sign? ?last/next-pos ?new-pstate) (lex-sign-if-present pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-lex-sign-if-present-cond (b* (((mv acl2::?erp ?sign? ?last/next-pos ?new-pstate) (lex-sign-if-present pstate))) (implies (and (not erp) sign?) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)