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