Expand function calls throughout an expression.
(vl-expr-expand-function-calls x ss nf vardecls assigns warnings ctx loc reclimit) → (mv successp warnings nf new-x vardecls assigns)
We recursively try to expand function calls throughout an expression (list). We return a new expression (list) that is equivalent, assuming that the generated variables and assigns are added to the module, and which is free of function calls on success.
Theorem:
(defthm return-type-of-vl-expr-expand-function-calls.successp (b* (((mv ?successp ?warnings ?nf ?new-x ?vardecls ?assigns) (vl-expr-expand-function-calls x ss nf vardecls assigns warnings ctx loc reclimit))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm return-type-of-vl-expr-expand-function-calls.warnings (b* (((mv ?successp ?warnings ?nf ?new-x ?vardecls ?assigns) (vl-expr-expand-function-calls x ss nf vardecls assigns warnings ctx loc reclimit))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-expr-expand-function-calls.nf (b* (((mv ?successp ?warnings ?nf ?new-x ?vardecls ?assigns) (vl-expr-expand-function-calls x ss nf vardecls assigns warnings ctx loc reclimit))) (vl-namefactory-p nf)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-expr-expand-function-calls.new-x (b* (((mv ?successp ?warnings ?nf ?new-x ?vardecls ?assigns) (vl-expr-expand-function-calls x ss nf vardecls assigns warnings ctx loc reclimit))) (vl-expr-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-expr-expand-function-calls.vardecls (b* (((mv ?successp ?warnings ?nf ?new-x ?vardecls ?assigns) (vl-expr-expand-function-calls x ss nf vardecls assigns warnings ctx loc reclimit))) (vl-vardecllist-p vardecls)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-expr-expand-function-calls.assigns (b* (((mv ?successp ?warnings ?nf ?new-x ?vardecls ?assigns) (vl-expr-expand-function-calls x ss nf vardecls assigns warnings ctx loc reclimit))) (vl-assignlist-p assigns)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-exprlist-expand-function-calls.successp (b* (((mv ?successp ?warnings ?nf ?new-x ?vardecls ?assigns) (vl-exprlist-expand-function-calls x ss nf vardecls assigns warnings ctx loc reclimit))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm return-type-of-vl-exprlist-expand-function-calls.warnings (b* (((mv ?successp ?warnings ?nf ?new-x ?vardecls ?assigns) (vl-exprlist-expand-function-calls x ss nf vardecls assigns warnings ctx loc reclimit))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-exprlist-expand-function-calls.nf (b* (((mv ?successp ?warnings ?nf ?new-x ?vardecls ?assigns) (vl-exprlist-expand-function-calls x ss nf vardecls assigns warnings ctx loc reclimit))) (vl-namefactory-p nf)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-exprlist-expand-function-calls.new-x (b* (((mv ?successp ?warnings ?nf ?new-x ?vardecls ?assigns) (vl-exprlist-expand-function-calls x ss nf vardecls assigns warnings ctx loc reclimit))) (and (vl-exprlist-p new-x) (equal (len new-x) (len x)))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-exprlist-expand-function-calls.vardecls (b* (((mv ?successp ?warnings ?nf ?new-x ?vardecls ?assigns) (vl-exprlist-expand-function-calls x ss nf vardecls assigns warnings ctx loc reclimit))) (vl-vardecllist-p vardecls)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-exprlist-expand-function-calls.assigns (b* (((mv ?successp ?warnings ?nf ?new-x ?vardecls ?assigns) (vl-exprlist-expand-function-calls x ss nf vardecls assigns warnings ctx loc reclimit))) (vl-assignlist-p assigns)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-fnname->template.successp (b* (((mv ?successp ?warnings ?template) (vl-fnname->template funname ss warnings reclimit))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm return-type-of-vl-fnname->template.warnings (b* (((mv ?successp ?warnings ?template) (vl-fnname->template funname ss warnings reclimit))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-fnname->template.template (b* (((mv ?successp ?warnings ?template) (vl-fnname->template funname ss warnings reclimit))) (implies successp (vl-funtemplate-p template))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-assignlist-expand-function-calls.successp (b* (((mv ?successp ?warnings ?nf ?new-x ?vardecls ?assigns) (vl-assignlist-expand-function-calls x ss nf vardecls assigns warnings reclimit))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm return-type-of-vl-assignlist-expand-function-calls.warnings (b* (((mv ?successp ?warnings ?nf ?new-x ?vardecls ?assigns) (vl-assignlist-expand-function-calls x ss nf vardecls assigns warnings reclimit))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-assignlist-expand-function-calls.nf (b* (((mv ?successp ?warnings ?nf ?new-x ?vardecls ?assigns) (vl-assignlist-expand-function-calls x ss nf vardecls assigns warnings reclimit))) (vl-namefactory-p nf)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-assignlist-expand-function-calls.new-x (b* (((mv ?successp ?warnings ?nf ?new-x ?vardecls ?assigns) (vl-assignlist-expand-function-calls x ss nf vardecls assigns warnings reclimit))) (and (vl-assignlist-p new-x) (equal (len new-x) (len x)))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-assignlist-expand-function-calls.vardecls (b* (((mv ?successp ?warnings ?nf ?new-x ?vardecls ?assigns) (vl-assignlist-expand-function-calls x ss nf vardecls assigns warnings reclimit))) (vl-vardecllist-p vardecls)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-assignlist-expand-function-calls.assigns (b* (((mv ?successp ?warnings ?nf ?new-x ?vardecls ?assigns) (vl-assignlist-expand-function-calls x ss nf vardecls assigns warnings reclimit))) (vl-assignlist-p assigns)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-assign-expand-function-calls.successp (b* (((mv ?successp ?warnings ?nf ?new-x ?vardecls ?assigns) (vl-assign-expand-function-calls x ss nf vardecls assigns warnings reclimit))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm return-type-of-vl-assign-expand-function-calls.warnings (b* (((mv ?successp ?warnings ?nf ?new-x ?vardecls ?assigns) (vl-assign-expand-function-calls x ss nf vardecls assigns warnings reclimit))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-assign-expand-function-calls.nf (b* (((mv ?successp ?warnings ?nf ?new-x ?vardecls ?assigns) (vl-assign-expand-function-calls x ss nf vardecls assigns warnings reclimit))) (vl-namefactory-p nf)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-assign-expand-function-calls.new-x (b* (((mv ?successp ?warnings ?nf ?new-x ?vardecls ?assigns) (vl-assign-expand-function-calls x ss nf vardecls assigns warnings reclimit))) (vl-assign-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-assign-expand-function-calls.vardecls (b* (((mv ?successp ?warnings ?nf ?new-x ?vardecls ?assigns) (vl-assign-expand-function-calls x ss nf vardecls assigns warnings reclimit))) (vl-vardecllist-p vardecls)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-assign-expand-function-calls.assigns (b* (((mv ?successp ?warnings ?nf ?new-x ?vardecls ?assigns) (vl-assign-expand-function-calls x ss nf vardecls assigns warnings reclimit))) (vl-assignlist-p assigns)) :rule-classes :rewrite)