Expand function calls throughout a vl-modinstlist-p
(vl-modinstlist-expand-function-calls x ss nf vardecls assigns warnings) → (mv successp warnings nf x-prime vardecls assigns)
Function:
(defun vl-modinstlist-expand-function-calls (x ss nf vardecls assigns warnings) (declare (xargs :guard (and (vl-modinstlist-p x) (vl-scopestack-p ss) (vl-namefactory-p nf) (vl-vardecllist-p vardecls) (vl-assignlist-p assigns) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-modinstlist-expand-function-calls)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv t (ok) (vl-namefactory-fix nf) nil (vl-vardecllist-fix vardecls) (vl-assignlist-fix assigns))) ((mv successp warnings nf car-prime vardecls assigns) (vl-modinst-expand-function-calls (car x) ss nf vardecls assigns warnings)) ((unless successp) (mv nil warnings nf nil vardecls assigns)) ((mv successp warnings nf cdr-prime vardecls assigns) (vl-modinstlist-expand-function-calls (cdr x) ss nf vardecls assigns warnings)) ((unless successp) (mv nil warnings nf nil vardecls assigns))) (mv t warnings nf (cons car-prime cdr-prime) vardecls assigns))))
Theorem:
(defthm booleanp-of-vl-modinstlist-expand-function-calls.successp (b* (((mv ?successp ?warnings ?nf ?x-prime ?vardecls ?assigns) (vl-modinstlist-expand-function-calls x ss nf vardecls assigns warnings))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-modinstlist-expand-function-calls.warnings (b* (((mv ?successp ?warnings ?nf ?x-prime ?vardecls ?assigns) (vl-modinstlist-expand-function-calls x ss nf vardecls assigns warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-namefactory-p-of-vl-modinstlist-expand-function-calls.nf (b* (((mv ?successp ?warnings ?nf ?x-prime ?vardecls ?assigns) (vl-modinstlist-expand-function-calls x ss nf vardecls assigns warnings))) (vl-namefactory-p nf)) :rule-classes :rewrite)
Theorem:
(defthm vl-modinstlist-p-of-vl-modinstlist-expand-function-calls.x-prime (b* (((mv ?successp ?warnings ?nf ?x-prime ?vardecls ?assigns) (vl-modinstlist-expand-function-calls x ss nf vardecls assigns warnings))) (vl-modinstlist-p x-prime)) :rule-classes :rewrite)
Theorem:
(defthm vl-vardecllist-p-of-vl-modinstlist-expand-function-calls.vardecls (b* (((mv ?successp ?warnings ?nf ?x-prime ?vardecls ?assigns) (vl-modinstlist-expand-function-calls x ss nf vardecls assigns warnings))) (vl-vardecllist-p vardecls)) :rule-classes :rewrite)
Theorem:
(defthm vl-assignlist-p-of-vl-modinstlist-expand-function-calls.assigns (b* (((mv ?successp ?warnings ?nf ?x-prime ?vardecls ?assigns) (vl-modinstlist-expand-function-calls x ss nf vardecls assigns warnings))) (vl-assignlist-p assigns)) :rule-classes :rewrite)
Theorem:
(defthm vl-modinstlist-expand-function-calls-mvtypes-3 (true-listp (mv-nth 3 (vl-modinstlist-expand-function-calls x ss nf vardecls assigns warnings))) :rule-classes :type-prescription)