Identify and remove useless parameters from a module.
(vl-module-clean-params x) → (mv new-x useless)
This is only one part of parameter cleaning. To safely remove the parameters, we must not only delete them from the module itself, but also eliminate the appropriate parameters from all instances of the module throughout the module list.
Function:
(defun vl-module-clean-params (x) (declare (xargs :guard (vl-module-p x))) (let ((__function__ 'vl-module-clean-params)) (declare (ignorable __function__)) (b* (((when (vl-module->hands-offp x)) (mv x nil)) (paramdecls (vl-module->paramdecls x)) ((when (not paramdecls)) (mv x nil)) (param-names (vl-paramdecllist->names paramdecls)) (all-used-names (vl-exprlist-names (vl-module-allexprs x))) (useful-param-names (intersection-equal all-used-names param-names)) (useless-param-names (set-difference-equal param-names useful-param-names)) ((unless useless-param-names) (mv x nil)) (useless-param-pos (vl-positions-of-params useless-param-names paramdecls)) (useless-struct (make-vl-useless-params :positions useless-param-pos :names useless-param-names)) (new-paramdecls (vl-delete-paramdecls useless-param-names paramdecls)) (x-prime (change-vl-module x :paramdecls new-paramdecls))) (mv x-prime useless-struct))))
Theorem:
(defthm vl-module-p-of-vl-module-clean-params.new-x (implies (and (force (vl-module-p x))) (b* (((mv ?new-x ?useless) (vl-module-clean-params x))) (vl-module-p new-x))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-module-clean-params.useless (implies (and (force (vl-module-p x))) (b* (((mv ?new-x ?useless) (vl-module-clean-params x))) (equal (vl-useless-params-p useless) (if useless t nil)))) :rule-classes :rewrite)