		Search-engine friendly clone of the ACL2 documentation.

Unelse

Vl-ifstmt-unelse

Just handles a single if statement (not recursive).

Signature
(vl-ifstmt-unelse x) → new-x
Arguments: x — any statement, but we only rewrite it when it's an if statement; this makes writing vl-stmt-unelse very simple.
Guard (vl-stmt-p x).
Returns: new-x — Type (vl-stmt-p new-x), given the guard.

Definitions and Theorems

Function: vl-ifstmt-unelse

(defun vl-ifstmt-unelse (x)
  (declare (xargs :guard (vl-stmt-p x)))
  (let ((__function__ 'vl-ifstmt-unelse))
    (declare (ignorable __function__))
    (b* (((unless (eq (vl-stmt-kind x) :vl-ifstmt))
          x)
         ((vl-ifstmt x) x)
         ((when (eq (vl-stmt-kind x.falsebranch)
                    :vl-nullstmt))
          x)
         ((unless (and (vl-expr->finaltype x.condition)
                       (posp (vl-expr->finalwidth x.condition))
                       (vl-expr-welltyped-p x.condition)))
          x)
         (!condition (vl-condition-neg x.condition))
         (nullstmt (make-vl-nullstmt))
         (stmt1 (make-vl-ifstmt :condition x.condition
                                :truebranch x.truebranch
                                :falsebranch nullstmt))
         (stmt2 (make-vl-ifstmt :condition !condition
                                :truebranch x.falsebranch
                                :falsebranch nullstmt))
         (new-x (make-vl-blockstmt :sequentialp t
                                   :stmts (list stmt1 stmt2))))
      new-x)))

Theorem: vl-stmt-p-of-vl-ifstmt-unelse

(defthm vl-stmt-p-of-vl-ifstmt-unelse
  (implies (and (force (vl-stmt-p x)))
           (b* ((new-x (vl-ifstmt-unelse x)))
             (vl-stmt-p new-x)))
  :rule-classes :rewrite)