		Search-engine friendly clone of the ACL2 documentation.

Expr

Expr-case

Case macro for the different kinds of expr structures.

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

Short Form

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

(expr-case x :ident)

is essentially just a safer alternative to writing:

(equal (expr-kind x) :ident)

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

Long Form

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

(expr-case x
  :ident ...
  :const ...
  :string ...
  :paren ...
  :gensel ...
  :arrsub ...
  :funcall ...
  :member ...
  :memberp ...
  :complit ...
  :unary ...
  :sizeof ...
  :sizeof-ambig ...
  :alignof ...
  :cast ...
  :binary ...
  :cond ...
  :comma ...
  :cast/call-ambig ...
  :cast/mul-ambig ...
  :cast/add-ambig ...
  :cast/sub-ambig ...
  :cast/and-ambig ...
  :stmt ...
  :tycompat ...
  :offsetof ...
  :va-arg ...
  :extension ...)

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 :ident case, you can use fty::defprod-style foo.bar style accessors for x without having to explicitly add a ident b* binder.