Check if an expression is postfix or primary.
According to the grammar definition, postfix expressions include primary expressions; the grammar defines expressions hierarchically. So this test, performed on abstract syntax, is equivalent to testing whether the expression is a postfix one according to the grammar.
Function:
(defun expr-postfix/primary-p (expr) (declare (xargs :guard (exprp expr))) (let ((__function__ 'expr-postfix/primary-p)) (declare (ignorable __function__)) (and (member-eq (expr-kind expr) '(:ident :const :string :paren :gensel :arrsub :funcall :member :memberp :complit :stmt :tycompat :offsetof)) t)))
Theorem:
(defthm booleanp-of-expr-postfix/primary-p (b* ((yes/no (expr-postfix/primary-p expr))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm expr-postfix/primary-p-of-expr-fix-expr (equal (expr-postfix/primary-p (expr-fix expr)) (expr-postfix/primary-p expr)))
Theorem:
(defthm expr-postfix/primary-p-expr-equiv-congruence-on-expr (implies (expr-equiv expr expr-equiv) (equal (expr-postfix/primary-p expr) (expr-postfix/primary-p expr-equiv))) :rule-classes :congruence)