		Search-engine friendly clone of the ACL2 documentation.

Vl-vardecl

Make-vl-vardecl

Basic constructor macro for vl-vardecl structures.

Syntax

(make-vl-vardecl [:name <name>] 
                 [:loc <loc>] 
                 [:type <type>] 
                 [:nettype <nettype>] 
                 [:atts <atts>] 
                 [:initval <initval>] 
                 [:constp <constp>] 
                 [:constval <constval>] 
                 [:varp <varp>] 
                 [:lifetime <lifetime>] 
                 [:vectoredp <vectoredp>] 
                 [:scalaredp <scalaredp>] 
                 [:delay <delay>] 
                 [:cstrength <cstrength>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-vardecl

(defmacro make-vl-vardecl (&rest args)
  (std::make-aggregate 'vl-vardecl
                       args
                       '((:name)
                         (:loc)
                         (:type)
                         (:nettype)
                         (:atts)
                         (:initval)
                         (:constp)
                         (:constval)
                         (:varp)
                         (:lifetime)
                         (:vectoredp)
                         (:scalaredp)
                         (:delay)
                         (:cstrength))
                       'make-vl-vardecl
                       nil))

Function: vl-vardecl

(defun vl-vardecl (name loc type nettype atts
                        initval constp constval varp lifetime
                        vectoredp scalaredp delay cstrength)
 (declare (xargs :guard (and (stringp name)
                             (vl-location-p loc)
                             (vl-datatype-p type)
                             (vl-maybe-nettypename-p nettype)
                             (vl-atts-p atts)
                             (vl-maybe-rhs-p initval)
                             (booleanp constp)
                             (sv::maybe-4vec-p constval)
                             (booleanp varp)
                             (vl-lifetime-p lifetime)
                             (booleanp vectoredp)
                             (booleanp scalaredp)
                             (vl-maybe-gatedelay-p delay)
                             (vl-maybe-cstrength-p cstrength))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-vardecl))
  (declare (ignorable __function__))
  (b* ((name (mbe :logic (str-fix name) :exec name))
       (loc (mbe :logic (vl-location-fix loc)
                 :exec loc))
       (type (mbe :logic (vl-datatype-fix type)
                  :exec type))
       (nettype (mbe :logic (vl-maybe-nettypename-fix nettype)
                     :exec nettype))
       (atts (mbe :logic (vl-atts-fix atts)
                  :exec atts))
       (initval (mbe :logic (vl-maybe-rhs-fix initval)
                     :exec initval))
       (constp (mbe :logic (acl2::bool-fix constp)
                    :exec constp))
       (constval (mbe :logic (sv::maybe-4vec-fix constval)
                      :exec constval))
       (varp (mbe :logic (acl2::bool-fix varp)
                  :exec varp))
       (lifetime (mbe :logic (vl-lifetime-fix lifetime)
                      :exec lifetime))
       (vectoredp (mbe :logic (acl2::bool-fix vectoredp)
                       :exec vectoredp))
       (scalaredp (mbe :logic (acl2::bool-fix scalaredp)
                       :exec scalaredp))
       (delay (mbe :logic (vl-maybe-gatedelay-fix delay)
                   :exec delay))
       (cstrength (mbe :logic (vl-maybe-cstrength-fix cstrength)
                       :exec cstrength)))
   (cons
    :vl-vardecl
    (std::prod-cons
       (std::prod-cons
            (std::prod-cons name (std::prod-cons loc type))
            (std::prod-cons (std::prod-cons nettype atts)
                            (std::prod-cons initval constp)))
       (std::prod-cons
            (std::prod-cons constval (std::prod-cons varp lifetime))
            (std::prod-cons (std::prod-cons vectoredp scalaredp)
                            (std::prod-cons delay cstrength))))))))