Mutate an arbitrary compound (non-atomic) statement.
(change-vl-compoundstmt-core x stmts exprs ctrl vardecls paramdecls) → new-x
Function:
(defun change-vl-compoundstmt-core (x stmts exprs ctrl vardecls paramdecls) (declare (xargs :guard (and (vl-stmt-p x) (vl-stmtlist-p stmts) (vl-exprlist-p exprs) (vl-maybe-delayoreventcontrol-p ctrl) (vl-vardecllist-p vardecls) (vl-paramdecllist-p paramdecls)))) (declare (xargs :guard (and (not (vl-atomicstmt-p x)) (same-lengthp stmts (vl-compoundstmt->stmts x)) (same-lengthp exprs (vl-compoundstmt->exprs x)) (iff ctrl (vl-compoundstmt->ctrl x)) (or (not vardecls) (member (vl-stmt-kind x) '(:vl-blockstmt :vl-forstmt))) (or (not paramdecls) (vl-stmt-case x :vl-blockstmt))))) (let ((__function__ 'change-vl-compoundstmt-core)) (declare (ignorable __function__)) (let ((x (vl-stmt-fix x))) (vl-stmt-case x :vl-casestmt (change-vl-casestmt x :default (first stmts) :test (first exprs) :caselist (vl-rebuild-caselist x.caselist (rest exprs) (rest stmts))) :vl-ifstmt (change-vl-ifstmt x :condition (first exprs) :truebranch (first stmts) :falsebranch (second stmts)) :vl-foreverstmt (change-vl-foreverstmt x :body (first stmts)) :vl-waitstmt (change-vl-waitstmt x :condition (first exprs) :body (first stmts)) :vl-whilestmt (change-vl-whilestmt x :condition (first exprs) :body (first stmts)) :vl-dostmt (change-vl-dostmt x :condition (first exprs) :body (first stmts)) :vl-forstmt (b* ((ninitassigns (len x.initassigns)) (nstepforms (len x.stepforms)) (stmts (vl-stmtlist-fix stmts)) (stmts-starting-with-stepforms (nthcdr ninitassigns stmts))) (change-vl-forstmt x :initdecls vardecls :initassigns (take ninitassigns stmts) :test (first exprs) :stepforms (take nstepforms stmts-starting-with-stepforms) :body (nth nstepforms stmts-starting-with-stepforms))) :vl-foreachstmt (change-vl-foreachstmt x :vardecls vardecls :body (first stmts)) :vl-repeatstmt (change-vl-repeatstmt x :condition (first exprs) :body (first stmts)) :vl-blockstmt (change-vl-blockstmt x :vardecls vardecls :paramdecls paramdecls :stmts stmts) :vl-timingstmt (change-vl-timingstmt x :ctrl ctrl :body (first stmts)) :vl-assertstmt (change-vl-assertstmt x :assertion (change-vl-assertion x.assertion :condition (first exprs) :success (first stmts) :failure (second stmts))) :vl-cassertstmt (change-vl-cassertstmt x :cassertion (change-vl-cassertion x.cassertion :success (first stmts) :failure (second stmts))) :vl-nullstmt (progn$ (impossible) x) :vl-assignstmt (progn$ (impossible) x) :vl-deassignstmt (progn$ (impossible) x) :vl-callstmt (progn$ (impossible) x) :vl-disablestmt (progn$ (impossible) x) :vl-breakstmt (progn$ (impossible) x) :vl-continuestmt (progn$ (impossible) x) :vl-returnstmt (progn$ (impossible) x) :vl-eventtriggerstmt (progn$ (impossible) x)))))
Theorem:
(defthm vl-stmt-p-of-change-vl-compoundstmt-core (b* ((new-x (change-vl-compoundstmt-core x stmts exprs ctrl vardecls paramdecls))) (vl-stmt-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm change-vl-compoundstmt-core-identity (equal (change-vl-compoundstmt-core x (vl-compoundstmt->stmts x) (vl-compoundstmt->exprs x) (vl-compoundstmt->ctrl x) (vl-compoundstmt->vardecls x) (vl-compoundstmt->paramdecls x)) (vl-stmt-fix x)))
Theorem:
(defthm vl-stmtlist-fix-of-take (implies (<= (nfix n) (len x)) (equal (vl-stmtlist-fix (take n x)) (take n (vl-stmtlist-fix x)))))
Theorem:
(defthm vl-stmtlist-fix-of-nthcdr (equal (vl-stmtlist-fix (nthcdr n x)) (nthcdr n (vl-stmtlist-fix x))))
Theorem:
(defthm vl-stmt-fix-of-nth (implies (< (nfix n) (len x)) (equal (vl-stmt-fix (nth n x)) (nth n (vl-stmtlist-fix x)))))
Theorem:
(defthm vl-compoundstmt->stmts-of-change-vl-compoundstmt-core (implies (same-lengthp stmts (vl-compoundstmt->stmts x)) (equal (vl-compoundstmt->stmts (change-vl-compoundstmt-core x stmts exprs ctrl vardecls paramdecls)) (vl-stmtlist-fix stmts))))
Theorem:
(defthm vl-compoundstmt->exprs-of-change-vl-compoundstmt-core (implies (same-lengthp exprs (vl-compoundstmt->exprs x)) (equal (vl-compoundstmt->exprs (change-vl-compoundstmt-core x stmts exprs ctrl vardecls paramdecls)) (list-fix (vl-exprlist-fix exprs)))))
Theorem:
(defthm vl-compoundstmt->ctrl-of-change-vl-compoundstmt-core (implies (iff ctrl (vl-compoundstmt->ctrl x)) (equal (vl-compoundstmt->ctrl (change-vl-compoundstmt-core x stmts exprs ctrl vardecls paramdecls)) (vl-maybe-delayoreventcontrol-fix ctrl))))
Theorem:
(defthm vl-compoundstmt->ctrl-of-change-vl-compoundstmt-vardecls (implies (or (not vardecls) (equal (vl-stmt-kind x) :vl-blockstmt) (equal (vl-stmt-kind x) :vl-forstmt)) (equal (vl-compoundstmt->vardecls (change-vl-compoundstmt-core x stmts exprs ctrl vardecls paramdecls)) (vl-vardecllist-fix vardecls))))
Theorem:
(defthm vl-compoundstmt->ctrl-of-change-vl-compoundstmt-paramdecls (implies (or (not paramdecls) (vl-stmt-case x :vl-blockstmt)) (equal (vl-compoundstmt->paramdecls (change-vl-compoundstmt-core x stmts exprs ctrl vardecls paramdecls)) (vl-paramdecllist-fix paramdecls))))
Theorem:
(defthm change-vl-compoundstmt-core-of-vl-stmt-fix-x (equal (change-vl-compoundstmt-core (vl-stmt-fix x) stmts exprs ctrl vardecls paramdecls) (change-vl-compoundstmt-core x stmts exprs ctrl vardecls paramdecls)))
Theorem:
(defthm change-vl-compoundstmt-core-vl-stmt-equiv-congruence-on-x (implies (vl-stmt-equiv x x-equiv) (equal (change-vl-compoundstmt-core x stmts exprs ctrl vardecls paramdecls) (change-vl-compoundstmt-core x-equiv stmts exprs ctrl vardecls paramdecls))) :rule-classes :congruence)
Theorem:
(defthm change-vl-compoundstmt-core-of-vl-stmtlist-fix-stmts (equal (change-vl-compoundstmt-core x (vl-stmtlist-fix stmts) exprs ctrl vardecls paramdecls) (change-vl-compoundstmt-core x stmts exprs ctrl vardecls paramdecls)))
Theorem:
(defthm change-vl-compoundstmt-core-vl-stmtlist-equiv-congruence-on-stmts (implies (vl-stmtlist-equiv stmts stmts-equiv) (equal (change-vl-compoundstmt-core x stmts exprs ctrl vardecls paramdecls) (change-vl-compoundstmt-core x stmts-equiv exprs ctrl vardecls paramdecls))) :rule-classes :congruence)
Theorem:
(defthm change-vl-compoundstmt-core-of-vl-exprlist-fix-exprs (equal (change-vl-compoundstmt-core x stmts (vl-exprlist-fix exprs) ctrl vardecls paramdecls) (change-vl-compoundstmt-core x stmts exprs ctrl vardecls paramdecls)))
Theorem:
(defthm change-vl-compoundstmt-core-vl-exprlist-equiv-congruence-on-exprs (implies (vl-exprlist-equiv exprs exprs-equiv) (equal (change-vl-compoundstmt-core x stmts exprs ctrl vardecls paramdecls) (change-vl-compoundstmt-core x stmts exprs-equiv ctrl vardecls paramdecls))) :rule-classes :congruence)
Theorem:
(defthm change-vl-compoundstmt-core-of-vl-maybe-delayoreventcontrol-fix-ctrl (equal (change-vl-compoundstmt-core x stmts exprs (vl-maybe-delayoreventcontrol-fix ctrl) vardecls paramdecls) (change-vl-compoundstmt-core x stmts exprs ctrl vardecls paramdecls)))
Theorem:
(defthm change-vl-compoundstmt-core-vl-maybe-delayoreventcontrol-equiv-congruence-on-ctrl (implies (vl-maybe-delayoreventcontrol-equiv ctrl ctrl-equiv) (equal (change-vl-compoundstmt-core x stmts exprs ctrl vardecls paramdecls) (change-vl-compoundstmt-core x stmts exprs ctrl-equiv vardecls paramdecls))) :rule-classes :congruence)
Theorem:
(defthm change-vl-compoundstmt-core-of-vl-vardecllist-fix-vardecls (equal (change-vl-compoundstmt-core x stmts exprs ctrl (vl-vardecllist-fix vardecls) paramdecls) (change-vl-compoundstmt-core x stmts exprs ctrl vardecls paramdecls)))
Theorem:
(defthm change-vl-compoundstmt-core-vl-vardecllist-equiv-congruence-on-vardecls (implies (vl-vardecllist-equiv vardecls vardecls-equiv) (equal (change-vl-compoundstmt-core x stmts exprs ctrl vardecls paramdecls) (change-vl-compoundstmt-core x stmts exprs ctrl vardecls-equiv paramdecls))) :rule-classes :congruence)
Theorem:
(defthm change-vl-compoundstmt-core-of-vl-paramdecllist-fix-paramdecls (equal (change-vl-compoundstmt-core x stmts exprs ctrl vardecls (vl-paramdecllist-fix paramdecls)) (change-vl-compoundstmt-core x stmts exprs ctrl vardecls paramdecls)))
Theorem:
(defthm change-vl-compoundstmt-core-vl-paramdecllist-equiv-congruence-on-paramdecls (implies (vl-paramdecllist-equiv paramdecls paramdecls-equiv) (equal (change-vl-compoundstmt-core x stmts exprs ctrl vardecls paramdecls) (change-vl-compoundstmt-core x stmts exprs ctrl vardecls paramdecls-equiv))) :rule-classes :congruence)