Basic constructor macro for vl-function-specialization structures.
(make-vl-function-specialization [:function <function>] [:body <body>] [:constraints <constraints>] [:successp <successp>])
This is the usual way to construct vl-function-specialization structures. It simply conses together a structure with the specified fields.
This macro generates a new vl-function-specialization structure from scratch. See also change-vl-function-specialization, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-vl-function-specialization (&rest args) (std::make-aggregate 'vl-function-specialization args '((:function) (:body) (:constraints) (:successp)) 'make-vl-function-specialization nil))
Function:
(defun vl-function-specialization (function body constraints successp) (declare (xargs :guard (and (sv::svex-p function) (vl-stmt-p body) (sv::constraintlist-p constraints)))) (declare (xargs :guard t)) (let ((__function__ 'vl-function-specialization)) (declare (ignorable __function__)) (b* ((function (mbe :logic (sv::svex-fix function) :exec function)) (body (mbe :logic (vl-stmt-fix body) :exec body)) (constraints (mbe :logic (sv::constraintlist-fix constraints) :exec constraints))) (list function body constraints successp))))