(vl-shadowcheck-reference-scopeexpr x ctx st warnings) → (mv st warnings)
Function:
(defun vl-shadowcheck-reference-scopeexpr (x ctx st warnings) (declare (xargs :guard (and (vl-scopeexpr-p x) (any-p ctx) (vl-shadowcheck-state-p st) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-shadowcheck-reference-scopeexpr)) (declare (ignorable __function__)) (b* ((st (vl-shadowcheck-state-fix st)) (warnings (vl-warninglist-fix warnings))) (vl-scopeexpr-case x :colon (mv st warnings) :end (vl-hidexpr-case x.hid :end (vl-shadowcheck-reference-name x.hid.name ctx st warnings) :dot (b* ((name (vl-hidindex->name x.hid.first)) ((unless (stringp name)) (mv st warnings)) ((vl-shadowcheck-state st)) ((when (vl-scopestack-find-definition name st.ss)) (mv st warnings))) (vl-shadowcheck-reference-name name ctx st warnings)))))))
Theorem:
(defthm vl-shadowcheck-state-p-of-vl-shadowcheck-reference-scopeexpr.st (b* (((mv ?st ?warnings) (vl-shadowcheck-reference-scopeexpr x ctx st warnings))) (vl-shadowcheck-state-p st)) :rule-classes :rewrite)
Theorem:
(defthm vl-warninglist-p-of-vl-shadowcheck-reference-scopeexpr.warnings (b* (((mv ?st ?warnings) (vl-shadowcheck-reference-scopeexpr x ctx st warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-shadowcheck-reference-scopeexpr-of-vl-scopeexpr-fix-x (equal (vl-shadowcheck-reference-scopeexpr (vl-scopeexpr-fix x) ctx st warnings) (vl-shadowcheck-reference-scopeexpr x ctx st warnings)))
Theorem:
(defthm vl-shadowcheck-reference-scopeexpr-vl-scopeexpr-equiv-congruence-on-x (implies (vl-scopeexpr-equiv x x-equiv) (equal (vl-shadowcheck-reference-scopeexpr x ctx st warnings) (vl-shadowcheck-reference-scopeexpr x-equiv ctx st warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-shadowcheck-reference-scopeexpr-of-identity-ctx (equal (vl-shadowcheck-reference-scopeexpr x (identity ctx) st warnings) (vl-shadowcheck-reference-scopeexpr x ctx st warnings)))
Theorem:
(defthm vl-shadowcheck-reference-scopeexpr-equal-congruence-on-ctx (implies (equal ctx ctx-equiv) (equal (vl-shadowcheck-reference-scopeexpr x ctx st warnings) (vl-shadowcheck-reference-scopeexpr x ctx-equiv st warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-shadowcheck-reference-scopeexpr-of-vl-shadowcheck-state-fix-st (equal (vl-shadowcheck-reference-scopeexpr x ctx (vl-shadowcheck-state-fix st) warnings) (vl-shadowcheck-reference-scopeexpr x ctx st warnings)))
Theorem:
(defthm vl-shadowcheck-reference-scopeexpr-vl-shadowcheck-state-equiv-congruence-on-st (implies (vl-shadowcheck-state-equiv st st-equiv) (equal (vl-shadowcheck-reference-scopeexpr x ctx st warnings) (vl-shadowcheck-reference-scopeexpr x ctx st-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-shadowcheck-reference-scopeexpr-of-vl-warninglist-fix-warnings (equal (vl-shadowcheck-reference-scopeexpr x ctx st (vl-warninglist-fix warnings)) (vl-shadowcheck-reference-scopeexpr x ctx st warnings)))
Theorem:
(defthm vl-shadowcheck-reference-scopeexpr-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-shadowcheck-reference-scopeexpr x ctx st warnings) (vl-shadowcheck-reference-scopeexpr x ctx st warnings-equiv))) :rule-classes :congruence)