Get a normalized right-hand side expression for an increment, decrement, or assignment expression.
Examples:
(a=1) --> 1 a++, ++a, (a+=1) --> a + 1 a--, --a, (a-=1) --> a - 1 (a += b) --> a + b (a *= 7) --> a * 7
Function:
(defun vl-incexpr->rhsexpr (x) (declare (xargs :guard (vl-expr-p x))) (declare (xargs :guard (vl-incexpr-p x))) (let ((__function__ 'vl-incexpr->rhsexpr)) (declare (ignorable __function__)) (b* ((x (vl-expr-fix x))) (vl-expr-case x :vl-unary (case x.op ((:vl-unary-preinc :vl-unary-postinc) (make-vl-binary :op :vl-binary-plus :left x.arg :right *vl-incexpr-1* :atts (list (cons "VL_INCREMENT" x)))) ((:vl-unary-predec :vl-unary-postdec) (make-vl-binary :op :vl-binary-minus :left x.arg :right *vl-incexpr-1* :atts (list (cons "VL_DECREMENT" x)))) (otherwise (progn$ (impossible) x))) :vl-binary (case x.op (:vl-binary-assign x.right) (otherwise (make-vl-binary :op (case x.op (:vl-binary-plusassign :vl-binary-plus) (:vl-binary-minusassign :vl-binary-minus) (:vl-binary-timesassign :vl-binary-times) (:vl-binary-divassign :vl-binary-div) (:vl-binary-remassign :vl-binary-rem) (:vl-binary-andassign :vl-binary-bitand) (:vl-binary-orassign :vl-binary-bitor) (:vl-binary-xorassign :vl-binary-xor) (:vl-binary-shlassign :vl-binary-shl) (:vl-binary-shrassign :vl-binary-shr) (:vl-binary-ashlassign :vl-binary-ashl) (:vl-binary-ashrassign :vl-binary-ashr)) :left x.left :right x.right :atts (list (cons "VL_ASSIGNEXPR" x))))) :otherwise (progn$ (impossible) x)))))
Theorem:
(defthm vl-expr-p-of-vl-incexpr->rhsexpr (b* ((rhs (vl-incexpr->rhsexpr x))) (vl-expr-p rhs)) :rule-classes :rewrite)
Theorem:
(defthm vl-incexpr->rhsexpr-of-vl-expr-fix-x (equal (vl-incexpr->rhsexpr (vl-expr-fix x)) (vl-incexpr->rhsexpr x)))
Theorem:
(defthm vl-incexpr->rhsexpr-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-incexpr->rhsexpr x) (vl-incexpr->rhsexpr x-equiv))) :rule-classes :congruence)