Eliminate parameters from a function.
(vl-fundecl-expand-params x warnings) → (mv successp warnings new-x)
We try to rewrite
The basic idea is to just construct a substitution list from the parameters and apply it throughout the function. But we do a lot of sanity checking to make sure that the parameters are very simple, aren't shadowing other things, and are defined before they are used (as some Verilog tools require). While we're at it, we also check the function's local namespace to make sure it is okay (since eliminating parameters changes the function's namespace).
Function:
(defun vl-fundecl-expand-params (x warnings) (declare (xargs :guard (and (vl-fundecl-p x) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-fundecl-expand-params)) (declare (ignorable __function__)) (b* ((x (vl-fundecl-fix x)) ((vl-fundecl x) x) (real-vardecls (vl-remove-fake-function-vardecls x.vardecls)) ((unless x.paramdecls) (mv t (ok) x)) (param-names (vl-paramdecllist->names x.paramdecls)) (local-namespace (append (list x.name) (vl-vardecllist->names real-vardecls) param-names)) (dupes (duplicated-members local-namespace)) ((when dupes) (mv nil (fatal :type :vl-bad-function-namespace :msg "In ~a0, there are multiple declarations for ~&1." :args (list x dupes)) x)) ((mv okp warnings) (vl-fun-paramdecllist-types-okp x.paramdecls warnings x)) ((unless okp) (mv nil warnings x)) (sigma (vl-fundecl-param-sigma x.paramdecls)) ((with-fast sigma)) (vardecls (vl-vardecllist-subst x.vardecls sigma)) (body (vl-stmt-subst x.body sigma)) (new-x (change-vl-fundecl x :vardecls vardecls :body body))) (mv t warnings new-x))))
Theorem:
(defthm booleanp-of-vl-fundecl-expand-params.successp (b* (((mv ?successp ?warnings ?new-x) (vl-fundecl-expand-params x warnings))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-fundecl-expand-params.warnings (b* (((mv ?successp ?warnings ?new-x) (vl-fundecl-expand-params x warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-fundecl-p-of-vl-fundecl-expand-params.new-x (b* (((mv ?successp ?warnings ?new-x) (vl-fundecl-expand-params x warnings))) (vl-fundecl-p new-x)) :rule-classes :rewrite)