		Search-engine friendly clone of the ACL2 documentation.

Stmtrewrite

Vl-blockstmt-rewrite

Flatten sub-blocks, eliminate unnecessary blocks, and remove any null statements from a block.

Signature
(vl-blockstmt-rewrite sequentialp name vardecls paramdecls stmts atts warnings) → (mv warnings stmt)
Arguments: sequentialp — Guard (booleanp sequentialp).; name — Guard (maybe-stringp name).; vardecls — Guard (vl-vardecllist-p vardecls).; paramdecls — Guard (vl-paramdecllist-p paramdecls).; stmts — Guard (vl-stmtlist-p stmts).; atts — Guard (vl-atts-p atts).; warnings — Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings), given the guard.; stmt — Type (vl-stmt-p stmt), given the guard.

This rewrite starts by flattening out nested, compatible blocks with vl-flatten-blocks and removing null statements. If then reduce the resulting block with these rules:

begin   --> null    // empty block rewrite
end

begin   --> stmt    // single statement rewrite
  stmt
end

We only do these extra rewrites when the block has no names/decls. Handling blocks with names/decls seems tricky due to hierarchical identifiers.

Definitions and Theorems

Function: vl-blockstmt-rewrite

(defun vl-blockstmt-rewrite
       (sequentialp name
                    vardecls paramdecls stmts atts warnings)
 (declare (xargs :guard (and (booleanp sequentialp)
                             (maybe-stringp name)
                             (vl-vardecllist-p vardecls)
                             (vl-paramdecllist-p paramdecls)
                             (vl-stmtlist-p stmts)
                             (vl-atts-p atts)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-blockstmt-rewrite))
  (declare (ignorable __function__))
  (b*
   ((stmts (vl-flatten-blocks sequentialp stmts))
    (stmts (vl-remove-null-statements stmts))
    ((when (and (or (atom stmts) (atom (cdr stmts)))
                (or name vardecls paramdecls)))
     (mv
      (warn
       :type :vl-collapse-fail
       :msg
       "Not collapsing ~s0 block ~x1 since it has a name or ~
                        declarations."
       :args (list (if sequentialp "begin/end" "fork/join")
                   name))
      (make-vl-blockstmt
           :sequentialp sequentialp
           :name name
           :vardecls vardecls
           :paramdecls paramdecls
           :stmts stmts
           :atts (acons "VL_COLLAPSE_FAIL" nil atts))))
    ((when (atom stmts))
     (mv warnings
         (make-vl-nullstmt :atts (acons "VL_COLLAPSE" nil atts))))
    ((when (atom (cdr stmts)))
     (mv warnings (car stmts))))
   (mv warnings
       (make-vl-blockstmt :sequentialp sequentialp
                          :name name
                          :vardecls vardecls
                          :paramdecls paramdecls
                          :stmts stmts
                          :atts atts)))))

Theorem: vl-warninglist-p-of-vl-blockstmt-rewrite.warnings

(defthm vl-warninglist-p-of-vl-blockstmt-rewrite.warnings
  (implies
       (and (force (booleanp sequentialp))
            (force (acl2::maybe-stringp$inline name))
            (force (vl-vardecllist-p vardecls))
            (force (vl-paramdecllist-p paramdecls))
            (force (vl-stmtlist-p stmts))
            (force (vl-atts-p atts))
            (force (vl-warninglist-p warnings)))
       (b* (((mv ?warnings ?stmt)
             (vl-blockstmt-rewrite sequentialp name vardecls
                                   paramdecls stmts atts warnings)))
         (vl-warninglist-p warnings)))
  :rule-classes :rewrite)

Theorem: vl-stmt-p-of-vl-blockstmt-rewrite.stmt

(defthm vl-stmt-p-of-vl-blockstmt-rewrite.stmt
  (implies
       (and (force (booleanp sequentialp))
            (force (acl2::maybe-stringp$inline name))
            (force (vl-vardecllist-p vardecls))
            (force (vl-paramdecllist-p paramdecls))
            (force (vl-stmtlist-p stmts))
            (force (vl-atts-p atts))
            (force (vl-warninglist-p warnings)))
       (b* (((mv ?warnings ?stmt)
             (vl-blockstmt-rewrite sequentialp name vardecls
                                   paramdecls stmts atts warnings)))
         (vl-stmt-p stmt)))
  :rule-classes :rewrite)