(vl-assignstmt->svstmts lhs rhs blockingp ss scopes) → (mv ok vttree res)
Function:
(defun vl-assignstmt->svstmts (lhs rhs blockingp ss scopes) (declare (xargs :guard (and (vl-expr-p lhs) (vl-rhs-p rhs) (booleanp blockingp) (vl-scopestack-p ss) (vl-elabscopes-p scopes)))) (let ((__function__ 'vl-assignstmt->svstmts)) (declare (ignorable __function__)) (b* ((vttree nil) ((unless (vl-rhs-case rhs :vl-rhsexpr)) (mv nil (vfatal :type :vl-assignstmt-fail :msg "Not yet supported: 'new' instances: ~a0" :args (list (vl-rhs-fix rhs))) nil)) (lhs (vl-expr-fix lhs)) (rhs (vl-rhsexpr->guts rhs))) (vl-expr-case lhs :vl-index (b* (((mv err opinfo) (vl-index-expr-typetrace lhs ss scopes)) ((when err) (mv nil (vfatal :type :vl-assignstmt-fail :msg "Failed to get type of LHS ~a0: ~@1" :args (list lhs err)) nil)) ((vl-operandinfo opinfo)) ((vmv vttree type-err rhssvex) (vl-expr-to-svex-datatyped rhs lhs opinfo.type ss scopes :compattype :assign)) ((wvmv vttree) (vl-type-error-basic-warn rhs nil type-err lhs opinfo.type ss)) ((vmv ok vttree writes ?shift) (vl-procedural-assign->svstmts lhs rhssvex blockingp ss scopes)) (svstmts (list (sv::make-svstmt-assign :writes writes :blockingp blockingp)))) (mv ok vttree svstmts)) :vl-concat (b* (((vmv vttree & lhssize) (vl-expr-to-svex-selfdet lhs nil ss scopes)) ((vmv vttree rhssvex ?rhssize) (vl-expr-to-svex-selfdet rhs lhssize ss scopes)) ((vmv ok vttree writes ?shift) (vl-procedural-assign->svstmts lhs rhssvex blockingp ss scopes)) (svstmts (list (sv::make-svstmt-assign :writes writes :blockingp blockingp)))) (mv ok vttree svstmts)) :otherwise (mv nil (vfatal :type :vl-lhs-malformed :msg "Bad lvalue: ~a0" :args (list lhs)) nil)))))
Theorem:
(defthm return-type-of-vl-assignstmt->svstmts.vttree (b* (((mv ?ok ?vttree ?res) (vl-assignstmt->svstmts lhs rhs blockingp ss scopes))) (and (vttree-p vttree) (sv::svarlist-addr-p (sv::constraintlist-vars (vttree->constraints vttree))))) :rule-classes :rewrite)
Theorem:
(defthm svstmtlist-p-of-vl-assignstmt->svstmts.res (b* (((mv ?ok ?vttree ?res) (vl-assignstmt->svstmts lhs rhs blockingp ss scopes))) (sv::svstmtlist-p res)) :rule-classes :rewrite)
Theorem:
(defthm vars-of-vl-assignstmt->svstmts (b* (((mv ?ok ?vttree ?res) (vl-assignstmt->svstmts lhs rhs blockingp ss scopes))) (sv::svarlist-addr-p (sv::svstmtlist-vars res))))
Theorem:
(defthm vl-assignstmt->svstmts-of-vl-expr-fix-lhs (equal (vl-assignstmt->svstmts (vl-expr-fix lhs) rhs blockingp ss scopes) (vl-assignstmt->svstmts lhs rhs blockingp ss scopes)))
Theorem:
(defthm vl-assignstmt->svstmts-vl-expr-equiv-congruence-on-lhs (implies (vl-expr-equiv lhs lhs-equiv) (equal (vl-assignstmt->svstmts lhs rhs blockingp ss scopes) (vl-assignstmt->svstmts lhs-equiv rhs blockingp ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-assignstmt->svstmts-of-vl-rhs-fix-rhs (equal (vl-assignstmt->svstmts lhs (vl-rhs-fix rhs) blockingp ss scopes) (vl-assignstmt->svstmts lhs rhs blockingp ss scopes)))
Theorem:
(defthm vl-assignstmt->svstmts-vl-rhs-equiv-congruence-on-rhs (implies (vl-rhs-equiv rhs rhs-equiv) (equal (vl-assignstmt->svstmts lhs rhs blockingp ss scopes) (vl-assignstmt->svstmts lhs rhs-equiv blockingp ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-assignstmt->svstmts-of-bool-fix-blockingp (equal (vl-assignstmt->svstmts lhs rhs (acl2::bool-fix blockingp) ss scopes) (vl-assignstmt->svstmts lhs rhs blockingp ss scopes)))
Theorem:
(defthm vl-assignstmt->svstmts-iff-congruence-on-blockingp (implies (iff blockingp blockingp-equiv) (equal (vl-assignstmt->svstmts lhs rhs blockingp ss scopes) (vl-assignstmt->svstmts lhs rhs blockingp-equiv ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-assignstmt->svstmts-of-vl-scopestack-fix-ss (equal (vl-assignstmt->svstmts lhs rhs blockingp (vl-scopestack-fix ss) scopes) (vl-assignstmt->svstmts lhs rhs blockingp ss scopes)))
Theorem:
(defthm vl-assignstmt->svstmts-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-assignstmt->svstmts lhs rhs blockingp ss scopes) (vl-assignstmt->svstmts lhs rhs blockingp ss-equiv scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-assignstmt->svstmts-of-vl-elabscopes-fix-scopes (equal (vl-assignstmt->svstmts lhs rhs blockingp ss (vl-elabscopes-fix scopes)) (vl-assignstmt->svstmts lhs rhs blockingp ss scopes)))
Theorem:
(defthm vl-assignstmt->svstmts-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-assignstmt->svstmts lhs rhs blockingp ss scopes) (vl-assignstmt->svstmts lhs rhs blockingp ss scopes-equiv))) :rule-classes :congruence)