		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Binop-expected-priorities

Expected expression priorities of the operands of the binary operators.

Signature
(binop-expected-priorities op) → (mv left-prio right-prio)
Arguments: op — Guard (binopp op).
Returns: left-prio — Type (expr-priorityp left-prio).; right-prio — Type (expr-priorityp right-prio).

These are straightforwardly based on the grammar rules.

Definitions and Theorems

Function: binop-expected-priorities

(defun binop-expected-priorities (op)
  (declare (xargs :guard (binopp op)))
  (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: expr-priorityp-of-binop-expected-priorities.left-prio

(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: expr-priorityp-of-binop-expected-priorities.right-prio

(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: binop-expected-priorities-of-binop-fix-op

(defthm binop-expected-priorities-of-binop-fix-op
  (equal (binop-expected-priorities (binop-fix op))
         (binop-expected-priorities op)))

Theorem: binop-expected-priorities-binop-equiv-congruence-on-op

(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)