(vl-atts->svex x allowed-atts ss scopes) → (mv atts warnings)
Function:
(defun vl-atts->svex (x allowed-atts ss scopes) (declare (xargs :guard (and (vl-atts-p x) (string-listp allowed-atts) (vl-scopestack-p ss) (vl-elabscopes-p scopes)))) (let ((__function__ 'vl-atts->svex)) (declare (ignorable __function__)) (b* ((x (vl-atts-fix x)) ((when (atom x)) (mv nil nil)) ((unless (member-equal (caar x) (string-list-fix allowed-atts))) (vl-atts->svex (cdr x) allowed-atts ss scopes)) ((mv val warnings) (if (cdar x) (b* (((mv vttree svex ?type size) (vl-expr-to-svex-untyped (cdar x) ss scopes)) (svex (if size (sv::svex-concat size (sv::svex-lhsrewrite svex size) (sv::svex-z)) svex))) (mv svex (vttree->warnings vttree))) (mv nil nil))) ((wmv rest warnings) (vl-atts->svex (cdr x) allowed-atts ss scopes))) (mv (cons (cons (caar x) val) rest) warnings))))
Theorem:
(defthm attributes-p-of-vl-atts->svex.atts (b* (((mv ?atts ?warnings) (vl-atts->svex x allowed-atts ss scopes))) (sv::attributes-p atts)) :rule-classes :rewrite)
Theorem:
(defthm vl-warninglist-p-of-vl-atts->svex.warnings (b* (((mv ?atts ?warnings) (vl-atts->svex x allowed-atts ss scopes))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-atts->svex-of-vl-atts-fix-x (equal (vl-atts->svex (vl-atts-fix x) allowed-atts ss scopes) (vl-atts->svex x allowed-atts ss scopes)))
Theorem:
(defthm vl-atts->svex-vl-atts-equiv-congruence-on-x (implies (vl-atts-equiv x x-equiv) (equal (vl-atts->svex x allowed-atts ss scopes) (vl-atts->svex x-equiv allowed-atts ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-atts->svex-of-string-list-fix-allowed-atts (equal (vl-atts->svex x (string-list-fix allowed-atts) ss scopes) (vl-atts->svex x allowed-atts ss scopes)))
Theorem:
(defthm vl-atts->svex-string-list-equiv-congruence-on-allowed-atts (implies (str::string-list-equiv allowed-atts allowed-atts-equiv) (equal (vl-atts->svex x allowed-atts ss scopes) (vl-atts->svex x allowed-atts-equiv ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-atts->svex-of-vl-scopestack-fix-ss (equal (vl-atts->svex x allowed-atts (vl-scopestack-fix ss) scopes) (vl-atts->svex x allowed-atts ss scopes)))
Theorem:
(defthm vl-atts->svex-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-atts->svex x allowed-atts ss scopes) (vl-atts->svex x allowed-atts ss-equiv scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-atts->svex-of-vl-elabscopes-fix-scopes (equal (vl-atts->svex x allowed-atts ss (vl-elabscopes-fix scopes)) (vl-atts->svex x allowed-atts ss scopes)))
Theorem:
(defthm vl-atts->svex-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-atts->svex x allowed-atts ss scopes) (vl-atts->svex x allowed-atts ss scopes-equiv))) :rule-classes :congruence)