(vl-unaryop-typedecide x arg-class) → (mv warnings class)
Function:
(defun vl-unaryop-typedecide (x arg-class) (declare (xargs :guard (and (vl-expr-p x) (vl-arithclass-p arg-class)))) (declare (xargs :guard (vl-expr-case x :vl-unary))) (let ((__function__ 'vl-unaryop-typedecide)) (declare (ignorable __function__)) (b* (((vl-unary x) (vl-expr-fix x)) (warnings nil) (arg-class (vl-arithclass-fix arg-class))) (case x.op ((:vl-unary-plus :vl-unary-minus :vl-unary-bitnot) (mv (ok) arg-class)) ((:vl-unary-lognot :vl-unary-bitand :vl-unary-bitor :vl-unary-nand :vl-unary-nor :vl-unary-xor :vl-unary-xnor) (mv (ok) :vl-unsigned-int-class)) ((:vl-unary-preinc :vl-unary-predec :vl-unary-postinc :vl-unary-postdec) (mv (fatal :type :vl-typedecide-fail :msg "Programming error: Increment/decrement ~ 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-unaryop-typedecide.warnings (b* (((mv ?warnings common-lisp::?class) (vl-unaryop-typedecide x arg-class))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-arithclass-p-of-vl-unaryop-typedecide.class (b* (((mv ?warnings common-lisp::?class) (vl-unaryop-typedecide x arg-class))) (vl-arithclass-p class)) :rule-classes :rewrite)
Theorem:
(defthm vl-unaryop-typedecide-of-vl-expr-fix-x (equal (vl-unaryop-typedecide (vl-expr-fix x) arg-class) (vl-unaryop-typedecide x arg-class)))
Theorem:
(defthm vl-unaryop-typedecide-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-unaryop-typedecide x arg-class) (vl-unaryop-typedecide x-equiv arg-class))) :rule-classes :congruence)
Theorem:
(defthm vl-unaryop-typedecide-of-vl-arithclass-fix-arg-class (equal (vl-unaryop-typedecide x (vl-arithclass-fix arg-class)) (vl-unaryop-typedecide x arg-class)))
Theorem:
(defthm vl-unaryop-typedecide-vl-arithclass-equiv-congruence-on-arg-class (implies (vl-arithclass-equiv arg-class arg-class-equiv) (equal (vl-unaryop-typedecide x arg-class) (vl-unaryop-typedecide x arg-class-equiv))) :rule-classes :congruence)