		Search-engine friendly clone of the ACL2 documentation.

Vl-foreachstmt

Make-vl-foreachstmt

Basic constructor macro for vl-foreachstmt structures.

Syntax

(make-vl-foreachstmt [:array <array>] 
                     [:loopvars <loopvars>] 
                     [:vardecls <vardecls>] 
                     [:body <body>] 
                     [:atts <atts>])

This is the usual way to construct vl-foreachstmt structures. It simply conses together a structure with the specified fields.

This macro generates a new vl-foreachstmt structure from scratch. See also change-vl-foreachstmt, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-foreachstmt

(defmacro make-vl-foreachstmt (&rest args)
  (std::make-aggregate 'vl-foreachstmt
                       args
                       '((:array)
                         (:loopvars)
                         (:vardecls)
                         (:body)
                         (:atts))
                       'make-vl-foreachstmt
                       nil))

Function: vl-foreachstmt

(defun vl-foreachstmt (array loopvars vardecls body atts)
 (declare (xargs :guard (and (vl-scopeexpr-p array)
                             (vl-maybe-string-list-p loopvars)
                             (vl-vardecllist-p vardecls)
                             (vl-stmt-p body)
                             (vl-atts-p atts))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-foreachstmt))
  (declare (ignorable __function__))
  (b* ((array (mbe :logic (vl-scopeexpr-fix array)
                   :exec array))
       (loopvars (mbe :logic (vl-maybe-string-list-fix loopvars)
                      :exec loopvars))
       (vardecls (mbe :logic (vl-vardecllist-fix vardecls)
                      :exec vardecls))
       (body (mbe :logic (vl-stmt-fix body)
                  :exec body))
       (atts (mbe :logic (vl-atts-fix atts)
                  :exec atts)))
   (cons
    :vl-foreachstmt
    (std::prod-cons (std::prod-cons array loopvars)
                    (std::prod-cons vardecls
                                    (std::prod-cons body atts)))))))