		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Expr-postfix/primary-p

Check if an expression is postfix or primary.

Signature
(expr-postfix/primary-p expr) → yes/no
Arguments: expr — Guard (exprp expr).
Returns: yes/no — Type (booleanp yes/no).

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.

Definitions and Theorems

Function: expr-postfix/primary-p

(defun expr-postfix/primary-p (expr)
  (declare (xargs :guard (exprp expr)))
  (and (member-eq (expr-kind expr)
                  '(:ident :const :string
                           :paren :gensel
                           :arrsub :funcall
                           :member :memberp
                           :complit :stmt
                           :tycompat :offsetof
                           :va-arg :extension))
       t))

Theorem: booleanp-of-expr-postfix/primary-p

(defthm booleanp-of-expr-postfix/primary-p
  (b* ((yes/no (expr-postfix/primary-p expr)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: expr-postfix/primary-p-of-expr-fix-expr

(defthm expr-postfix/primary-p-of-expr-fix-expr
  (equal (expr-postfix/primary-p (expr-fix expr))
         (expr-postfix/primary-p expr)))

Theorem: expr-postfix/primary-p-expr-equiv-congruence-on-expr

(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)