		Search-engine friendly clone of the ACL2 documentation.

Vl-stmt

Vl-stmt-case

Case macro for the different kinds of vl-stmt structures.

This is an fty sum-type case macro, typically introduced by defflexsum or deftagsum. It allows you to safely check the type of a vl-stmt structure, or to split into cases based on its type.

Short Form

In its short form, vl-stmt-case allows you to safely check the type of a vl-stmt structure. For example:

(vl-stmt-case x :vl-nullstmt)

is essentially just a safer alternative to writing:

(equal (vl-stmt-kind x) :vl-nullstmt)

Why is using vl-stmt-case safer? When we directly inspect the kind with equal, there is no static checking being done to ensure that, e.g., :vl-nullstmt is a valid kind of vl-stmt structure. That means there is nothing to save you if, later, you change the kind keyword for this type from :vl-nullstmt to something else. It also means you get no help if you just make a typo when writing the :vl-nullstmt symbol. Over the course of developing VL, we found that such issues were very frequent sources of errors!

Long Form

In its longer form, vl-stmt-case allows you to split into cases based on the kind of structure you are looking at. A typical example would be:

(vl-stmt-case x
  :vl-nullstmt ...
  :vl-assignstmt ...
  :vl-deassignstmt ...
  :vl-callstmt ...
  :vl-disablestmt ...
  :vl-eventtriggerstmt ...
  :vl-casestmt ...
  :vl-ifstmt ...
  :vl-foreverstmt ...
  :vl-waitstmt ...
  :vl-repeatstmt ...
  :vl-whilestmt ...
  :vl-dostmt ...
  :vl-forstmt ...
  :vl-foreachstmt ...
  :vl-breakstmt ...
  :vl-continuestmt ...
  :vl-blockstmt ...
  :vl-timingstmt ...
  :vl-returnstmt ...
  :vl-assertstmt ...
  :vl-cassertstmt ...)

It is also possible to consolidate ``uninteresting'' cases using :otherwise.

For convenience, the case macro automatically binds the fields of x for you, as appropriate for each case. That is, in the :vl-nullstmt case, you can use defprod-style foo.bar style accessors for x without having to explicitly add a vl-nullstmt b* binder.