		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Jbinop-expected-ranks

Expression ranks of the operands of a binary operator.

Signature
(jbinop-expected-ranks op) → (mv left-rank right-rank)
Arguments: op — Guard (jbinopp op).
Returns: left-rank — Type (jexpr-rankp left-rank).; right-rank — Type (jexpr-rankp right-rank).

These are based on the grammar rules.

Definitions and Theorems

Function: jbinop-expected-ranks

(defun jbinop-expected-ranks (op)
  (declare (xargs :guard (jbinopp op)))
  (let ((__function__ 'jbinop-expected-ranks))
    (declare (ignorable __function__))
    (jbinop-case op
                 :mul (mv (jexpr-rank-multiplicative)
                          (jexpr-rank-unary))
                 :div (mv (jexpr-rank-multiplicative)
                          (jexpr-rank-unary))
                 :rem (mv (jexpr-rank-multiplicative)
                          (jexpr-rank-unary))
                 :add (mv (jexpr-rank-additive)
                          (jexpr-rank-multiplicative))
                 :sub (mv (jexpr-rank-additive)
                          (jexpr-rank-multiplicative))
                 :shl (mv (jexpr-rank-shift)
                          (jexpr-rank-additive))
                 :sshr (mv (jexpr-rank-shift)
                           (jexpr-rank-additive))
                 :ushr (mv (jexpr-rank-shift)
                           (jexpr-rank-additive))
                 :lt (mv (jexpr-rank-relational)
                         (jexpr-rank-shift))
                 :gt (mv (jexpr-rank-relational)
                         (jexpr-rank-shift))
                 :le (mv (jexpr-rank-relational)
                         (jexpr-rank-shift))
                 :ge (mv (jexpr-rank-relational)
                         (jexpr-rank-shift))
                 :eq (mv (jexpr-rank-equality)
                         (jexpr-rank-relational))
                 :ne (mv (jexpr-rank-equality)
                         (jexpr-rank-relational))
                 :and (mv (jexpr-rank-and)
                          (jexpr-rank-equality))
                 :xor (mv (jexpr-rank-exclusive-or)
                          (jexpr-rank-and))
                 :ior (mv (jexpr-rank-inclusive-or)
                          (jexpr-rank-exclusive-or))
                 :condand (mv (jexpr-rank-conditional-and)
                              (jexpr-rank-inclusive-or))
                 :condor (mv (jexpr-rank-conditional-or)
                             (jexpr-rank-conditional-and))
                 :asg (mv (jexpr-rank-postfix)
                          (jexpr-rank-expression))
                 :asg-mul (mv (jexpr-rank-postfix)
                              (jexpr-rank-expression))
                 :asg-div (mv (jexpr-rank-postfix)
                              (jexpr-rank-expression))
                 :asg-rem (mv (jexpr-rank-postfix)
                              (jexpr-rank-expression))
                 :asg-add (mv (jexpr-rank-postfix)
                              (jexpr-rank-expression))
                 :asg-sub (mv (jexpr-rank-postfix)
                              (jexpr-rank-expression))
                 :asg-shl (mv (jexpr-rank-postfix)
                              (jexpr-rank-expression))
                 :asg-sshr (mv (jexpr-rank-postfix)
                               (jexpr-rank-expression))
                 :asg-ushr (mv (jexpr-rank-postfix)
                               (jexpr-rank-expression))
                 :asg-and (mv (jexpr-rank-postfix)
                              (jexpr-rank-expression))
                 :asg-xor (mv (jexpr-rank-postfix)
                              (jexpr-rank-expression))
                 :asg-ior (mv (jexpr-rank-postfix)
                              (jexpr-rank-expression)))))

Theorem: jexpr-rankp-of-jbinop-expected-ranks.left-rank

(defthm jexpr-rankp-of-jbinop-expected-ranks.left-rank
  (b* (((mv ?left-rank ?right-rank)
        (jbinop-expected-ranks op)))
    (jexpr-rankp left-rank))
  :rule-classes :rewrite)

Theorem: jexpr-rankp-of-jbinop-expected-ranks.right-rank

(defthm jexpr-rankp-of-jbinop-expected-ranks.right-rank
  (b* (((mv ?left-rank ?right-rank)
        (jbinop-expected-ranks op)))
    (jexpr-rankp right-rank))
  :rule-classes :rewrite)