(vl-genblob->elems-aux orig-elements portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc) → final-acc
Function:
(defun vl-genblob->elems-aux (orig-elements portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc) (declare (xargs :guard (and (vl-genelementlist-p orig-elements) (vl-portdecllist-p portdecls) (vl-assignlist-p assigns) (vl-aliaslist-p aliases) (vl-vardecllist-p vardecls) (vl-paramdecllist-p paramdecls) (vl-fundecllist-p fundecls) (vl-taskdecllist-p taskdecls) (vl-modinstlist-p modinsts) (vl-gateinstlist-p gateinsts) (vl-alwayslist-p alwayses) (vl-initiallist-p initials) (vl-finallist-p finals) (vl-typedeflist-p typedefs) (vl-importlist-p imports) (vl-fwdtypedeflist-p fwdtypedefs) (vl-modportlist-p modports) (vl-genvarlist-p genvars) (vl-assertionlist-p assertions) (vl-cassertionlist-p cassertions) (vl-propertylist-p properties) (vl-sequencelist-p sequences) (vl-clkdecllist-p clkdecls) (vl-gclkdecllist-p gclkdecls) (vl-defaultdisablelist-p defaultdisables) (vl-dpiimportlist-p dpiimports) (vl-dpiexportlist-p dpiexports) (vl-bindlist-p binds) (vl-classlist-p classes) (vl-covergrouplist-p covergroups) (vl-elabtasklist-p elabtasks) (vl-letdecllist-p letdecls) (vl-genelementlist-p generates) (vl-genelementlist-p acc)))) (let ((__function__ 'vl-genblob->elems-aux)) (declare (ignorable __function__)) (b* (((when (atom orig-elements)) (revappend-without-guard (vl-genelementlist-fix acc) (append-without-guard (vl-modelementlist->genelements (append-without-guard portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls)) (vl-genelementlist-fix generates)))) (x (car orig-elements))) (vl-genelement-case x :vl-genbase (case (tag x.item) (:vl-portdecl (b* (((mv acc portdecls) (if (consp portdecls) (mv (cons (make-vl-genbase :item (vl-portdecl-fix (car portdecls))) acc) (cdr portdecls)) (mv acc portdecls)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-assign (b* (((mv acc assigns) (if (consp assigns) (mv (cons (make-vl-genbase :item (vl-assign-fix (car assigns))) acc) (cdr assigns)) (mv acc assigns)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-alias (b* (((mv acc aliases) (if (consp aliases) (mv (cons (make-vl-genbase :item (vl-alias-fix (car aliases))) acc) (cdr aliases)) (mv acc aliases)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-vardecl (b* (((mv acc vardecls) (if (consp vardecls) (mv (cons (make-vl-genbase :item (vl-vardecl-fix (car vardecls))) acc) (cdr vardecls)) (mv acc vardecls)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-paramdecl (b* (((mv acc paramdecls) (if (consp paramdecls) (mv (cons (make-vl-genbase :item (vl-paramdecl-fix (car paramdecls))) acc) (cdr paramdecls)) (mv acc paramdecls)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-fundecl (b* (((mv acc fundecls) (if (consp fundecls) (mv (cons (make-vl-genbase :item (vl-fundecl-fix (car fundecls))) acc) (cdr fundecls)) (mv acc fundecls)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-taskdecl (b* (((mv acc taskdecls) (if (consp taskdecls) (mv (cons (make-vl-genbase :item (vl-taskdecl-fix (car taskdecls))) acc) (cdr taskdecls)) (mv acc taskdecls)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-modinst (b* (((mv acc modinsts) (if (consp modinsts) (mv (cons (make-vl-genbase :item (vl-modinst-fix (car modinsts))) acc) (cdr modinsts)) (mv acc modinsts)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-gateinst (b* (((mv acc gateinsts) (if (consp gateinsts) (mv (cons (make-vl-genbase :item (vl-gateinst-fix (car gateinsts))) acc) (cdr gateinsts)) (mv acc gateinsts)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-always (b* (((mv acc alwayses) (if (consp alwayses) (mv (cons (make-vl-genbase :item (vl-always-fix (car alwayses))) acc) (cdr alwayses)) (mv acc alwayses)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-initial (b* (((mv acc initials) (if (consp initials) (mv (cons (make-vl-genbase :item (vl-initial-fix (car initials))) acc) (cdr initials)) (mv acc initials)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-final (b* (((mv acc finals) (if (consp finals) (mv (cons (make-vl-genbase :item (vl-final-fix (car finals))) acc) (cdr finals)) (mv acc finals)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-typedef (b* (((mv acc typedefs) (if (consp typedefs) (mv (cons (make-vl-genbase :item (vl-typedef-fix (car typedefs))) acc) (cdr typedefs)) (mv acc typedefs)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-import (b* (((mv acc imports) (if (consp imports) (mv (cons (make-vl-genbase :item (vl-import-fix (car imports))) acc) (cdr imports)) (mv acc imports)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-fwdtypedef (b* (((mv acc fwdtypedefs) (if (consp fwdtypedefs) (mv (cons (make-vl-genbase :item (vl-fwdtypedef-fix (car fwdtypedefs))) acc) (cdr fwdtypedefs)) (mv acc fwdtypedefs)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-modport (b* (((mv acc modports) (if (consp modports) (mv (cons (make-vl-genbase :item (vl-modport-fix (car modports))) acc) (cdr modports)) (mv acc modports)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-genvar (b* (((mv acc genvars) (if (consp genvars) (mv (cons (make-vl-genbase :item (vl-genvar-fix (car genvars))) acc) (cdr genvars)) (mv acc genvars)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-assertion (b* (((mv acc assertions) (if (consp assertions) (mv (cons (make-vl-genbase :item (vl-assertion-fix (car assertions))) acc) (cdr assertions)) (mv acc assertions)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-cassertion (b* (((mv acc cassertions) (if (consp cassertions) (mv (cons (make-vl-genbase :item (vl-cassertion-fix (car cassertions))) acc) (cdr cassertions)) (mv acc cassertions)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-property (b* (((mv acc properties) (if (consp properties) (mv (cons (make-vl-genbase :item (vl-property-fix (car properties))) acc) (cdr properties)) (mv acc properties)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-sequence (b* (((mv acc sequences) (if (consp sequences) (mv (cons (make-vl-genbase :item (vl-sequence-fix (car sequences))) acc) (cdr sequences)) (mv acc sequences)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-clkdecl (b* (((mv acc clkdecls) (if (consp clkdecls) (mv (cons (make-vl-genbase :item (vl-clkdecl-fix (car clkdecls))) acc) (cdr clkdecls)) (mv acc clkdecls)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-gclkdecl (b* (((mv acc gclkdecls) (if (consp gclkdecls) (mv (cons (make-vl-genbase :item (vl-gclkdecl-fix (car gclkdecls))) acc) (cdr gclkdecls)) (mv acc gclkdecls)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-defaultdisable (b* (((mv acc defaultdisables) (if (consp defaultdisables) (mv (cons (make-vl-genbase :item (vl-defaultdisable-fix (car defaultdisables))) acc) (cdr defaultdisables)) (mv acc defaultdisables)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-dpiimport (b* (((mv acc dpiimports) (if (consp dpiimports) (mv (cons (make-vl-genbase :item (vl-dpiimport-fix (car dpiimports))) acc) (cdr dpiimports)) (mv acc dpiimports)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-dpiexport (b* (((mv acc dpiexports) (if (consp dpiexports) (mv (cons (make-vl-genbase :item (vl-dpiexport-fix (car dpiexports))) acc) (cdr dpiexports)) (mv acc dpiexports)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-bind (b* (((mv acc binds) (if (consp binds) (mv (cons (make-vl-genbase :item (vl-bind-fix (car binds))) acc) (cdr binds)) (mv acc binds)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-class (b* (((mv acc classes) (if (consp classes) (mv (cons (make-vl-genbase :item (vl-class-fix (car classes))) acc) (cdr classes)) (mv acc classes)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-covergroup (b* (((mv acc covergroups) (if (consp covergroups) (mv (cons (make-vl-genbase :item (vl-covergroup-fix (car covergroups))) acc) (cdr covergroups)) (mv acc covergroups)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-elabtask (b* (((mv acc elabtasks) (if (consp elabtasks) (mv (cons (make-vl-genbase :item (vl-elabtask-fix (car elabtasks))) acc) (cdr elabtasks)) (mv acc elabtasks)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (:vl-letdecl (b* (((mv acc letdecls) (if (consp letdecls) (mv (cons (make-vl-genbase :item (vl-letdecl-fix (car letdecls))) acc) (cdr letdecls)) (mv acc letdecls)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc)))) :otherwise (b* (((mv acc generates) (if (consp generates) (mv (cons (car generates) acc) (cdr generates)) (mv acc generates)))) (vl-genblob->elems-aux (cdr orig-elements) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))))))
Theorem:
(defthm vl-genelementlist-p-of-vl-genblob->elems-aux (b* ((final-acc (vl-genblob->elems-aux orig-elements portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials finals typedefs imports fwdtypedefs modports genvars assertions cassertions properties sequences clkdecls gclkdecls defaultdisables dpiimports dpiexports binds classes covergroups elabtasks letdecls generates acc))) (vl-genelementlist-p final-acc)) :rule-classes :rewrite)