		Search-engine friendly clone of the ACL2 documentation.

Stmtrewrite

Vl-flatten-blocks

Collapse nested begin/end and fork/join blocks.

Signature
(vl-flatten-blocks sequentialp stmts) → new-stmts
Arguments: sequentialp — are we working with a sequential (begin/end) or parallel (fork/join) block.
Guard (booleanp sequentialp).; stmts — Guard (vl-stmtlist-p stmts).
Returns: new-stmts — Type (vl-stmtlist-p new-stmts), given the guard.

This function carries out rewrites such as:

begin               begin
  foo = a;    -->     foo = a;
  begin               bar = b;
    bar = b;          baz = c;
    baz = c;          goo = d;
  end               end
  goo = d;
end

It can similarly collapse fork/join blocks with inner fork/join blocks.

We don't try to merge blocks that have their own scopes (i.e., names/decls). Handling them correctly seems very tricky because of hierarchical identifiers, etc.

BOZO. We recursively flatten sub-blocks. I'm not sure if we need to do this, given the way that vl-stmt-rewrite works. Well, it's probably just some useless computation if it's not necessary.

Definitions and Theorems

Function: vl-flatten-blocks

(defun vl-flatten-blocks (sequentialp stmts)
 (declare (xargs :guard (and (booleanp sequentialp)
                             (vl-stmtlist-p stmts))))
 (let ((__function__ 'vl-flatten-blocks))
  (declare (ignorable __function__))
  (b* ((stmts (vl-stmtlist-fix stmts))
       ((when (atom stmts)) nil)
       ((unless (and (vl-blockstmt-p (car stmts))
                     (eq (vl-blockstmt->sequentialp (car stmts))
                         sequentialp)
                     (not (vl-blockstmt->name (car stmts)))
                     (atom (vl-blockstmt->vardecls (car stmts)))
                     (atom (vl-blockstmt->paramdecls (car stmts)))))
        (cons (car stmts)
              (vl-flatten-blocks sequentialp (cdr stmts))))
       (merged-stmts
            (append-without-guard (vl-blockstmt->stmts (car stmts))
                                  (cdr stmts))))
    (vl-flatten-blocks sequentialp merged-stmts))))

Theorem: vl-stmtlist-p-of-vl-flatten-blocks

(defthm vl-stmtlist-p-of-vl-flatten-blocks
  (implies (and (force (booleanp sequentialp))
                (force (vl-stmtlist-p stmts)))
           (b* ((new-stmts (vl-flatten-blocks sequentialp stmts)))
             (vl-stmtlist-p new-stmts)))
  :rule-classes :rewrite)