Basic constructor macro for addnames-indices structures.
(make-addnames-indices [:genblk-idx <genblk-idx>] [:gateinst-idx <gateinst-idx>] [:blockstmt-idx <blockstmt-idx>] [:modinst-idx <modinst-idx>])
This is the usual way to construct addnames-indices structures. It simply conses together a structure with the specified fields.
This macro generates a new addnames-indices structure from scratch. See also change-addnames-indices, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-addnames-indices (&rest args) (std::make-aggregate 'addnames-indices args '((:genblk-idx . 1) (:gateinst-idx . 1) (:blockstmt-idx . 1) (:modinst-idx . 1)) 'make-addnames-indices nil))
Function:
(defun addnames-indices (genblk-idx gateinst-idx blockstmt-idx modinst-idx) (declare (xargs :guard (and (posp genblk-idx) (posp gateinst-idx) (posp blockstmt-idx) (posp modinst-idx)))) (declare (xargs :guard t)) (let ((__function__ 'addnames-indices)) (declare (ignorable __function__)) (b* ((genblk-idx (mbe :logic (pos-fix genblk-idx) :exec genblk-idx)) (gateinst-idx (mbe :logic (pos-fix gateinst-idx) :exec gateinst-idx)) (blockstmt-idx (mbe :logic (pos-fix blockstmt-idx) :exec blockstmt-idx)) (modinst-idx (mbe :logic (pos-fix modinst-idx) :exec modinst-idx))) (std::prod-cons (std::prod-cons genblk-idx gateinst-idx) (std::prod-cons blockstmt-idx modinst-idx)))))