Check if an optional token may start a unary expression.
(token-unary-expression-start-p token?) → yes/no
Looking at the grammar,
a unary expression may be a postfix expression,
which always starts with (or is) a primary expression,
or it is a compound literal,
which starts with an open parenthesis,
which is already covered by the possible starts of a primary expression.
In addition, a unary expression may start with
a preincrement or predecrement operator,
or a unary operator as defined in the grammar,
or a
We also compare the token against
the GCC extension variants
Function:
(defun token-unary-expression-start-p (token?) (declare (xargs :guard (token-optionp token?))) (let ((__function__ 'token-unary-expression-start-p)) (declare (ignorable __function__)) (or (token-primary-expression-start-p token?) (token-punctuatorp token? "++") (token-punctuatorp token? "--") (token-punctuatorp token? "&") (token-punctuatorp token? "*") (token-punctuatorp token? "+") (token-punctuatorp token? "-") (token-punctuatorp token? "~") (token-punctuatorp token? "!") (token-keywordp token? "sizeof") (token-keywordp token? "_Alignof") (token-keywordp token? "__alignof") (token-keywordp token? "__alignof__"))))
Theorem:
(defthm booleanp-of-token-unary-expression-start-p (b* ((yes/no (token-unary-expression-start-p token?))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm non-nil-when-token-unary-expression-start-p (implies (token-unary-expression-start-p token?) token?) :rule-classes :compound-recognizer)