Parse zero or more increment and decrement operators.
(parse-*-increment/decrement pstate) → (mv erp ops new-pstate)
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 (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-*-increment/decrement)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-parstate)) ((erp token & pstate) (read-token pstate)) ((when (equal token (token-punctuator "++"))) (b* (((erp ops pstate) (parse-*-increment/decrement pstate))) (retok (cons (inc/dec-op-inc) ops) pstate))) ((when (equal token (token-punctuator "--"))) (b* (((erp ops pstate) (parse-*-increment/decrement pstate))) (retok (cons (inc/dec-op-dec) ops) pstate))) (pstate (if token (unread-token pstate) pstate))) (retok nil pstate))))
Theorem:
(defthm inc/dec-op-listp-of-parse-*-increment/decrement.ops (b* (((mv acl2::?erp ?ops ?new-pstate) (parse-*-increment/decrement pstate))) (inc/dec-op-listp ops)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-*-increment/decrement.new-pstate (b* (((mv acl2::?erp ?ops ?new-pstate) (parse-*-increment/decrement pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-*-increment/decrement (b* (((mv acl2::?erp ?ops ?new-pstate) (parse-*-increment/decrement pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)