(vl-shadowcheck-reference-name name ctx st warnings) → (mv st warnings)
Function:
(defun vl-shadowcheck-reference-name (name ctx st warnings) (declare (xargs :guard (and (stringp name) (acl2::any-p ctx) (vl-shadowcheck-state-p st) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-shadowcheck-reference-name)) (declare (ignorable __function__)) (b* ((name (string-fix name)) ((vl-shadowcheck-state st) (vl-shadowcheck-state-fix st)) (- (vl-shadowcheck-debug " vl-shadowcheck-reference-name: ~s0 for ~a1.~%" name ctx)) ((mv entry tail) (vl-lexscopes-find name st.lexscopes)) ((unless entry) (mv st (fatal :type :vl-undeclared-identifier :msg "~a0: reference to undeclared identifier ~s1.~%" :args (list ctx name)))) ((vl-lexscope-entry entry)) ((when (and (not entry.decl) (not entry.direct-pkg) (>= (len entry.wildpkgs) 2))) (mv st (fatal :type :vl-illegal-import :msg "~a0: the name ~s1 is imported by multiple wildcard ~ imports: ~&2." :args (list ctx name entry.wildpkgs)))) ((mv item scopestack-at-import pkg-name) (vl-scopestack-find-item/context name st.ss)) ((unless (or item pkg-name)) (mv st (fatal :type :vl-programming-error :msg "~a0: scopestack can't resolve ~s1 but it is found ~ in the lexical scope, so how could that happen? ~x2." :args (list ctx name entry)))) (ss-level (vl-scopestack-nesting-level scopestack-at-import)) (lex-level (len tail)) ((unless (equal ss-level lex-level)) (mv st (fatal :type :vl-tricky-scope :msg "~a0: the name ~s1 has complex scoping that we do not ~ support. Lexical level ~x2, scopestack level ~x3." :args (list ctx name lex-level ss-level)))) ((unless pkg-name) (b* (((unless entry.decl) (mv st (fatal :type :vl-tricky-scope :msg "~a0: the name ~s1 has complex scoping that ~ we do not support. Lexically it appears to ~ be imported from a package, but there is a ~ subsequent declaration (~a2) which makes ~ scoping confusing." :args (list ctx name item))))) (mv st (ok)))) ((when entry.decl) (mv st (fatal :type :vl-programming-error :msg "~a0: scopestack thinks ~s1 is imported from ~s2 ~ but lexically it seems to be locally declared, ~ ~a3." :args (list ctx name pkg-name entry.decl)))) ((when entry.direct-pkg) (b* (((unless (equal entry.direct-pkg pkg-name)) (mv st (fatal :type :vl-import-conflict :msg "~a0: scopestack thinks ~s1 is imported from ~ ~s2, but lexically it is directly imported from ~s3." :args (list ctx name pkg-name entry.direct-pkg))))) (mv st (ok)))) ((unless (consp entry.wildpkgs)) (mv st (fatal :type :vl-programming-error :msg "~a0: name ~s1 has a lexscope entry with no local ~ declaration, direct package, or wild packages. ~ How did this happen?" :args (list ctx name)))) (lex-pkg (and (mbt (equal (len entry.wildpkgs) 1)) (first entry.wildpkgs))) ((unless (equal lex-pkg pkg-name)) (mv st (fatal :type :vl-import-conflict :msg "~a0: scopestack thinks ~s1 is imported from ~s2, ~ but lexically it is wildly imported from ~s3." :args (list ctx name pkg-name lex-pkg))))) (mv st (ok)))))
Theorem:
(defthm vl-shadowcheck-state-p-of-vl-shadowcheck-reference-name.st (b* (((mv ?st ?warnings) (vl-shadowcheck-reference-name name ctx st warnings))) (vl-shadowcheck-state-p st)) :rule-classes :rewrite)
Theorem:
(defthm vl-warninglist-p-of-vl-shadowcheck-reference-name.warnings (b* (((mv ?st ?warnings) (vl-shadowcheck-reference-name name ctx st warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-shadowcheck-reference-name-of-str-fix-name (equal (vl-shadowcheck-reference-name (str-fix name) ctx st warnings) (vl-shadowcheck-reference-name name ctx st warnings)))
Theorem:
(defthm vl-shadowcheck-reference-name-streqv-congruence-on-name (implies (streqv name name-equiv) (equal (vl-shadowcheck-reference-name name ctx st warnings) (vl-shadowcheck-reference-name name-equiv ctx st warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-shadowcheck-reference-name-of-identity-ctx (equal (vl-shadowcheck-reference-name name (identity ctx) st warnings) (vl-shadowcheck-reference-name name ctx st warnings)))
Theorem:
(defthm vl-shadowcheck-reference-name-equal-congruence-on-ctx (implies (equal ctx ctx-equiv) (equal (vl-shadowcheck-reference-name name ctx st warnings) (vl-shadowcheck-reference-name name ctx-equiv st warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-shadowcheck-reference-name-of-vl-shadowcheck-state-fix-st (equal (vl-shadowcheck-reference-name name ctx (vl-shadowcheck-state-fix st) warnings) (vl-shadowcheck-reference-name name ctx st warnings)))
Theorem:
(defthm vl-shadowcheck-reference-name-vl-shadowcheck-state-equiv-congruence-on-st (implies (vl-shadowcheck-state-equiv st st-equiv) (equal (vl-shadowcheck-reference-name name ctx st warnings) (vl-shadowcheck-reference-name name ctx st-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-shadowcheck-reference-name-of-vl-warninglist-fix-warnings (equal (vl-shadowcheck-reference-name name ctx st (vl-warninglist-fix warnings)) (vl-shadowcheck-reference-name name ctx st warnings)))
Theorem:
(defthm vl-shadowcheck-reference-name-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-shadowcheck-reference-name name ctx st warnings) (vl-shadowcheck-reference-name name ctx st warnings-equiv))) :rule-classes :congruence)