(vl-binaryop-typedecide x left-class right-class) → (mv warnings class)
Function:
(defun vl-binaryop-typedecide (x left-class right-class) (declare (xargs :guard (and (vl-expr-p x) (vl-arithclass-p left-class) (vl-arithclass-p right-class)))) (declare (xargs :guard (vl-expr-case x :vl-binary))) (let ((__function__ 'vl-binaryop-typedecide)) (declare (ignorable __function__)) (b* (((vl-binary x) (vl-expr-fix x)) (warnings nil) (left-class (vl-arithclass-fix left-class)) (right-class (vl-arithclass-fix right-class))) (case x.op ((:vl-binary-eq :vl-binary-neq :vl-binary-ceq :vl-binary-cne :vl-binary-lt :vl-binary-lte :vl-binary-gt :vl-binary-gte :vl-binary-wildneq :vl-binary-wildeq) (mv (ok) :vl-unsigned-int-class)) ((:vl-binary-logand :vl-binary-logor :vl-implies :vl-equiv) (mv (ok) :vl-unsigned-int-class)) ((:vl-binary-plus :vl-binary-minus :vl-binary-times :vl-binary-div :vl-binary-rem :vl-binary-bitand :vl-binary-bitor :vl-binary-xor :vl-binary-xnor) (mv (ok) (vl-arithclass-max left-class right-class))) ((:vl-binary-shr :vl-binary-shl :vl-binary-ashr :vl-binary-ashl :vl-binary-power) (mv (ok) left-class)) ((:vl-binary-assign :vl-binary-plusassign :vl-binary-minusassign :vl-binary-timesassign :vl-binary-divassign :vl-binary-remassign :vl-binary-andassign :vl-binary-orassign :vl-binary-xorassign :vl-binary-shlassign :vl-binary-shrassign :vl-binary-ashlassign :vl-binary-ashrassign) (mv (fatal :type :vl-typedecide-fail :msg "Programming error: Assignment operators should ~ be handled before now. (~a0)" :args (list x)) :vl-error-class)) (otherwise (progn$ (impossible) (mv (ok) :vl-error-class)))))))
Theorem:
(defthm vl-warninglist-p-of-vl-binaryop-typedecide.warnings (b* (((mv ?warnings common-lisp::?class) (vl-binaryop-typedecide x left-class right-class))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-arithclass-p-of-vl-binaryop-typedecide.class (b* (((mv ?warnings common-lisp::?class) (vl-binaryop-typedecide x left-class right-class))) (vl-arithclass-p class)) :rule-classes :rewrite)
Theorem:
(defthm vl-binaryop-typedecide-of-vl-expr-fix-x (equal (vl-binaryop-typedecide (vl-expr-fix x) left-class right-class) (vl-binaryop-typedecide x left-class right-class)))
Theorem:
(defthm vl-binaryop-typedecide-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-binaryop-typedecide x left-class right-class) (vl-binaryop-typedecide x-equiv left-class right-class))) :rule-classes :congruence)
Theorem:
(defthm vl-binaryop-typedecide-of-vl-arithclass-fix-left-class (equal (vl-binaryop-typedecide x (vl-arithclass-fix left-class) right-class) (vl-binaryop-typedecide x left-class right-class)))
Theorem:
(defthm vl-binaryop-typedecide-vl-arithclass-equiv-congruence-on-left-class (implies (vl-arithclass-equiv left-class left-class-equiv) (equal (vl-binaryop-typedecide x left-class right-class) (vl-binaryop-typedecide x left-class-equiv right-class))) :rule-classes :congruence)
Theorem:
(defthm vl-binaryop-typedecide-of-vl-arithclass-fix-right-class (equal (vl-binaryop-typedecide x left-class (vl-arithclass-fix right-class)) (vl-binaryop-typedecide x left-class right-class)))
Theorem:
(defthm vl-binaryop-typedecide-vl-arithclass-equiv-congruence-on-right-class (implies (vl-arithclass-equiv right-class right-class-equiv) (equal (vl-binaryop-typedecide x left-class right-class) (vl-binaryop-typedecide x left-class right-class-equiv))) :rule-classes :congruence)