Collect all resolved block names in a vl-genelementlist-p.
(vl-genelementlist->blocknames x) → names
Note the elements may be unresolved or may not be blocks at all, in which case we do not add anything. In other words, the list of names returned may be shorter than the number of elements in the list.
Function:
(defun vl-genelementlist->blocknames (x) (declare (xargs :guard (vl-genelementlist-p x))) (let ((__function__ 'vl-genelementlist->blocknames)) (declare (ignorable __function__)) (mbe :logic (if (consp x) (if (vl-genelement->blockname (car x)) (cons (vl-genelement->blockname (car x)) (vl-genelementlist->blocknames (cdr x))) (vl-genelementlist->blocknames (cdr x))) nil) :exec (with-local-nrev (vl-genelementlist->blocknames-nrev x nrev)))))
Theorem:
(defthm string-listp-of-vl-genelementlist->blocknames (b* ((names (vl-genelementlist->blocknames x))) (string-listp names)) :rule-classes :rewrite)
Theorem:
(defthm vl-genelementlist->blocknames-nrev-removal (equal (vl-genelementlist->blocknames-nrev x nrev) (append nrev (vl-genelementlist->blocknames x))))
Theorem:
(defthm vl-genelementlist->blocknames-when-not-consp (implies (not (consp x)) (equal (vl-genelementlist->blocknames x) nil)))
Theorem:
(defthm vl-genelementlist->blocknames-of-cons (equal (vl-genelementlist->blocknames (cons a x)) (if (vl-genelement->blockname a) (cons (vl-genelement->blockname a) (vl-genelementlist->blocknames x)) (vl-genelementlist->blocknames x))))
Theorem:
(defthm vl-genelementlist->blocknames-of-list-fix (equal (vl-genelementlist->blocknames (list-fix x)) (vl-genelementlist->blocknames x)))
Theorem:
(defthm vl-genelementlist->blocknames-preserves-list-equiv (implies (list-equiv x x-equiv) (equal (vl-genelementlist->blocknames x) (vl-genelementlist->blocknames x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm vl-genelementlist->blocknames-of-append (equal (vl-genelementlist->blocknames (append x y)) (append (vl-genelementlist->blocknames x) (vl-genelementlist->blocknames y))))
Theorem:
(defthm vl-genelementlist->blocknames-of-rev (equal (vl-genelementlist->blocknames (rev x)) (rev (vl-genelementlist->blocknames x))))
Theorem:
(defthm vl-genelementlist->blocknames-of-vl-genelementlist-fix-x (equal (vl-genelementlist->blocknames (vl-genelementlist-fix x)) (vl-genelementlist->blocknames x)))
Theorem:
(defthm vl-genelementlist->blocknames-vl-genelementlist-equiv-congruence-on-x (implies (vl-genelementlist-equiv x x-equiv) (equal (vl-genelementlist->blocknames x) (vl-genelementlist->blocknames x-equiv))) :rule-classes :congruence)