		Search-engine friendly clone of the ACL2 documentation.

Stmtrewrite

Vl-casestmt-rewrite

Eliminate pure-null case statements.

Signature
(vl-casestmt-rewrite check casetype test caselist default atts) → stmt
Arguments: check — Guard (vl-casecheck-p check).; casetype — Guard (vl-casetype-p casetype).; test — Guard (vl-expr-p test).; caselist — Guard (vl-caselist-p caselist).; default — Guard (vl-stmt-p default).; atts — Guard (vl-atts-p atts).
Returns: stmt — Type (vl-stmt-p stmt), given the guard.

This is a pretty silly rewrite:

[priority/unique/unique0/nil] [case/casex/casez](expr):    -->   [null stmt]
  expr1 : [null stmt];
  expr2 : [null stmt];
  ...
  exprN : [null stmt];
  default: [null stmt];
endcase

This seems safe and along with our other rewrites it lets us fizzle away, e.g., case-based $display statements into nothing. But if we implement a real case-statement → if-statement transform we shouldn't need this anymore.

Definitions and Theorems

Function: vl-casestmt-rewrite

(defun vl-casestmt-rewrite
       (check casetype test caselist default atts)
  (declare (xargs :guard (and (vl-casecheck-p check)
                              (vl-casetype-p casetype)
                              (vl-expr-p test)
                              (vl-caselist-p caselist)
                              (vl-stmt-p default)
                              (vl-atts-p atts))))
  (let ((__function__ 'vl-casestmt-rewrite))
    (declare (ignorable __function__))
    (if (and (vl-nullstmt-p default)
             (vl-caselist-all-null-p caselist))
        (make-vl-nullstmt)
      (make-vl-casestmt :check check
                        :casetype casetype
                        :test test
                        :caselist caselist
                        :default default
                        :atts atts))))

Theorem: vl-stmt-p-of-vl-casestmt-rewrite

(defthm vl-stmt-p-of-vl-casestmt-rewrite
 (implies
  (and (force (vl-casecheck-p check))
       (force (vl-casetype-p casetype))
       (force (vl-expr-p test))
       (force (vl-caselist-p caselist))
       (force (vl-stmt-p default))
       (force (vl-atts-p atts)))
  (b*
   ((stmt
         (vl-casestmt-rewrite check
                              casetype test caselist default atts)))
   (vl-stmt-p stmt)))
 :rule-classes :rewrite)