Main routine for expanding a single function call.
(vl-expand-function-call x actuals nf vardecls assigns warnings ctx loc) → (mv successp warnings nf expr? vardecls assigns)
We might fail if there is an arity problem. But if everything lines up,
Function:
(defun vl-expand-function-call (x actuals nf vardecls assigns warnings ctx loc) (declare (xargs :guard (and (vl-funtemplate-p x) (vl-exprlist-p actuals) (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-expand-function-call)) (declare (ignorable __function__)) (b* ((nf (vl-namefactory-fix nf)) (vardecls (vl-vardecllist-fix vardecls)) (assigns (vl-assignlist-fix assigns)) ((vl-funtemplate x) x) ((unless (same-lengthp x.inputs actuals)) (b* ((funname-atom (make-vl-atom :guts (make-vl-funname :name x.name))) (this-call (make-vl-nonatom :op :vl-funcall :args (cons funname-atom actuals)))) (mv nil (fatal :type :vl-bad-funcall :msg "In ~a0, trying to call function ~w1 with ~x2 ~ argument~s3, but it takes ~x4 input~s5. ~ Expression: ~a6." :args (list ctx x.name (len actuals) (if (vl-plural-p actuals) "s" "") (len x.inputs) (if (vl-plural-p x.inputs) "s" "") this-call)) nf nil vardecls assigns))) ((mv input-vars nf) (vl-funexpand-rename-vardecls x.inputs nf loc)) ((mv local-vars nf) (vl-funexpand-rename-vardecls x.locals nf loc)) ((mv ret-vars nf) (vl-funexpand-rename-vardecls (list x.out) nf loc)) (ret-var (car ret-vars)) (gen-input-names (vl-vardecllist->names input-vars)) (gen-local-names (vl-vardecllist->names local-vars)) (gen-ret-name (vl-vardecl->name ret-var)) (gen-input-wires (vl-make-idexpr-list gen-input-names nil nil)) (gen-local-wires (vl-make-idexpr-list gen-local-names nil nil)) (gen-ret-wire (vl-idexpr gen-ret-name nil nil)) (sigma (cons (cons (vl-vardecl->name x.out) gen-ret-wire) (append (pairlis$ (vl-vardecllist->names x.inputs) gen-input-wires) (pairlis$ (vl-vardecllist->names x.locals) gen-local-wires)))) ((with-fast sigma)) (body-assigns (vl-assignlist-subst x.assigns sigma)) (body-assigns (vl-relocate-assignments body-assigns loc)) (input-assigns (vl-fun-make-assignments-to-inputs gen-input-names actuals loc)) (vardecls (append input-vars local-vars ret-vars vardecls)) (assigns (append input-assigns body-assigns assigns))) (mv t (ok) nf gen-ret-wire vardecls assigns))))
Theorem:
(defthm booleanp-of-vl-expand-function-call.successp (b* (((mv ?successp ?warnings ?nf ?expr? ?vardecls ?assigns) (vl-expand-function-call x actuals nf vardecls assigns warnings ctx loc))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-expand-function-call.warnings (b* (((mv ?successp ?warnings ?nf ?expr? ?vardecls ?assigns) (vl-expand-function-call x actuals nf vardecls assigns warnings ctx loc))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-namefactory-p-of-vl-expand-function-call.nf (b* (((mv ?successp ?warnings ?nf ?expr? ?vardecls ?assigns) (vl-expand-function-call x actuals nf vardecls assigns warnings ctx loc))) (vl-namefactory-p nf)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-expand-function-call.expr? (b* (((mv ?successp ?warnings ?nf ?expr? ?vardecls ?assigns) (vl-expand-function-call x actuals nf vardecls assigns warnings ctx loc))) (equal (vl-expr-p expr?) successp)) :rule-classes :rewrite)
Theorem:
(defthm vl-vardecllist-p-of-vl-expand-function-call.vardecls (b* (((mv ?successp ?warnings ?nf ?expr? ?vardecls ?assigns) (vl-expand-function-call x actuals nf vardecls assigns warnings ctx loc))) (vl-vardecllist-p vardecls)) :rule-classes :rewrite)
Theorem:
(defthm vl-assignlist-p-of-vl-expand-function-call.assigns (b* (((mv ?successp ?warnings ?nf ?expr? ?vardecls ?assigns) (vl-expand-function-call x actuals nf vardecls assigns warnings ctx loc))) (vl-assignlist-p assigns)) :rule-classes :rewrite)