		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Binop-expected-grades

Expression grades of the operands of the binary operators.

Signature
(binop-expected-grades op) → (mv left-grade right-grade)
Arguments: op — Guard (binopp op).
Returns: left-grade — Type (expr-gradep left-grade).; right-grade — Type (expr-gradep right-grade).

See pprint-expression-algorithm for background.

These are based on the grammar rules.

Definitions and Theorems

Function: binop-expected-grades

(defun binop-expected-grades (op)
  (declare (xargs :guard (binopp op)))
  (let ((__function__ 'binop-expected-grades))
    (declare (ignorable __function__))
    (binop-case op
                :pow (mv (expr-grade-unary)
                         (expr-grade-exponential))
                :mul (mv (expr-grade-multiplicative)
                         (expr-grade-exponential))
                :div (mv (expr-grade-multiplicative)
                         (expr-grade-exponential))
                :rem (mv (expr-grade-multiplicative)
                         (expr-grade-exponential))
                :add (mv (expr-grade-additive)
                         (expr-grade-multiplicative))
                :sub (mv (expr-grade-additive)
                         (expr-grade-multiplicative))
                :shl (mv (expr-grade-shift)
                         (expr-grade-additive))
                :shr (mv (expr-grade-shift)
                         (expr-grade-additive))
                :bitand (mv (expr-grade-bitwise-and)
                            (expr-grade-shift))
                :bitior (mv (expr-grade-bitwise-ior)
                            (expr-grade-bitwise-and))
                :bitxor (mv (expr-grade-bitwise-xor)
                            (expr-grade-bitwise-ior))
                :lt (mv (expr-grade-additive)
                        (expr-grade-additive))
                :gt (mv (expr-grade-additive)
                        (expr-grade-additive))
                :le (mv (expr-grade-additive)
                        (expr-grade-additive))
                :ge (mv (expr-grade-additive)
                        (expr-grade-additive))
                :eq (mv (expr-grade-ordering)
                        (expr-grade-ordering))
                :ne (mv (expr-grade-ordering)
                        (expr-grade-ordering))
                :and (mv (expr-grade-conjunctive)
                         (expr-grade-equality))
                :or (mv (expr-grade-disjunctive)
                        (expr-grade-conjunctive))
                :nand (mv (expr-grade-postfix)
                          (expr-grade-top))
                :nor (mv (expr-grade-postfix)
                         (expr-grade-top))
                :pow-wrapped (mv (expr-grade-postfix)
                                 (expr-grade-top))
                :mul-wrapped (mv (expr-grade-postfix)
                                 (expr-grade-top))
                :div-wrapped (mv (expr-grade-postfix)
                                 (expr-grade-top))
                :rem-wrapped (mv (expr-grade-postfix)
                                 (expr-grade-top))
                :add-wrapped (mv (expr-grade-postfix)
                                 (expr-grade-top))
                :sub-wrapped (mv (expr-grade-postfix)
                                 (expr-grade-top))
                :shl-wrapped (mv (expr-grade-postfix)
                                 (expr-grade-top))
                :shr-wrapped (mv (expr-grade-postfix)
                                 (expr-grade-top)))))

Theorem: expr-gradep-of-binop-expected-grades.left-grade

(defthm expr-gradep-of-binop-expected-grades.left-grade
  (b* (((mv ?left-grade ?right-grade)
        (binop-expected-grades op)))
    (expr-gradep left-grade))
  :rule-classes :rewrite)

Theorem: expr-gradep-of-binop-expected-grades.right-grade

(defthm expr-gradep-of-binop-expected-grades.right-grade
  (b* (((mv ?left-grade ?right-grade)
        (binop-expected-grades op)))
    (expr-gradep right-grade))
  :rule-classes :rewrite)

Theorem: binop-expected-grades-of-binop-fix-op

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

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

(defthm binop-expected-grades-binop-equiv-congruence-on-op
  (implies (binop-equiv op op-equiv)
           (equal (binop-expected-grades op)
                  (binop-expected-grades op-equiv)))
  :rule-classes :congruence)