Expected expression priorities of the operands of the binary operators.
(binop-expected-priorities op) → (mv left-prio right-prio)
These are straightforwardly based on the grammar rules.
Function:
(defun binop-expected-priorities (op) (declare (xargs :guard (binopp op))) (let ((__function__ 'binop-expected-priorities)) (declare (ignorable __function__)) (binop-case op :mul (mv (expr-priority-mul) (expr-priority-cast)) :div (mv (expr-priority-mul) (expr-priority-cast)) :rem (mv (expr-priority-mul) (expr-priority-cast)) :add (mv (expr-priority-add) (expr-priority-mul)) :sub (mv (expr-priority-add) (expr-priority-mul)) :shl (mv (expr-priority-sh) (expr-priority-add)) :shr (mv (expr-priority-sh) (expr-priority-add)) :lt (mv (expr-priority-rel) (expr-priority-sh)) :gt (mv (expr-priority-rel) (expr-priority-sh)) :le (mv (expr-priority-rel) (expr-priority-sh)) :ge (mv (expr-priority-rel) (expr-priority-sh)) :eq (mv (expr-priority-eq) (expr-priority-rel)) :ne (mv (expr-priority-eq) (expr-priority-rel)) :bitand (mv (expr-priority-and) (expr-priority-eq)) :bitxor (mv (expr-priority-xor) (expr-priority-and)) :bitior (mv (expr-priority-ior) (expr-priority-xor)) :logand (mv (expr-priority-logand) (expr-priority-ior)) :logor (mv (expr-priority-logor) (expr-priority-logand)) :asg (mv (expr-priority-unary) (expr-priority-asg)) :asg-mul (mv (expr-priority-unary) (expr-priority-asg)) :asg-div (mv (expr-priority-unary) (expr-priority-asg)) :asg-rem (mv (expr-priority-unary) (expr-priority-asg)) :asg-add (mv (expr-priority-unary) (expr-priority-asg)) :asg-sub (mv (expr-priority-unary) (expr-priority-asg)) :asg-shl (mv (expr-priority-unary) (expr-priority-asg)) :asg-shr (mv (expr-priority-unary) (expr-priority-asg)) :asg-and (mv (expr-priority-unary) (expr-priority-asg)) :asg-xor (mv (expr-priority-unary) (expr-priority-asg)) :asg-ior (mv (expr-priority-unary) (expr-priority-asg)))))
Theorem:
(defthm expr-priorityp-of-binop-expected-priorities.left-prio (b* (((mv ?left-prio ?right-prio) (binop-expected-priorities op))) (expr-priorityp left-prio)) :rule-classes :rewrite)
Theorem:
(defthm expr-priorityp-of-binop-expected-priorities.right-prio (b* (((mv ?left-prio ?right-prio) (binop-expected-priorities op))) (expr-priorityp right-prio)) :rule-classes :rewrite)
Theorem:
(defthm binop-expected-priorities-of-binop-fix-op (equal (binop-expected-priorities (binop-fix op)) (binop-expected-priorities op)))
Theorem:
(defthm binop-expected-priorities-binop-equiv-congruence-on-op (implies (binop-equiv op op-equiv) (equal (binop-expected-priorities op) (binop-expected-priorities op-equiv))) :rule-classes :congruence)