|
|
|---|
|
|
|
|---|
Basic constructor macro for vl-vardecl structures.
(make-vl-vardecl [:name <name>]
[:type <type>]
[:nettype <nettype>]
[:constp <constp>]
[:varp <varp>]
[:lifetime <lifetime>]
[:initval <initval>]
[:vectoredp <vectoredp>]
[:scalaredp <scalaredp>]
[:delay <delay>]
[:cstrength <cstrength>]
[:atts <atts>]
[:loc <loc>])
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.
This is an ordinary
Macro:
(defmacro make-vl-vardecl (&rest args) (std::make-aggregate 'vl-vardecl args '((:name) (:type) (:nettype) (:constp) (:varp) (:lifetime) (:initval) (:vectoredp) (:scalaredp) (:delay) (:cstrength) (:atts) (:loc)) 'make-vl-vardecl nil))
Function:
(defun vl-vardecl (name type nettype constp varp lifetime initval vectoredp scalaredp delay cstrength atts loc) (declare (xargs :guard (and (stringp name) (vl-datatype-p type) (vl-maybe-nettypename-p nettype) (booleanp constp) (booleanp varp) (vl-lifetime-p lifetime) (vl-maybe-expr-p initval) (booleanp vectoredp) (booleanp scalaredp) (vl-maybe-gatedelay-p delay) (vl-maybe-cstrength-p cstrength) (vl-atts-p atts) (vl-location-p loc)))) (declare (xargs :guard t)) (let ((__function__ 'vl-vardecl)) (declare (ignorable __function__)) (b* ((name (mbe :logic (str-fix name) :exec name)) (type (mbe :logic (vl-datatype-fix type) :exec type)) (nettype (mbe :logic (vl-maybe-nettypename-fix nettype) :exec nettype)) (constp (mbe :logic (acl2::bool-fix constp) :exec constp)) (varp (mbe :logic (acl2::bool-fix varp) :exec varp)) (lifetime (mbe :logic (vl-lifetime-fix lifetime) :exec lifetime)) (initval (mbe :logic (vl-maybe-expr-fix initval) :exec initval)) (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)) (atts (mbe :logic (vl-atts-fix atts) :exec atts)) (loc (mbe :logic (vl-location-fix loc) :exec loc))) (cons :vl-vardecl (std::prod-cons (std::prod-cons (std::prod-cons name (std::prod-cons type nettype)) (std::prod-cons constp (std::prod-cons varp lifetime))) (std::prod-cons (std::prod-cons initval (std::prod-cons vectoredp scalaredp)) (std::prod-cons (std::prod-cons delay cstrength) (std::prod-cons atts loc))))))))