		Search-engine friendly clone of the ACL2 documentation.

Vl-forstmt

Make-vl-forstmt

Basic constructor macro for vl-forstmt structures.

Syntax

(make-vl-forstmt [:test <test>] 
                 [:stepforms <stepforms>] 
                 [:body <body>] 
                 [:initdecls <initdecls>] 
                 [:initassigns <initassigns>] 
                 [:atts <atts>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-forstmt

(defmacro make-vl-forstmt (&rest args)
  (std::make-aggregate 'vl-forstmt
                       args
                       '((:test)
                         (:stepforms)
                         (:body)
                         (:initdecls)
                         (:initassigns)
                         (:atts))
                       'make-vl-forstmt
                       nil))

Function: vl-forstmt

(defun vl-forstmt (test stepforms
                        body initdecls initassigns atts)
 (declare (xargs :guard (and (vl-expr-p test)
                             (vl-stmtlist-p stepforms)
                             (vl-stmt-p body)
                             (vl-vardecllist-p initdecls)
                             (vl-stmtlist-p initassigns)
                             (vl-atts-p atts))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-forstmt))
  (declare (ignorable __function__))
  (b* ((test (mbe :logic (vl-expr-fix test)
                  :exec test))
       (stepforms (mbe :logic (vl-stmtlist-fix stepforms)
                       :exec stepforms))
       (body (mbe :logic (vl-stmt-fix body)
                  :exec body))
       (initdecls (mbe :logic (vl-vardecllist-fix initdecls)
                       :exec initdecls))
       (initassigns (mbe :logic (vl-stmtlist-fix initassigns)
                         :exec initassigns))
       (atts (mbe :logic (vl-atts-fix atts)
                  :exec atts)))
   (cons
        :vl-forstmt
        (std::prod-cons
             (std::prod-cons test (std::prod-cons stepforms body))
             (std::prod-cons initdecls
                             (std::prod-cons initassigns atts)))))))