Get all immediate sub-expressions from any compound statement.
(vl-compoundstmt->exprs x) → exprs
Note that this only returns the top-level expressions that are directly part of the statement.
Function:
(defun vl-compoundstmt->exprs (x) (declare (xargs :guard (vl-stmt-p x))) (declare (xargs :guard (not (vl-atomicstmt-p x)))) (let ((__function__ 'vl-compoundstmt->exprs)) (declare (ignorable __function__)) (vl-stmt-case x :vl-casestmt (cons x.test (flatten (alist-keys x.caselist))) :vl-ifstmt (list x.condition) :vl-foreverstmt nil :vl-waitstmt (list x.condition) :vl-whilestmt (list x.condition) :vl-dostmt (list x.condition) :vl-forstmt (list x.test) :vl-repeatstmt (list x.condition) :vl-blockstmt nil :vl-timingstmt nil :vl-assertstmt (b* (((vl-assertion x.assertion))) (list x.assertion.condition)) :vl-cassertstmt nil :otherwise nil)))
Theorem:
(defthm vl-exprlist-p-of-vl-compoundstmt->exprs (b* ((exprs (vl-compoundstmt->exprs x))) (vl-exprlist-p exprs)) :rule-classes :rewrite)
Theorem:
(defthm vl-compoundstmt->exprs-of-vl-stmt-fix-x (equal (vl-compoundstmt->exprs (vl-stmt-fix x)) (vl-compoundstmt->exprs x)))
Theorem:
(defthm vl-compoundstmt->exprs-vl-stmt-equiv-congruence-on-x (implies (vl-stmt-equiv x x-equiv) (equal (vl-compoundstmt->exprs x) (vl-compoundstmt->exprs x-equiv))) :rule-classes :congruence)