Eliminate param decls for useless params from each module, and build a map that explains what has been eliminated (i.e., what needs to be cleaned up from each module instance.)
(vl-modulelist-clean-params-aux x) → (mv x-prime map)
Function:
(defun vl-modulelist-clean-params-aux (x) (declare (xargs :guard (vl-modulelist-p x))) (let ((__function__ 'vl-modulelist-clean-params-aux)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv nil nil)) ((mv car-prime car-entry) (vl-module-clean-params (car x))) ((mv cdr-prime map) (vl-modulelist-clean-params-aux (cdr x))) (map (if car-entry (hons-acons (vl-module->name (car x)) car-entry map) map))) (mv (cons car-prime cdr-prime) map))))
Theorem:
(defthm vl-modulelist-p-of-vl-modulelist-clean-params-aux.x-prime (implies (and (force (vl-modulelist-p x))) (b* (((mv ?x-prime ?map) (vl-modulelist-clean-params-aux x))) (vl-modulelist-p x-prime))) :rule-classes :rewrite)
Theorem:
(defthm vl-useless-params-map-p-of-vl-modulelist-clean-params-aux.map (implies (and (force (vl-modulelist-p x))) (b* (((mv ?x-prime ?map) (vl-modulelist-clean-params-aux x))) (vl-useless-params-map-p map))) :rule-classes :rewrite)