		Search-engine friendly clone of the ACL2 documentation.

Atc-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).

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
                :mul (mv (expr-grade-multiplicative)
                         (expr-grade-cast))
                :div (mv (expr-grade-multiplicative)
                         (expr-grade-cast))
                :rem (mv (expr-grade-multiplicative)
                         (expr-grade-cast))
                :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))
                :lt (mv (expr-grade-relational)
                        (expr-grade-shift))
                :gt (mv (expr-grade-relational)
                        (expr-grade-shift))
                :le (mv (expr-grade-relational)
                        (expr-grade-shift))
                :ge (mv (expr-grade-relational)
                        (expr-grade-shift))
                :eq (mv (expr-grade-equality)
                        (expr-grade-relational))
                :ne (mv (expr-grade-equality)
                        (expr-grade-relational))
                :bitand (mv (expr-grade-and)
                            (expr-grade-equality))
                :bitxor (mv (expr-grade-xor) (expr-grade-and))
                :bitior (mv (expr-grade-ior) (expr-grade-xor))
                :logand (mv (expr-grade-ior)
                            (expr-grade-logical-and))
                :logor (mv (expr-grade-logical-or)
                           (expr-grade-logical-and))
                :asg (mv (expr-grade-unary)
                         (expr-grade-assignment))
                :asg-mul (mv (expr-grade-unary)
                             (expr-grade-assignment))
                :asg-div (mv (expr-grade-unary)
                             (expr-grade-assignment))
                :asg-rem (mv (expr-grade-unary)
                             (expr-grade-assignment))
                :asg-add (mv (expr-grade-unary)
                             (expr-grade-assignment))
                :asg-sub (mv (expr-grade-unary)
                             (expr-grade-assignment))
                :asg-shl (mv (expr-grade-unary)
                             (expr-grade-assignment))
                :asg-shr (mv (expr-grade-unary)
                             (expr-grade-assignment))
                :asg-and (mv (expr-grade-unary)
                             (expr-grade-assignment))
                :asg-xor (mv (expr-grade-unary)
                             (expr-grade-assignment))
                :asg-ior (mv (expr-grade-unary)
                             (expr-grade-assignment)))))

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)