(vl-genblob->elems-aux orig-elements portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates acc) → final-acc
Function:
(defun vl-genblob->elems-aux (orig-elements portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars 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-typedeflist-p typedefs) (vl-importlist-p imports) (vl-fwdtypedeflist-p fwdtypedefs) (vl-modportlist-p modports) (vl-genvarlist-p genvars) (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 typedefs imports fwdtypedefs modports genvars)) (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 typedefs imports fwdtypedefs modports genvars 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 typedefs imports fwdtypedefs modports genvars 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 typedefs imports fwdtypedefs modports genvars 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 typedefs imports fwdtypedefs modports genvars 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 typedefs imports fwdtypedefs modports genvars 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 typedefs imports fwdtypedefs modports genvars 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 typedefs imports fwdtypedefs modports genvars 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 typedefs imports fwdtypedefs modports genvars 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 typedefs imports fwdtypedefs modports genvars 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 typedefs imports fwdtypedefs modports genvars 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 typedefs imports fwdtypedefs modports genvars 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 typedefs imports fwdtypedefs modports genvars 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 typedefs imports fwdtypedefs modports genvars 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 typedefs imports fwdtypedefs modports genvars 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 typedefs imports fwdtypedefs modports genvars 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 typedefs imports fwdtypedefs modports genvars 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 typedefs imports fwdtypedefs modports genvars 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 typedefs imports fwdtypedefs modports genvars generates acc))) (vl-genelementlist-p final-acc)) :rule-classes :rewrite)