(vl-portlist-reasonable-p x) determines if a vl-portlist-p is reasonable.
We just require that any externally visible names are unique. A number of additional well-formedness checks are done in argresolve and e-conversion.
Function:
(defun vl-portlist-reasonable-p (x) (declare (xargs :guard (vl-portlist-p x))) (let* ((names (remove nil (vl-portlist->names x))) (dupes (duplicated-members names))) (if (not dupes) t nil)))
Function:
(defun vl-portlist-reasonable-p-warn (x warnings) (declare (xargs :guard (and (vl-portlist-p x) (vl-warninglist-p warnings))) (ignorable warnings)) (let* ((names (remove nil (vl-portlist->names x))) (dupes (duplicated-members names))) (if (not dupes) (mv t warnings) (mv nil (cons (make-vl-warning :type :vl-bad-ports :msg "Duplicate port names: ~&0." :args (list dupes)) warnings)))))
Theorem:
(defthm eliminate-vl-portlist-reasonable-p-warn (equal (mv-nth 0 (vl-portlist-reasonable-p-warn x warnings)) (vl-portlist-reasonable-p x)))
Theorem:
(defthm vl-warninglist-p-of-vl-portlist-reasonable-p-warn (implies (force (vl-warninglist-p warnings)) (vl-warninglist-p (mv-nth 1 (vl-portlist-reasonable-p-warn x warnings)))))