		Search-engine friendly clone of the ACL2 documentation.

Ifmerge

Vl-stmt-ifmerge

Main if-merging rewrite.

Signature
(vl-stmt-ifmerge x outer-cond warnings elem) → (mv warnings flat-stmts)
Arguments: x — Statement to rewrite.
Guard (vl-stmt-p x).; outer-cond — Initially nil, but becomes the merged outer-condition as we descend through ifs.
Guard (or (not outer-cond) (and (vl-expr-p outer-cond) (posp (vl-expr->finalwidth outer-cond)) (equal (vl-expr->finaltype outer-cond) :vl-unsigned))) .; warnings — Guard (vl-warninglist-p warnings).; elem — Context for error messages.
Guard (vl-modelement-p elem).
Returns: warnings — Type (vl-warninglist-p warnings).; flat-stmts — Type (vl-stmtlist-p flat-stmts).

Theorem: return-type-of-vl-stmt-ifmerge.warnings

(defthm return-type-of-vl-stmt-ifmerge.warnings
  (b* (((mv ?warnings ?flat-stmts)
        (vl-stmt-ifmerge x outer-cond warnings elem)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-stmt-ifmerge.flat-stmts

(defthm return-type-of-vl-stmt-ifmerge.flat-stmts
  (b* (((mv ?warnings ?flat-stmts)
        (vl-stmt-ifmerge x outer-cond warnings elem)))
    (vl-stmtlist-p flat-stmts))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-stmtlist-ifmerge.warnings

(defthm return-type-of-vl-stmtlist-ifmerge.warnings
  (b* (((mv ?warnings ?flat-stmts)
        (vl-stmtlist-ifmerge x outer-cond warnings elem)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-stmtlist-ifmerge.flat-stmts

(defthm return-type-of-vl-stmtlist-ifmerge.flat-stmts
  (b* (((mv ?warnings ?flat-stmts)
        (vl-stmtlist-ifmerge x outer-cond warnings elem)))
    (vl-stmtlist-p flat-stmts))
  :rule-classes :rewrite)

Subtopics

Vl-stmtlist-ifmerge