Generate a (fast) wirealist from a vl-vardecllist-p.
(vl-vardecllist-to-wirealist x warnings) → (mv successp warnings wire-alist)
Function:
(defun vl-vardecllist-to-wirealist (x warnings) (declare (xargs :guard (and (vl-vardecllist-p x) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-vardecllist-to-wirealist)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv t (ok) nil)) ((mv successp1 warnings wires1) (vl-vardecl-msb-emodwires (car x) warnings)) ((mv successp2 warnings walist) (vl-vardecllist-to-wirealist (cdr x) warnings)) (successp (and successp1 successp2)) (walist (if successp1 (hons-acons (vl-vardecl->name (car x)) wires1 walist) walist))) (mv successp warnings walist))))
Theorem:
(defthm booleanp-of-vl-vardecllist-to-wirealist.successp (b* (((mv ?successp ?warnings ?wire-alist) (vl-vardecllist-to-wirealist x warnings))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-vardecllist-to-wirealist.warnings (b* (((mv ?successp ?warnings ?wire-alist) (vl-vardecllist-to-wirealist x warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-wirealist-p-of-vl-vardecllist-to-wirealist.wire-alist (b* (((mv ?successp ?warnings ?wire-alist) (vl-vardecllist-to-wirealist x warnings))) (vl-wirealist-p wire-alist)) :rule-classes :rewrite)
Theorem:
(defthm subsetp-equal-of-strip-cars-of-vl-vardecllist-to-wirealist (subsetp-equal (strip-cars (mv-nth 2 (vl-vardecllist-to-wirealist x warnings))) (vl-vardecllist->names x)))