Check an arbitrary vl-stmt-p for uses of undeclared names.
(vl-stmt-check-undeclared ctx x st warnings) → new-warnings
Most statements are totally straightforward; we just need to make sure that all identifiers used anywhere within them have been declared.
Named blocks are the only complication. They have their own scope and can have their own declarations and imports, which come before their sub-statements. So, if we see a named block, we basically fork the decls and imports to create a local namespace, add all of the local declarations to it, and then check all the sub-statements in this extended namespace.
Theorem:
(defthm return-type-of-vl-stmt-check-undeclared.new-warnings (b* ((?new-warnings (vl-stmt-check-undeclared ctx x st warnings))) (vl-warninglist-p new-warnings)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-stmtlist-check-undeclared.new-warnings (b* ((?new-warnings (vl-stmtlist-check-undeclared ctx x st warnings))) (vl-warninglist-p new-warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-stmt-check-undeclared-of-vl-modelement-fix-ctx (equal (vl-stmt-check-undeclared (vl-modelement-fix ctx) x st warnings) (vl-stmt-check-undeclared ctx x st warnings)))
Theorem:
(defthm vl-stmt-check-undeclared-of-vl-stmt-fix-x (equal (vl-stmt-check-undeclared ctx (vl-stmt-fix x) st warnings) (vl-stmt-check-undeclared ctx x st warnings)))
Theorem:
(defthm vl-stmt-check-undeclared-of-vl-implicitst-fix-st (equal (vl-stmt-check-undeclared ctx x (vl-implicitst-fix st) warnings) (vl-stmt-check-undeclared ctx x st warnings)))
Theorem:
(defthm vl-stmt-check-undeclared-of-vl-warninglist-fix-warnings (equal (vl-stmt-check-undeclared ctx x st (vl-warninglist-fix warnings)) (vl-stmt-check-undeclared ctx x st warnings)))
Theorem:
(defthm vl-stmtlist-check-undeclared-of-vl-modelement-fix-ctx (equal (vl-stmtlist-check-undeclared (vl-modelement-fix ctx) x st warnings) (vl-stmtlist-check-undeclared ctx x st warnings)))
Theorem:
(defthm vl-stmtlist-check-undeclared-of-vl-stmtlist-fix-x (equal (vl-stmtlist-check-undeclared ctx (vl-stmtlist-fix x) st warnings) (vl-stmtlist-check-undeclared ctx x st warnings)))
Theorem:
(defthm vl-stmtlist-check-undeclared-of-vl-implicitst-fix-st (equal (vl-stmtlist-check-undeclared ctx x (vl-implicitst-fix st) warnings) (vl-stmtlist-check-undeclared ctx x st warnings)))
Theorem:
(defthm vl-stmtlist-check-undeclared-of-vl-warninglist-fix-warnings (equal (vl-stmtlist-check-undeclared ctx x st (vl-warninglist-fix warnings)) (vl-stmtlist-check-undeclared ctx x st warnings)))
Theorem:
(defthm vl-stmt-check-undeclared-vl-modelement-equiv-congruence-on-ctx (implies (vl-modelement-equiv ctx ctx-equiv) (equal (vl-stmt-check-undeclared ctx x st warnings) (vl-stmt-check-undeclared ctx-equiv x st warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-stmt-check-undeclared-vl-stmt-equiv-congruence-on-x (implies (vl-stmt-equiv x x-equiv) (equal (vl-stmt-check-undeclared ctx x st warnings) (vl-stmt-check-undeclared ctx x-equiv st warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-stmt-check-undeclared-vl-implicitst-equiv-congruence-on-st (implies (vl-implicitst-equiv st st-equiv) (equal (vl-stmt-check-undeclared ctx x st warnings) (vl-stmt-check-undeclared ctx x st-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-stmt-check-undeclared-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-stmt-check-undeclared ctx x st warnings) (vl-stmt-check-undeclared ctx x st warnings-equiv))) :rule-classes :congruence)
Theorem:
(defthm vl-stmtlist-check-undeclared-vl-modelement-equiv-congruence-on-ctx (implies (vl-modelement-equiv ctx ctx-equiv) (equal (vl-stmtlist-check-undeclared ctx x st warnings) (vl-stmtlist-check-undeclared ctx-equiv x st warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-stmtlist-check-undeclared-vl-stmtlist-equiv-congruence-on-x (implies (vl-stmtlist-equiv x x-equiv) (equal (vl-stmtlist-check-undeclared ctx x st warnings) (vl-stmtlist-check-undeclared ctx x-equiv st warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-stmtlist-check-undeclared-vl-implicitst-equiv-congruence-on-st (implies (vl-implicitst-equiv st st-equiv) (equal (vl-stmtlist-check-undeclared ctx x st warnings) (vl-stmtlist-check-undeclared ctx x st-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-stmtlist-check-undeclared-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-stmtlist-check-undeclared ctx x st warnings) (vl-stmtlist-check-undeclared ctx x st warnings-equiv))) :rule-classes :congruence)