Collects svex module components for a list of aliases by collecting results from vl-alias->svex-alias.
(vl-aliases->svex-aliases x ss scopes aliases) → (mv vttree aliases1)
Function:
(defun vl-aliases->svex-aliases (x ss scopes aliases) (declare (xargs :guard (and (vl-aliaslist-p x) (vl-scopestack-p ss) (vl-elabscopes-p scopes) (sv::lhspairs-p aliases)))) (let ((__function__ 'vl-aliases->svex-aliases)) (declare (ignorable __function__)) (if (atom x) (mv nil (sv::lhspairs-fix aliases)) (b* ((vttree nil) ((vmv vttree aliases1) (vl-alias->svex-alias (car x) ss scopes)) ((vmv vttree aliases) (vl-aliases->svex-aliases (cdr x) ss scopes (append aliases1 aliases)))) (mv vttree aliases)))))
Theorem:
(defthm return-type-of-vl-aliases->svex-aliases.vttree (b* (((mv ?vttree ?aliases1) (vl-aliases->svex-aliases x ss scopes aliases))) (and (vttree-p vttree) (sv::svarlist-addr-p (sv::constraintlist-vars (vttree->constraints vttree))))) :rule-classes :rewrite)
Theorem:
(defthm lhspairs-p-of-vl-aliases->svex-aliases.aliases1 (b* (((mv ?vttree ?aliases1) (vl-aliases->svex-aliases x ss scopes aliases))) (sv::lhspairs-p aliases1)) :rule-classes :rewrite)
Theorem:
(defthm vars-of-vl-aliases->svex-aliases-aliases (b* (((mv ?vttree ?aliases1) (vl-aliases->svex-aliases x ss scopes aliases))) (implies (sv::svarlist-addr-p (sv::lhspairs-vars aliases)) (sv::svarlist-addr-p (sv::lhspairs-vars aliases1)))) :rule-classes :rewrite)
Theorem:
(defthm vl-aliases->svex-aliases-of-vl-aliaslist-fix-x (equal (vl-aliases->svex-aliases (vl-aliaslist-fix x) ss scopes aliases) (vl-aliases->svex-aliases x ss scopes aliases)))
Theorem:
(defthm vl-aliases->svex-aliases-vl-aliaslist-equiv-congruence-on-x (implies (vl-aliaslist-equiv x x-equiv) (equal (vl-aliases->svex-aliases x ss scopes aliases) (vl-aliases->svex-aliases x-equiv ss scopes aliases))) :rule-classes :congruence)
Theorem:
(defthm vl-aliases->svex-aliases-of-vl-scopestack-fix-ss (equal (vl-aliases->svex-aliases x (vl-scopestack-fix ss) scopes aliases) (vl-aliases->svex-aliases x ss scopes aliases)))
Theorem:
(defthm vl-aliases->svex-aliases-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-aliases->svex-aliases x ss scopes aliases) (vl-aliases->svex-aliases x ss-equiv scopes aliases))) :rule-classes :congruence)
Theorem:
(defthm vl-aliases->svex-aliases-of-vl-elabscopes-fix-scopes (equal (vl-aliases->svex-aliases x ss (vl-elabscopes-fix scopes) aliases) (vl-aliases->svex-aliases x ss scopes aliases)))
Theorem:
(defthm vl-aliases->svex-aliases-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-aliases->svex-aliases x ss scopes aliases) (vl-aliases->svex-aliases x ss scopes-equiv aliases))) :rule-classes :congruence)
Theorem:
(defthm vl-aliases->svex-aliases-of-lhspairs-fix-aliases (equal (vl-aliases->svex-aliases x ss scopes (sv::lhspairs-fix aliases)) (vl-aliases->svex-aliases x ss scopes aliases)))
Theorem:
(defthm vl-aliases->svex-aliases-lhspairs-equiv-congruence-on-aliases (implies (sv::lhspairs-equiv aliases aliases-equiv) (equal (vl-aliases->svex-aliases x ss scopes aliases) (vl-aliases->svex-aliases x ss scopes aliases-equiv))) :rule-classes :congruence)