Check if an optional token may start a primary expression.
(token-primary-expression-start-p token?) → yes/no
A primary expression is
an identifier (which is a token),
or a constant (which is a token),
or a string literal (which is a token),
or a parenthesizes expression (which starts with a certain punctuator),
or a generic selection (which starts a certain keyword),
or a call of the GCC built-in function
Function:
(defun token-primary-expression-start-p (token?) (declare (xargs :guard (token-optionp token?))) (let ((__function__ 'token-primary-expression-start-p)) (declare (ignorable __function__)) (and token? (or (token-case token? :ident) (token-case token? :const) (token-case token? :string) (token-punctuatorp token? "(") (token-keywordp token? "_Generic") (token-keywordp token? "__builtin_offsetof") (token-keywordp token? "__builtin_types_compatible_p")))))
Theorem:
(defthm booleanp-of-token-primary-expression-start-p (b* ((yes/no (token-primary-expression-start-p token?))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm non-nil-when-token-primary-expression-start-p (implies (token-primary-expression-start-p token?) token?) :rule-classes :compound-recognizer)