		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 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)))
  (let ((__function__ 'expr->priority))
    (declare (ignorable __function__))
    (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)
               :sizeof (expr-priority-unary)
               :sizeof-ambig (expr-priority-unary)
               :alignof (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)
               :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)