Generate new names for a list of net declarations and change their locations; this is used to give new names to the wires in a function call.
(vl-funexpand-rename-vardecls x nf loc) → (mv new-x nf)
Function:
(defun vl-funexpand-rename-vardecls (x nf loc) (declare (xargs :guard (and (vl-vardecllist-p x) (vl-namefactory-p nf) (vl-location-p loc)))) (let ((__function__ 'vl-funexpand-rename-vardecls)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv nil (vl-namefactory-fix nf))) ((mv new-name nf) (vl-namefactory-indexed-name (vl-vardecl->name (car x)) nf)) (car-renamed (change-vl-vardecl (car x) :name new-name :loc loc)) ((mv cdr-renamed nf) (vl-funexpand-rename-vardecls (cdr x) nf loc))) (mv (cons car-renamed cdr-renamed) nf))))
Theorem:
(defthm vl-vardecllist-p-of-vl-funexpand-rename-vardecls.new-x (b* (((mv ?new-x ?nf) (vl-funexpand-rename-vardecls x nf loc))) (vl-vardecllist-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-namefactory-p-of-vl-funexpand-rename-vardecls.nf (b* (((mv ?new-x ?nf) (vl-funexpand-rename-vardecls x nf loc))) (vl-namefactory-p nf)) :rule-classes :rewrite)
Theorem:
(defthm consp-of-vl-funexpand-rename-vardecls (equal (consp (mv-nth 0 (vl-funexpand-rename-vardecls x nf loc))) (consp x)))
Theorem:
(defthm len-of-vl-funexpand-rename-vardecls (equal (len (mv-nth 0 (vl-funexpand-rename-vardecls x nf loc))) (len x)))
Theorem:
(defthm true-listp-of-vl-funexpand-rename-vardecls (true-listp (mv-nth 0 (vl-funexpand-rename-vardecls x nf loc))) :rule-classes :type-prescription)