Basic constructor macro for vl-loadstate structures.
(make-vl-loadstate [:config <config>] [:descs <descs>] [:descalist <descalist>] [:defines <defines>] [:reportcard <reportcard>] [:pstate <pstate>] [:filemap <filemap>])
This is the usual way to construct vl-loadstate structures. It simply conses together a structure with the specified fields.
This macro generates a new vl-loadstate structure from scratch. See also change-vl-loadstate, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-vl-loadstate (&rest args) (std::make-aggregate 'vl-loadstate args '((:config) (:descs) (:descalist) (:defines) (:reportcard) (:pstate) (:filemap)) 'make-vl-loadstate nil))
Function:
(defun vl-loadstate (config descs descalist defines reportcard pstate filemap) (declare (xargs :guard (and (vl-loadconfig-p config) (vl-descriptionlist-p descs) (vl-defines-p defines) (vl-reportcard-p reportcard) (vl-parsestate-p pstate) (vl-filemap-p filemap)))) (declare (xargs :guard (equal descalist (vl-make-descalist descs)))) (let ((__function__ 'vl-loadstate)) (declare (ignorable __function__)) (b* ((config (mbe :logic (vl-loadconfig-fix config) :exec config)) (descs (mbe :logic (vl-descriptionlist-fix descs) :exec descs)) (defines (mbe :logic (vl-defines-fix defines) :exec defines) ) (reportcard (mbe :logic (vl-reportcard-fix reportcard) :exec reportcard)) (pstate (mbe :logic (vl-parsestate-fix pstate) :exec pstate)) (filemap (mbe :logic (vl-filemap-fix filemap) :exec filemap))) (let ((descalist (mbe :logic (vl-make-descalist descs) :exec descalist))) (cons :vl-loadstate (std::prod-cons (std::prod-cons config (std::prod-cons descs descalist)) (std::prod-cons (std::prod-cons defines reportcard) (std::prod-cons pstate filemap))))))))