Get all immediate sub-statements from any compound statement.
(vl-compoundstmt->stmts x) → stmts
This is useful for functions that want to recur over statements
without paying much attention to the kinds of statements being traversed. For
instance, if you just want to collect up all of the expressions everywhere
throughout a statement, you can recur through the
Function:
(defun vl-compoundstmt->stmts (x) (declare (xargs :guard (vl-stmt-p x))) (declare (xargs :guard (not (vl-atomicstmt-p x)))) (let ((__function__ 'vl-compoundstmt->stmts)) (declare (ignorable __function__)) (vl-stmt-case x :vl-casestmt (cons x.default (alist-vals x.caselist)) :vl-ifstmt (list x.truebranch x.falsebranch) :vl-foreverstmt (list x.body) :vl-waitstmt (list x.body) :vl-whilestmt (list x.body) :vl-forstmt (append-without-guard x.initassigns x.stepforms (list x.body)) :vl-blockstmt x.stmts :vl-repeatstmt (list x.body) :vl-timingstmt (list x.body) :otherwise nil)))
Theorem:
(defthm vl-stmtlist-p-of-vl-compoundstmt->stmts (b* ((stmts (vl-compoundstmt->stmts x))) (vl-stmtlist-p stmts)) :rule-classes :rewrite)
Theorem:
(defthm vl-stmtlist-count-of-vl-compoundstmt->stmts-weak (<= (vl-stmtlist-count (vl-compoundstmt->stmts x)) (vl-stmt-count x)) :rule-classes ((:rewrite) (:linear)))
Theorem:
(defthm vl-stmtlist-count-of-vl-compoundstmt->stmts-strong (implies (not (vl-atomicstmt-p x)) (< (vl-stmtlist-count (vl-compoundstmt->stmts x)) (vl-stmt-count x))) :rule-classes ((:rewrite) (:linear)))
Theorem:
(defthm vl-compoundstmt->stmts-of-vl-stmt-fix-x (equal (vl-compoundstmt->stmts (vl-stmt-fix x)) (vl-compoundstmt->stmts x)))
Theorem:
(defthm vl-compoundstmt->stmts-vl-stmt-equiv-congruence-on-x (implies (vl-stmt-equiv x x-equiv) (equal (vl-compoundstmt->stmts x) (vl-compoundstmt->stmts x-equiv))) :rule-classes :congruence)