Collects svex module components for a list of vardecls, by collecting results from vl-vardecl->svex.
(vl-vardecllist->svex x portdecls modalist interfacep ss scopes config) → (mv vttree width wires fixups aliases modinsts assigns modalist1)
Function:
(defun vl-vardecllist->svex (x portdecls modalist interfacep ss scopes config) (declare (xargs :guard (and (vl-vardecllist-p x) (sv::modalist-p modalist) (vl-scopestack-p ss) (vl-elabscopes-p scopes) (vl-simpconfig-p config)))) (let ((__function__ 'vl-vardecllist->svex)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv nil 0 nil nil nil nil nil (sv::modalist-fix modalist))) (vttree nil) ((vmv vttree width2 wires2 fixups2 aliases2 modinsts2 assigns2 modalist) (vl-vardecllist->svex (cdr x) portdecls modalist interfacep ss scopes config)) ((vmv vttree width1 wire1 fixups1 aliases1 modinsts1 assigns1 modalist) (vl-vardecl->svex (car x) portdecls modalist (and interfacep width2) ss scopes config))) (mv vttree (+ width1 width2) (append-without-guard wire1 wires2) (append-without-guard fixups1 fixups2) (append-without-guard aliases1 aliases2) (append-without-guard modinsts1 modinsts2) (append-without-guard assigns1 assigns2) modalist))))
Theorem:
(defthm return-type-of-vl-vardecllist->svex.vttree (b* (((mv ?vttree ?width ?wires ?fixups ?aliases ?modinsts ?assigns ?modalist1) (vl-vardecllist->svex x portdecls modalist interfacep ss scopes config))) (and (vttree-p vttree) (sv::svarlist-addr-p (sv::constraintlist-vars (vttree->constraints vttree))))) :rule-classes :rewrite)
Theorem:
(defthm natp-of-vl-vardecllist->svex.width (b* (((mv ?vttree ?width ?wires ?fixups ?aliases ?modinsts ?assigns ?modalist1) (vl-vardecllist->svex x portdecls modalist interfacep ss scopes config))) (natp width)) :rule-classes :type-prescription)
Theorem:
(defthm wirelist-p-of-vl-vardecllist->svex.wires (b* (((mv ?vttree ?width ?wires ?fixups ?aliases ?modinsts ?assigns ?modalist1) (vl-vardecllist->svex x portdecls modalist interfacep ss scopes config))) (sv::wirelist-p wires)) :rule-classes :rewrite)
Theorem:
(defthm assigns-p-of-vl-vardecllist->svex.fixups (b* (((mv ?vttree ?width ?wires ?fixups ?aliases ?modinsts ?assigns ?modalist1) (vl-vardecllist->svex x portdecls modalist interfacep ss scopes config))) (sv::assigns-p fixups)) :rule-classes :rewrite)
Theorem:
(defthm lhspairs-p-of-vl-vardecllist->svex.aliases (b* (((mv ?vttree ?width ?wires ?fixups ?aliases ?modinsts ?assigns ?modalist1) (vl-vardecllist->svex x portdecls modalist interfacep ss scopes config))) (sv::lhspairs-p aliases)) :rule-classes :rewrite)
Theorem:
(defthm modinstlist-p-of-vl-vardecllist->svex.modinsts (b* (((mv ?vttree ?width ?wires ?fixups ?aliases ?modinsts ?assigns ?modalist1) (vl-vardecllist->svex x portdecls modalist interfacep ss scopes config))) (sv::modinstlist-p modinsts)) :rule-classes :rewrite)
Theorem:
(defthm assigns-p-of-vl-vardecllist->svex.assigns (b* (((mv ?vttree ?width ?wires ?fixups ?aliases ?modinsts ?assigns ?modalist1) (vl-vardecllist->svex x portdecls modalist interfacep ss scopes config))) (sv::assigns-p assigns)) :rule-classes :rewrite)
Theorem:
(defthm modalist-p-of-vl-vardecllist->svex.modalist1 (b* (((mv ?vttree ?width ?wires ?fixups ?aliases ?modinsts ?assigns ?modalist1) (vl-vardecllist->svex x portdecls modalist interfacep ss scopes config))) (sv::modalist-p modalist1)) :rule-classes :rewrite)
Theorem:
(defthm vars-of-vl-vardecllist->svex-modalist (b* (((mv ?vttree ?width ?wires ?fixups ?aliases ?modinsts ?assigns ?modalist1) (vl-vardecllist->svex x portdecls modalist interfacep ss scopes config))) (implies (sv::svarlist-addr-p (sv::modalist-vars modalist)) (sv::svarlist-addr-p (sv::modalist-vars modalist1)))))
Theorem:
(defthm vars-of-vl-vardecllist->svex-aliases (b* (((mv ?vttree ?width ?wires ?fixups ?aliases ?modinsts ?assigns ?modalist1) (vl-vardecllist->svex x portdecls modalist interfacep ss scopes config))) (sv::svarlist-addr-p (sv::lhspairs-vars aliases))))
Theorem:
(defthm vars-of-vl-vardecllist->svex-fixups (b* (((mv ?vttree ?width ?wires ?fixups ?aliases ?modinsts ?assigns ?modalist1) (vl-vardecllist->svex x portdecls modalist interfacep ss scopes config))) (sv::svarlist-addr-p (sv::assigns-vars fixups))))
Theorem:
(defthm vars-of-vl-vardecllist->svex-assigns (b* (((mv ?vttree ?width ?wires ?fixups ?aliases ?modinsts ?assigns ?modalist1) (vl-vardecllist->svex x portdecls modalist interfacep ss scopes config))) (sv::svarlist-addr-p (sv::assigns-vars assigns))))
Theorem:
(defthm vl-vardecllist->svex-of-vl-vardecllist-fix-x (equal (vl-vardecllist->svex (vl-vardecllist-fix x) portdecls modalist interfacep ss scopes config) (vl-vardecllist->svex x portdecls modalist interfacep ss scopes config)))
Theorem:
(defthm vl-vardecllist->svex-vl-vardecllist-equiv-congruence-on-x (implies (vl-vardecllist-equiv x x-equiv) (equal (vl-vardecllist->svex x portdecls modalist interfacep ss scopes config) (vl-vardecllist->svex x-equiv portdecls modalist interfacep ss scopes config))) :rule-classes :congruence)
Theorem:
(defthm vl-vardecllist->svex-of-modalist-fix-modalist (equal (vl-vardecllist->svex x portdecls (sv::modalist-fix modalist) interfacep ss scopes config) (vl-vardecllist->svex x portdecls modalist interfacep ss scopes config)))
Theorem:
(defthm vl-vardecllist->svex-modalist-equiv-congruence-on-modalist (implies (sv::modalist-equiv modalist modalist-equiv) (equal (vl-vardecllist->svex x portdecls modalist interfacep ss scopes config) (vl-vardecllist->svex x portdecls modalist-equiv interfacep ss scopes config))) :rule-classes :congruence)
Theorem:
(defthm vl-vardecllist->svex-of-vl-scopestack-fix-ss (equal (vl-vardecllist->svex x portdecls modalist interfacep (vl-scopestack-fix ss) scopes config) (vl-vardecllist->svex x portdecls modalist interfacep ss scopes config)))
Theorem:
(defthm vl-vardecllist->svex-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-vardecllist->svex x portdecls modalist interfacep ss scopes config) (vl-vardecllist->svex x portdecls modalist interfacep ss-equiv scopes config))) :rule-classes :congruence)
Theorem:
(defthm vl-vardecllist->svex-of-vl-elabscopes-fix-scopes (equal (vl-vardecllist->svex x portdecls modalist interfacep ss (vl-elabscopes-fix scopes) config) (vl-vardecllist->svex x portdecls modalist interfacep ss scopes config)))
Theorem:
(defthm vl-vardecllist->svex-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-vardecllist->svex x portdecls modalist interfacep ss scopes config) (vl-vardecllist->svex x portdecls modalist interfacep ss scopes-equiv config))) :rule-classes :congruence)
Theorem:
(defthm vl-vardecllist->svex-of-vl-simpconfig-fix-config (equal (vl-vardecllist->svex x portdecls modalist interfacep ss scopes (vl-simpconfig-fix config)) (vl-vardecllist->svex x portdecls modalist interfacep ss scopes config)))
Theorem:
(defthm vl-vardecllist->svex-vl-simpconfig-equiv-congruence-on-config (implies (vl-simpconfig-equiv config config-equiv) (equal (vl-vardecllist->svex x portdecls modalist interfacep ss scopes config) (vl-vardecllist->svex x portdecls modalist interfacep ss scopes config-equiv))) :rule-classes :congruence)