		Search-engine friendly clone of the ACL2 documentation.

Binop

Binop-case

Case macro for the different kinds of binop 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 binop structure, or to split into cases based on its type.

Short Form

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

(binop-case x :mul)

is essentially just a safer alternative to writing:

(equal (binop-kind x) :mul)

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

Long Form

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

(binop-case x
  :mul ...
  :div ...
  :rem ...
  :add ...
  :sub ...
  :shl ...
  :shr ...
  :lt ...
  :gt ...
  :le ...
  :ge ...
  :eq ...
  :ne ...
  :bitand ...
  :bitxor ...
  :bitior ...
  :logand ...
  :logor ...
  :asg ...
  :asg-mul ...
  :asg-div ...
  :asg-rem ...
  :asg-add ...
  :asg-sub ...
  :asg-shl ...
  :asg-shr ...
  :asg-and ...
  :asg-xor ...
  :asg-ior ...)

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