Check if an optional token may start the rest of a postfix expression.
(token-postfix-expression-rest-start-p token?) → yes/no
Looking at the grammar, a postfix expression may starts with (or is) a primary expression, followed by a sequence of constructs for array subscripting, function calls, member access (by value or pointer), and postincrement or postdecrement. The other kind of postfix expression is different: it consists of a parenthesized type name followed by an initializer list in curly braces. Here we are only concerned with the first kind of postfix expressions, the ones that start with a primary expression and continue with a sequence of the constructs listed above. This predicate recognizes the tokens that may start one of these constructs, after the primary expression.
Function:
(defun token-postfix-expression-rest-start-p (token?) (declare (xargs :guard (token-optionp token?))) (let ((__function__ 'token-postfix-expression-rest-start-p)) (declare (ignorable __function__)) (or (token-punctuatorp token? "[") (token-punctuatorp token? "(") (token-punctuatorp token? ".") (token-punctuatorp token? "->") (token-punctuatorp token? "++") (token-punctuatorp token? "--"))))
Theorem:
(defthm booleanp-of-token-postfix-expression-rest-start-p (b* ((yes/no (token-postfix-expression-rest-start-p token?))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm non-nil-when-token-postfix-expression-rest-start-p (implies (token-postfix-expression-rest-start-p token?) token?) :rule-classes :compound-recognizer)