Check an arbitrary vl-taskdecl-p for uses of undeclared names.
(vl-taskdecl-check-undeclared x st warnings) → new-warnings
This is nearly identical to vl-fundecl-check-undeclared and it has the same problems with parameters.
Function:
(defun vl-taskdecl-check-undeclared (x st warnings) (declare (xargs :guard (and (vl-taskdecl-p x) (vl-implicitst-p st) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-taskdecl-check-undeclared)) (declare (ignorable __function__)) (b* ((x (vl-taskdecl-fix x)) ((vl-taskdecl x) x) (other-names (vl-exprlist-varnames (vl-portdecllist-allexprs x.portdecls))) (warnings (vl-warn-about-undeclared-wires x other-names st warnings)) (local-decls (hons-shrink-alist (vl-implicitst->decls st) nil)) (local-imports (hons-shrink-alist (vl-implicitst->imports st) nil)) (local-st (change-vl-implicitst st :decls local-decls :imports local-imports)) ((mv warnings local-st) (vl-blockitemlist-check-undeclared x.blockitems local-st warnings)) (local-decls (vl-implicitst->decls local-st)) (local-decls (make-fal (pairlis$ (vl-portdecllist->names x.portdecls) nil) local-decls)) (local-st (change-vl-implicitst local-st :decls local-decls)) (warnings (vl-stmt-check-undeclared x x.body local-st warnings))) (fast-alist-free local-decls) warnings)))
Theorem:
(defthm vl-warninglist-p-of-vl-taskdecl-check-undeclared (b* ((new-warnings (vl-taskdecl-check-undeclared x st warnings))) (vl-warninglist-p new-warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-taskdecl-check-undeclared-of-vl-taskdecl-fix-x (equal (vl-taskdecl-check-undeclared (vl-taskdecl-fix x) st warnings) (vl-taskdecl-check-undeclared x st warnings)))
Theorem:
(defthm vl-taskdecl-check-undeclared-vl-taskdecl-equiv-congruence-on-x (implies (vl-taskdecl-equiv x x-equiv) (equal (vl-taskdecl-check-undeclared x st warnings) (vl-taskdecl-check-undeclared x-equiv st warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-taskdecl-check-undeclared-of-vl-implicitst-fix-st (equal (vl-taskdecl-check-undeclared x (vl-implicitst-fix st) warnings) (vl-taskdecl-check-undeclared x st warnings)))
Theorem:
(defthm vl-taskdecl-check-undeclared-vl-implicitst-equiv-congruence-on-st (implies (vl-implicitst-equiv st st-equiv) (equal (vl-taskdecl-check-undeclared x st warnings) (vl-taskdecl-check-undeclared x st-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-taskdecl-check-undeclared-of-vl-warninglist-fix-warnings (equal (vl-taskdecl-check-undeclared x st (vl-warninglist-fix warnings)) (vl-taskdecl-check-undeclared x st warnings)))
Theorem:
(defthm vl-taskdecl-check-undeclared-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-taskdecl-check-undeclared x st warnings) (vl-taskdecl-check-undeclared x st warnings-equiv))) :rule-classes :congruence)