Expand function calls throughout a vl-plainarg-p
(vl-plainarg-expand-function-calls x ss nf vardecls assigns warnings ctx loc) → (mv successp warnings nf x-prime vardecls assigns)
Function:
(defun vl-plainarg-expand-function-calls (x ss nf vardecls assigns warnings ctx loc) (declare (xargs :guard (and (vl-plainarg-p x) (vl-scopestack-p ss) (vl-namefactory-p nf) (vl-vardecllist-p vardecls) (vl-assignlist-p assigns) (vl-warninglist-p warnings) (vl-context-p ctx) (vl-location-p loc)))) (let ((__function__ 'vl-plainarg-expand-function-calls)) (declare (ignorable __function__)) (b* ((nf (vl-namefactory-fix nf)) (assigns (vl-assignlist-fix assigns)) (vardecls (vl-vardecllist-fix vardecls))) (b* ((x (vl-plainarg-fix x)) ((vl-plainarg x) x) ((unless x.expr) (mv t (ok) nf x vardecls assigns)) ((unless (vl-expr-has-funcalls x.expr)) (mv t (ok) nf x vardecls assigns)) ((unless x.dir) (mv nil (fatal :type :vl-bad-instance :msg "In ~a0, expected all arguments to be resolved before ~ function expansion." :args (list ctx)) nf x vardecls assigns)) ((unless (eq x.dir :vl-input)) (mv nil (fatal :type :vl-bad-argument :msg "In ~a0, we found a function call in a ~s1-port ~ connection, ~a2, but we only allow function calls in ~ input-port connections." :args (list ctx x.dir x)) nf x vardecls assigns)) ((mv okp warnings nf expr-prime vardecls assigns) (vl-expr-expand-function-calls x.expr ss nf vardecls assigns warnings ctx loc 100)) (x-prime (change-vl-plainarg x :expr expr-prime))) (mv okp warnings nf x-prime vardecls assigns)))))
Theorem:
(defthm booleanp-of-vl-plainarg-expand-function-calls.successp (b* (((mv ?successp ?warnings ?nf ?x-prime ?vardecls ?assigns) (vl-plainarg-expand-function-calls x ss nf vardecls assigns warnings ctx loc))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-plainarg-expand-function-calls.warnings (b* (((mv ?successp ?warnings ?nf ?x-prime ?vardecls ?assigns) (vl-plainarg-expand-function-calls x ss nf vardecls assigns warnings ctx loc))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-namefactory-p-of-vl-plainarg-expand-function-calls.nf (b* (((mv ?successp ?warnings ?nf ?x-prime ?vardecls ?assigns) (vl-plainarg-expand-function-calls x ss nf vardecls assigns warnings ctx loc))) (vl-namefactory-p nf)) :rule-classes :rewrite)
Theorem:
(defthm vl-plainarg-p-of-vl-plainarg-expand-function-calls.x-prime (b* (((mv ?successp ?warnings ?nf ?x-prime ?vardecls ?assigns) (vl-plainarg-expand-function-calls x ss nf vardecls assigns warnings ctx loc))) (vl-plainarg-p x-prime)) :rule-classes :rewrite)
Theorem:
(defthm vl-vardecllist-p-of-vl-plainarg-expand-function-calls.vardecls (b* (((mv ?successp ?warnings ?nf ?x-prime ?vardecls ?assigns) (vl-plainarg-expand-function-calls x ss nf vardecls assigns warnings ctx loc))) (vl-vardecllist-p vardecls)) :rule-classes :rewrite)
Theorem:
(defthm vl-assignlist-p-of-vl-plainarg-expand-function-calls.assigns (b* (((mv ?successp ?warnings ?nf ?x-prime ?vardecls ?assigns) (vl-plainarg-expand-function-calls x ss nf vardecls assigns warnings ctx loc))) (vl-assignlist-p assigns)) :rule-classes :rewrite)