Basic constructor macro for vl-parsed-portdecl-head structures.
(make-vl-parsed-portdecl-head [:nettype <nettype>] [:var-p <var-p>] [:type <type>] [:signing <signing>] [:dims <dims>])
This is the usual way to construct vl-parsed-portdecl-head structures. It simply conses together a structure with the specified fields.
This macro generates a new vl-parsed-portdecl-head structure from scratch. See also change-vl-parsed-portdecl-head, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-vl-parsed-portdecl-head (&rest args) (std::make-aggregate 'vl-parsed-portdecl-head args '((:nettype) (:var-p) (:type) (:signing) (:dims)) 'make-vl-parsed-portdecl-head nil))
Function:
(defun vl-parsed-portdecl-head (nettype var-p type signing dims) (declare (xargs :guard (and (vl-maybe-nettypename-p nettype) (booleanp var-p) (vl-maybe-datatype-p type) (vl-maybe-exprsign-p signing) (vl-dimensionlist-p dims)))) (declare (xargs :guard t)) (let ((__function__ 'vl-parsed-portdecl-head)) (declare (ignorable __function__)) (b* ((nettype (mbe :logic (vl-maybe-nettypename-fix nettype) :exec nettype)) (var-p (mbe :logic (acl2::bool-fix var-p) :exec var-p)) (type (mbe :logic (vl-maybe-datatype-fix type) :exec type)) (signing (mbe :logic (vl-maybe-exprsign-fix signing) :exec signing)) (dims (mbe :logic (vl-dimensionlist-fix dims) :exec dims))) (cons :vl-parsed-portdecl-head (std::prod-cons (std::prod-cons nettype var-p) (std::prod-cons type (std::prod-cons signing dims)))))))