		Search-engine friendly clone of the ACL2 documentation.

Parse-statements

Vl-assign-op-expr

Normalized right-hand side of an assignment operator expression.

Signature
(vl-assign-op-expr var op rhs) → expr
Arguments: var — Guard (vl-expr-p var).; op — Guard (member op *vl-assignment-operators*).; rhs — Guard (vl-expr-p rhs).
Returns: expr — Type (vl-expr-p expr).

Given an expression like a = b we return b. Given an expression like a %= b we return a % b.

Definitions and Theorems

Function: vl-assign-op-expr

(defun vl-assign-op-expr (var op rhs)
  (declare (xargs :guard (and (vl-expr-p var)
                              (member op *vl-assignment-operators*)
                              (vl-expr-p rhs))))
  (let ((__function__ 'vl-assign-op-expr))
    (declare (ignorable __function__))
    (if (eq op :vl-equalsign)
        (vl-expr-fix rhs)
      (make-vl-binary :op (case op (:vl-pluseq :vl-binary-plus)
                                (:vl-minuseq :vl-binary-minus)
                                (:vl-timeseq :vl-binary-times)
                                (:vl-diveq :vl-binary-div)
                                (:vl-remeq :vl-binary-rem)
                                (:vl-andeq :vl-binary-bitand)
                                (:vl-oreq :vl-binary-bitor)
                                (:vl-xoreq :vl-binary-xor)
                                (:vl-shleq :vl-binary-shl)
                                (:vl-shreq :vl-binary-shr)
                                (:vl-ashleq :vl-binary-ashl)
                                (:vl-ashreq :vl-binary-ashr))
                      :left var
                      :right rhs))))

Theorem: vl-expr-p-of-vl-assign-op-expr

(defthm vl-expr-p-of-vl-assign-op-expr
  (b* ((expr (vl-assign-op-expr var op rhs)))
    (vl-expr-p expr))
  :rule-classes :rewrite)