(vl-vardecllist->svstmts x ss scopes) → (mv ok vttree locals res)
Function:
(defun vl-vardecllist->svstmts (x ss scopes) (declare (xargs :guard (and (vl-vardecllist-p x) (vl-scopestack-p ss) (vl-elabscopes-p scopes)))) (let ((__function__ 'vl-vardecllist->svstmts)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv t nil nil nil)) (x1 (vl-vardecl-fix (car x))) ((mv ok vttree rest-locals rest-stmts) (vl-vardecllist->svstmts (cdr x) ss scopes)) ((unless ok) (mv nil vttree rest-locals rest-stmts)) ((vl-vardecl x1) x1) (locals (cons (sv::make-svar :name (sv::make-address :path (sv::make-path-wire :name x1.name) :scope 0)) rest-locals)) ((unless x1.initval) (mv ok vttree locals rest-stmts)) (lhs (vl-idexpr x1.name)) ((vmv ok vttree assign) (vl-assignstmt->svstmts lhs x1.initval t ss scopes))) (mv ok vttree locals (append-without-guard assign rest-stmts)))))
Theorem:
(defthm return-type-of-vl-vardecllist->svstmts.vttree (b* (((mv ?ok ?vttree ?locals ?res) (vl-vardecllist->svstmts x ss scopes))) (and (vttree-p vttree) (sv::svarlist-addr-p (sv::constraintlist-vars (vttree->constraints vttree))))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-vardecllist->svstmts.locals (b* (((mv ?ok ?vttree ?locals ?res) (vl-vardecllist->svstmts x ss scopes))) (and (sv::svarlist-p locals) (sv::svarlist-addr-p locals))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-vardecllist->svstmts.res (b* (((mv ?ok ?vttree ?locals ?res) (vl-vardecllist->svstmts x ss scopes))) (and (sv::svstmtlist-p res) (sv::svarlist-addr-p (sv::svstmtlist-vars res)))) :rule-classes :rewrite)
Theorem:
(defthm vl-vardecllist->svstmts-of-vl-vardecllist-fix-x (equal (vl-vardecllist->svstmts (vl-vardecllist-fix x) ss scopes) (vl-vardecllist->svstmts x ss scopes)))
Theorem:
(defthm vl-vardecllist->svstmts-vl-vardecllist-equiv-congruence-on-x (implies (vl-vardecllist-equiv x x-equiv) (equal (vl-vardecllist->svstmts x ss scopes) (vl-vardecllist->svstmts x-equiv ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-vardecllist->svstmts-of-vl-scopestack-fix-ss (equal (vl-vardecllist->svstmts x (vl-scopestack-fix ss) scopes) (vl-vardecllist->svstmts x ss scopes)))
Theorem:
(defthm vl-vardecllist->svstmts-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-vardecllist->svstmts x ss scopes) (vl-vardecllist->svstmts x ss-equiv scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-vardecllist->svstmts-of-vl-elabscopes-fix-scopes (equal (vl-vardecllist->svstmts x ss (vl-elabscopes-fix scopes)) (vl-vardecllist->svstmts x ss scopes)))
Theorem:
(defthm vl-vardecllist->svstmts-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-vardecllist->svstmts x ss scopes) (vl-vardecllist->svstmts x ss scopes-equiv))) :rule-classes :congruence)