Priorities of expressions.
(expr->priority expr) → priority
Each expression in the abstract syntax has an associated priority (see expr-priority), straightforwardly according to the grammar.
An ambiguous
Function:
(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-case expr.op :mul (expr-priority-mul) :div (expr-priority-mul) :rem (expr-priority-mul) :add (expr-priority-add) :sub (expr-priority-add) :shl (expr-priority-sh) :shr (expr-priority-sh) :lt (expr-priority-rel) :gt (expr-priority-rel) :le (expr-priority-rel) :ge (expr-priority-rel) :eq (expr-priority-eq) :ne (expr-priority-eq) :bitand (expr-priority-and) :bitxor (expr-priority-xor) :bitior (expr-priority-ior) :logand (expr-priority-logand) :logor (expr-priority-logor) :asg (expr-priority-asg) :asg-mul (expr-priority-asg) :asg-div (expr-priority-asg) :asg-rem (expr-priority-asg) :asg-add (expr-priority-asg) :asg-sub (expr-priority-asg) :asg-shl (expr-priority-asg) :asg-shr (expr-priority-asg) :asg-and (expr-priority-asg) :asg-xor (expr-priority-asg) :asg-ior (expr-priority-asg)) :cond (expr-priority-cond) :comma (expr-priority-expr) :cast/call-ambig (expr-priority-cast) :cast/mul-ambig (expr-priority-mul) :cast/add-ambig (expr-priority-add) :cast/sub-ambig (expr-priority-add) :cast/and-ambig (expr-priority-and) :stmt (expr-priority-primary) :tycompat (expr-priority-primary) :offsetof (expr-priority-primary))))
Theorem:
(defthm expr-priorityp-of-expr->priority (b* ((priority (expr->priority expr))) (expr-priorityp priority)) :rule-classes :rewrite)
Theorem:
(defthm expr->priority-of-expr-fix-expr (equal (expr->priority (expr-fix expr)) (expr->priority expr)))
Theorem:
(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)