Legacy -- Use scopestack instead. Main routine for building an fast alist for looking up module items.
(vl-make-moditem-alist x) → *
Note that the order the alist is constructed in is particularly important: we want it to agree, completely, with the naive vl-find-moduleitem. The alist can be constructed in a one pass, using our fast-finding-by-name functions.
Function:
(defun vl-make-moditem-alist (x) (declare (xargs :guard (vl-module-p x))) (let ((__function__ 'vl-make-moditem-alist)) (declare (ignorable __function__)) (b* (((vl-module x) x) (acc (vl-gateinstlist-alist x.gateinsts nil)) (acc (vl-modinstlist-alist x.modinsts acc)) (acc (vl-taskdecllist-alist x.taskdecls acc)) (acc (vl-fundecllist-alist x.fundecls acc)) (acc (vl-paramdecllist-alist x.paramdecls acc)) (acc (vl-vardecllist-alist x.vardecls acc))) (make-fast-alist acc))))
Theorem:
(defthm vl-moditem-alist-p-of-vl-make-moditem-alist (vl-moditem-alist-p (vl-make-moditem-alist x)))
Theorem:
(defthm hons-assoc-equal-of-vl-make-moditem-alist (implies (force (stringp name)) (equal (hons-assoc-equal name (vl-make-moditem-alist x)) (if (vl-find-moduleitem name x) (cons name (vl-find-moduleitem name x)) nil))))
Theorem:
(defthm vl-make-moditem-alist-of-vl-module-fix-x (equal (vl-make-moditem-alist (vl-module-fix x)) (vl-make-moditem-alist x)))
Theorem:
(defthm vl-make-moditem-alist-vl-module-equiv-congruence-on-x (implies (vl-module-equiv x x-equiv) (equal (vl-make-moditem-alist x) (vl-make-moditem-alist x-equiv))) :rule-classes :congruence)