Parse zero or more increment and decrement operators.
(parse-*-increment/decrement parstate) → (mv erp ops new-parstate)
This is used to handle possibly ambiguous cast expressions. We never need the spans of these operators, so this function returns no span.
Function:
(defun parse-*-increment/decrement (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-*-increment/decrement)) (declare (ignorable __function__)) (b* (((reterr) nil parstate) ((erp token & parstate) (read-token parstate)) ((when (token-punctuatorp token "++")) (b* (((erp ops parstate) (parse-*-increment/decrement parstate))) (retok (cons (inc/dec-op-inc) ops) parstate))) ((when (token-punctuatorp token "--")) (b* (((erp ops parstate) (parse-*-increment/decrement parstate))) (retok (cons (inc/dec-op-dec) ops) parstate))) (parstate (if token (unread-token parstate) parstate))) (retok nil parstate))))
Theorem:
(defthm inc/dec-op-listp-of-parse-*-increment/decrement.ops (b* (((mv acl2::?erp ?ops ?new-parstate) (parse-*-increment/decrement parstate))) (inc/dec-op-listp ops)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-*-increment/decrement.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?ops ?new-parstate) (parse-*-increment/decrement parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-*-increment/decrement (b* (((mv acl2::?erp ?ops ?new-parstate) (parse-*-increment/decrement parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)