Extend an alist by binding the names of vl-genelements to their definitions.
(vl-genelementlist-alist x acc) → alist
This can be used as an alternative to vl-find-genelement when you need to perform a lot of lookups.
Function:
(defun vl-genelementlist-alist (x acc) (declare (xargs :guard (vl-genelementlist-p x))) (let ((__function__ 'vl-genelementlist-alist)) (declare (ignorable __function__)) (b* (((when (atom x)) acc) (name (hons-copy (vl-genelement->blockname (car x)))) ((when (stringp name)) (cons (cons name (vl-genelement-fix (car x))) (vl-genelementlist-alist (cdr x) acc)))) (vl-genelementlist-alist (cdr x) acc))))
Theorem:
(defthm return-type-of-vl-genelementlist-alist (b* ((alist (vl-genelementlist-alist x acc))) (equal (vl-genelement-alist-p alist) (vl-genelement-alist-p acc))) :rule-classes :rewrite)
Theorem:
(defthm lookup-in-vl-genelementlist-alist-acc-elim (implies (syntaxp (not (equal acc ''nil))) (equal (hons-assoc-equal name (vl-genelementlist-alist x acc)) (or (hons-assoc-equal name (vl-genelementlist-alist x nil)) (hons-assoc-equal name acc)))))
Theorem:
(defthm lookup-in-vl-genelementlist-alist-fast (implies (stringp name) (equal (hons-assoc-equal name (vl-genelementlist-alist x nil)) (let ((val (vl-find-genelement name x))) (and val (cons name val))))))
Theorem:
(defthm vl-genelementlist-alist-of-vl-genelementlist-fix-x (equal (vl-genelementlist-alist (vl-genelementlist-fix x) acc) (vl-genelementlist-alist x acc)))
Theorem:
(defthm vl-genelementlist-alist-vl-genelementlist-equiv-congruence-on-x (implies (vl-genelementlist-equiv x x-equiv) (equal (vl-genelementlist-alist x acc) (vl-genelementlist-alist x-equiv acc))) :rule-classes :congruence)