		Search-engine friendly clone of the ACL2 documentation.

Vl-genloop

Make-vl-genloop

Basic constructor macro for vl-genloop structures.

Syntax

(make-vl-genloop [:var <var>] 
                 [:genvarp <genvarp>] 
                 [:initval <initval>] 
                 [:continue <continue>] 
                 [:nextval <nextval>] 
                 [:body <body>] 
                 [:loc <loc>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-genloop

(defmacro make-vl-genloop (&rest args)
  (std::make-aggregate 'vl-genloop
                       args
                       '((:var)
                         (:genvarp)
                         (:initval)
                         (:continue)
                         (:nextval)
                         (:body)
                         (:loc))
                       'make-vl-genloop
                       nil))

Function: vl-genloop

(defun vl-genloop (var genvarp
                       initval continue nextval body loc)
 (declare (xargs :guard (and (stringp var)
                             (booleanp genvarp)
                             (vl-expr-p initval)
                             (vl-expr-p continue)
                             (vl-expr-p nextval)
                             (vl-genblock-p body)
                             (vl-location-p loc))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-genloop))
  (declare (ignorable __function__))
  (b* ((var (mbe :logic (str-fix var) :exec var))
       (genvarp (mbe :logic (acl2::bool-fix genvarp)
                     :exec genvarp))
       (initval (mbe :logic (vl-expr-fix initval)
                     :exec initval))
       (continue (mbe :logic (vl-expr-fix continue)
                      :exec continue))
       (nextval (mbe :logic (vl-expr-fix nextval)
                     :exec nextval))
       (body (mbe :logic (vl-genblock-fix body)
                  :exec body))
       (loc (mbe :logic (vl-location-fix loc)
                 :exec loc)))
    (cons :vl-genloop
          (std::prod-cons
               (std::prod-cons var (std::prod-cons genvarp initval))
               (std::prod-cons (std::prod-cons continue nextval)
                               (std::prod-cons body loc)))))))