Tail-recursive implementation of vl-module->modnamespace.
(vl-module->modnamespace-nrev x nrev) → nrev
This is sort of an inherently inefficient operation, since we are to perform a cons for every object in the module. But we can at least do everything tail recursively, etc.
Function:
(defun vl-module->modnamespace-nrev (x nrev) (declare (xargs :stobjs (nrev))) (declare (xargs :guard (vl-module-p x))) (let ((__function__ 'vl-module->modnamespace-nrev)) (declare (ignorable __function__)) (b* (((vl-module x) x) (nrev (vl-vardecllist->names-nrev x.vardecls nrev)) (nrev (vl-paramdecllist->names-nrev x.paramdecls nrev)) (nrev (vl-fundecllist->names-nrev x.fundecls nrev)) (nrev (vl-taskdecllist->names-nrev x.taskdecls nrev)) (nrev (vl-modinstlist->instnames-nrev x.modinsts nrev)) (nrev (vl-gateinstlist->names-nrev x.gateinsts nrev))) nrev)))
Theorem:
(defthm vl-module->modnamespace-nrev-of-vl-module-fix-x (equal (vl-module->modnamespace-nrev (vl-module-fix x) nrev) (vl-module->modnamespace-nrev x nrev)))
Theorem:
(defthm vl-module->modnamespace-nrev-vl-module-equiv-congruence-on-x (implies (vl-module-equiv x x-equiv) (equal (vl-module->modnamespace-nrev x nrev) (vl-module->modnamespace-nrev x-equiv nrev))) :rule-classes :congruence)