		Search-engine friendly clone of the ACL2 documentation.

Stmtrewrite

Vl-ifstmt-combine-rewrite

Eliminate pure-null if statements and merge simply nested ifs.

Signature
(vl-ifstmt-combine-rewrite condition truebranch falsebranch atts) → stmt
Arguments: condition — Guard (vl-expr-p condition).; truebranch — Guard (vl-stmt-p truebranch).; falsebranch — Guard (vl-stmt-p falsebranch).; atts — Guard (vl-atts-p atts).
Returns: stmt — Type (vl-stmt-p stmt), given the guard.

There are probably other things we could do here. For now, we just carry out two simple rewrites:

// Rewrite 1:

   if (test)      -->    null
      [null]
   else
      [null]

// Rewrite 2:

   if (test1)            if (test1 && test2)
     if (test2)   -->       body
       body

Definitions and Theorems

Function: vl-ifstmt-combine-rewrite

(defun vl-ifstmt-combine-rewrite
       (condition truebranch falsebranch atts)
 (declare (xargs :guard (and (vl-expr-p condition)
                             (vl-stmt-p truebranch)
                             (vl-stmt-p falsebranch)
                             (vl-atts-p atts))))
 (let ((__function__ 'vl-ifstmt-combine-rewrite))
   (declare (ignorable __function__))
   (b*
    ((fail-to-apply (make-vl-ifstmt :condition condition
                                    :truebranch truebranch
                                    :falsebranch falsebranch
                                    :atts atts))
     ((when (and (vl-nullstmt-p truebranch)
                 (vl-nullstmt-p falsebranch)))
      (make-vl-nullstmt))
     ((unless (vl-ifstmt-p truebranch))
      fail-to-apply)
     ((unless (vl-nullstmt-p falsebranch))
      fail-to-apply)
     ((vl-ifstmt inner) truebranch)
     ((unless (vl-nullstmt-p inner.falsebranch))
      fail-to-apply)
     (new-condition
          (make-vl-nonatom :op :vl-binary-logand
                           :args (list condition inner.condition))))
    (make-vl-ifstmt :condition new-condition
                    :truebranch inner.truebranch
                    :falsebranch falsebranch
                    :atts (acons "VL_COMBINED_IF" nil atts)))))

Theorem: vl-stmt-p-of-vl-ifstmt-combine-rewrite

(defthm vl-stmt-p-of-vl-ifstmt-combine-rewrite
  (implies (and (force (vl-expr-p condition))
                (force (vl-stmt-p truebranch))
                (force (vl-stmt-p falsebranch))
                (force (vl-atts-p atts)))
           (b* ((stmt (vl-ifstmt-combine-rewrite
                           condition truebranch falsebranch atts)))
             (vl-stmt-p stmt)))
  :rule-classes :rewrite)