Function:
(defun vl-overlap-compatible-p (names x palist ialist) (declare (xargs :guard (and (string-listp names) (vl-module-p x) (equal palist (vl-make-portdecl-alist (vl-module->portdecls x))) (equal ialist (vl-make-moditem-alist x)) (subsetp-equal names (vl-portdecllist->names (vl-module->portdecls x))) (subsetp-equal names (vl-module->modnamespace x))))) (if (atom names) (progn$ (fast-alist-free ialist) (fast-alist-free palist) t) (and (vl-portdecl-and-moduleitem-compatible-p (vl-fast-find-portdecl (car names) (vl-module->portdecls x) palist) (vl-fast-find-moduleitem (car names) x ialist)) (vl-overlap-compatible-p (cdr names) x palist ialist))))
Function:
(defun vl-overlap-compatible-p-warn (names x palist ialist warnings) (declare (xargs :guard (and (and (string-listp names) (vl-module-p x) (equal palist (vl-make-portdecl-alist (vl-module->portdecls x))) (equal ialist (vl-make-moditem-alist x)) (subsetp-equal names (vl-portdecllist->names (vl-module->portdecls x))) (subsetp-equal names (vl-module->modnamespace x))) (vl-warninglist-p warnings))) (ignorable warnings)) (if (atom names) (progn$ (fast-alist-free ialist) (fast-alist-free palist) (mv t warnings)) (b* (((mv __ok1__ warnings) (vl-portdecl-and-moduleitem-compatible-p-warn (vl-fast-find-portdecl (car names) (vl-module->portdecls x) palist) (vl-fast-find-moduleitem (car names) x ialist) warnings)) ((mv __ok2__ warnings) (b* (((mv __ok1__ warnings) (vl-overlap-compatible-p-warn (cdr names) x palist ialist warnings)) ((mv __ok2__ warnings) (mv t warnings))) (mv (and __ok1__ __ok2__) warnings)))) (mv (and __ok1__ __ok2__) warnings))))
Theorem:
(defthm eliminate-vl-overlap-compatible-p-warn (equal (mv-nth 0 (vl-overlap-compatible-p-warn names x palist ialist warnings)) (vl-overlap-compatible-p names x palist ialist)))
Theorem:
(defthm vl-warninglist-p-of-vl-overlap-compatible-p-warn (implies (force (vl-warninglist-p warnings)) (vl-warninglist-p (mv-nth 1 (vl-overlap-compatible-p-warn names x palist ialist warnings)))))