		Search-engine friendly clone of the ACL2 documentation.

Clean-params

Vl-modinst-elim-useless-params

Clean up a module instance, removing any useless parameters.

Signature
(vl-modinst-elim-useless-params x map) → new-x
Arguments: x — Guard (vl-modinst-p x).; map — Guard (vl-useless-params-map-p map).
Returns: new-x — Type (vl-modinst-p new-x), given (force (vl-modinst-p x)).

Definitions and Theorems

Function: vl-modinst-elim-useless-params

(defun vl-modinst-elim-useless-params (x map)
 (declare (xargs :guard (and (vl-modinst-p x)
                             (vl-useless-params-map-p map))))
 (let ((__function__ 'vl-modinst-elim-useless-params))
   (declare (ignorable __function__))
   (b* (((vl-modinst x) x)
        ((when (vl-paramargs-empty-p x.paramargs))
         x)
        (entry (hons-get x.modname map))
        ((unless entry) x)
        (args-prime (vl-paramargs-elim-useless-params (cdr entry)
                                                      x.paramargs)))
     (change-vl-modinst x
                        :paramargs args-prime))))

Theorem: vl-modinst-p-of-vl-modinst-elim-useless-params

(defthm vl-modinst-p-of-vl-modinst-elim-useless-params
  (implies (force (vl-modinst-p x))
           (b* ((new-x (vl-modinst-elim-useless-params x map)))
             (vl-modinst-p new-x)))
  :rule-classes :rewrite)