		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Expr->priority

Priorities of expressions.

Signature
(expr->priority expr) → priority
Arguments: expr — Guard (exprp expr).
Returns: priority — Type (expr-priorityp priority).

Each expression in the abstract syntax has an associated priority (see expr-priority), straightforwardly according to the grammar.

An ambiguous sizeof has the same priority as an unambiguous one. An ambiguous _Alignof (and keyword variants) has the same priority as an unambiguous one. An ambiguous cast/call expression is given the higher priority of the two possibilities, i.e. the priority of a postfix expression. Ambiguous cast/binary expressions are given the higher priority of the two possibilities, i.e. the priority of a cast expression.

Definitions and Theorems

Function: expr->priority

(defun expr->priority (expr)
  (declare (xargs :guard (exprp expr)))
  (expr-case expr
             :ident (expr-priority-primary)
             :const (expr-priority-primary)
             :string (expr-priority-primary)
             :paren (expr-priority-primary)
             :gensel (expr-priority-primary)
             :arrsub (expr-priority-postfix)
             :funcall (expr-priority-postfix)
             :member (expr-priority-postfix)
             :memberp (expr-priority-postfix)
             :complit (expr-priority-postfix)
             :unary (expr-priority-unary)
             :label-addr (expr-priority-unary)
             :sizeof (expr-priority-unary)
             :sizeof-ambig (expr-priority-unary)
             :alignof (expr-priority-unary)
             :alignof-ambig (expr-priority-unary)
             :cast (expr-priority-cast)
             :binary (binop->priority expr.op)
             :cond (expr-priority-cond)
             :comma (expr-priority-expr)
             :cast/call-ambig (expr-priority-postfix)
             :cast/mul-ambig (expr-priority-cast)
             :cast/add-ambig (expr-priority-cast)
             :cast/sub-ambig (expr-priority-cast)
             :cast/and-ambig (expr-priority-cast)
             :cast/logand-ambig (expr-priority-cast)
             :stmt (expr-priority-primary)
             :tycompat (expr-priority-primary)
             :offsetof (expr-priority-primary)
             :va-arg (expr-priority-primary)
             :extension (expr-priority-primary)))

Theorem: expr-priorityp-of-expr->priority

(defthm expr-priorityp-of-expr->priority
  (b* ((priority (expr->priority expr)))
    (expr-priorityp priority))
  :rule-classes :rewrite)

Theorem: expr->priority-of-expr-fix-expr

(defthm expr->priority-of-expr-fix-expr
  (equal (expr->priority (expr-fix expr))
         (expr->priority expr)))

Theorem: expr->priority-expr-equiv-congruence-on-expr

(defthm expr->priority-expr-equiv-congruence-on-expr
  (implies (expr-equiv expr expr-equiv)
           (equal (expr->priority expr)
                  (expr->priority expr-equiv)))
  :rule-classes :congruence)