Function:
(defun vl-module-reasonable-p (x) (declare (xargs :guard (vl-module-p x))) (b* (((vl-module x) x) (pdnames (vl-portdecllist->names x.portdecls)) (pdnames-s (mergesort pdnames)) (namespace (vl-module->modnamespace x)) (namespace-s (mergesort namespace)) (overlap (intersect pdnames-s namespace-s)) (palist (vl-make-portdecl-alist x.portdecls)) (ialist (vl-make-moditem-alist x))) (and (vl-portlist-reasonable-p x.ports) (vl-vardecllist-reasonable-p x.vardecls) t (if (mbe :logic (no-duplicatesp-equal namespace) :exec (same-lengthp namespace namespace-s)) t nil) (vl-overlap-compatible-p overlap x palist ialist))))
Function:
(defun vl-module-reasonable-p-warn (x warnings) (declare (xargs :guard (and (vl-module-p x) (vl-warninglist-p warnings))) (ignorable warnings)) (b* (((vl-module x) x) (pdnames (vl-portdecllist->names x.portdecls)) (pdnames-s (mergesort pdnames)) (namespace (vl-module->modnamespace x)) (namespace-s (mergesort namespace)) (overlap (intersect pdnames-s namespace-s)) (palist (vl-make-portdecl-alist x.portdecls)) (ialist (vl-make-moditem-alist x))) (b* (((mv __ok1__ warnings) (vl-portlist-reasonable-p-warn x.ports warnings)) ((mv __ok2__ warnings) (b* (((mv __ok1__ warnings) (vl-vardecllist-reasonable-p-warn x.vardecls warnings)) ((mv __ok2__ warnings) (b* (((mv __ok1__ warnings) (if (not x.initials) (mv t warnings) (mv t (cons (make-vl-warning :type :vl-initial-stmts :msg "~l0: module ~s1 contains initial statements." :args (list x.minloc x.name)) warnings)))) ((mv __ok2__ warnings) (b* (((mv __ok1__ warnings) (if (mbe :logic (no-duplicatesp-equal namespace) :exec (same-lengthp namespace namespace-s)) (mv t warnings) (mv nil (cons (make-vl-warning :type :vl-namespace-error :msg "~l0: ~s1 illegally redefines ~&2." :args (list x.minloc x.name (duplicated-members namespace))) warnings)))) ((mv __ok2__ warnings) (b* (((mv __ok1__ warnings) (vl-overlap-compatible-p-warn overlap x palist ialist warnings)) ((mv __ok2__ warnings) (mv t warnings))) (mv (and __ok1__ __ok2__) warnings)))) (mv (and __ok1__ __ok2__) warnings)))) (mv (and __ok1__ __ok2__) warnings)))) (mv (and __ok1__ __ok2__) warnings)))) (mv (and __ok1__ __ok2__) warnings))))
Theorem:
(defthm eliminate-vl-module-reasonable-p-warn (equal (mv-nth 0 (vl-module-reasonable-p-warn x warnings)) (vl-module-reasonable-p x)))
Theorem:
(defthm vl-warninglist-p-of-vl-module-reasonable-p-warn (implies (force (vl-warninglist-p warnings)) (vl-warninglist-p (mv-nth 1 (vl-module-reasonable-p-warn x warnings)))))