Turn a VL alias into an SVEX alias.
(vl-alias->svex-alias x ss scopes) → (mv vttree aliases)
This just straightforwardly converts the LHS and RHS to svex expressions, then sv::lhs-p objects.
Function:
(defun vl-alias->svex-alias (x ss scopes) (declare (xargs :guard (and (vl-alias-p x) (vl-scopestack-p ss) (vl-elabscopes-p scopes)))) (let ((__function__ 'vl-alias->svex-alias)) (declare (ignorable __function__)) (b* (((vl-alias x) (vl-alias-fix x)) (vttree nil) ((vmv vttree lhs lhs-type :ctx x) (vl-expr-to-svex-lhs x.lhs ss scopes)) ((vmv vttree rhs rhs-type :ctx x) (vl-expr-to-svex-lhs x.rhs ss scopes)) ((unless (and lhs-type rhs-type)) (mv vttree nil)) (err (vl-check-datatype-compatibility lhs-type rhs-type :equiv)) ((when err) (mv (vfatal :type :vl-bad-alias :msg "~a0: Incompatible LHS/RHS types: ~@1." :args (list x err)) nil))) (mv vttree (list (cons lhs rhs))))))
Theorem:
(defthm return-type-of-vl-alias->svex-alias.vttree (b* (((mv ?vttree ?aliases) (vl-alias->svex-alias x ss scopes))) (and (vttree-p vttree) (sv::svarlist-addr-p (sv::constraintlist-vars (vttree->constraints vttree))))) :rule-classes :rewrite)
Theorem:
(defthm lhspairs-p-of-vl-alias->svex-alias.aliases (b* (((mv ?vttree ?aliases) (vl-alias->svex-alias x ss scopes))) (sv::lhspairs-p aliases)) :rule-classes :rewrite)
Theorem:
(defthm vl-alias->svex-alias-mvtypes-1 (true-listp (mv-nth 1 (vl-alias->svex-alias x ss scopes))) :rule-classes :type-prescription)
Theorem:
(defthm vars-of-vl-alias->svex-alias (b* (((mv ?vttree ?aliases) (vl-alias->svex-alias x ss scopes))) (sv::svarlist-addr-p (sv::lhspairs-vars aliases))))
Theorem:
(defthm vl-alias->svex-alias-of-vl-alias-fix-x (equal (vl-alias->svex-alias (vl-alias-fix x) ss scopes) (vl-alias->svex-alias x ss scopes)))
Theorem:
(defthm vl-alias->svex-alias-vl-alias-equiv-congruence-on-x (implies (vl-alias-equiv x x-equiv) (equal (vl-alias->svex-alias x ss scopes) (vl-alias->svex-alias x-equiv ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-alias->svex-alias-of-vl-scopestack-fix-ss (equal (vl-alias->svex-alias x (vl-scopestack-fix ss) scopes) (vl-alias->svex-alias x ss scopes)))
Theorem:
(defthm vl-alias->svex-alias-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-alias->svex-alias x ss scopes) (vl-alias->svex-alias x ss-equiv scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-alias->svex-alias-of-vl-elabscopes-fix-scopes (equal (vl-alias->svex-alias x ss (vl-elabscopes-fix scopes)) (vl-alias->svex-alias x ss scopes)))
Theorem:
(defthm vl-alias->svex-alias-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-alias->svex-alias x ss scopes) (vl-alias->svex-alias x ss scopes-equiv))) :rule-classes :congruence)