|
|
|---|
|
|
|
|---|
Priority of (binary expressions with) operators.
(binop->priority op) → priority
Function:
(defun binop->priority (op) (declare (xargs :guard (binopp op))) (binop-case 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)))
Theorem:
(defthm expr-priorityp-of-binop->priority (b* ((priority (binop->priority op))) (expr-priorityp priority)) :rule-classes :rewrite)
Theorem:
(defthm binop->priority-of-binop-fix-op (equal (binop->priority (binop-fix op)) (binop->priority op)))
Theorem:
(defthm binop->priority-binop-equiv-congruence-on-op (implies (binop-equiv op op-equiv) (equal (binop->priority op) (binop->priority op-equiv))) :rule-classes :congruence)